Theorem alexsublem 19585

Description: Lemma for alexsub 19586. (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 3331	. . . . . . . . . 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 2504	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( y e. J <-> y e. ( topGen ` ( fi ` B ) ) ) )
4	3	anbi1d 704	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ( y e. J /\ x e. y ) <-> ( y e. ( topGen ` ( fi ` B ) ) /\ x e. y ) ) )
5	4	biimpa 484	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( y e. J /\ x e. y ) ) -> ( y e. ( topGen ` ( fi ` B ) ) /\ x e. y ) )
6	5	adantlr 714	. . . . . . . . . . . . . . . 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 18539	. . . . . . . . . . . . . . . 16 |- ( ( y e. ( topGen ` ( fi ` B ) ) /\ x e. y ) -> E. z e. ( fi ` B ) ( x e. z /\ z C_ y ) )
8	6, 7	syl 16	. . . . . . . . . . . . . . 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 19446	. . . . . . . . . . . . . . . . . 18 |- ( F e. ( UFil ` X ) -> F e. ( Fil ` X ) )
11	9, 10	syl 16	. . . . . . . . . . . . . . . . 17 |- ( ph -> F e. ( Fil ` X ) )
12	11	ad3antrrr 729	. . . . . . . . . . . . . . . 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 5711	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> X e. _V )
15	13, 14	eqeltrrd 2512	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> U. B e. _V )
16		uniexb 6381	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( B e. _V <-> U. B e. _V )
17	15, 16	sylibr 212	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> B e. _V )
18		elfi2 7656	. . . . . . . . . . . . . . . . . . . . . 22 |- ( B e. _V -> ( z e. ( fi ` B ) <-> E. y e. ( ( ~P B i^i Fin ) \ { (/) } ) z = |^| y ) )
19	17, 18	syl 16	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( z e. ( fi ` B ) <-> E. y e. ( ( ~P B i^i Fin ) \ { (/) } ) z = |^| y ) )
20	19	adantr 465	. . . . . . . . . . . . . . . . . . . 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 725	. . . . . . . . . . . . . . . . . . . . . . . . 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 760	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4136	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( z e. y -> |^| y C_ z )
24	23	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( y e. ( ( ~P B i^i Fin ) \ { (/) } ) /\ x e. |^| y ) /\ z e. y ) -> |^| y C_ z )
25		simplr 754	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( y e. ( ( ~P B i^i Fin ) \ { (/) } ) /\ x e. |^| y ) /\ z e. y ) -> x e. |^| y )
26	24, 25	sseldd 3350	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( y e. ( ( ~P B i^i Fin ) \ { (/) } ) /\ x e. |^| y ) /\ z e. y ) -> x e. z )
27	26	ad2antlr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3993	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( y e. ( ( ~P B i^i Fin ) \ { (/) } ) <-> ( y e. ( ~P B i^i Fin ) /\ y =/= (/) ) )
29	28	simplbi 460	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( y e. ( ( ~P B i^i Fin ) \ { (/) } ) -> y e. ( ~P B i^i Fin ) )
30	29	ad2antrl 727	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 7605	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( y e. ( ~P B i^i Fin ) <-> ( y C_ B /\ y e. Fin ) )
32	31	simplbi 460	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( y e. ( ~P B i^i Fin ) -> y C_ B )
33	30, 32	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3349	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 647	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 568	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3331	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( z e. ( B \ F ) <-> ( z e. B /\ -. z e. F ) )
38	36, 37	sylibr 212	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4089	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( x e. z /\ z e. ( B \ F ) ) -> x e. U. ( B \ F ) )
40	27, 38, 39	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 434	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 125	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 615	. . . . . . . . . . . . . . . . . . . . . . . . . 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 3355	. . . . . . . . . . . . . . . . . . . . . . . . 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 464	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( y e. ( ( ~P B i^i Fin ) \ { (/) } ) -> y =/= (/) )
46	45	ad2antrl 727	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ ( x e. X /\ -. x e. U. ( B \ F ) ) ) /\ ( y e. ( ( ~P B i^i Fin ) \ { (/) } ) /\ x e. |^| y ) ) -> y =/= (/) )
47	31	simprbi 464	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( y e. ( ~P B i^i Fin ) -> y e. Fin )
48	30, 47	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . 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 7657	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( F e. ( Fil ` X ) /\ ( y C_ F /\ y =/= (/) /\ y e. Fin ) ) -> |^| y e. ( fi ` F ) )
50	21, 44, 46, 48, 49	syl13anc 1220	. . . . . . . . . . . . . . . . . . . . . . . 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 19401	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( F e. ( Fil ` X ) -> ( fi ` F ) = F )
52	21, 51	syl 16	. . . . . . . . . . . . . . . . . . . . . . . 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 615	. . . . . . . . . . . . . . . . . . . . . 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 2498	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( z = |^| y -> ( x e. z <-> x e. |^| y ) )
56		eleq1 2497	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( z = |^| y -> ( z e. F <-> |^| y e. F ) )
57	55, 56	imbi12d 320	. . . . . . . . . . . . . . . . . . . . . 22 |- ( z = |^| y -> ( ( x e. z -> z e. F ) <-> ( x e. |^| y -> |^| y e. F ) ) )
58	54, 57	syl5ibrcom 222	. . . . . . . . . . . . . . . . . . . . 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 2835	. . . . . . . . . . . . . . . . . . . 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 215	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( x e. X /\ -. x e. U. ( B \ F ) ) ) -> ( z e. ( fi ` B ) -> ( x e. z -> z e. F ) ) )
61	60	imp32 433	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ ( x e. X /\ -. x e. U. ( B \ F ) ) ) /\ ( z e. ( fi ` B ) /\ x e. z ) ) -> z e. F )
62	61	adantrrr 724	. . . . . . . . . . . . . . . . 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 714	. . . . . . . . . . . . . . . 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 4114	. . . . . . . . . . . . . . . . . . 19 |- ( y e. J -> y C_ U. J )
65	64	ad2antrl 727	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ ( x e. X /\ -. x e. U. ( B \ F ) ) ) /\ ( y e. J /\ x e. y ) ) -> y C_ U. J )
66		fibas 18551	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( fi ` B ) e. TopBases
67		tgtopon 18545	. . . . . . . . . . . . . . . . . . . . . . 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 2525	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> J e. (TopOn ` U. ( fi ` B ) ) )
70		fiuni 7670	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( B e. _V -> U. B = U. ( fi ` B ) )
71	17, 70	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> U. B = U. ( fi ` B ) )
72	13, 71	eqtrd 2469	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> X = U. ( fi ` B ) )
73	72	fveq2d 5688	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> (TopOn ` X ) = (TopOn ` U. ( fi ` B ) ) )
74	69, 73	eleqtrrd 2514	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> J e. (TopOn ` X ) )
75		toponuni 18501	. . . . . . . . . . . . . . . . . . . 20 |- ( J e. (TopOn ` X ) -> X = U. J )
76	74, 75	syl 16	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> X = U. J )
77	76	ad2antrr 725	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ ( x e. X /\ -. x e. U. ( B \ F ) ) ) /\ ( y e. J /\ x e. y ) ) -> X = U. J )
78	65, 77	sseqtr4d 3386	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( x e. X /\ -. x e. U. ( B \ F ) ) ) /\ ( y e. J /\ x e. y ) ) -> y C_ X )
79	78	adantr 465	. . . . . . . . . . . . . . . 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 764	. . . . . . . . . . . . . . . 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 19395	. . . . . . . . . . . . . . . 16 |- ( ( F e. ( Fil ` X ) /\ ( z e. F /\ y C_ X /\ z C_ y ) ) -> y e. F )
82	12, 63, 79, 80, 81	syl13anc 1220	. . . . . . . . . . . . . . 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 2839	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( x e. X /\ -. x e. U. ( B \ F ) ) ) /\ ( y e. J /\ x e. y ) ) -> y e. F )
84	83	expr 615	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( x e. X /\ -. x e. U. ( B \ F ) ) ) /\ y e. J ) -> ( x e. y -> y e. F ) )
85	84	ralrimiva 2793	. . . . . . . . . . . 12 |- ( ( ph /\ ( x e. X /\ -. x e. U. ( B \ F ) ) ) -> A. y e. J ( x e. y -> y e. F ) )
86	85	expr 615	. . . . . . . . . . 11 |- ( ( ph /\ x e. X ) -> ( -. x e. U. ( B \ F ) -> A. y e. J ( x e. y -> y e. F ) ) )
87	86	imdistanda 693	. . . . . . . . . 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 217	. . . . . . . . 9 |- ( ph -> ( x e. ( X \ U. ( B \ F ) ) -> ( x e. X /\ A. y e. J ( x e. y -> y e. F ) ) ) )
89		flimopn 19517	. . . . . . . . . 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 661	. . . . . . . . 9 |- ( ph -> ( x e. ( J fLim F ) <-> ( x e. X /\ A. y e. J ( x e. y -> y e. F ) ) ) )
91	88, 90	sylibrd 234	. . . . . . . 8 |- ( ph -> ( x e. ( X \ U. ( B \ F ) ) -> x e. ( J fLim F ) ) )
92	91	ssrdv 3355	. . . . . . 7 |- ( ph -> ( X \ U. ( B \ F ) ) C_ ( J fLim F ) )
93		alexsub.6	. . . . . . 7 |- ( ph -> ( J fLim F ) = (/) )
94		sseq0 3662	. . . . . . 7 |- ( ( ( X \ U. ( B \ F ) ) C_ ( J fLim F ) /\ ( J fLim F ) = (/) ) -> ( X \ U. ( B \ F ) ) = (/) )
95	92, 93, 94	syl2anc 661	. . . . . 6 |- ( ph -> ( X \ U. ( B \ F ) ) = (/) )
96		ssdif0 3730	. . . . . 6 |- ( X C_ U. ( B \ F ) <-> ( X \ U. ( B \ F ) ) = (/) )
97	95, 96	sylibr 212	. . . . 5 |- ( ph -> X C_ U. ( B \ F ) )
98		difss 3476	. . . . . . 7 |- ( B \ F ) C_ B
99	98	unissi 4107	. . . . . 6 |- U. ( B \ F ) C_ U. B
100	99, 13	syl5sseqr 3398	. . . . 5 |- ( ph -> U. ( B \ F ) C_ X )
101	97, 100	eqssd 3366	. . . 4 |- ( ph -> X = U. ( B \ F ) )
102	101, 98	jctil 537	. . 3 |- ( ph -> ( ( B \ F ) C_ B /\ X = U. ( B \ F ) ) )
103		difexg 4433	. . . . . 6 |- ( B e. _V -> ( B \ F ) e. _V )
104	17, 103	syl 16	. . . . 5 |- ( ph -> ( B \ F ) e. _V )
105	104	adantr 465	. . . 4 |- ( ( ph /\ ( ( B \ F ) C_ B /\ X = U. ( B \ F ) ) ) -> ( B \ F ) e. _V )
106		sseq1 3370	. . . . . . . 8 |- ( x = ( B \ F ) -> ( x C_ B <-> ( B \ F ) C_ B ) )
107		unieq 4092	. . . . . . . . 9 |- ( x = ( B \ F ) -> U. x = U. ( B \ F ) )
108	107	eqeq2d 2448	. . . . . . . 8 |- ( x = ( B \ F ) -> ( X = U. x <-> X = U. ( B \ F ) ) )
109	106, 108	anbi12d 710	. . . . . . 7 |- ( x = ( B \ F ) -> ( ( x C_ B /\ X = U. x ) <-> ( ( B \ F ) C_ B /\ X = U. ( B \ F ) ) ) )
110	109	anbi2d 703	. . . . . 6 |- ( x = ( B \ F ) -> ( ( ph /\ ( x C_ B /\ X = U. x ) ) <-> ( ph /\ ( ( B \ F ) C_ B /\ X = U. ( B \ F ) ) ) ) )
111		pweq 3856	. . . . . . . 8 |- ( x = ( B \ F ) -> ~P x = ~P ( B \ F ) )
112	111	ineq1d 3544	. . . . . . 7 |- ( x = ( B \ F ) -> ( ~P x i^i Fin ) = ( ~P ( B \ F ) i^i Fin ) )
113	112	rexeqdv 2918	. . . . . 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 320	. . . . 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 3023	. . . 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 36	. . 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 668	. 2 |- ( ph -> E. y e. ( ~P ( B \ F ) i^i Fin ) X = U. y )
119		unieq 4092	. . . . . . 7 |- ( y = (/) -> U. y = U. (/) )
120		uni0 4111	. . . . . . 7 |- U. (/) = (/)
121	119, 120	syl6eq 2485	. . . . . 6 |- ( y = (/) -> U. y = (/) )
122	121	neeq2d 2616	. . . . 5 |- ( y = (/) -> ( X =/= U. y <-> X =/= (/) ) )
123		difssd 3477	. . . . . . . . . . 11 |- ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) -> ( X \ z ) C_ X )
124	123	ralrimivw 2794	. . . . . . . . . 10 |- ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) -> A. z e. y ( X \ z ) C_ X )
125		riinn0 4238	. . . . . . . . . 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 471	. . . . . . . . 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 725	. . . . . . . . . . . . 13 |- ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> X e. _V )
128		difexg 4433	. . . . . . . . . . . . 13 |- ( X e. _V -> ( X \ z ) e. _V )
129	127, 128	syl 16	. . . . . . . . . . . 12 |- ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> ( X \ z ) e. _V )
130	129	ralrimivw 2794	. . . . . . . . . . 11 |- ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> A. z e. y ( X \ z ) e. _V )
131		dfiin2g 4196	. . . . . . . . . . 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 16	. . . . . . . . . 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 2437	. . . . . . . . . . . 12 |- ( z e. y |-> ( X \ z ) ) = ( z e. y |-> ( X \ z ) )
134	133	rnmpt 5077	. . . . . . . . . . 11 |- ran ( z e. y |-> ( X \ z ) ) = { x | E. z e. y x = ( X \ z ) }
135	134	inteqi 4125	. . . . . . . . . 10 |- |^| ran ( z e. y |-> ( X \ z ) ) = |^| { x | E. z e. y x = ( X \ z ) }
136	132, 135	syl6eqr 2487	. . . . . . . . 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 2469	. . . . . . . 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 725	. . . . . . . . 9 |- ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> F e. ( Fil ` X ) )
139		elfpw 7605	. . . . . . . . . . . . . . . 16 |- ( y e. ( ~P ( B \ F ) i^i Fin ) <-> ( y C_ ( B \ F ) /\ y e. Fin ) )
140	139	simplbi 460	. . . . . . . . . . . . . . 15 |- ( y e. ( ~P ( B \ F ) i^i Fin ) -> y C_ ( B \ F ) )
141	140	ad2antlr 726	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> y C_ ( B \ F ) )
142	141	sselda 3349	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) /\ z e. y ) -> z e. ( B \ F ) )
143	142	eldifbd 3334	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) /\ z e. y ) -> -. z e. F )
144	9	ad3antrrr 729	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) /\ z e. y ) -> F e. ( UFil ` X ) )
145	141	difss2d 3479	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> y C_ B )
146	145	sselda 3349	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) /\ z e. y ) -> z e. B )
147		elssuni 4114	. . . . . . . . . . . . . . 15 |- ( z e. B -> z C_ U. B )
148	146, 147	syl 16	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) /\ z e. y ) -> z C_ U. B )
149	13	ad3antrrr 729	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) /\ z e. y ) -> X = U. B )
150	148, 149	sseqtr4d 3386	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) /\ z e. y ) -> z C_ X )
151		ufilb 19448	. . . . . . . . . . . . 13 |- ( ( F e. ( UFil ` X ) /\ z C_ X ) -> ( -. z e. F <-> ( X \ z ) e. F ) )
152	144, 150, 151	syl2anc 661	. . . . . . . . . . . 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 210	. . . . . . . . . . 11 |- ( ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) /\ z e. y ) -> ( X \ z ) e. F )
154	153, 133	fmptd 5860	. . . . . . . . . 10 |- ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> ( z e. y |-> ( X \ z ) ) : y --> F )
155		frn 5558	. . . . . . . . . 10 |- ( ( z e. y |-> ( X \ z ) ) : y --> F -> ran ( z e. y |-> ( X \ z ) ) C_ F )
156	154, 155	syl 16	. . . . . . . . 9 |- ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> ran ( z e. y |-> ( X \ z ) ) C_ F )
157		fdm 5556	. . . . . . . . . . . 12 |- ( ( z e. y |-> ( X \ z ) ) : y --> F -> dom ( z e. y |-> ( X \ z ) ) = y )
158	154, 157	syl 16	. . . . . . . . . . 11 |- ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> dom ( z e. y |-> ( X \ z ) ) = y )
159		simpr 461	. . . . . . . . . . 11 |- ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> y =/= (/) )
160	158, 159	eqnetrd 2620	. . . . . . . . . 10 |- ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> dom ( z e. y |-> ( X \ z ) ) =/= (/) )
161		dm0rn0 5048	. . . . . . . . . . 11 |- ( dom ( z e. y |-> ( X \ z ) ) = (/) <-> ran ( z e. y |-> ( X \ z ) ) = (/) )
162	161	necon3bii 2634	. . . . . . . . . 10 |- ( dom ( z e. y |-> ( X \ z ) ) =/= (/) <-> ran ( z e. y |-> ( X \ z ) ) =/= (/) )
163	160, 162	sylib 196	. . . . . . . . 9 |- ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> ran ( z e. y |-> ( X \ z ) ) =/= (/) )
164	139	simprbi 464	. . . . . . . . . . 11 |- ( y e. ( ~P ( B \ F ) i^i Fin ) -> y e. Fin )
165	164	ad2antlr 726	. . . . . . . . . 10 |- ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> y e. Fin )
166		abrexfi 7603	. . . . . . . . . . 11 |- ( y e. Fin -> { x | E. z e. y x = ( X \ z ) } e. Fin )
167	134, 166	syl5eqel 2521	. . . . . . . . . 10 |- ( y e. Fin -> ran ( z e. y |-> ( X \ z ) ) e. Fin )
168	165, 167	syl 16	. . . . . . . . 9 |- ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> ran ( z e. y |-> ( X \ z ) ) e. Fin )
169		filintn0 19403	. . . . . . . . 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 ) ) =/= (/) )
170	138, 156, 163, 168, 169	syl13anc 1220	. . . . . . . 8 |- ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> |^| ran ( z e. y |-> ( X \ z ) ) =/= (/) )
171	137, 170	eqnetrd 2620	. . . . . . 7 |- ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> ( X i^i |^|_ z e. y ( X \ z ) ) =/= (/) )
172		disj3 3716	. . . . . . . 8 |- ( ( X i^i |^|_ z e. y ( X \ z ) ) = (/) <-> X = ( X \ |^|_ z e. y ( X \ z ) ) )
173	172	necon3bii 2634	. . . . . . 7 |- ( ( X i^i |^|_ z e. y ( X \ z ) ) =/= (/) <-> X =/= ( X \ |^|_ z e. y ( X \ z ) ) )
174	171, 173	sylib 196	. . . . . 6 |- ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> X =/= ( X \ |^|_ z e. y ( X \ z ) ) )
175		iundif2 4230	. . . . . . 7 |- U_ z e. y ( X \ ( X \ z ) ) = ( X \ |^|_ z e. y ( X \ z ) )
176		dfss4 3577	. . . . . . . . . 10 |- ( z C_ X <-> ( X \ ( X \ z ) ) = z )
177	150, 176	sylib 196	. . . . . . . . 9 |- ( ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) /\ z e. y ) -> ( X \ ( X \ z ) ) = z )
178	177	iuneq2dv 4185	. . . . . . . 8 |- ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> U_ z e. y ( X \ ( X \ z ) ) = U_ z e. y z )
179		uniiun 4216	. . . . . . . 8 |- U. y = U_ z e. y z
180	178, 179	syl6eqr 2487	. . . . . . 7 |- ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> U_ z e. y ( X \ ( X \ z ) ) = U. y )
181	175, 180	syl5eqr 2483	. . . . . 6 |- ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> ( X \ |^|_ z e. y ( X \ z ) ) = U. y )
182	174, 181	neeqtrd 2624	. . . . 5 |- ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> X =/= U. y )
183	11	adantr 465	. . . . . 6 |- ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) -> F e. ( Fil ` X ) )
184		filtop 19397	. . . . . . 7 |- ( F e. ( Fil ` X ) -> X e. F )
185		fileln0 19392	. . . . . . 7 |- ( ( F e. ( Fil ` X ) /\ X e. F ) -> X =/= (/) )
186	184, 185	mpdan 668	. . . . . 6 |- ( F e. ( Fil ` X ) -> X =/= (/) )
187	183, 186	syl 16	. . . . 5 |- ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) -> X =/= (/) )
188	122, 182, 187	pm2.61ne 2680	. . . 4 |- ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) -> X =/= U. y )
189	188	neneqd 2618	. . 3 |- ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) -> -. X = U. y )
190	189	nrexdv 2813	. 2 |- ( ph -> -. E. y e. ( ~P ( B \ F ) i^i Fin ) X = U. y )
191	118, 190	pm2.65i 173	1 |- -. ph

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   /\ wa 369   = wceq 1369   e. wcel 1756   {cab 2423   =/= wne 2600   A.wral 2709   E.wrex 2710   _Vcvv 2966   \ cdif 3318   i^i cin 3320   C_ wss 3321   (/)c0 3630   ~Pcpw 3853   {csn 3870   U.cuni 4084   |^|cint 4121   U_ciun 4164   |^|_ciin 4165   e. cmpt 4343   dom cdm 4832   ran crn 4833   -->wf 5407   ` cfv 5411  (class class class)co 6086   Fincfn 7302   ficfi 7652   topGenctg 14368  TopOnctopon 18468   TopBasesctb 18471   Filcfil 19387   UFilcufil 19441  UFLcufl 19442   fLim cflim 19476

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2418  ax-rep 4396  ax-sep 4406  ax-nul 4414  ax-pow 4463  ax-pr 4524  ax-un 6367

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-ne 2602  df-nel 2603  df-ral 2714  df-rex 2715  df-reu 2716  df-rab 2718  df-v 2968  df-sbc 3180  df-csb 3282  df-dif 3324  df-un 3326  df-in 3328  df-ss 3335  df-pss 3337  df-nul 3631  df-if 3785  df-pw 3855  df-sn 3871  df-pr 3873  df-tp 3875  df-op 3877  df-uni 4085  df-int 4122  df-iun 4166  df-iin 4167  df-br 4286  df-opab 4344  df-mpt 4345  df-tr 4379  df-eprel 4624  df-id 4628  df-po 4633  df-so 4634  df-fr 4671  df-we 4673  df-ord 4714  df-on 4715  df-lim 4716  df-suc 4717  df-xp 4838  df-rel 4839  df-cnv 4840  df-co 4841  df-dm 4842  df-rn 4843  df-res 4844  df-ima 4845  df-iota 5374  df-fun 5413  df-fn 5414  df-f 5415  df-f1 5416  df-fo 5417  df-f1o 5418  df-fv 5419  df-ov 6089  df-oprab 6090  df-mpt2 6091  df-om 6472  df-1st 6572  df-2nd 6573  df-recs 6824  df-rdg 6858  df-1o 6912  df-oadd 6916  df-er 7093  df-en 7303  df-dom 7304  df-fin 7306  df-fi 7653  df-topgen 14374  df-fbas 17783  df-top 18472  df-bases 18474  df-topon 18475  df-ntr 18593  df-nei 18671  df-fil 19388  df-ufil 19443  df-flim 19481

This theorem is referenced by:  alexsub  19586