Theorem supfil 15560

Description: The supersets of a nonempty set which are also subsets of a given base set form a filter.

Assertion

Ref	Expression
supfil	|- ((A e. C /\ B C_ A /\ B =/= (/)) -> ({x | (x C_ A /\ B C_ x)} e. Fil /\ A = U.{x | (x C_ A /\ B C_ x)}))

Distinct variable groups:   x,A   x,B   x,C

Proof of Theorem supfil

Step	Hyp	Ref	Expression
1		simp2 877	. . . . . . 7 |- ((A e. C /\ B C_ A /\ B =/= (/)) -> B C_ A)
2		ssid 2634	. . . . . . 7 |- A C_ A
3	1, 2	jctil 316	. . . . . 6 |- ((A e. C /\ B C_ A /\ B =/= (/)) -> (A C_ A /\ B C_ A))
4		sseq2 2639	. . . . . . . 8 |- (x = A -> (B C_ x <-> B C_ A))
5	4	elssabg 3462	. . . . . . 7 |- (A e. C -> (A e. {x | (x C_ A /\ B C_ x)} <-> (A C_ A /\ B C_ A)))
6	5	3ad2ant1 897	. . . . . 6 |- ((A e. C /\ B C_ A /\ B =/= (/)) -> (A e. {x | (x C_ A /\ B C_ x)} <-> (A C_ A /\ B C_ A)))
7	3, 6	mpbird 213	. . . . 5 |- ((A e. C /\ B C_ A /\ B =/= (/)) -> A e. {x | (x C_ A /\ B C_ x)})
8		elssuni 3206	. . . . 5 |- (A e. {x | (x C_ A /\ B C_ x)} -> A C_ U.{x | (x C_ A /\ B C_ x)})
9	7, 8	syl 12	. . . 4 |- ((A e. C /\ B C_ A /\ B =/= (/)) -> A C_ U.{x | (x C_ A /\ B C_ x)})
10		simpl 346	. . . . . . . 8 |- ((y C_ A /\ B C_ y) -> y C_ A)
11	10	a1i 8	. . . . . . 7 |- ((A e. C /\ B C_ A /\ B =/= (/)) -> ((y C_ A /\ B C_ y) -> y C_ A))
12		visset 2295	. . . . . . . 8 |- y e. _V
13		sseq1 2637	. . . . . . . . 9 |- (x = y -> (x C_ A <-> y C_ A))
14		sseq2 2639	. . . . . . . . 9 |- (x = y -> (B C_ x <-> B C_ y))
15	13, 14	anbi12d 690	. . . . . . . 8 |- (x = y -> ((x C_ A /\ B C_ x) <-> (y C_ A /\ B C_ y)))
16	12, 15	elab 2403	. . . . . . 7 |- (y e. {x | (x C_ A /\ B C_ x)} <-> (y C_ A /\ B C_ y))
17	11, 16	syl5ib 223	. . . . . 6 |- ((A e. C /\ B C_ A /\ B =/= (/)) -> (y e. {x | (x C_ A /\ B C_ x)} -> y C_ A))
18	17	r19.21aiv 2175	. . . . 5 |- ((A e. C /\ B C_ A /\ B =/= (/)) -> A.y e. {x | (x C_ A /\ B C_ x)}y C_ A)
19		unissb 3208	. . . . 5 |- (U.{x | (x C_ A /\ B C_ x)} C_ A <-> A.y e. {x | (x C_ A /\ B C_ x)}y C_ A)
20	18, 19	sylibr 217	. . . 4 |- ((A e. C /\ B C_ A /\ B =/= (/)) -> U.{x | (x C_ A /\ B C_ x)} C_ A)
21	9, 20	eqssd 2633	. . 3 |- ((A e. C /\ B C_ A /\ B =/= (/)) -> A = U.{x | (x C_ A /\ B C_ x)})
22		df-ne 2019	. . . . . . . . . . . 12 |- (B =/= (/) <-> -. B = (/))
23	22	biimpi 168	. . . . . . . . . . 11 |- (B =/= (/) -> -. B = (/))
24	23	3ad2ant3 899	. . . . . . . . . 10 |- ((A e. C /\ B C_ A /\ B =/= (/)) -> -. B = (/))
25		ss0 2902	. . . . . . . . . . 11 |- (B C_ (/) -> B = (/))
26	25	adantl 424	. . . . . . . . . 10 |- (((/) C_ A /\ B C_ (/)) -> B = (/))
27	24, 26	nsyl 131	. . . . . . . . 9 |- ((A e. C /\ B C_ A /\ B =/= (/)) -> -. ((/) C_ A /\ B C_ (/)))
28		0ex 3446	. . . . . . . . . . 11 |- (/) e. _V
29		sseq1 2637	. . . . . . . . . . . 12 |- (x = (/) -> (x C_ A <-> (/) C_ A))
30		sseq2 2639	. . . . . . . . . . . 12 |- (x = (/) -> (B C_ x <-> B C_ (/)))
31	29, 30	anbi12d 690	. . . . . . . . . . 11 |- (x = (/) -> ((x C_ A /\ B C_ x) <-> ((/) C_ A /\ B C_ (/))))
32	28, 31	elab 2403	. . . . . . . . . 10 |- ((/) e. {x | (x C_ A /\ B C_ x)} <-> ((/) C_ A /\ B C_ (/)))
33	32	a1i 8	. . . . . . . . 9 |- ((A e. C /\ B C_ A /\ B =/= (/)) -> ((/) e. {x | (x C_ A /\ B C_ x)} <-> ((/) C_ A /\ B C_ (/))))
34	27, 33	mtbird 783	. . . . . . . 8 |- ((A e. C /\ B C_ A /\ B =/= (/)) -> -. (/) e. {x | (x C_ A /\ B C_ x)})
35	34	adantr 425	. . . . . . 7 |- (((A e. C /\ B C_ A /\ B =/= (/)) /\ A = U.{x | (x C_ A /\ B C_ x)}) -> -. (/) e. {x | (x C_ A /\ B C_ x)})
36		simpr 350	. . . . . . . 8 |- (((A e. C /\ B C_ A /\ B =/= (/)) /\ A = U.{x | (x C_ A /\ B C_ x)}) -> A = U.{x | (x C_ A /\ B C_ x)})
37	7	adantr 425	. . . . . . . 8 |- (((A e. C /\ B C_ A /\ B =/= (/)) /\ A = U.{x | (x C_ A /\ B C_ x)}) -> A e. {x | (x C_ A /\ B C_ x)})
38	36, 37	eqeltrrd 1972	. . . . . . 7 |- (((A e. C /\ B C_ A /\ B =/= (/)) /\ A = U.{x | (x C_ A /\ B C_ x)}) -> U.{x | (x C_ A /\ B C_ x)} e. {x | (x C_ A /\ B C_ x)})
39	35, 38	jca 310	. . . . . 6 |- (((A e. C /\ B C_ A /\ B =/= (/)) /\ A = U.{x | (x C_ A /\ B C_ x)}) -> (-. (/) e. {x | (x C_ A /\ B C_ x)} /\ U.{x | (x C_ A /\ B C_ x)} e. {x | (x C_ A /\ B C_ x)}))
40		visset 2295	. . . . . . . . . 10 |- z e. _V
41		sseq1 2637	. . . . . . . . . . 11 |- (x = z -> (x C_ A <-> z C_ A))
42		sseq2 2639	. . . . . . . . . . 11 |- (x = z -> (B C_ x <-> B C_ z))
43	41, 42	anbi12d 690	. . . . . . . . . 10 |- (x = z -> ((x C_ A /\ B C_ x) <-> (z C_ A /\ B C_ z)))
44	40, 43	elab 2403	. . . . . . . . 9 |- (z e. {x | (x C_ A /\ B C_ x)} <-> (z C_ A /\ B C_ z))
45		sseq2 2639	. . . . . . . . . . . . 13 |- (A = U.{x | (x C_ A /\ B C_ x)} -> (z C_ A <-> z C_ U.{x | (x C_ A /\ B C_ x)}))
46	45	biimpar 461	. . . . . . . . . . . 12 |- ((A = U.{x | (x C_ A /\ B C_ x)} /\ z C_ U.{x | (x C_ A /\ B C_ x)}) -> z C_ A)
47	46	adantll 428	. . . . . . . . . . 11 |- ((((A e. C /\ B C_ A /\ B =/= (/)) /\ A = U.{x | (x C_ A /\ B C_ x)}) /\ z C_ U.{x | (x C_ A /\ B C_ x)}) -> z C_ A)
48	47	3ad2antr2 1042	. . . . . . . . . 10 |- ((((A e. C /\ B C_ A /\ B =/= (/)) /\ A = U.{x | (x C_ A /\ B C_ x)}) /\ (y e. {x | (x C_ A /\ B C_ x)} /\ z C_ U.{x | (x C_ A /\ B C_ x)} /\ y C_ z)) -> z C_ A)
49	48	anasss 488	. . . . . . . . 9 |- (((A e. C /\ B C_ A /\ B =/= (/)) /\ (A = U.{x | (x C_ A /\ B C_ x)} /\ (y e. {x | (x C_ A /\ B C_ x)} /\ z C_ U.{x | (x C_ A /\ B C_ x)} /\ y C_ z))) -> z C_ A)
50		sstr2 2623	. . . . . . . . . . . . . 14 |- (B C_ y -> (y C_ z -> B C_ z))
51	50	adantl 424	. . . . . . . . . . . . 13 |- ((y C_ A /\ B C_ y) -> (y C_ z -> B C_ z))
52	16, 51	sylbi 216	. . . . . . . . . . . 12 |- (y e. {x | (x C_ A /\ B C_ x)} -> (y C_ z -> B C_ z))
53	52	imp 377	. . . . . . . . . . 11 |- ((y e. {x | (x C_ A /\ B C_ x)} /\ y C_ z) -> B C_ z)
54	53	3adant2 895	. . . . . . . . . 10 |- ((y e. {x | (x C_ A /\ B C_ x)} /\ z C_ U.{x | (x C_ A /\ B C_ x)} /\ y C_ z) -> B C_ z)
55	54	ad2antll 443	. . . . . . . . 9 |- (((A e. C /\ B C_ A /\ B =/= (/)) /\ (A = U.{x | (x C_ A /\ B C_ x)} /\ (y e. {x | (x C_ A /\ B C_ x)} /\ z C_ U.{x | (x C_ A /\ B C_ x)} /\ y C_ z))) -> B C_ z)
56	44, 49, 55	sylanbrc 527	. . . . . . . 8 |- (((A e. C /\ B C_ A /\ B =/= (/)) /\ (A = U.{x | (x C_ A /\ B C_ x)} /\ (y e. {x | (x C_ A /\ B C_ x)} /\ z C_ U.{x | (x C_ A /\ B C_ x)} /\ y C_ z))) -> z e. {x | (x C_ A /\ B C_ x)})
57	56	expr 418	. . . . . . 7 |- (((A e. C /\ B C_ A /\ B =/= (/)) /\ A = U.{x | (x C_ A /\ B C_ x)}) -> ((y e. {x | (x C_ A /\ B C_ x)} /\ z C_ U.{x | (x C_ A /\ B C_ x)} /\ y C_ z) -> z e. {x | (x C_ A /\ B C_ x)}))
58	57	19.21aivv 1665	. . . . . 6 |- (((A e. C /\ B C_ A /\ B =/= (/)) /\ A = U.{x | (x C_ A /\ B C_ x)}) -> A.yA.z((y e. {x | (x C_ A /\ B C_ x)} /\ z C_ U.{x | (x C_ A /\ B C_ x)} /\ y C_ z) -> z e. {x | (x C_ A /\ B C_ x)}))
59	12	inex1 3452	. . . . . . . . . . 11 |- (y i^i z) e. _V
60		sseq1 2637	. . . . . . . . . . . 12 |- (x = (y i^i z) -> (x C_ A <-> (y i^i z) C_ A))
61		sseq2 2639	. . . . . . . . . . . 12 |- (x = (y i^i z) -> (B C_ x <-> B C_ (y i^i z)))
62	60, 61	anbi12d 690	. . . . . . . . . . 11 |- (x = (y i^i z) -> ((x C_ A /\ B C_ x) <-> ((y i^i z) C_ A /\ B C_ (y i^i z))))
63	59, 62	elab 2403	. . . . . . . . . 10 |- ((y i^i z) e. {x | (x C_ A /\ B C_ x)} <-> ((y i^i z) C_ A /\ B C_ (y i^i z)))
64		ssinss1 2821	. . . . . . . . . . 11 |- (y C_ A -> (y i^i z) C_ A)
65	64	ad2antrr 440	. . . . . . . . . 10 |- (((y C_ A /\ B C_ y) /\ (z C_ A /\ B C_ z)) -> (y i^i z) C_ A)
66		ssin 2814	. . . . . . . . . . . 12 |- ((B C_ y /\ B C_ z) <-> B C_ (y i^i z))
67	66	biimpi 168	. . . . . . . . . . 11 |- ((B C_ y /\ B C_ z) -> B C_ (y i^i z))
68	67	ad2ant2l 444	. . . . . . . . . 10 |- (((y C_ A /\ B C_ y) /\ (z C_ A /\ B C_ z)) -> B C_ (y i^i z))
69	63, 65, 68	sylanbrc 527	. . . . . . . . 9 |- (((y C_ A /\ B C_ y) /\ (z C_ A /\ B C_ z)) -> (y i^i z) e. {x | (x C_ A /\ B C_ x)})
70	69, 16, 44	syl2anb 504	. . . . . . . 8 |- ((y e. {x | (x C_ A /\ B C_ x)} /\ z e. {x | (x C_ A /\ B C_ x)}) -> (y i^i z) e. {x | (x C_ A /\ B C_ x)})
71	70	rgen2a 2160	. . . . . . 7 |- A.y e. {x | (x C_ A /\ B C_ x)}A.z e. {x | (x C_ A /\ B C_ x)} (y i^i z) e. {x | (x C_ A /\ B C_ x)}
72	71	a1i 8	. . . . . 6 |- (((A e. C /\ B C_ A /\ B =/= (/)) /\ A = U.{x | (x C_ A /\ B C_ x)}) -> A.y e. {x | (x C_ A /\ B C_ x)}A.z e. {x | (x C_ A /\ B C_ x)} (y i^i z) e. {x | (x C_ A /\ B C_ x)})
73	39, 58, 72	3jca 1050	. . . . 5 |- (((A e. C /\ B C_ A /\ B =/= (/)) /\ A = U.{x | (x C_ A /\ B C_ x)}) -> ((-. (/) e. {x | (x C_ A /\ B C_ x)} /\ U.{x | (x C_ A /\ B C_ x)} e. {x | (x C_ A /\ B C_ x)}) /\ A.yA.z((y e. {x | (x C_ A /\ B C_ x)} /\ z C_ U.{x | (x C_ A /\ B C_ x)} /\ y C_ z) -> z e. {x | (x C_ A /\ B C_ x)}) /\ A.y e. {x | (x C_ A /\ B C_ x)}A.z e. {x | (x C_ A /\ B C_ x)} (y i^i z) e. {x | (x C_ A /\ B C_ x)}))
74		abssexg 3490	. . . . . . . 8 |- (A e. C -> {x | (x C_ A /\ B C_ x)} e. _V)
75		eqid 1884	. . . . . . . . 9 |- U.{x | (x C_ A /\ B C_ x)} = U.{x | (x C_ A /\ B C_ x)}
76	75	isfil 10266	. . . . . . . 8 |- ({x | (x C_ A /\ B C_ x)} e. _V -> ({x | (x C_ A /\ B C_ x)} e. Fil <-> ((-. (/) e. {x | (x C_ A /\ B C_ x)} /\ U.{x | (x C_ A /\ B C_ x)} e. {x | (x C_ A /\ B C_ x)}) /\ A.yA.z((y e. {x | (x C_ A /\ B C_ x)} /\ z C_ U.{x | (x C_ A /\ B C_ x)} /\ y C_ z) -> z e. {x | (x C_ A /\ B C_ x)}) /\ A.y e. {x | (x C_ A /\ B C_ x)}A.z e. {x | (x C_ A /\ B C_ x)} (y i^i z) e. {x | (x C_ A /\ B C_ x)})))
77	74, 76	syl 12	. . . . . . 7 |- (A e. C -> ({x | (x C_ A /\ B C_ x)} e. Fil <-> ((-. (/) e. {x | (x C_ A /\ B C_ x)} /\ U.{x | (x C_ A /\ B C_ x)} e. {x | (x C_ A /\ B C_ x)}) /\ A.yA.z((y e. {x | (x C_ A /\ B C_ x)} /\ z C_ U.{x | (x C_ A /\ B C_ x)} /\ y C_ z) -> z e. {x | (x C_ A /\ B C_ x)}) /\ A.y e. {x | (x C_ A /\ B C_ x)}A.z e. {x | (x C_ A /\ B C_ x)} (y i^i z) e. {x | (x C_ A /\ B C_ x)})))
78	77	3ad2ant1 897	. . . . . 6 |- ((A e. C /\ B C_ A /\ B =/= (/)) -> ({x | (x C_ A /\ B C_ x)} e. Fil <-> ((-. (/) e. {x | (x C_ A /\ B C_ x)} /\ U.{x | (x C_ A /\ B C_ x)} e. {x | (x C_ A /\ B C_ x)}) /\ A.yA.z((y e. {x | (x C_ A /\ B C_ x)} /\ z C_ U.{x | (x C_ A /\ B C_ x)} /\ y C_ z) -> z e. {x | (x C_ A /\ B C_ x)}) /\ A.y e. {x | (x C_ A /\ B C_ x)}A.z e. {x | (x C_ A /\ B C_ x)} (y i^i z) e. {x | (x C_ A /\ B C_ x)})))
79	78	adantr 425	. . . . 5 |- (((A e. C /\ B C_ A /\ B =/= (/)) /\ A = U.{x | (x C_ A /\ B C_ x)}) -> ({x | (x C_ A /\ B C_ x)} e. Fil <-> ((-. (/) e. {x | (x C_ A /\ B C_ x)} /\ U.{x | (x C_ A /\ B C_ x)} e. {x | (x C_ A /\ B C_ x)}) /\ A.yA.z((y e. {x | (x C_ A /\ B C_ x)} /\ z C_ U.{x | (x C_ A /\ B C_ x)} /\ y C_ z) -> z e. {x | (x C_ A /\ B C_ x)}) /\ A.y e. {x | (x C_ A /\ B C_ x)}A.z e. {x | (x C_ A /\ B C_ x)} (y i^i z) e. {x | (x C_ A /\ B C_ x)})))
80	73, 79	mpbird 213	. . . 4 |- (((A e. C /\ B C_ A /\ B =/= (/)) /\ A = U.{x | (x C_ A /\ B C_ x)}) -> {x | (x C_ A /\ B C_ x)} e. Fil)
81	80	ex 402	. . 3 |- ((A e. C /\ B C_ A /\ B =/= (/)) -> (A = U.{x | (x C_ A /\ B C_ x)} -> {x | (x C_ A /\ B C_ x)} e. Fil))
82	21, 81	jcai 313	. 2 |- ((A e. C /\ B C_ A /\ B =/= (/)) -> (A = U.{x | (x C_ A /\ B C_ x)} /\ {x | (x C_ A /\ B C_ x)} e. Fil))
83	82	ancomd 483	1 |- ((A e. C /\ B C_ A /\ B =/= (/)) -> ({x | (x C_ A /\ B C_ x)} e. Fil /\ A = U.{x | (x C_ A /\ B C_ x)}))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858  A.wal 1296   = wceq 1298   e. wcel 1300  {cab 1871   =/= wne 2017  A.wral 2105  _Vcvv 2292   i^i cin 2592   C_ wss 2593  (/)c0 2875  U.cuni 3177  Filcfil 10264

This theorem is referenced by:  fixufil 15576  fcluscf 15612  flimfnfcls 15615

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-sep 3438  ax-nul 3445  ax-pow 3481

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3an 860  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-v 2294  df-dif 2597  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-uni 3178  df-fil 10265

Copyright terms: Public domain