Theorem alexsublem 21051

Description: Lemma for alexsub 21052. (Contributed by Mario Carneiro, 26-Aug-2015.)

Hypotheses

Ref	Expression
alexsub.1	|- ( ph -> X e. UFL )
alexsub.2	|- ( ph -> X = U. B )
alexsub.3	|- ( ph -> J = ( topGen ` ( fi ` B ) ) )
alexsub.4	|- ( ( ph /\ ( x C_ B /\ X = U. x ) ) -> E. y e. ( ~P x i^i Fin ) X = U. y )
alexsub.5	|- ( ph -> F e. ( UFil ` X ) )
alexsub.6	|- ( ph -> ( J fLim F ) = (/) )

Assertion

Ref	Expression
alexsublem	|- -. ph

Distinct variable groups:   x, y, B   x, J, y   ph, x, y   x, X, y   x, F, y

Proof of Theorem alexsublem

Dummy variable z is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eldif 3447	. . . . . . . . . 10 |- ( x e. ( X \ U. ( B \ F ) ) <-> ( x e. X /\ -. x e. U. ( B \ F ) ) )
2		alexsub.3	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> J = ( topGen ` ( fi ` B ) ) )
3	2	eleq2d 2493	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( y e. J <-> y e. ( topGen ` ( fi ` B ) ) ) )
4	3	anbi1d 710	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ( y e. J /\ x e. y ) <-> ( y e. ( topGen ` ( fi ` B ) ) /\ x e. y ) ) )
5	4	biimpa 487	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( y e. J /\ x e. y ) ) -> ( y e. ( topGen ` ( fi ` B ) ) /\ x e. y ) )
6	5	adantlr 720	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( x e. X /\ -. x e. U. ( B \ F ) ) ) /\ ( y e. J /\ x e. y ) ) -> ( y e. ( topGen ` ( fi ` B ) ) /\ x e. y ) )
7		tg2 19972	. . . . . . . . . . . . . . . 16 |- ( ( y e. ( topGen ` ( fi ` B ) ) /\ x e. y ) -> E. z e. ( fi ` B ) ( x e. z /\ z C_ y ) )
8	6, 7	syl 17	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( x e. X /\ -. x e. U. ( B \ F ) ) ) /\ ( y e. J /\ x e. y ) ) -> E. z e. ( fi ` B ) ( x e. z /\ z C_ y ) )
9		alexsub.5	. . . . . . . . . . . . . . . . . 18 |- ( ph -> F e. ( UFil ` X ) )
10		ufilfil 20911	. . . . . . . . . . . . . . . . . 18 |- ( F e. ( UFil ` X ) -> F e. ( Fil ` X ) )
11	9, 10	syl 17	. . . . . . . . . . . . . . . . 17 |- ( ph -> F e. ( Fil ` X ) )
12	11	ad3antrrr 735	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ ( x e. X /\ -. x e. U. ( B \ F ) ) ) /\ ( y e. J /\ x e. y ) ) /\ ( z e. ( fi ` B ) /\ ( x e. z /\ z C_ y ) ) ) -> F e. ( Fil ` X ) )
13		alexsub.2	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> X = U. B )
14	9	elfvexd 5907	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> X e. _V )
15	13, 14	eqeltrrd 2512	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> U. B e. _V )
16		uniexb 6613	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( B e. _V <-> U. B e. _V )
17	15, 16	sylibr 216	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> B e. _V )
18		elfi2 7932	. . . . . . . . . . . . . . . . . . . . . 22 |- ( B e. _V -> ( z e. ( fi ` B ) <-> E. y e. ( ( ~P B i^i Fin ) \ { (/) } ) z = |^| y ) )
19	17, 18	syl 17	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( z e. ( fi ` B ) <-> E. y e. ( ( ~P B i^i Fin ) \ { (/) } ) z = |^| y ) )
20	19	adantr 467	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ ( x e. X /\ -. x e. U. ( B \ F ) ) ) -> ( z e. ( fi ` B ) <-> E. y e. ( ( ~P B i^i Fin ) \ { (/) } ) z = |^| y ) )
21	11	ad2antrr 731	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ ( x e. X /\ -. x e. U. ( B \ F ) ) ) /\ ( y e. ( ( ~P B i^i Fin ) \ { (/) } ) /\ x e. |^| y ) ) -> F e. ( Fil ` X ) )
22		simplrr 770	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ph /\ ( x e. X /\ -. x e. U. ( B \ F ) ) ) /\ ( ( y e. ( ( ~P B i^i Fin ) \ { (/) } ) /\ x e. |^| y ) /\ z e. y ) ) -> -. x e. U. ( B \ F ) )
23		intss1 4268	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( z e. y -> |^| y C_ z )
24	23	adantl 468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( y e. ( ( ~P B i^i Fin ) \ { (/) } ) /\ x e. |^| y ) /\ z e. y ) -> |^| y C_ z )
25		simplr 761	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( y e. ( ( ~P B i^i Fin ) \ { (/) } ) /\ x e. |^| y ) /\ z e. y ) -> x e. |^| y )
26	24, 25	sseldd 3466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( y e. ( ( ~P B i^i Fin ) \ { (/) } ) /\ x e. |^| y ) /\ z e. y ) -> x e. z )
27	26	ad2antlr 732	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ( ph /\ ( x e. X /\ -. x e. U. ( B \ F ) ) ) /\ ( ( y e. ( ( ~P B i^i Fin ) \ { (/) } ) /\ x e. |^| y ) /\ z e. y ) ) /\ -. z e. F ) -> x e. z )
28		eldifsn 4123	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( y e. ( ( ~P B i^i Fin ) \ { (/) } ) <-> ( y e. ( ~P B i^i Fin ) /\ y =/= (/) ) )
29	28	simplbi 462	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( y e. ( ( ~P B i^i Fin ) \ { (/) } ) -> y e. ( ~P B i^i Fin ) )
30	29	ad2antrl 733	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( ph /\ ( x e. X /\ -. x e. U. ( B \ F ) ) ) /\ ( y e. ( ( ~P B i^i Fin ) \ { (/) } ) /\ x e. |^| y ) ) -> y e. ( ~P B i^i Fin ) )
31		elfpw 7880	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( y e. ( ~P B i^i Fin ) <-> ( y C_ B /\ y e. Fin ) )
32	31	simplbi 462	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( y e. ( ~P B i^i Fin ) -> y C_ B )
33	30, 32	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ph /\ ( x e. X /\ -. x e. U. ( B \ F ) ) ) /\ ( y e. ( ( ~P B i^i Fin ) \ { (/) } ) /\ x e. |^| y ) ) -> y C_ B )
34	33	sselda 3465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ( ph /\ ( x e. X /\ -. x e. U. ( B \ F ) ) ) /\ ( y e. ( ( ~P B i^i Fin ) \ { (/) } ) /\ x e. |^| y ) ) /\ z e. y ) -> z e. B )
35	34	anasss 652	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ph /\ ( x e. X /\ -. x e. U. ( B \ F ) ) ) /\ ( ( y e. ( ( ~P B i^i Fin ) \ { (/) } ) /\ x e. |^| y ) /\ z e. y ) ) -> z e. B )
36	35	anim1i 571	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ( ph /\ ( x e. X /\ -. x e. U. ( B \ F ) ) ) /\ ( ( y e. ( ( ~P B i^i Fin ) \ { (/) } ) /\ x e. |^| y ) /\ z e. y ) ) /\ -. z e. F ) -> ( z e. B /\ -. z e. F ) )
37		eldif 3447	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( z e. ( B \ F ) <-> ( z e. B /\ -. z e. F ) )
38	36, 37	sylibr 216	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ( ph /\ ( x e. X /\ -. x e. U. ( B \ F ) ) ) /\ ( ( y e. ( ( ~P B i^i Fin ) \ { (/) } ) /\ x e. |^| y ) /\ z e. y ) ) /\ -. z e. F ) -> z e. ( B \ F ) )
39		elunii 4222	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( x e. z /\ z e. ( B \ F ) ) -> x e. U. ( B \ F ) )
40	27, 38, 39	syl2anc 666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ( ph /\ ( x e. X /\ -. x e. U. ( B \ F ) ) ) /\ ( ( y e. ( ( ~P B i^i Fin ) \ { (/) } ) /\ x e. |^| y ) /\ z e. y ) ) /\ -. z e. F ) -> x e. U. ( B \ F ) )
41	40	ex 436	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ph /\ ( x e. X /\ -. x e. U. ( B \ F ) ) ) /\ ( ( y e. ( ( ~P B i^i Fin ) \ { (/) } ) /\ x e. |^| y ) /\ z e. y ) ) -> ( -. z e. F -> x e. U. ( B \ F ) ) )
42	22, 41	mt3d 129	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ph /\ ( x e. X /\ -. x e. U. ( B \ F ) ) ) /\ ( ( y e. ( ( ~P B i^i Fin ) \ { (/) } ) /\ x e. |^| y ) /\ z e. y ) ) -> z e. F )
43	42	expr 619	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ ( x e. X /\ -. x e. U. ( B \ F ) ) ) /\ ( y e. ( ( ~P B i^i Fin ) \ { (/) } ) /\ x e. |^| y ) ) -> ( z e. y -> z e. F ) )
44	43	ssrdv 3471	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ ( x e. X /\ -. x e. U. ( B \ F ) ) ) /\ ( y e. ( ( ~P B i^i Fin ) \ { (/) } ) /\ x e. |^| y ) ) -> y C_ F )
45	28	simprbi 466	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( y e. ( ( ~P B i^i Fin ) \ { (/) } ) -> y =/= (/) )
46	45	ad2antrl 733	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ ( x e. X /\ -. x e. U. ( B \ F ) ) ) /\ ( y e. ( ( ~P B i^i Fin ) \ { (/) } ) /\ x e. |^| y ) ) -> y =/= (/) )
47	31	simprbi 466	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( y e. ( ~P B i^i Fin ) -> y e. Fin )
48	30, 47	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ ( x e. X /\ -. x e. U. ( B \ F ) ) ) /\ ( y e. ( ( ~P B i^i Fin ) \ { (/) } ) /\ x e. |^| y ) ) -> y e. Fin )
49		elfir 7933	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( F e. ( Fil ` X ) /\ ( y C_ F /\ y =/= (/) /\ y e. Fin ) ) -> |^| y e. ( fi ` F ) )
50	21, 44, 46, 48, 49	syl13anc 1267	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ ( x e. X /\ -. x e. U. ( B \ F ) ) ) /\ ( y e. ( ( ~P B i^i Fin ) \ { (/) } ) /\ x e. |^| y ) ) -> |^| y e. ( fi ` F ) )
51		filfi 20866	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( F e. ( Fil ` X ) -> ( fi ` F ) = F )
52	21, 51	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ ( x e. X /\ -. x e. U. ( B \ F ) ) ) /\ ( y e. ( ( ~P B i^i Fin ) \ { (/) } ) /\ x e. |^| y ) ) -> ( fi ` F ) = F )
53	50, 52	eleqtrd 2513	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ ( x e. X /\ -. x e. U. ( B \ F ) ) ) /\ ( y e. ( ( ~P B i^i Fin ) \ { (/) } ) /\ x e. |^| y ) ) -> |^| y e. F )
54	53	expr 619	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ ( x e. X /\ -. x e. U. ( B \ F ) ) ) /\ y e. ( ( ~P B i^i Fin ) \ { (/) } ) ) -> ( x e. |^| y -> |^| y e. F ) )
55		eleq2 2496	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( z = |^| y -> ( x e. z <-> x e. |^| y ) )
56		eleq1 2495	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( z = |^| y -> ( z e. F <-> |^| y e. F ) )
57	55, 56	imbi12d 322	. . . . . . . . . . . . . . . . . . . . . 22 |- ( z = |^| y -> ( ( x e. z -> z e. F ) <-> ( x e. |^| y -> |^| y e. F ) ) )
58	54, 57	syl5ibrcom 226	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ ( x e. X /\ -. x e. U. ( B \ F ) ) ) /\ y e. ( ( ~P B i^i Fin ) \ { (/) } ) ) -> ( z = |^| y -> ( x e. z -> z e. F ) ) )
59	58	rexlimdva 2918	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ ( x e. X /\ -. x e. U. ( B \ F ) ) ) -> ( E. y e. ( ( ~P B i^i Fin ) \ { (/) } ) z = |^| y -> ( x e. z -> z e. F ) ) )
60	20, 59	sylbid 219	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( x e. X /\ -. x e. U. ( B \ F ) ) ) -> ( z e. ( fi ` B ) -> ( x e. z -> z e. F ) ) )
61	60	imp32 435	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ ( x e. X /\ -. x e. U. ( B \ F ) ) ) /\ ( z e. ( fi ` B ) /\ x e. z ) ) -> z e. F )
62	61	adantrrr 730	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( x e. X /\ -. x e. U. ( B \ F ) ) ) /\ ( z e. ( fi ` B ) /\ ( x e. z /\ z C_ y ) ) ) -> z e. F )
63	62	adantlr 720	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ ( x e. X /\ -. x e. U. ( B \ F ) ) ) /\ ( y e. J /\ x e. y ) ) /\ ( z e. ( fi ` B ) /\ ( x e. z /\ z C_ y ) ) ) -> z e. F )
64		elssuni 4246	. . . . . . . . . . . . . . . . . . 19 |- ( y e. J -> y C_ U. J )
65	64	ad2antrl 733	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ ( x e. X /\ -. x e. U. ( B \ F ) ) ) /\ ( y e. J /\ x e. y ) ) -> y C_ U. J )
66		fibas 19985	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( fi ` B ) e. TopBases
67		tgtopon 19979	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( fi ` B ) e. TopBases -> ( topGen ` ( fi ` B ) ) e. (TopOn ` U. ( fi ` B ) ) )
68	66, 67	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 |- ( topGen ` ( fi ` B ) ) e. (TopOn ` U. ( fi ` B ) )
69	2, 68	syl6eqel 2519	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> J e. (TopOn ` U. ( fi ` B ) ) )
70		fiuni 7946	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( B e. _V -> U. B = U. ( fi ` B ) )
71	17, 70	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> U. B = U. ( fi ` B ) )
72	13, 71	eqtrd 2464	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> X = U. ( fi ` B ) )
73	72	fveq2d 5883	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> (TopOn ` X ) = (TopOn ` U. ( fi ` B ) ) )
74	69, 73	eleqtrrd 2514	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> J e. (TopOn ` X ) )
75		toponuni 19934	. . . . . . . . . . . . . . . . . . . 20 |- ( J e. (TopOn ` X ) -> X = U. J )
76	74, 75	syl 17	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> X = U. J )
77	76	ad2antrr 731	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ ( x e. X /\ -. x e. U. ( B \ F ) ) ) /\ ( y e. J /\ x e. y ) ) -> X = U. J )
78	65, 77	sseqtr4d 3502	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( x e. X /\ -. x e. U. ( B \ F ) ) ) /\ ( y e. J /\ x e. y ) ) -> y C_ X )
79	78	adantr 467	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ ( x e. X /\ -. x e. U. ( B \ F ) ) ) /\ ( y e. J /\ x e. y ) ) /\ ( z e. ( fi ` B ) /\ ( x e. z /\ z C_ y ) ) ) -> y C_ X )
80		simprrr 774	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ ( x e. X /\ -. x e. U. ( B \ F ) ) ) /\ ( y e. J /\ x e. y ) ) /\ ( z e. ( fi ` B ) /\ ( x e. z /\ z C_ y ) ) ) -> z C_ y )
81		filss 20860	. . . . . . . . . . . . . . . 16 |- ( ( F e. ( Fil ` X ) /\ ( z e. F /\ y C_ X /\ z C_ y ) ) -> y e. F )
82	12, 63, 79, 80, 81	syl13anc 1267	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ ( x e. X /\ -. x e. U. ( B \ F ) ) ) /\ ( y e. J /\ x e. y ) ) /\ ( z e. ( fi ` B ) /\ ( x e. z /\ z C_ y ) ) ) -> y e. F )
83	8, 82	rexlimddv 2922	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( x e. X /\ -. x e. U. ( B \ F ) ) ) /\ ( y e. J /\ x e. y ) ) -> y e. F )
84	83	expr 619	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( x e. X /\ -. x e. U. ( B \ F ) ) ) /\ y e. J ) -> ( x e. y -> y e. F ) )
85	84	ralrimiva 2840	. . . . . . . . . . . 12 |- ( ( ph /\ ( x e. X /\ -. x e. U. ( B \ F ) ) ) -> A. y e. J ( x e. y -> y e. F ) )
86	85	expr 619	. . . . . . . . . . 11 |- ( ( ph /\ x e. X ) -> ( -. x e. U. ( B \ F ) -> A. y e. J ( x e. y -> y e. F ) ) )
87	86	imdistanda 698	. . . . . . . . . 10 |- ( ph -> ( ( x e. X /\ -. x e. U. ( B \ F ) ) -> ( x e. X /\ A. y e. J ( x e. y -> y e. F ) ) ) )
88	1, 87	syl5bi 221	. . . . . . . . 9 |- ( ph -> ( x e. ( X \ U. ( B \ F ) ) -> ( x e. X /\ A. y e. J ( x e. y -> y e. F ) ) ) )
89		flimopn 20982	. . . . . . . . . 10 |- ( ( J e. (TopOn ` X ) /\ F e. ( Fil ` X ) ) -> ( x e. ( J fLim F ) <-> ( x e. X /\ A. y e. J ( x e. y -> y e. F ) ) ) )
90	74, 11, 89	syl2anc 666	. . . . . . . . 9 |- ( ph -> ( x e. ( J fLim F ) <-> ( x e. X /\ A. y e. J ( x e. y -> y e. F ) ) ) )
91	88, 90	sylibrd 238	. . . . . . . 8 |- ( ph -> ( x e. ( X \ U. ( B \ F ) ) -> x e. ( J fLim F ) ) )
92	91	ssrdv 3471	. . . . . . 7 |- ( ph -> ( X \ U. ( B \ F ) ) C_ ( J fLim F ) )
93		alexsub.6	. . . . . . 7 |- ( ph -> ( J fLim F ) = (/) )
94		sseq0 3795	. . . . . . 7 |- ( ( ( X \ U. ( B \ F ) ) C_ ( J fLim F ) /\ ( J fLim F ) = (/) ) -> ( X \ U. ( B \ F ) ) = (/) )
95	92, 93, 94	syl2anc 666	. . . . . 6 |- ( ph -> ( X \ U. ( B \ F ) ) = (/) )
96		ssdif0 3852	. . . . . 6 |- ( X C_ U. ( B \ F ) <-> ( X \ U. ( B \ F ) ) = (/) )
97	95, 96	sylibr 216	. . . . 5 |- ( ph -> X C_ U. ( B \ F ) )
98		difss 3593	. . . . . . 7 |- ( B \ F ) C_ B
99	98	unissi 4240	. . . . . 6 |- U. ( B \ F ) C_ U. B
100	99, 13	syl5sseqr 3514	. . . . 5 |- ( ph -> U. ( B \ F ) C_ X )
101	97, 100	eqssd 3482	. . . 4 |- ( ph -> X = U. ( B \ F ) )
102	101, 98	jctil 540	. . 3 |- ( ph -> ( ( B \ F ) C_ B /\ X = U. ( B \ F ) ) )
103		difexg 4570	. . . . . 6 |- ( B e. _V -> ( B \ F ) e. _V )
104	17, 103	syl 17	. . . . 5 |- ( ph -> ( B \ F ) e. _V )
105	104	adantr 467	. . . 4 |- ( ( ph /\ ( ( B \ F ) C_ B /\ X = U. ( B \ F ) ) ) -> ( B \ F ) e. _V )
106		sseq1 3486	. . . . . . . 8 |- ( x = ( B \ F ) -> ( x C_ B <-> ( B \ F ) C_ B ) )
107		unieq 4225	. . . . . . . . 9 |- ( x = ( B \ F ) -> U. x = U. ( B \ F ) )
108	107	eqeq2d 2437	. . . . . . . 8 |- ( x = ( B \ F ) -> ( X = U. x <-> X = U. ( B \ F ) ) )
109	106, 108	anbi12d 716	. . . . . . 7 |- ( x = ( B \ F ) -> ( ( x C_ B /\ X = U. x ) <-> ( ( B \ F ) C_ B /\ X = U. ( B \ F ) ) ) )
110	109	anbi2d 709	. . . . . 6 |- ( x = ( B \ F ) -> ( ( ph /\ ( x C_ B /\ X = U. x ) ) <-> ( ph /\ ( ( B \ F ) C_ B /\ X = U. ( B \ F ) ) ) ) )
111		pweq 3983	. . . . . . . 8 |- ( x = ( B \ F ) -> ~P x = ~P ( B \ F ) )
112	111	ineq1d 3664	. . . . . . 7 |- ( x = ( B \ F ) -> ( ~P x i^i Fin ) = ( ~P ( B \ F ) i^i Fin ) )
113	112	rexeqdv 3033	. . . . . 6 |- ( x = ( B \ F ) -> ( E. y e. ( ~P x i^i Fin ) X = U. y <-> E. y e. ( ~P ( B \ F ) i^i Fin ) X = U. y ) )
114	110, 113	imbi12d 322	. . . . 5 |- ( x = ( B \ F ) -> ( ( ( ph /\ ( x C_ B /\ X = U. x ) ) -> E. y e. ( ~P x i^i Fin ) X = U. y ) <-> ( ( ph /\ ( ( B \ F ) C_ B /\ X = U. ( B \ F ) ) ) -> E. y e. ( ~P ( B \ F ) i^i Fin ) X = U. y ) ) )
115		alexsub.4	. . . . 5 |- ( ( ph /\ ( x C_ B /\ X = U. x ) ) -> E. y e. ( ~P x i^i Fin ) X = U. y )
116	114, 115	vtoclg 3140	. . . 4 |- ( ( B \ F ) e. _V -> ( ( ph /\ ( ( B \ F ) C_ B /\ X = U. ( B \ F ) ) ) -> E. y e. ( ~P ( B \ F ) i^i Fin ) X = U. y ) )
117	105, 116	mpcom 38	. . 3 |- ( ( ph /\ ( ( B \ F ) C_ B /\ X = U. ( B \ F ) ) ) -> E. y e. ( ~P ( B \ F ) i^i Fin ) X = U. y )
118	102, 117	mpdan 673	. 2 |- ( ph -> E. y e. ( ~P ( B \ F ) i^i Fin ) X = U. y )
119		unieq 4225	. . . . . . 7 |- ( y = (/) -> U. y = U. (/) )
120		uni0 4244	. . . . . . 7 |- U. (/) = (/)
121	119, 120	syl6eq 2480	. . . . . 6 |- ( y = (/) -> U. y = (/) )
122	121	neeq2d 2703	. . . . 5 |- ( y = (/) -> ( X =/= U. y <-> X =/= (/) ) )
123		difssd 3594	. . . . . . . . . . 11 |- ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) -> ( X \ z ) C_ X )
124	123	ralrimivw 2841	. . . . . . . . . 10 |- ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) -> A. z e. y ( X \ z ) C_ X )
125		riinn0 4372	. . . . . . . . . 10 |- ( ( A. z e. y ( X \ z ) C_ X /\ y =/= (/) ) -> ( X i^i |^|_ z e. y ( X \ z ) ) = |^|_ z e. y ( X \ z ) )
126	124, 125	sylan 474	. . . . . . . . 9 |- ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> ( X i^i |^|_ z e. y ( X \ z ) ) = |^|_ z e. y ( X \ z ) )
127	14	ad2antrr 731	. . . . . . . . . . . . 13 |- ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> X e. _V )
128		difexg 4570	. . . . . . . . . . . . 13 |- ( X e. _V -> ( X \ z ) e. _V )
129	127, 128	syl 17	. . . . . . . . . . . 12 |- ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> ( X \ z ) e. _V )
130	129	ralrimivw 2841	. . . . . . . . . . 11 |- ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> A. z e. y ( X \ z ) e. _V )
131		dfiin2g 4330	. . . . . . . . . . 11 |- ( A. z e. y ( X \ z ) e. _V -> |^|_ z e. y ( X \ z ) = |^| { x | E. z e. y x = ( X \ z ) } )
132	130, 131	syl 17	. . . . . . . . . 10 |- ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> |^|_ z e. y ( X \ z ) = |^| { x | E. z e. y x = ( X \ z ) } )
133		eqid 2423	. . . . . . . . . . . 12 |- ( z e. y |-> ( X \ z ) ) = ( z e. y |-> ( X \ z ) )
134	133	rnmpt 5097	. . . . . . . . . . 11 |- ran ( z e. y |-> ( X \ z ) ) = { x | E. z e. y x = ( X \ z ) }
135	134	inteqi 4257	. . . . . . . . . 10 |- |^| ran ( z e. y |-> ( X \ z ) ) = |^| { x | E. z e. y x = ( X \ z ) }
136	132, 135	syl6eqr 2482	. . . . . . . . 9 |- ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> |^|_ z e. y ( X \ z ) = |^| ran ( z e. y |-> ( X \ z ) ) )
137	126, 136	eqtrd 2464	. . . . . . . 8 |- ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> ( X i^i |^|_ z e. y ( X \ z ) ) = |^| ran ( z e. y |-> ( X \ z ) ) )
138	11	ad2antrr 731	. . . . . . . . 9 |- ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> F e. ( Fil ` X ) )
139		elfpw 7880	. . . . . . . . . . . . . . . 16 |- ( y e. ( ~P ( B \ F ) i^i Fin ) <-> ( y C_ ( B \ F ) /\ y e. Fin ) )
140	139	simplbi 462	. . . . . . . . . . . . . . 15 |- ( y e. ( ~P ( B \ F ) i^i Fin ) -> y C_ ( B \ F ) )
141	140	ad2antlr 732	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> y C_ ( B \ F ) )
142	141	sselda 3465	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) /\ z e. y ) -> z e. ( B \ F ) )
143	142	eldifbd 3450	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) /\ z e. y ) -> -. z e. F )
144	9	ad3antrrr 735	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) /\ z e. y ) -> F e. ( UFil ` X ) )
145	141	difss2d 3596	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> y C_ B )
146	145	sselda 3465	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) /\ z e. y ) -> z e. B )
147		elssuni 4246	. . . . . . . . . . . . . . 15 |- ( z e. B -> z C_ U. B )
148	146, 147	syl 17	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) /\ z e. y ) -> z C_ U. B )
149	13	ad3antrrr 735	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) /\ z e. y ) -> X = U. B )
150	148, 149	sseqtr4d 3502	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) /\ z e. y ) -> z C_ X )
151		ufilb 20913	. . . . . . . . . . . . 13 |- ( ( F e. ( UFil ` X ) /\ z C_ X ) -> ( -. z e. F <-> ( X \ z ) e. F ) )
152	144, 150, 151	syl2anc 666	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) /\ z e. y ) -> ( -. z e. F <-> ( X \ z ) e. F ) )
153	143, 152	mpbid 214	. . . . . . . . . . 11 |- ( ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) /\ z e. y ) -> ( X \ z ) e. F )
154	153, 133	fmptd 6059	. . . . . . . . . 10 |- ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> ( z e. y |-> ( X \ z ) ) : y --> F )
155		frn 5750	. . . . . . . . . 10 |- ( ( z e. y |-> ( X \ z ) ) : y --> F -> ran ( z e. y |-> ( X \ z ) ) C_ F )
156	154, 155	syl 17	. . . . . . . . 9 |- ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> ran ( z e. y |-> ( X \ z ) ) C_ F )
157	133, 153	dmmptd 5724	. . . . . . . . . . 11 |- ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> dom ( z e. y |-> ( X \ z ) ) = y )
158		simpr 463	. . . . . . . . . . 11 |- ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> y =/= (/) )
159	157, 158	eqnetrd 2718	. . . . . . . . . 10 |- ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> dom ( z e. y |-> ( X \ z ) ) =/= (/) )
160		dm0rn0 5068	. . . . . . . . . . 11 |- ( dom ( z e. y |-> ( X \ z ) ) = (/) <-> ran ( z e. y |-> ( X \ z ) ) = (/) )
161	160	necon3bii 2693	. . . . . . . . . 10 |- ( dom ( z e. y |-> ( X \ z ) ) =/= (/) <-> ran ( z e. y |-> ( X \ z ) ) =/= (/) )
162	159, 161	sylib 200	. . . . . . . . 9 |- ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> ran ( z e. y |-> ( X \ z ) ) =/= (/) )
163	139	simprbi 466	. . . . . . . . . . 11 |- ( y e. ( ~P ( B \ F ) i^i Fin ) -> y e. Fin )
164	163	ad2antlr 732	. . . . . . . . . 10 |- ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> y e. Fin )
165		abrexfi 7878	. . . . . . . . . . 11 |- ( y e. Fin -> { x | E. z e. y x = ( X \ z ) } e. Fin )
166	134, 165	syl5eqel 2515	. . . . . . . . . 10 |- ( y e. Fin -> ran ( z e. y |-> ( X \ z ) ) e. Fin )
167	164, 166	syl 17	. . . . . . . . 9 |- ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> ran ( z e. y |-> ( X \ z ) ) e. Fin )
168		filintn0 20868	. . . . . . . . 9 |- ( ( F e. ( Fil ` X ) /\ ( ran ( z e. y |-> ( X \ z ) ) C_ F /\ ran ( z e. y |-> ( X \ z ) ) =/= (/) /\ ran ( z e. y |-> ( X \ z ) ) e. Fin ) ) -> |^| ran ( z e. y |-> ( X \ z ) ) =/= (/) )
169	138, 156, 162, 167, 168	syl13anc 1267	. . . . . . . 8 |- ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> |^| ran ( z e. y |-> ( X \ z ) ) =/= (/) )
170	137, 169	eqnetrd 2718	. . . . . . 7 |- ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> ( X i^i |^|_ z e. y ( X \ z ) ) =/= (/) )
171		disj3 3838	. . . . . . . 8 |- ( ( X i^i |^|_ z e. y ( X \ z ) ) = (/) <-> X = ( X \ |^|_ z e. y ( X \ z ) ) )
172	171	necon3bii 2693	. . . . . . 7 |- ( ( X i^i |^|_ z e. y ( X \ z ) ) =/= (/) <-> X =/= ( X \ |^|_ z e. y ( X \ z ) ) )
173	170, 172	sylib 200	. . . . . 6 |- ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> X =/= ( X \ |^|_ z e. y ( X \ z ) ) )
174		iundif2 4364	. . . . . . 7 |- U_ z e. y ( X \ ( X \ z ) ) = ( X \ |^|_ z e. y ( X \ z ) )
175		dfss4 3708	. . . . . . . . . 10 |- ( z C_ X <-> ( X \ ( X \ z ) ) = z )
176	150, 175	sylib 200	. . . . . . . . 9 |- ( ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) /\ z e. y ) -> ( X \ ( X \ z ) ) = z )
177	176	iuneq2dv 4319	. . . . . . . 8 |- ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> U_ z e. y ( X \ ( X \ z ) ) = U_ z e. y z )
178		uniiun 4350	. . . . . . . 8 |- U. y = U_ z e. y z
179	177, 178	syl6eqr 2482	. . . . . . 7 |- ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> U_ z e. y ( X \ ( X \ z ) ) = U. y )
180	174, 179	syl5eqr 2478	. . . . . 6 |- ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> ( X \ |^|_ z e. y ( X \ z ) ) = U. y )
181	173, 180	neeqtrd 2720	. . . . 5 |- ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> X =/= U. y )
182	11	adantr 467	. . . . . 6 |- ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) -> F e. ( Fil ` X ) )
183		filtop 20862	. . . . . . 7 |- ( F e. ( Fil ` X ) -> X e. F )
184		fileln0 20857	. . . . . . 7 |- ( ( F e. ( Fil ` X ) /\ X e. F ) -> X =/= (/) )
185	183, 184	mpdan 673	. . . . . 6 |- ( F e. ( Fil ` X ) -> X =/= (/) )
186	182, 185	syl 17	. . . . 5 |- ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) -> X =/= (/) )
187	122, 181, 186	pm2.61ne 2740	. . . 4 |- ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) -> X =/= U. y )
188	187	neneqd 2626	. . 3 |- ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) -> -. X = U. y )
189	188	nrexdv 2882	. 2 |- ( ph -> -. E. y e. ( ~P ( B \ F ) i^i Fin ) X = U. y )
190	118, 189	pm2.65i 177	1 |- -. ph

Syntax hints:   -. wn 3   -> wi 4   <-> wb 188   /\ wa 371   = wceq 1438   e. wcel 1869   {cab 2408   =/= wne 2619   A.wral 2776   E.wrex 2777   _Vcvv 3082   \ cdif 3434   i^i cin 3436   C_ wss 3437   (/)c0 3762   ~Pcpw 3980   {csn 3997   U.cuni 4217   |^|cint 4253   U_ciun 4297   |^|_ciin 4298   |-> cmpt 4480   dom cdm 4851   ran crn 4852   -->wf 5595   ` cfv 5599  (class class class)co 6303   Fincfn 7575   ficfi 7928   topGenctg 15329  TopOnctopon 19910   TopBasesctb 19912   Filcfil 20852   UFilcufil 20906  UFLcufl 20907   fLim cflim 20941

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-8 1871  ax-9 1873  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401  ax-rep 4534  ax-sep 4544  ax-nul 4553  ax-pow 4600  ax-pr 4658  ax-un 6595

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 984  df-3an 985  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-eu 2270  df-mo 2271  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ne 2621  df-nel 2622  df-ral 2781  df-rex 2782  df-reu 2783  df-rab 2785  df-v 3084  df-sbc 3301  df-csb 3397  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-pss 3453  df-nul 3763  df-if 3911  df-pw 3982  df-sn 3998  df-pr 4000  df-tp 4002  df-op 4004  df-uni 4218  df-int 4254  df-iun 4299  df-iin 4300  df-br 4422  df-opab 4481  df-mpt 4482  df-tr 4517  df-eprel 4762  df-id 4766  df-po 4772  df-so 4773  df-fr 4810  df-we 4812  df-xp 4857  df-rel 4858  df-cnv 4859  df-co 4860  df-dm 4861  df-rn 4862  df-res 4863  df-ima 4864  df-pred 5397  df-ord 5443  df-on 5444  df-lim 5445  df-suc 5446  df-iota 5563  df-fun 5601  df-fn 5602  df-f 5603  df-f1 5604  df-fo 5605  df-f1o 5606  df-fv 5607  df-ov 6306  df-oprab 6307  df-mpt2 6308  df-om 6705  df-1st 6805  df-2nd 6806  df-wrecs 7034  df-recs 7096  df-rdg 7134  df-1o 7188  df-oadd 7192  df-er 7369  df-en 7576  df-dom 7577  df-fin 7579  df-fi 7929  df-topgen 15335  df-fbas 18960  df-top 19913  df-bases 19914  df-topon 19915  df-ntr 20027  df-nei 20106  df-fil 20853  df-ufil 20908  df-flim 20946

This theorem is referenced by:  alexsub  21052