Theorem fgsb 14921

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.

Hypothesis

Ref	Expression
fgsb.1	|- B = {x | E.y(y C_ A /\ y e. Fin /\ x = |^|y)}

Assertion

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

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

Proof of Theorem fgsb

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

This theorem is referenced by:  efilcp 14922

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-fil 10265

Copyright terms: Public domain