Theorem fgsb 10555

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 (_ A /\ y e. Fin /\ x = |^|y)}

Assertion

Ref	Expression
fgsb	|- ((A (_ P~X /\ X e. V /\ A =/= (/)) -> (-. (/) e. B -> {x e. P~X | E.y e. B y (_ 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 2086	. . . . . . . . . 10 |- (x = (/) -> (y (_ x <-> y (_ (/)))
2	1	rexbidv 1667	. . . . . . . . 9 |- (x = (/) -> (E.y e. B y (_ x <-> E.y e. B y (_ (/)))
3	2	elrab 1908	. . . . . . . 8 |- ((/) e. {x e. P~X | E.y e. B y (_ x} <-> ((/) e. P~X /\ E.y e. B y (_ (/)))
4		ss0 2307	. . . . . . . . . . . 12 |- (y (_ (/) -> y = (/))
5	4	eleq1d 1543	. . . . . . . . . . 11 |- (y (_ (/) -> (y e. B <-> (/) e. B))
6	5	biimpcd 155	. . . . . . . . . 10 |- (y e. B -> (y (_ (/) -> (/) e. B))
7	6	r19.23aiv 1746	. . . . . . . . 9 |- (E.y e. B y (_ (/) -> (/) e. B)
8	7	adantl 390	. . . . . . . 8 |- (((/) e. P~X /\ E.y e. B y (_ (/)) -> (/) e. B)
9	3, 8	sylbi 199	. . . . . . 7 |- ((/) e. {x e. P~X | E.y e. B y (_ x} -> (/) e. B)
10	9	con3i 98	. . . . . 6 |- (-. (/) e. B -> -. (/) e. {x e. P~X | E.y e. B y (_ x})
11	10	adantl 390	. . . . 5 |- (((A (_ P~X /\ X e. V /\ A =/= (/)) /\ -. (/) e. B) -> -. (/) e. {x e. P~X | E.y e. B y (_ x})
12		ump 10449	. . . . . . . . 9 |- (X e. V -> U.{x e. P~X | E.y e. B y (_ x} e. P~X)
13	12	3ad2ant2 803	. . . . . . . 8 |- ((A (_ P~X /\ X e. V /\ A =/= (/)) -> U.{x e. P~X | E.y e. B y (_ x} e. P~X)
14		r19.2z 2351	. . . . . . . . 9 |- ((B =/= (/) /\ A.y e. B y (_ U.{x e. P~X | E.y e. B y (_ x}) -> E.y e. B y (_ U.{x e. P~X | E.y e. B y (_ x})
15		fine 10442	. . . . . . . . . . 11 |- (A =/= (/) -> {x | E.y(y (_ A /\ y e. Fin /\ x = |^|y)} =/= (/))
16		fgsb.1	. . . . . . . . . . . 12 |- B = {x | E.y(y (_ A /\ y e. Fin /\ x = |^|y)}
17	16	neeq1i 1595	. . . . . . . . . . 11 |- (B =/= (/) <-> {x | E.y(y (_ A /\ y e. Fin /\ x = |^|y)} =/= (/))
18	15, 17	sylibr 200	. . . . . . . . . 10 |- (A =/= (/) -> B =/= (/))
19	18	3ad2ant3 804	. . . . . . . . 9 |- ((A (_ P~X /\ X e. V /\ A =/= (/)) -> B =/= (/))
20		ax-17 973	. . . . . . . . . . . . . . . . . 18 |- ((y e. B -> y (_ U.A) -> A.u(y e. B -> y (_ U.A))
21		eleq1 1537	. . . . . . . . . . . . . . . . . . 19 |- (u = y -> (u e. B <-> y e. B))
22		sseq1 2085	. . . . . . . . . . . . . . . . . . 19 |- (u = y -> (u (_ U.A <-> y (_ U.A))
23	21, 22	imbi12d 628	. . . . . . . . . . . . . . . . . 18 |- (u = y -> ((u e. B -> u (_ U.A) <-> (y e. B -> y (_ U.A)))
24	16	eleq2i 1541	. . . . . . . . . . . . . . . . . . 19 |- (u e. B <-> u e. {x | E.y(y (_ A /\ y e. Fin /\ x = |^|y)})
25		fiiu 10444	. . . . . . . . . . . . . . . . . . 19 |- (u e. {x | E.y(y (_ A /\ y e. Fin /\ x = |^|y)} -> u (_ U.A)
26	24, 25	sylbi 199	. . . . . . . . . . . . . . . . . 18 |- (u e. B -> u (_ U.A)
27	20, 23, 26	chvar 1169	. . . . . . . . . . . . . . . . 17 |- (y e. B -> y (_ U.A)
28		uniss 2525	. . . . . . . . . . . . . . . . . 18 |- (A (_ P~X -> U.A (_ U.P~X)
29	28	3ad2ant1 802	. . . . . . . . . . . . . . . . 17 |- ((A (_ P~X /\ X e. V /\ A =/= (/)) -> U.A (_ U.P~X)
30	27, 29	sylan9ssr 2079	. . . . . . . . . . . . . . . 16 |- (((A (_ P~X /\ X e. V /\ A =/= (/)) /\ y e. B) -> y (_ U.P~X)
31		unipw 2762	. . . . . . . . . . . . . . . 16 |- U.P~X = X
32	30, 31	syl6ss 2110	. . . . . . . . . . . . . . 15 |- (((A (_ P~X /\ X e. V /\ A =/= (/)) /\ y e. B) -> y (_ X)
33		visset 1816	. . . . . . . . . . . . . . . 16 |- y e. V
34	33	elpw 2408	. . . . . . . . . . . . . . 15 |- (y e. P~X <-> y (_ X)
35	32, 34	sylibr 200	. . . . . . . . . . . . . 14 |- (((A (_ P~X /\ X e. V /\ A =/= (/)) /\ y e. B) -> y e. P~X)
36		pm3.27 323	. . . . . . . . . . . . . . . 16 |- (((A (_ P~X /\ X e. V /\ A =/= (/)) /\ y e. B) -> y e. B)
37		ssid 2083	. . . . . . . . . . . . . . . 16 |- y (_ y
38	36, 37	jctir 293	. . . . . . . . . . . . . . 15 |- (((A (_ P~X /\ X e. V /\ A =/= (/)) /\ y e. B) -> (y e. B /\ y (_ y))
39		sseq1 2085	. . . . . . . . . . . . . . . 16 |- (z = y -> (z (_ y <-> y (_ y))
40	39	rcla4ev 1880	. . . . . . . . . . . . . . 15 |- ((y e. B /\ y (_ y) -> E.z e. B z (_ y)
41	38, 40	syl 10	. . . . . . . . . . . . . 14 |- (((A (_ P~X /\ X e. V /\ A =/= (/)) /\ y e. B) -> E.z e. B z (_ y)
42	35, 41	jca 288	. . . . . . . . . . . . 13 |- (((A (_ P~X /\ X e. V /\ A =/= (/)) /\ y e. B) -> (y e. P~X /\ E.z e. B z (_ y))
43		sseq2 2086	. . . . . . . . . . . . . . . 16 |- (x = y -> (z (_ x <-> z (_ y))
44	43	rexbidv 1667	. . . . . . . . . . . . . . 15 |- (x = y -> (E.z e. B z (_ x <-> E.z e. B z (_ y))
45		sseq1 2085	. . . . . . . . . . . . . . . 16 |- (y = z -> (y (_ x <-> z (_ x))
46	45	cbvrexv 1804	. . . . . . . . . . . . . . 15 |- (E.y e. B y (_ x <-> E.z e. B z (_ x)
47	44, 46	syl5bb 534	. . . . . . . . . . . . . 14 |- (x = y -> (E.y e. B y (_ x <-> E.z e. B z (_ y))
48	47	elrab 1908	. . . . . . . . . . . . 13 |- (y e. {x e. P~X | E.y e. B y (_ x} <-> (y e. P~X /\ E.z e. B z (_ y))
49	42, 48	sylibr 200	. . . . . . . . . . . 12 |- (((A (_ P~X /\ X e. V /\ A =/= (/)) /\ y e. B) -> y e. {x e. P~X | E.y e. B y (_ x})
50	49, 37	jctil 292	. . . . . . . . . . 11 |- (((A (_ P~X /\ X e. V /\ A =/= (/)) /\ y e. B) -> (y (_ y /\ y e. {x e. P~X | E.y e. B y (_ x}))
51		ssuni 2526	. . . . . . . . . . 11 |- ((y (_ y /\ y e. {x e. P~X | E.y e. B y (_ x}) -> y (_ U.{x e. P~X | E.y e. B y (_ x})
52	50, 51	syl 10	. . . . . . . . . 10 |- (((A (_ P~X /\ X e. V /\ A =/= (/)) /\ y e. B) -> y (_ U.{x e. P~X | E.y e. B y (_ x})
53	52	r19.21aiva 1717	. . . . . . . . 9 |- ((A (_ P~X /\ X e. V /\ A =/= (/)) -> A.y e. B y (_ U.{x e. P~X | E.y e. B y (_ x})
54	14, 19, 53	sylanc 473	. . . . . . . 8 |- ((A (_ P~X /\ X e. V /\ A =/= (/)) -> E.y e. B y (_ U.{x e. P~X | E.y e. B y (_ x})
55	13, 54	jca 288	. . . . . . 7 |- ((A (_ P~X /\ X e. V /\ A =/= (/)) -> (U.{x e. P~X | E.y e. B y (_ x} e. P~X /\ E.y e. B y (_ U.{x e. P~X | E.y e. B y (_ x}))
56	55	adantr 391	. . . . . 6 |- (((A (_ P~X /\ X e. V /\ A =/= (/)) /\ -. (/) e. B) -> (U.{x e. P~X | E.y e. B y (_ x} e. P~X /\ E.y e. B y (_ U.{x e. P~X | E.y e. B y (_ x}))
57		hbrab1 1775	. . . . . . . 8 |- (z e. {x e. P~X | E.y e. B y (_ x} -> A.x z e. {x e. P~X | E.y e. B y (_ x})
58	57	hbuni 2513	. . . . . . 7 |- (z e. U.{x e. P~X | E.y e. B y (_ x} -> A.x z e. U.{x e. P~X | E.y e. B y (_ x})
59		ax-17 973	. . . . . . . 8 |- (z e. X -> A.x z e. X)
60	59	hbpw 2411	. . . . . . 7 |- (z e. P~X -> A.x z e. P~X)
61		ax-17 973	. . . . . . . 8 |- (y e. B -> A.x y e. B)
62		ax-17 973	. . . . . . . . 9 |- (z e. y -> A.x z e. y)
63	62, 58	hbss 2065	. . . . . . . 8 |- (y (_ U.{x e. P~X | E.y e. B y (_ x} -> A.x y (_ U.{x e. P~X | E.y e. B y (_ x})
64	61, 63	hbrex 1691	. . . . . . 7 |- (E.y e. B y (_ U.{x e. P~X | E.y e. B y (_ x} -> A.xE.y e. B y (_ U.{x e. P~X | E.y e. B y (_ x})
65		ax-17 973	. . . . . . . . 9 |- (w e. x -> A.y w e. x)
66		hbre1 1692	. . . . . . . . . . 11 |- (E.y e. B y (_ x -> A.yE.y e. B y (_ x)
67		ax-17 973	. . . . . . . . . . 11 |- (z e. P~X -> A.y z e. P~X)
68	66, 67	hbrab 1776	. . . . . . . . . 10 |- (z e. {x e. P~X | E.y e. B y (_ x} -> A.y z e. {x e. P~X | E.y e. B y (_ x})
69	68	hbuni 2513	. . . . . . . . 9 |- (z e. U.{x e. P~X | E.y e. B y (_ x} -> A.y z e. U.{x e. P~X | E.y e. B y (_ x})
70	65, 69	hbeq 1568	. . . . . . . 8 |- (x = U.{x e. P~X | E.y e. B y (_ x} -> A.y x = U.{x e. P~X | E.y