Theorem fgsb2 14925

Description: Filter generated by a subbasis A. Bourbaki TG I.37 paragraph above prop. 1. (The theorem has been slightly modified because the definitions of the empty set are different in Bourbaki and Metamath.)

Assertion

Ref	Expression
fgsb2	|- ((A C_ ~PX /\ X e. _V /\ A =/= (/)) -> (-. (/) e. ( fi ` A) -> {x e. ~PX | E.y e. ( fi ` A)y C_ x} e. Fil))

Distinct variable groups:   y,A,x   x,X,y

Proof of Theorem fgsb2

Step	Hyp	Ref	Expression
1		sseq2 2639	. . . . . . . . . 10 |- (x = (/) -> (y C_ x <-> y C_ (/)))
2	1	rexbidv 2124	. . . . . . . . 9 |- (x = (/) -> (E.y e. ( fi ` A)y C_ x <-> E.y e. ( fi ` A)y C_ (/)))
3	2	elrab 2414	. . . . . . . 8 |- ((/) e. {x e. ~PX | E.y e. ( fi ` A)y C_ x} <-> ((/) e. ~PX /\ E.y e. ( fi ` A)y C_ (/)))
4		ss0 2902	. . . . . . . . . . . 12 |- (y C_ (/) -> y = (/))
5	4	eleq1d 1963	. . . . . . . . . . 11 |- (y C_ (/) -> (y e. ( fi ` A) <-> (/) e. ( fi ` A)))
6	5	biimpcd 172	. . . . . . . . . 10 |- (y e. ( fi ` A) -> (y C_ (/) -> (/) e. ( fi ` A)))
7	6	r19.23aiv 2211	. . . . . . . . 9 |- (E.y e. ( fi ` A)y C_ (/) -> (/) e. ( fi ` A))
8	7	adantl 424	. . . . . . . 8 |- (((/) e. ~PX /\ E.y e. ( fi ` A)y C_ (/)) -> (/) e. ( fi ` A))
9	3, 8	sylbi 216	. . . . . . 7 |- ((/) e. {x e. ~PX | E.y e. ( fi ` A)y C_ x} -> (/) e. ( fi ` A))
10	9	con3i 114	. . . . . 6 |- (-. (/) e. ( fi ` A) -> -. (/) e. {x e. ~PX | E.y e. ( fi ` A)y C_ x})
11	10	adantl 424	. . . . 5 |- (((A C_ ~PX /\ X e. _V /\ A =/= (/)) /\ -. (/) e. ( fi ` A)) -> -. (/) e. {x e. ~PX | E.y e. ( fi ` A)y C_ x})
12		ump 14349	. . . . . . . . 9 |- (X e. _V -> U.{x e. ~PX | E.y e. ( fi ` A)y C_ x} e. ~PX)
13	12	3ad2ant2 898	. . . . . . . 8 |- ((A C_ ~PX /\ X e. _V /\ A =/= (/)) -> U.{x e. ~PX | E.y e. ( fi ` A)y C_ x} e. ~PX)
14		simp1 876	. . . . . . . . . . 11 |- ((A C_ ~PX /\ X e. _V /\ A =/= (/)) -> A C_ ~PX)
15		pwexg 3489	. . . . . . . . . . . 12 |- (X e. _V -> ~PX e. _V)
16	15	3ad2ant2 898	. . . . . . . . . . 11 |- ((A C_ ~PX /\ X e. _V /\ A =/= (/)) -> ~PX e. _V)
17		ssexg 3457	. . . . . . . . . . 11 |- ((A C_ ~PX /\ ~PX e. _V) -> A e. _V)
18	14, 16, 17	syl11anc 524	. . . . . . . . . 10 |- ((A C_ ~PX /\ X e. _V /\ A =/= (/)) -> A e. _V)
19		simp3 878	. . . . . . . . . 10 |- ((A C_ ~PX /\ X e. _V /\ A =/= (/)) -> A =/= (/))
20		fine2 10214	. . . . . . . . . 10 |- (A e. _V -> (A =/= (/) -> ( fi ` A) =/= (/)))
21	18, 19, 20	sylc 83	. . . . . . . . 9 |- ((A C_ ~PX /\ X e. _V /\ A =/= (/)) -> ( fi ` A) =/= (/))
22		fiiu2 10220	. . . . . . . . . . . . . . . . . . 19 |- (A e. _V -> (y e. ( fi ` A) -> y C_ U.A))
23	17, 22	syl 12	. . . . . . . . . . . . . . . . . 18 |- ((A C_ ~PX /\ ~PX e. _V) -> (y e. ( fi ` A) -> y C_ U.A))
24	14, 16, 23	syl11anc 524	. . . . . . . . . . . . . . . . 17 |- ((A C_ ~PX /\ X e. _V /\ A =/= (/)) -> (y e. ( fi ` A) -> y C_ U.A))
25	24	imp 377	. . . . . . . . . . . . . . . 16 |- (((A C_ ~PX /\ X e. _V /\ A =/= (/)) /\ y e. ( fi ` A)) -> y C_ U.A)
26		sspwuni 3333	. . . . . . . . . . . . . . . . . 18 |- (A C_ ~PX <-> U.A C_ X)
27	14, 26	sylib 215	. . . . . . . . . . . . . . . . 17 |- ((A C_ ~PX /\ X e. _V /\ A =/= (/)) -> U.A C_ X)
28	27	adantr 425	. . . . . . . . . . . . . . . 16 |- (((A C_ ~PX /\ X e. _V /\ A =/= (/)) /\ y e. ( fi ` A)) -> U.A C_ X)
29	25, 28	sstrd 2627	. . . . . . . . . . . . . . 15 |- (((A C_ ~PX /\ X e. _V /\ A =/= (/)) /\ y e. ( fi ` A)) -> y C_ X)
30		visset 2295	. . . . . . . . . . . . . . . 16 |- y e. _V
31	30	elpw 3037	. . . . . . . . . . . . . . 15 |- (y e. ~PX <-> y C_ X)
32	29, 31	sylibr 217	. . . . . . . . . . . . . 14 |- (((A C_ ~PX /\ X e. _V /\ A =/= (/)) /\ y e. ( fi ` A)) -> y e. ~PX)
33		simpr 350	. . . . . . . . . . . . . . . 16 |- (((A C_ ~PX /\ X e. _V /\ A =/= (/)) /\ y e. ( fi ` A)) -> y e. ( fi ` A))
34		ssid 2634	. . . . . . . . . . . . . . . 16 |- y C_ y
35	33, 34	jctir 317	. . . . . . . . . . . . . . 15 |- (((A C_ ~PX /\ X e. _V /\ A =/= (/)) /\ y e. ( fi ` A)) -> (y e. ( fi ` A) /\ y C_ y))
36		sseq1 2637	. . . . . . . . . . . . . . . 16 |- (z = y -> (z C_ y <-> y C_ y))
37	36	rcla4ev 2381	. . . . . . . . . . . . . . 15 |- ((y e. ( fi ` A) /\ y C_ y) -> E.z e. ( fi ` A)z C_ y)
38	35, 37	syl 12	. . . . . . . . . . . . . 14 |- (((A C_ ~PX /\ X e. _V /\ A =/= (/)) /\ y e. ( fi ` A)) -> E.z e. ( fi ` A)z C_ y)
39	32, 38	jca 310	. . . . . . . . . . . . 13 |- (((A C_ ~PX /\ X e. _V /\ A =/= (/)) /\ y e. ( fi ` A)) -> (y e. ~PX /\ E.z e. ( fi ` A)z C_ y))
40		sseq2 2639	. . . . . . . . . . . . . . . 16 |- (x = y -> (z C_ x <-> z C_ y))
41	40	rexbidv 2124	. . . . . . . . . . . . . . 15 |- (x = y -> (E.z e. ( fi ` A)z C_ x <-> E.z e. ( fi ` A)z C_ y))
42		sseq1 2637	. . . . . . . . . . . . . . . 16 |- (y = z -> (y C_ x <-> z C_ x))
43	42	cbvrexv 2281	. . . . . . . . . . . . . . 15 |- (E.y e. ( fi ` A)y C_ x <-> E.z e. ( fi ` A)z C_ x)
44	41, 43	syl5bb 591	. . . . . . . . . . . . . 14 |- (x = y -> (E.y e. ( fi ` A)y C_ x <-> E.z e. ( fi ` A)z C_ y))
45	44	elrab 2414	. . . . . . . . . . . . 13 |- (y e. {x e. ~PX | E.y e. ( fi ` A)y C_ x} <-> (y e. ~PX /\ E.z e. ( fi ` A)z C_ y))
46	39, 45	sylibr 217	. . . . . . . . . . . 12 |- (((A C_ ~PX /\ X e. _V /\ A =/= (/)) /\ y e. ( fi ` A)) -> y e. {x e. ~PX | E.y e. ( fi ` A)y C_ x})
47	46, 34	jctil 316	. . . . . . . . . . 11 |- (((A C_ ~PX /\ X e. _V /\ A =/= (/)) /\ y e. ( fi ` A)) -> (y C_ y /\ y e. {x e. ~PX | E.y e. ( fi ` A)y C_ x}))
48		ssuni 3201	. . . . . . . . . . 11 |- ((y C_ y /\ y e. {x e. ~PX | E.y e. ( fi ` A)y C_ x}) -> y C_ U.{x e. ~PX | E.y e. ( fi ` A)y C_ x})
49	47, 48	syl 12	. . . . . . . . . 10 |- (((A C_ ~PX /\ X e. _V /\ A =/= (/)) /\ y e. ( fi ` A)) -> y C_ U.{x e. ~PX | E.y e. ( fi ` A)y C_ x})
50	49	r19.21aiva 2176	. . . . . . . . 9 |- ((A C_ ~PX /\ X e. _V /\ A =/= (/)) -> A.y e. ( fi ` A)y C_ U.{x e. ~PX | E.y e. ( fi ` A)y C_ x})
51		r19.2z 2958	. . . . . . . . 9 |- ((( fi ` A) =/= (/) /\ A.y e. ( fi ` A)y C_ U.{x e. ~PX | E.y e. ( fi ` A)y C_ x}) -> E.y e. ( fi ` A)y C_ U.{x e. ~PX | E.y e. ( fi ` A)y C_ x})
52	21, 50, 51	syl11anc 524	. . . . . . . 8 |- ((A C_ ~PX /\ X e. _V /\ A =/= (/)) -> E.y e. ( fi ` A)y C_ U.{x e. ~PX | E.y e. ( fi ` A)y C_ x})
53	13, 52	jca 310	. . . . . . 7 |- ((A C_ ~PX /\ X e. _V /\ A =/= (/)) -> (U.{x e. ~PX | E.y e. ( fi ` A)y C_ x} e. ~PX /\ E.y e. ( fi ` A)y C_ U.{x e. ~PX | E.y e. ( fi ` A)y C_ x}))
54	53	adantr 425	. . . . . 6 |- (((A C_ ~PX /\ X e. _V /\ A =/= (/)) /\ -. (/) e. ( fi ` A)) -> (U.{x e. ~PX | E.y e. ( fi ` A)y C_ x} e. ~PX /\ E.y e. ( fi ` A)y C_ U.{x e. ~PX | E.y e. ( fi ` A)y C_ x}))
55		hbrab1 2257	. . . . . . . 8 |- (z e. {x e. ~PX | E.y e. ( fi ` A)y C_ x} -> A.x z e. {x e. ~PX | E.y e. ( fi ` A)y C_ x})
56	55	hbuni 3183	. . . . . . 7 |- (z e. U.{x e. ~PX | E.y e. ( fi ` A)y C_ x} -> A.x z e. U.{x e. ~PX | E.y e. ( fi ` A)y C_ x})
57		ax-17 1317	. . . . . . . 8 |- (z e. X -> A.x z e. X)
58	57	hbpw 3041	. . . . . . 7 |- (z e. ~PX -> A.x z e. ~PX)
59		ax-17 1317	. . . . . . . 8 |- (y e. ( fi ` A) -> A.x y e. ( fi ` A))
60		ax-17 1317	. . . . . . . . 9 |- (z e. y -> A.x z e. y)
61	60, 56	hbss 2614	. . . . . . . 8 |- (y C_ U.{x e. ~PX | E.y e. ( fi ` A)y C_ x} -> A.x y C_ U.{x e. ~PX | E.y e. ( fi ` A)y C_ x})
62	59, 61	hbrex 2149	. . . . . . 7 |- (E.y e. ( fi ` A)y C_ U.{x e. ~PX | E.y e. ( fi ` A)y C_ x} -> A.xE.y e. ( fi ` A)y C_ U.{x e. ~PX | E.y e. ( fi ` A)y C_ x})
63		ax-17 1317	. . . . . . . . 9 |- (w e. x -> A.y w e. x)
64		hbre1 2150	. . . . . . . . . . 11 |- (E.y e. ( fi ` A)y C_ x -> A.yE.y e. ( fi ` A)y C_ x)
65		ax-17 1317	. . . . . . . . . . 11 |- (z e. ~PX -> A.y z e. ~PX)
66	64, 65	hbrab 2258	. . . . . . . . . 10 |- (z e. {x e. ~PX | E.y e. ( fi ` A)y C_ x} -> A.y z e. {x e. ~PX | E.y e. ( fi ` A)y C_ x})
67	66	hbuni 3183	. . . . . . . . 9 |- (z e. U.{x e. ~PX | E.y e. ( fi ` A)y C_ x} -> A.y z e. U.{x e. ~PX | E.y e. ( fi ` A)y C_ x})
68	63, 67	hbeq 1995	. . . . . . . 8 |- (x = U.{x e. ~PX | E.y e. ( fi ` A)y C_ x} -> A.y x = U.{x e. ~PX | E.y e. ( fi ` A)y C_ x})
69		sseq2 2639	. . . . . . . 8 |- (x = U.{x e. ~PX | E.y e. ( fi ` A)y C_ x} -> (y C_ x <-> y C_ U.{x e. ~PX | E.y e. ( fi ` A)y C_ x}))
70	68, 69	rexbid 2122	. . . . . . 7 |- (x = U.{x e. ~PX | E.y e. ( fi ` A)y C_ x} -> (E.y e. ( fi ` A)y C_ x <-> E.y e. ( fi ` A)y C_ U.{x e. ~PX | E.y e. ( fi ` A)y C_ x}))
71	56, 58, 62, 70	elrabf 2413	. . . . . 6 |- (U.{x e. ~PX | E.y e. ( fi ` A)y C_ x} e. {x e. ~PX | E.y e. ( fi ` A)y C_ x} <-> (U.{x e. ~PX | E.y e. ( fi ` A)y C_ x} e. ~PX /\ E.y e. ( fi ` A)y C_ U.{x e. ~PX | E.y e. ( fi ` A)y C_ x}))
72	54, 71	sylibr 217	. . . . 5 |- (((A C_ ~PX /\ X e. _V /\ A =/= (/)) /\ -. (/) e. ( fi ` A)) -> U.{x e. ~PX | E.y e. ( fi ` A)y C_ x} e. {x e. ~PX | E.y e. ( fi ` A)y C_ x})
73	11, 72	jca 310	. . . 4 |- (((A C_ ~PX /\ X e. _V /\ A =/= (/)) /\ -. (/) e. ( fi ` A)) -> (-. (/) e. {x e. ~PX | E.y e. ( fi ` A)y C_ x} /\ U.{x e. ~PX | E.y e. ( fi ` A)y C_ x} e. {x e. ~PX | E.y e. ( fi ` A)y C_ x}))
74		visset 2295	. . . . . . . . . . . 12 |- b e. _V
75	74	elpw 3037	. . . . . . . . . . 11 |- (b e. ~PU.{x e. ~PX | E.y e. ( fi ` A)y C_ x} <-> b C_ U.{x e. ~PX | E.y e. ( fi ` A)y C_ x})
76		unissb 3208	. . . . . . . . . . . . . 14 |- (U.{x e. ~PX | E.y e. ( fi ` A)y C_ x} C_ X <-> A.t e. {x e. ~PX | E.y e. ( fi ` A)y C_ x}t C_ X)
77		sseq2 2639	. . . . . . . . . . . . . . . . 17 |- (x = t -> (y C_ x <-> y C_ t))
78	77	rexbidv 2124	. . . . . . . . . . . . . . . 16 |- (x = t -> (E.y e. ( fi ` A)y C_ x <-> E.y e. ( fi ` A)y C_ t))
79	78	elrab 2414	. . . . . . . . . . . . . . 15 |- (t e. {x e. ~PX | E.y e. ( fi ` A)y C_ x} <-> (t e. ~PX /\ E.y e. ( fi ` A)y C_ t))
80		elpwi 3039	. . . . . . . . . . . . . . . 16 |- (t e. ~PX -> t C_ X)
81	80	adantr 425	. . . . . . . . . . . . . . 15 |- ((t e. ~PX /\ E.y e. ( fi ` A)y C_ t) -> t C_ X)
82	79, 81	sylbi 216	. . . . . . . . . . . . . 14 |- (t e. {x e. ~PX | E.y e. ( fi ` A)y C_ x} -> t C_ X)
83	76, 82	mprgbir 2163	. . . . . . . . . . . . 13 |- U.{x e. ~PX | E.y e. ( fi ` A)y C_ x} C_ X
84		sspwb 3503	. . . . . . . . . . . . 13 |- (U.{x e. ~PX | E.y e. ( fi ` A)y C_ x} C_ X <-> ~PU.{x e. ~PX | E.y e. ( fi ` A)y C_ x} C_ ~PX)
85	83, 84	mpbi 206	. . . . . . . . . . . 12 |- ~PU.{x e. ~PX | E.y e. ( fi ` A)y C_ x} C_ ~PX
86	85	sseli 2617	. . . . . . . . . . 11 |- (b e. ~PU.{x e. ~PX | E.y e. ( fi ` A)y C_ x} -> b e. ~PX)
87	75, 86	sylbir 218	. . . . . . . . . 10 |- (b C_ U.{x e. ~PX | E.y e. ( fi ` A)y C_ x} -> b e. ~PX)
88	87	3ad2ant2 898	. . . . . . . . 9 |- (((a e. ~PX /\ E.y e. ( fi ` A)y C_ a) /\ b C_ U.{x e. ~PX | E.y e. ( fi ` A)y C_ x} /\ a C_ b) -> b e. ~PX)
89		r19.41v 2236	. . . . . . . . . . . 12 |- (E.y e. ( fi ` A)(y C_ a /\ a C_ b) <-> (E.y e. ( fi ` A)y C_ a /\ a C_ b))
90		sstr 2625	. . . . . . . . . . . . 13 |- ((y C_ a /\ a C_ b) -> y C_ b)
91	90	reximi 2198	. . . . . . . . . . . 12 |- (E.y e. ( fi ` A)(y C_ a /\ a C_ b) -> E.y e. ( fi ` A)y C_ b)
92	89, 91	sylbir 218	. . . . . . . . . . 11 |- ((E.y e. ( fi ` A)y C_ a /\ a C_ b) -> E.y e. ( fi ` A)y C_ b)
93	92	adantll 428	. . . . . . . . . 10 |- (((a e. ~PX /\ E.y e. ( fi ` A)y C_ a) /\ a C_ b) -> E.y e. ( fi ` A)y C_ b)
94	93	3adant2 895	. . . . . . . . 9 |- (((a e. ~PX /\ E.y e. ( fi ` A)y C_ a) /\ b C_ U.{x e. ~PX | E.y e. ( fi ` A)y C_ x} /\ a C_ b) -> E.y e. ( fi ` A)y C_ b)
95	88, 94	jca 310	. . . . . . . 8 |- (((a e. ~PX /\ E.y e. ( fi ` A)y C_ a) /\ b C_ U.{x e. ~PX | E.y e. ( fi ` A)y C_ x} /\ a C_ b) -> (b e. ~PX /\ E.y e. ( fi ` A)y C_ b))
96		sseq2 2639	. . . . . . . . . 10 |- (x = a -> (y C_ x <-> y C_ a))
97	96	rexbidv 2124	. . . . . . . . 9 |- (x = a -> (E.y e. ( fi ` A)y C_ x <-> E.y e. ( fi ` A)y C_ a))
98	97	elrab 2414	. . . . . . . 8 |- (a e. {x e. ~PX | E.y e. ( fi ` A)y C_ x} <-> (a e. ~PX /\ E.y e. ( fi ` A)y C_ a))
99	95, 98	syl3an1b 1133	. . . . . . 7 |- ((a e. {x e. ~PX | E.y e. ( fi ` A)y C_ x} /\ b C_ U.{x e. ~PX | E.y e. ( fi ` A)y C_ x} /\ a C_ b) -> (b e. ~PX /\ E.y e. ( fi ` A)y C_ b))
100		sseq2 2639	. . . . . . . . 9 |- (x = b -> (y C_ x <-> y C_ b))
101	100	rexbidv 2124	. . . . . . . 8 |- (x = b -> (E.y e. ( fi ` A)y C_ x <-> E.y e. ( fi ` A)y C_ b))
102	101	elrab 2414	. . . . . . 7 |- (b e. {x e. ~PX | E.y e. ( fi ` A)y C_ x} <-> (b e. ~PX /\ E.y e. ( fi ` A)y C_ b))
103	99, 102	sylibr 217	. . . . . 6 |- ((a e. {x e. ~PX | E.y e. ( fi ` A)y C_ x} /\ b C_ U.{x e. ~PX | E.y e. ( fi ` A)y C_ x} /\ a C_ b) -> b e. {x e. ~PX | E.y e. ( fi ` A)y C_ x})
104	103	gen2 1329	. . . . 5 |- A.aA.b((a e. {x e. ~PX | E.y e. ( fi ` A)y C_ x} /\ b C_ U.{x e. ~PX | E.y e. ( fi ` A)y C_ x} /\ a C_ b) -> b e. {x e. ~PX | E.y e. ( fi ` A)y C_ x})
105	104	a1i 8	. . . 4 |- (((A C_ ~PX /\ X e. _V /\ A =/= (/)) /\ -. (/) e. ( fi ` A)) -> A.aA.b((a e. {x e. ~PX | E.y e. ( fi ` A)y C_ x} /\ b C_ U.{x e. ~PX | E.y e. ( fi ` A)y C_ x} /\ a C_ b) -> b e. {x e. ~PX | E.y e. ( fi ` A)y C_ x}))
106		inpws1 14345	. . . . . . . . . . 11 |- (a e. ~PX -> (a i^i b) e. ~PX)
107	106	adantr 425	. . . . . . . . . 10 |- ((a e. ~PX /\ b e. ~PX) -> (a i^i b) e. ~PX)
108		ax-17 1317	. . . . . . . . . . . . . . . . . . 19 |- ((u i^i v) C_ (a i^i b) -> A.y(u i^i v) C_ (a i^i b))
109		sseq1 2637	. . . . . . . . . . . . . . . . . . 19 |- (y = (u i^i v) -> (y C_ (a i^i b) <-> (u i^i v) C_ (a i^i b)))
110	108, 109	rcla4e 2375	. . . . . . . . . . . . . . . . . 18 |- (((u i^i v) e. ( fi ` A) /\ (u i^i v) C_ (a i^i b)) -> E.y e. ( fi ` A)y C_ (a i^i b))
111		elfvdm 4704	. . . . . . . . . . . . . . . . . . . 20 |- (u e. ( fi ` A) -> A e. dom fi )
112		infi 10280	. . . . . . . . . . . . . . . . . . . . 21 |- (A e. dom fi -> ((u e. ( fi ` A) /\ v e. ( fi ` A)) -> (u i^i v) e. ( fi ` A)))
113	112	exp3a 405	. . . . . . . . . . . . . . . . . . . 20 |- (A e. dom fi -> (u e. ( fi ` A) -> (v e. ( fi ` A) -> (u i^i v) e. ( fi ` A))))
114	111, 113	mpcom 60	. . . . . . . . . . . . . . . . . . 19 |- (u e. ( fi ` A) -> (v e. ( fi ` A) -> (u i^i v) e. ( fi ` A)))
115	114	imp 377	. . . . . . . . . . . . . . . . . 18 |- ((u e. ( fi ` A) /\ v e. ( fi ` A)) -> (u i^i v) e. ( fi ` A))
116		ss2in 2820	. . . . . . . . . . . . . . . . . 18 |- ((u C_ a /\ v C_ b) -> (u i^i v) C_ (a i^i b))
117	110, 115, 116	syl2an 503	. . . . . . . . . . . . . . . . 17 |- (((u e. ( fi ` A) /\ v e. ( fi ` A)) /\ (u C_ a /\ v C_ b)) -> E.y e. ( fi ` A)y C_ (a i^i b))
118	117	an4s 566	. . . . . . . . . . . . . . . 16 |- (((u e. ( fi ` A) /\ u C_ a) /\ (v e. ( fi ` A) /\ v C_ b)) -> E.y e. ( fi ` A)y C_ (a i^i b))
119	118	expcom 403	. . . . . . . . . . . . . . 15 |- ((v e. ( fi ` A) /\ v C_ b) -> ((u e. ( fi ` A) /\ u C_ a) -> E.y e. ( fi ` A)y C_ (a i^i b)))
120	119	r19.23aiva 2212	. . . . . . . . . . . . . 14 |- (E.v e. ( fi ` A)v C_ b -> ((u e. ( fi ` A) /\ u C_ a) -> E.y e. ( fi ` A)y C_ (a i^i b)))
121	120	com12 14	. . . . . . . . . . . . 13 |- ((u e. ( fi ` A) /\ u C_ a) -> (E.v e. ( fi ` A)v C_ b -> E.y e. ( fi ` A)y C_ (a i^i b)))
122	121	r19.23aiva 2212	. . . . . . . . . . . 12 |- (E.u e. ( fi ` A)u C_ a -> (E.v e. ( fi ` A)v C_ b -> E.y e. ( fi ` A)y C_ (a i^i b)))
123	122	imp 377	. . . . . . . . . . 11 |- ((E.u e. ( fi ` A)u C_ a /\ E.v e. ( fi ` A)v C_ b) -> E.y e. ( fi ` A)y C_ (a i^i b))
124		sseq1 2637	. . . . . . . . . . . 12 |- (y = u -> (y C_ a <-> u C_ a))
125	124	cbvrexv 2281	. . . . . . . . . . 11 |- (E.y e. ( fi ` A)y C_ a <-> E.u e. ( fi ` A)u C_ a)
126		sseq1 2637	. . . . . . . . . . . 12 |- (y = v -> (y C_ b <-> v C_ b))
127	126	cbvrexv 2281	. . . . . . . . . . 11 |- (E.y e. ( fi ` A)y C_ b <-> E.v e. ( fi ` A)v C_ b)
128	123, 125, 127	syl2anb 504	. . . . . . . . . 10 |- ((E.y e. ( fi ` A)y C_ a /\ E.y e. ( fi ` A)y C_ b) -> E.y e. ( fi ` A)y C_ (a i^i b))
129	107, 128	anim12i 360	. . . . . . . . 9 |- (((a e. ~PX /\ b e. ~PX) /\ (E.y e. ( fi ` A)y C_ a /\ E.y e. ( fi ` A)y C_ b)) -> ((a i^i b) e. ~PX /\ E.y e. ( fi ` A)y C_ (a i^i b)))
130	129	an4s 566	. . . . . . . 8 |- (((a e. ~PX /\ E.y e. ( fi ` A)y C_ a) /\ (b e. ~PX /\ E.y e. ( fi ` A)y C_ b)) -> ((a i^i b) e. ~PX /\ E.y e. ( fi ` A)y C_ (a i^i b)))
131		simpl 346	. . . . . . . . . . 11 |- ((x = (a i^i b) /\ y e. ( fi ` A)) -> x = (a i^i b))
132	131	sseq2d 2645	. . . . . . . . . 10 |- ((x = (a i^i b) /\ y e. ( fi ` A)) -> (y C_ x <-> y C_ (a i^i b)))
133	132	rexbidva 2120	. . . . . . . . 9 |- (x = (a i^i b) -> (E.y e. ( fi ` A)y C_ x <-> E.y e. ( fi ` A)y C_ (a i^i b)))
134	133	elrab 2414	. . . . . . . 8 |- ((a i^i b) e. {x e. ~PX | E.y e. ( fi ` A)y C_ x} <-> ((a i^i b) e. ~PX /\ E.y e. ( fi ` A)y C_ (a i^i b)))
135	130, 134	sylibr 217	. . . . . . 7 |- (((a e. ~PX /\ E.y e. ( fi ` A)y C_ a) /\ (b e. ~PX /\ E.y e. ( fi ` A)y C_ b)) -> (a i^i b) e. {x e. ~PX | E.y e. ( fi ` A)y C_ x})
136		simpl 346	. . . . . . . . . 10 |- ((x = a /\ y e. ( fi ` A)) -> x = a)
137	136	sseq2d 2645	. . . . . . . . 9 |- ((x = a /\ y e. ( fi ` A)) -> (y C_ x <-> y C_ a))
138	137	rexbidva 2120	. . . . . . . 8 |- (x = a -> (E.y e. ( fi ` A)y C_ x <-> E.y e. ( fi ` A)y C_ a))
139	138	elrab 2414	. . . . . . 7 |- (a e. {x e. ~PX | E.y e. ( fi ` A)y C_ x} <-> (a e. ~PX /\ E.y e. ( fi ` A)y C_ a))
140		simpl 346	. . . . . . . . . 10 |- ((x = b /\ y e. ( fi ` A)) -> x = b)
141	140	sseq2d 2645	. . . . . . . . 9 |- ((x = b /\ y e. ( fi ` A)) -> (y C_ x <-> y C_ b))
142	141	rexbidva 2120	. . . . . . . 8 |- (x = b -> (E.y e. ( fi ` A)y C_ x <-> E.y e. ( fi ` A)y C_ b))
143	142	elrab 2414	. . . . . . 7 |- (b e. {x e. ~PX | E.y e. ( fi ` A)y C_ x} <-> (b e. ~PX /\ E.y e. ( fi ` A)y C_ b))
144	135, 139, 143	syl2anb 504	. . . . . 6 |- ((a e. {x e. ~PX | E.y e. ( fi ` A)y C_ x} /\ b e. {x e. ~PX | E.y e. ( fi ` A)y C_ x}) -> (a i^i b) e. {x e. ~PX | E.y e. ( fi ` A)y C_ x})
145	144	rgen2 2186	. . . . 5 |- A.a e. {x e. ~PX | E.y e. ( fi ` A)y C_ x}A.b e. {x e. ~PX | E.y e. ( fi ` A)y C_ x} (a i^i b) e. {x e. ~PX | E.y e. ( fi ` A)y C_ x}
146	145	a1i 8	. . . 4 |- (((A C_ ~PX /\ X e. _V /\ A =/= (/)) /\ -. (/) e. ( fi ` A)) -> A.a e. {x e. ~PX | E.y e. ( fi ` A)y C_ x}A.b e. {x e. ~PX | E.y e. ( fi ` A)y C_ x} (a i^i b) e. {x e. ~PX | E.y e. ( fi ` A)y C_ x})
147	73, 105, 146	3jca 1050	. . 3 |- (((A C_ ~PX /\ X e. _V /\ A =/= (/)) /\ -. (/) e. ( fi ` A)) -> ((-. (/) e. {x e. ~PX | E.y e. ( fi ` A)y C_ x} /\ U.{x e. ~PX | E.y e. ( fi ` A)y C_ x} e. {x e. ~PX | E.y e. ( fi ` A)y C_ x}) /\ A.aA.b((a e. {x e. ~PX | E.y e. ( fi ` A)y C_ x} /\ b C_ U.{x e. ~PX | E.y e. ( fi ` A)y C_ x} /\ a C_ b) -> b e. {x e. ~PX | E.y e. ( fi ` A)y C_ x}) /\ A.a e. {x e. ~PX | E.y e. ( fi ` A)y C_ x}A.b e. {x e. ~PX | E.y e. ( fi ` A)y C_ x} (a i^i b) e. {x e. ~PX | E.y e. ( fi ` A)y C_ x}))
148		rabexg 3460	. . . . . . 7 |- (~PX e. _V -> {x e. ~PX | E.y e. ( fi ` A)y C_ x} e. _V)
149	15, 148	syl 12	. . . . . 6 |- (X e. _V -> {x e. ~PX | E.y e. ( fi ` A)y C_ x} e. _V)
150	149	3ad2ant2 898	. . . . 5 |- ((A C_ ~PX /\ X e. _V /\ A =/= (/)) -> {x e. ~PX | E.y e. ( fi ` A)y C_ x} e. _V)
151	150	adantr 425	. . . 4 |- (((A C_ ~PX /\ X e. _V /\ A =/= (/)) /\ -. (/) e. ( fi ` A)) -> {x e. ~PX | E.y e. ( fi ` A)y C_ x} e. _V)
152		eqid 1884	. . . . 5 |- U.{x e. ~PX | E.y e. ( fi ` A)y C_ x} = U.{x e. ~PX | E.y e. ( fi ` A)y C_ x}
153	152	isfil 10266	. . . 4 |- ({x e. ~PX | E.y e. ( fi ` A)y C_ x} e. _V -> ({x e. ~PX | E.y e. ( fi ` A)y C_ x} e. Fil <-> ((-. (/) e. {x e. ~PX | E.y e. ( fi ` A)y C_ x} /\ U.{x e. ~PX | E.y e. ( fi ` A)y C_ x} e. {x e. ~PX | E.y e. ( fi ` A)y C_ x}) /\ A.aA.b((a e. {x e. ~PX | E.y e. ( fi ` A)y C_ x} /\ b C_ U.{x e. ~PX | E.y e. ( fi ` A)y C_ x} /\ a C_ b) -> b e. {x e. ~PX | E.y e. ( fi ` A)y C_ x}) /\ A.a e. {x e. ~PX | E.y e. ( fi ` A)y C_ x}A.b e. {x e. ~PX | E.y e. ( fi ` A)y C_ x} (a i^i b) e. {x e. ~PX | E.y e. ( fi ` A)y C_ x})))
154	151, 153	syl 12	. . 3 |- (((A C_ ~PX /\ X e. _V /\ A =/= (/)) /\ -. (/) e. ( fi ` A)) -> ({x e. ~PX | E.y e. ( fi ` A)y C_ x} e. Fil <-> ((-. (/) e. {x e. ~PX | E.y e. ( fi ` A)y C_ x} /\ U.{x e. ~PX | E.y e. ( fi ` A)y C_ x} e. {x e. ~PX | E.y e. ( fi ` A)y C_ x}) /\ A.aA.b((a e. {x e. ~PX | E.y e. ( fi ` A)y C_ x} /\ b C_ U.{x e. ~PX | E.y e. ( fi ` A)y C_ x} /\ a C_ b) -> b e. {x e. ~PX | E.y e. ( fi ` A)y C_ x}) /\ A.a e. {x e. ~PX | E.y e. ( fi ` A)y C_ x}A.b e. {x e. ~PX | E.y e. ( fi ` A)y C_ x} (a i^i b) e. {x e. ~PX | E.y e. ( fi ` A)y C_ x})))
155	147, 154	mpbird 213	. 2 |- (((A C_ ~PX /\ X e. _V /\ A =/= (/)) /\ -. (/) e. ( fi ` A)) -> {x e. ~PX | E.y e. ( fi ` A)y C_ x} e. Fil)
156	155	ex 402	1 |- ((A C_ ~PX /\ X e. _V /\ A =/= (/)) -> (-. (/) e. ( fi ` A) -> {x e. ~PX | E.y e. ( fi ` A)y C_ x} e. Fil))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858  A.wal 1296   = wceq 1298   e. wcel 1300   =/= wne 2017  A.wral 2105  E.wrex 2106  {crab 2108  _Vcvv 2292   i^i cin 2592   C_ wss 2593  (/)c0 2875  ~Pcpw 3032  U.cuni 3177  dom cdm 3986  ` cfv 3998   fi cfi 10210  Filcfil 10264

This theorem is referenced by:  efilcp2 14926

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-13 1311  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-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3or 859  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-reu 2111  df-rab 2112  df-v 2294  df-sbc 2454  df-csb 2541  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-pss 2607  df-nul 2876  df-if 2983  df-pw 3035  df-sn 3049  df-pr 3050  df-tp 3052  df-op 3053  df-uni 3178  df-int 3215  df-iun 3257  df-br 3339  df-opab 3396  df-tr 3412  df-eprel 3583  df-id 3586  df-po 3591  df-so 3604  df-fr 3625  df-we 3644  df-ord 3660  df-on 3661  df-lim 3662  df-suc 3663  df-om 3950  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-f1 4011  df-fo 4012  df-f1o 4013  df-fv 4014  df-opr 4886  df-oprab 4887  df-rdg 5140  df-1o 5177  df-oadd 5179  df-er 5318  df-en 5427  df-fin 5430  df-fi 10211  df-fil 10265

Copyright terms: Public domain