Theorem fgsb2 10580

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 2083	. . . . . . . . . 10 |- (x = (/) -> (y (_ x <-> y (_ (/)))
2	1	rexbidv 1664	. . . . . . . . 9 |- (x = (/) -> (E.y e. (fi` A)y (_ x <-> E.y e. (fi` A)y (_ (/)))
3	2	elrab 1905	. . . . . . . 8 |- ((/) e. {x e. P~X | E.y e. (fi` A)y (_ x} <-> ((/) e. P~X /\ E.y e. (fi` A)y (_ (/)))
4		ss0 2303	. . . . . . . . . . . 12 |- (y (_ (/) -> y = (/))
5	4	eleq1d 1540	. . . . . . . . . . 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 1743	. . . . . . . . 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 10459	. . . . . . . . 9 |- (X e. V -> U.{x e. P~X | E.y e. (fi` A)y (_ x} e. P~X)
13	12	3ad2ant2 801	. . . . . . . 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 2347	. . . . . . . . 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 10484	. . . . . . . . . 10 |- (A e. V -> (A =/= (/) -> (fi` A) =/= (/)))
16		ssexg 2721	. . . . . . . . . . 11 |- ((A (_ P~X /\ P~X e. V) -> A e. V)
17		3simp1 788	. . . . . . . . . . 11 |- ((A (_ P~X /\ X e. V /\ A =/= (/)) -> A (_ P~X)
18		pwexg 2746	. . . . . . . . . . . 12 |- (X e. V -> P~X e. V)
19	18	3ad2ant2 801	. . . . . . . . . . 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 790	. . . . . . . . . 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 10488	. . . . . . . . . . . . . . . . . . 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 2758	. . . . . . . . . . . . . . . . . 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 2074	. . . . . . . . . . . . . . 15 |- (((A (_ P~X /\ X e. V /\ A =/= (/)) /\ y e. (fi` A)) -> y (_ X)
31		visset 1813	. . . . . . . . . . . . . . . 16 |- y e. V
32	31	elpw 2404	. . . . . . . . . . . . . . 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 2080	. . . . . . . . . . . . . . . 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 2082	. . . . . . . . . . . . . . . 16 |- (z = y -> (z (_ y <-> y (_ y))
38	37	rcla4ev 1877	. . . . . . . . . . . . . . 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 2083	. . . . . . . . . . . . . . . 16 |- (x = y -> (z (_ x <-> z (_ y))
42	41	rexbidv 1664	. . . . . . . . . . . . . . 15 |- (x = y -> (E.z e. (fi` A)z (_ x <-> E.z e. (fi` A)z (_ y))
43		sseq1 2082	. . . . . . . . . . . . . . . 16 |- (y = z -> (y (_ x <-> z (_ x))
44	43	cbvrexv 1801	. . . . . . . . . . . . . . 15 |- (E.y e. (fi` A)y (_ x <-> E.z e. (fi` A)z (_ x)
45	42, 44	syl5bb 532	. . . . . . . . . . . . . 14 |- (x = y -> (E.y e. (fi` A)y (_ x <-> E.z e. (fi` A)z (_ y))
46	45	elrab 1905	. . . . . . . . . . . . 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 2522	. . . . . . . . . . 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 1714	. . . . . . . . 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 1772	. . . . . . . 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 2509	. . . . . . 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 971	. . . . . . . 8 |- (z e. X -> A.x z e. X)
58	57	hbpw 2407	. . . . . . 7 |- (z e. P~X -> A.x z e. P~X)
59		ax-17 971	. . . . . . . 8 |- (y e. (fi` A) -> A.x y e. (fi` A))
60		ax-17 971	. . . . . . . . 9 |- (z e. y -> A.x z e. y)
61	60, 56	hbss 2062	. . . . . . . 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 1688	. . . . . . 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 971	. . . . . . . . 9 |- (w e. x -> A.y w e.