Theorem fgsb2 10508

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 (_ P~X /\ X e. V /\ A =/= (/)) -> (-. (/) e. (fi` A) -> {x e. P~X | E.y e. (fi` A)y (_ x} e. Fil))

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

Proof of Theorem fgsb2

Step	Hyp	Ref	Expression
1		sseq2 2080	. . . . . . . . . 10 |- (x = (/) -> (y (_ x <-> y (_ (/)))
2	1	rexbidv 1662	. . . . . . . . 9 |- (x = (/) -> (E.y e. (fi` A)y (_ x <-> E.y e. (fi` A)y (_ (/)))
3	2	elrab 1902	. . . . . . . 8 |- ((/) e. {x e. P~X | E.y e. (fi` A)y (_ x} <-> ((/) e. P~X /\ E.y e. (fi` A)y (_ (/)))
4		ss0 2300	. . . . . . . . . . . 12 |- (y (_ (/) -> y = (/))
5	4	eleq1d 1538	. . . . . . . . . . 11 |- (y (_ (/) -> (y e. (fi` A) <-> (/) e. (fi` A)))
6	5	biimpcd 155	. . . . . . . . . 10 |- (y e. (fi` A) -> (y (_ (/) -> (/) e. (fi` A)))
7	6	r19.23aiv 1741	. . . . . . . . 9 |- (E.y e. (fi` A)y (_ (/) -> (/) e. (fi` A))
8	7	adantl 388	. . . . . . . 8 |- (((/) e. P~X /\ E.y e. (fi` A)y (_ (/)) -> (/) e. (fi` A))
9	3, 8	sylbi 199	. . . . . . 7 |- ((/) e. {x e. P~X | E.y e. (fi` A)y (_ x} -> (/) e. (fi` A))
10	9	con3i 98	. . . . . 6 |- (-. (/) e. (fi` A) -> -. (/) e. {x e. P~X | E.y e. (fi` A)y (_ x})
11	10	adantl 388	. . . . 5 |- (((A (_ P~X /\ X e. V /\ A =/= (/)) /\ -. (/) e. (fi` A)) -> -. (/) e. {x e. P~X | E.y e. (fi` A)y (_ x})
12		ump 10413	. . . . . . . . 9 |- (X e. V -> U.{x e. P~X | E.y e. (fi` A)y (_ x} e. P~X)
13	12	3ad2ant2 800	. . . . . . . 8 |- ((A (_ P~X /\ X e. V /\ A =/= (/)) -> U.{x e. P~X | E.y e. (fi` A)y (_ x} e. P~X)
14		r19.2z 2344	. . . . . . . . 9 |- (((fi` A) =/= (/) /\ A.y e. (fi` A)y (_ U.{x e. P~X | E.y e. (fi` A)y (_ x}) -> E.y e. (fi` A)y (_ U.{x e. P~X | E.y e. (fi` A)y (_ x})
15		fine2 10434	. . . . . . . . . 10 |- (A e. V -> (A =/= (/) -> (fi` A) =/= (/)))
16		ssexg 2717	. . . . . . . . . . 11 |- ((A (_ P~X /\ P~X e. V) -> A e. V)
17		3simp1 787	. . . . . . . . . . 11 |- ((A (_ P~X /\ X e. V /\ A =/= (/)) -> A (_ P~X)
18		pwexg 2742	. . . . . . . . . . . 12 |- (X e. V -> P~X e. V)
19	18	3ad2ant2 800	. . . . . . . . . . 11 |- ((A (_ P~X /\ X e. V /\ A =/= (/)) -> P~X e. V)
20	16, 17, 19	sylanc 471	. . . . . . . . . 10 |- ((A (_ P~X /\ X e. V /\ A =/= (/)) -> A e. V)
21		3simp3 789	. . . . . . . . . 10 |- ((A (_ P~X /\ X e. V /\ A =/= (/)) -> A =/= (/))
22	15, 20, 21	sylc 68	. . . . . . . . 9 |- ((A (_ P~X /\ X e. V /\ A =/= (/)) -> (fi` A) =/= (/))
23		fiiu2 10436	. . . . . . . . . . . . . . . . . . 19 |- (A e. V -> (y e. (fi` A) -> y (_ U.A))
24	16, 23	syl 10	. . . . . . . . . . . . . . . . . 18 |- ((A (_ P~X /\ P~X e. V) -> (y e. (fi` A) -> y (_ U.A))
25	24, 17, 19	sylanc 471	. . . . . . . . . . . . . . . . 17 |- ((A (_ P~X /\ X e. V /\ A =/= (/)) -> (y e. (fi` A) -> y (_ U.A))
26	25	imp 350	. . . . . . . . . . . . . . . 16 |- (((A (_ P~X /\ X e. V /\ A =/= (/)) /\ y e. (fi` A)) -> y (_ U.A)
27		sspwuni 2754	. . . . . . . . . . . . . . . . . 18 |- (A (_ P~X <-> U.A (_ X)
28	17, 27	sylib 198	. . . . . . . . . . . . . . . . 17 |- ((A (_ P~X /\ X e. V /\ A =/= (/)) -> U.A (_ X)
29	28	adantr 389	. . . . . . . . . . . . . . . 16 |- (((A (_ P~X /\ X e. V /\ A =/= (/)) /\ y e. (fi` A)) -> U.A (_ X)
30	26, 29	sstrd 2071	. . . . . . . . . . . . . . 15 |- (((A (_ P~X /\ X e. V /\ A =/= (/)) /\ y e. (fi` A)) -> y (_ X)
31		visset 1810	. . . . . . . . . . . . . . . 16 |- y e. V
32	31	elpw 2401	. . . . . . . . . . . . . . 15 |- (y e. P~X <-> y (_ X)
33	30, 32	sylibr 200	. . . . . . . . . . . . . 14 |- (((A (_ P~X /\ X e. V /\ A =/= (/)) /\ y e. (fi` A)) -> y e. P~X)
34		pm3.27 323	. . . . . . . . . . . . . . . 16 |- (((A (_ P~X /\ X e. V /\ A =/= (/)) /\ y e. (fi` A)) -> y e. (fi` A))
35		ssid 2077	. . . . . . . . . . . . . . . 16 |- y (_ y
36	34, 35	jctir 293	. . . . . . . . . . . . . . 15 |- (((A (_ P~X /\ X e. V /\ A =/= (/)) /\ y e. (fi` A)) -> (y e. (fi` A) /\ y (_ y))
37		sseq1 2079	. . . . . . . . . . . . . . . 16 |- (z = y -> (z (_ y <-> y (_ y))
38	37	rcla4ev 1874	. . . . . . . . . . . . . . 15 |- ((y e. (fi` A) /\ y (_ y) -> E.z e. (fi` A)z (_ y)
39	36, 38	syl 10	. . . . . . . . . . . . . 14 |- (((A (_ P~X /\ X e. V /\ A =/= (/)) /\ y e. (fi` A)) -> E.z e. (fi` A)z (_ y)
40	33, 39	jca 288	. . . . . . . . . . . . 13 |- (((A (_ P~X /\ X e. V /\ A =/= (/)) /\ y e. (fi` A)) -> (y e. P~X /\ E.z e. (fi` A)z (_ y))
41		sseq2 2080	. . . . . . . . . . . . . . . 16 |- (x = y -> (z (_ x <-> z (_ y))
42	41	rexbidv 1662	. . . . . . . . . . . . . . 15 |- (x = y -> (E.z e. (fi` A)z (_ x <-> E.z e. (fi` A)z (_ y))
43		sseq1 2079	. . . . . . . . . . . . . . . 16 |- (y = z -> (y (_ x <-> z (_ x))
44	43	cbvrexv 1798	. . . . . . . . . . . . . . 15 |- (E.y e. (fi` A)y (_ x <-> E.z e. (fi` A)z (_ x)
45	42, 44	syl5bb 531	. . . . . . . . . . . . . 14 |- (x = y -> (E.y e. (fi` A)y (_ x <-> E.z e. (fi` A)z (_ y))
46	45	elrab 1902	. . . . . . . . . . . . 13 |- (y e. {x e. P~X | E.y e. (fi` A)y (_ x} <-> (y e. P~X /\ E.z e. (fi` A)z (_ y))
47	40, 46	sylibr 200	. . . . . . . . . . . 12 |- (((A (_ P~X /\ X e. V /\ A =/= (/)) /\ y e. (fi` A)) -> y e. {x e. P~X | E.y e. (fi` A)y (_ x})
48	47, 35	jctil 292	. . . . . . . . . . 11 |- (((A (_ P~X /\ X e. V /\ A =/= (/)) /\ y e. (fi` A)) -> (y (_ y /\ y e. {x e. P~X | E.y e. (fi` A)y (_ x}))
49		ssuni 2518	. . . . . . . . . . 11 |- ((y (_ y /\ y e. {x e. P~X | E.y e. (fi` A)y (_ x}) -> y (_ U.{x e. P~X | E.y e. (fi` A)y (_ x})
50	48, 49	syl 10	. . . . . . . . . 10 |- (((A (_ P~X /\ X e. V /\ A =/= (/)) /\ y e. (fi` A)) -> y (_ U.{x e. P~X | E.y e. (fi` A)y (_ x})
51	50	r19.21aiva 1712	. . . . . . . . 9 |- ((A (_ P~X /\ X e. V /\ A =/= (/)) -> A.y e. (fi` A)y (_ U.{x e. P~X | E.y e. (fi` A)y (_ x})
52	14, 22, 51	sylanc 471	. . . . . . . 8 |- ((A (_ P~X /\ X e. V /\ A =/= (/)) -> E.y e. (fi` A)y (_ U.{x e. P~X | E.y e. (fi` A)y (_ x})
53	13, 52	jca 288	. . . . . . 7 |- ((A (_ P~X /\ X e. V /\ A =/= (/)) -> (U.{x e. P~X | E.y e. (fi` A)y (_ x} e. P~X /\ E.y e. (fi` A)y (_ U.{x e. P~X | E.y e. (fi` A)y (_ x}))
54	53	adantr 389	. . . . . 6 |- (((A (_ P~X /\ X e. V /\ A =/= (/)) /\ -. (/) e. (fi` A)) -> (U.{x e. P~X | E.y e. (fi` A)y (_ x} e. P~X /\ E.y e. (fi` A)y (_ U.{x e. P~X | E.y e. (fi` A)y (_ x}))
55		hbrab1 1770	. . . . . . . 8 |- (z e. {x e. P~X | E.y e. (fi` A)y (_ x} -> A.x z e. {x e. P~X | E.y e. (fi` A)y (_ x})
56	55	hbuni 2505	. . . . . . 7 |- (z e. U.{x e. P~X | E.y e. (fi` A)y (_ x} -> A.x z e. U.{x e. P~X | E.y e. (fi` A)y (_ x})
57		ax-17 970	. . . . . . . 8 |- (z e. X -> A.x z e. X)
58	57	hbpw 2404	. . . . . . 7 |- (z e. P~X -> A.x z e. P~X)
59		ax-17 970	. . . . . . . 8 |- (y e. (fi` A) -> A.x y e. (fi` A))
60		ax-17 970	. . . . . . . . 9 |- (z e. y -> A.x z e. y)
61	60, 56	hbss 2059	. . . . . . . 8 |- (y (_ U.{x e. P~X | E.y e. (fi` A)y (_ x} -> A.x y (_ U.{x e. P~X | E.y e. (fi` A)y (_ x})
62	59, 61	hbrex 1686	. . . . . . 7 |- (E.y e. (fi` A)y (_ U.{x e. P~X | E.y e. (fi` A)y (_ x} -> A.xE.y e. (fi` A)y (_ U.{x e. P~X | E.y e. (fi` A)y (_ x})
63		ax-17 970	. . . . . . . . 9 |- (w e. x -> A.y w e. x