Theorem alexsublem 20629

Description: Lemma for alexsub 20630. (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 3399	. . . . . . . . . 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 2452	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( y e. J <-> y e. ( topGen ` ( fi ` B ) ) ) )
4	3	anbi1d 702	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ( y e. J /\ x e. y ) <-> ( y e. ( topGen ` ( fi ` B ) ) /\ x e. y ) ) )
5	4	biimpa 482	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( y e. J /\ x e. y ) ) -> ( y e. ( topGen ` ( fi ` B ) ) /\ x e. y ) )
6	5	adantlr 712	. . . . . . . . . . . . . . . 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 19551	. . . . . . . . . . . . . . . 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 20490	. . . . . . . . . . . . . . . . . 18 |- ( F e. ( UFil ` X ) -> F e. ( Fil ` X ) )
11	9, 10	syl 16	. . . . . . . . . . . . . . . . 17 |- ( ph -> F e. ( Fil ` X ) )
12	11	ad3antrrr 727	. . . . . . . . . . . . . . . 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 5802	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> X e. _V )
15	13, 14	eqeltrrd 2471	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> U. B e. _V )
16		uniexb 6509	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( B e. _V <-> U. B e. _V )
17	15, 16	sylibr 212	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> B e. _V )
18		elfi2 7789	. . . . . . . . . . . . . . . . . . . . . 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 463	. . . . . . . . . . . . . . . . . . . 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 723	. . . . . . . . . . . . . . . . . . . . . . . . 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 4214	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( z e. y -> |^| y C_ z )
24	23	adantl 464	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( y e. ( ( ~P B i^i Fin ) \ { (/) } ) /\ x e. |^| y ) /\ z e. y ) -> |^| y C_ z )
25		simplr 753	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( y e. ( ( ~P B i^i Fin ) \ { (/) } ) /\ x e. |^| y ) /\ z e. y ) -> x e. |^| y )
26	24, 25	sseldd 3418	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( y e. ( ( ~P B i^i Fin ) \ { (/) } ) /\ x e. |^| y ) /\ z e. y ) -> x e. z )
27	26	ad2antlr 724	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4069	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( y e. ( ( ~P B i^i Fin ) \ { (/) } ) <-> ( y e. ( ~P B i^i Fin ) /\ y =/= (/) ) )
29	28	simplbi 458	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( y e. ( ( ~P B i^i Fin ) \ { (/) } ) -> y e. ( ~P B i^i Fin ) )
30	29	ad2antrl 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 7737	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( y e. ( ~P B i^i Fin ) <-> ( y C_ B /\ y e. Fin ) )
32	31	simplbi 458	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3417	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 645	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 566	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3399	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4168	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( x e. z /\ z e. ( B \ F ) ) -> x e. U. ( B \ F ) )
40	27, 38, 39	syl2anc 659	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 432	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 613	. . . . . . . . . . . . . . . . . . . . . . . . . 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 3423	. . . . . . . . . . . . . . . . . . . . . . . . 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 462	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( y e. ( ( ~P B i^i Fin ) \ { (/) } ) -> y =/= (/) )
46	45	ad2antrl 725	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ ( x e. X /\ -. x e. U. ( B \ F ) ) ) /\ ( y e. ( ( ~P B i^i Fin ) \ { (/) } ) /\ x e. |^| y ) ) -> y =/= (/) )
47	31	simprbi 462	. . . . . . . . . . . . . . . . . . . . . . . . . 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 7790	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( F e. ( Fil ` X ) /\ ( y C_ F /\ y =/= (/) /\ y e. Fin ) ) -> |^| y e. ( fi ` F ) )
50	21, 44, 46, 48, 49	syl13anc 1228	. . . . . . . . . . . . . . . . . . . . . . . 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 20445	. . . . . . . . . . . . . . . . . . . . . . . . 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 2472	. . . . . . . . . . . . . . . . . . . . . . 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 613	. . . . . . . . . . . . . . . . . . . . . 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 2455	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( z = |^| y -> ( x e. z <-> x e. |^| y ) )
56		eleq1 2454	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( z = |^| y -> ( z e. F <-> |^| y e. F ) )
57	55, 56	imbi12d 318	. . . . . . . . . . . . . . . . . . . . . 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 2874	. . . . . . . . . . . . . . . . . . . 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 431	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ ( x e. X /\ -. x e. U. ( B \ F ) ) ) /\ ( z e. ( fi ` B ) /\ x e. z ) ) -> z e. F )
62	61	adantrrr 722	. . . . . . . . . . . . . . . . 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 712	. . . . . . . . . . . . . . . 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 4192	. . . . . . . . . . . . . . . . . . 19 |- ( y e. J -> y C_ U. J )
65	64	ad2antrl 725	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ ( x e. X /\ -. x e. U. ( B \ F ) ) ) /\ ( y e. J /\ x e. y ) ) -> y C_ U. J )
66		fibas 19564	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( fi ` B ) e. TopBases
67		tgtopon 19558	. . . . . . . . . . . . . . . . . . . . . . 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 2478	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> J e. (TopOn ` U. ( fi ` B ) ) )
70		fiuni 7803	. . . . . . . . . . . . . . . . . . . . . . . 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 2423	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> X = U. ( fi ` B ) )
73	72	fveq2d 5778	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> (TopOn ` X ) = (TopOn ` U. ( fi ` B ) ) )
74	69, 73	eleqtrrd 2473	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> J e. (TopOn ` X ) )
75		toponuni 19513	. . . . . . . . . . . . . . . . . . . 20 |- ( J e. (TopOn ` X ) -> X = U. J )
76	74, 75	syl 16	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> X = U. J )
77	76	ad2antrr 723	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ ( x e. X /\ -. x e. U. ( B \ F ) ) ) /\ ( y e. J /\ x e. y ) ) -> X = U. J )
78	65, 77	sseqtr4d 3454	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( x e. X /\ -. x e. U. ( B \ F ) ) ) /\ ( y e. J /\ x e. y ) ) -> y C_ X )
79	78	adantr 463	. . . . . . . . . . . . . . . 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 20439	. . . . . . . . . . . . . . . 16 |- ( ( F e. ( Fil ` X ) /\ ( z e. F /\ y C_ X /\ z C_ y ) ) -> y e. F )
82	12, 63, 79, 80, 81	syl13anc 1228	. . . . . . . . . . . . . . 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 2878	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( x e. X /\ -. x e. U. ( B \ F ) ) ) /\ ( y e. J /\ x e. y ) ) -> y e. F )
84	83	expr 613	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( x e. X /\ -. x e. U. ( B \ F ) ) ) /\ y e. J ) -> ( x e. y -> y e. F ) )
85	84	ralrimiva 2796	. . . . . . . . . . . 12 |- ( ( ph /\ ( x e. X /\ -. x e. U. ( B \ F ) ) ) -> A. y e. J ( x e. y -> y e. F ) )
86	85	expr 613	. . . . . . . . . . 11 |- ( ( ph /\ x e. X ) -> ( -. x e. U. ( B \ F ) -> A. y e. J ( x e. y -> y e. F ) ) )
87	86	imdistanda 691	. . . . . . . . . 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 20561	. . . . . . . . . 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 659	. . . . . . . . 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 3423	. . . . . . 7 |- ( ph -> ( X \ U. ( B \ F ) ) C_ ( J fLim F ) )
93		alexsub.6	. . . . . . 7 |- ( ph -> ( J fLim F ) = (/) )
94		sseq0 3744	. . . . . . 7 |- ( ( ( X \ U. ( B \ F ) ) C_ ( J fLim F ) /\ ( J fLim F ) = (/) ) -> ( X \ U. ( B \ F ) ) = (/) )
95	92, 93, 94	syl2anc 659	. . . . . 6 |- ( ph -> ( X \ U. ( B \ F ) ) = (/) )
96		ssdif0 3801	. . . . . 6 |- ( X C_ U. ( B \ F ) <-> ( X \ U. ( B \ F ) ) = (/) )
97	95, 96	sylibr 212	. . . . 5 |- ( ph -> X C_ U. ( B \ F ) )
98		difss 3545	. . . . . . 7 |- ( B \ F ) C_ B
99	98	unissi 4186	. . . . . 6 |- U. ( B \ F ) C_ U. B
100	99, 13	syl5sseqr 3466	. . . . 5 |- ( ph -> U. ( B \ F ) C_ X )
101	97, 100	eqssd 3434	. . . 4 |- ( ph -> X = U. ( B \ F ) )
102	101, 98	jctil 535	. . 3 |- ( ph -> ( ( B \ F ) C_ B /\ X = U. ( B \ F ) ) )
103		difexg 4513	. . . . . 6 |- ( B e. _V -> ( B \ F ) e. _V )
104	17, 103	syl 16	. . . . 5 |- ( ph -> ( B \ F ) e. _V )
105	104	adantr 463	. . . 4 |- ( ( ph /\ ( ( B \ F ) C_ B /\ X = U. ( B \ F ) ) ) -> ( B \ F ) e. _V )
106		sseq1 3438	. . . . . . . 8 |- ( x = ( B \ F ) -> ( x C_ B <-> ( B \ F ) C_ B ) )
107		unieq 4171	. . . . . . . . 9 |- ( x = ( B \ F ) -> U. x = U. ( B \ F ) )
108	107	eqeq2d 2396	. . . . . . . 8 |- ( x = ( B \ F ) -> ( X = U. x <-> X = U. ( B \ F ) ) )
109	106, 108	anbi12d 708	. . . . . . 7 |- ( x = ( B \ F ) -> ( ( x C_ B /\ X = U. x ) <-> ( ( B \ F ) C_ B /\ X = U. ( B \ F ) ) ) )
110	109	anbi2d 701	. . . . . 6 |- ( x = ( B \ F ) -> ( ( ph /\ ( x C_ B /\ X = U. x ) ) <-> ( ph /\ ( ( B \ F ) C_ B /\ X = U. ( B \ F ) ) ) ) )
111		pweq 3930	. . . . . . . 8 |- ( x = ( B \ F ) -> ~P x = ~P ( B \ F ) )
112	111	ineq1d 3613	. . . . . . 7 |- ( x = ( B \ F ) -> ( ~P x i^i Fin ) = ( ~P ( B \ F ) i^i Fin ) )
113	112	rexeqdv 2986	. . . . . 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 318	. . . . 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 3092	. . . 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 666	. 2 |- ( ph -> E. y e. ( ~P ( B \ F ) i^i Fin ) X = U. y )
119		unieq 4171	. . . . . . 7 |- ( y = (/) -> U. y = U. (/) )
120		uni0 4190	. . . . . . 7 |- U. (/) = (/)
121	119, 120	syl6eq 2439	. . . . . 6 |- ( y = (/) -> U. y = (/) )
122	121	neeq2d 2660	. . . . 5 |- ( y = (/) -> ( X =/= U. y <-> X =/= (/) ) )
123		difssd 3546	. . . . . . . . . . 11 |- ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) -> ( X \ z ) C_ X )
124	123	ralrimivw 2797	. . . . . . . . . 10 |- ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) -> A. z e. y ( X \ z ) C_ X )
125		riinn0 4318	. . . . . . . . . 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 469	. . . . . . . . 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 723	. . . . . . . . . . . . 13 |- ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> X e. _V )
128		difexg 4513	. . . . . . . . . . . . 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 2797	. . . . . . . . . . 11 |- ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> A. z e. y ( X \ z ) e. _V )
131		dfiin2g 4276	. . . . . . . . . . 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 2382	. . . . . . . . . . . 12 |- ( z e. y |-> ( X \ z ) ) = ( z e. y |-> ( X \ z ) )
134	133	rnmpt 5161	. . . . . . . . . . 11 |- ran ( z e. y |-> ( X \ z ) ) = { x | E. z e. y x = ( X \ z ) }
135	134	inteqi 4203	. . . . . . . . . 10 |- |^| ran ( z e. y |-> ( X \ z ) ) = |^| { x | E. z e. y x = ( X \ z ) }
136	132, 135	syl6eqr 2441	. . . . . . . . 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 2423	. . . . . . . 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 723	. . . . . . . . 9 |- ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> F e. ( Fil ` X ) )
139		elfpw 7737	. . . . . . . . . . . . . . . 16 |- ( y e. ( ~P ( B \ F ) i^i Fin ) <-> ( y C_ ( B \ F ) /\ y e. Fin ) )
140	139	simplbi 458	. . . . . . . . . . . . . . 15 |- ( y e. ( ~P ( B \ F ) i^i Fin ) -> y C_ ( B \ F ) )
141	140	ad2antlr 724	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> y C_ ( B \ F ) )
142	141	sselda 3417	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) /\ z e. y ) -> z e. ( B \ F ) )
143	142	eldifbd 3402	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) /\ z e. y ) -> -. z e. F )
144	9	ad3antrrr 727	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) /\ z e. y ) -> F e. ( UFil ` X ) )
145	141	difss2d 3548	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> y C_ B )
146	145	sselda 3417	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) /\ z e. y ) -> z e. B )
147		elssuni 4192	. . . . . . . . . . . . . . 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 727	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) /\ z e. y ) -> X = U. B )
150	148, 149	sseqtr4d 3454	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) /\ z e. y ) -> z C_ X )
151		ufilb 20492	. . . . . . . . . . . . 13 |- ( ( F e. ( UFil ` X ) /\ z C_ X ) -> ( -. z e. F <-> ( X \ z ) e. F ) )
152	144, 150, 151	syl2anc 659	. . . . . . . . . . . 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 5957	. . . . . . . . . 10 |- ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> ( z e. y |-> ( X \ z ) ) : y --> F )
155		frn 5645	. . . . . . . . . 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	133, 153	dmmptd 5619	. . . . . . . . . . 11 |- ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> dom ( z e. y |-> ( X \ z ) ) = y )
158		simpr 459	. . . . . . . . . . 11 |- ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> y =/= (/) )
159	157, 158	eqnetrd 2675	. . . . . . . . . 10 |- ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> dom ( z e. y |-> ( X \ z ) ) =/= (/) )
160		dm0rn0 5132	. . . . . . . . . . 11 |- ( dom ( z e. y |-> ( X \ z ) ) = (/) <-> ran ( z e. y |-> ( X \ z ) ) = (/) )
161	160	necon3bii 2650	. . . . . . . . . 10 |- ( dom ( z e. y |-> ( X \ z ) ) =/= (/) <-> ran ( z e. y |-> ( X \ z ) ) =/= (/) )
162	159, 161	sylib 196	. . . . . . . . 9 |- ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> ran ( z e. y |-> ( X \ z ) ) =/= (/) )
163	139	simprbi 462	. . . . . . . . . . 11 |- ( y e. ( ~P ( B \ F ) i^i Fin ) -> y e. Fin )
164	163	ad2antlr 724	. . . . . . . . . 10 |- ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> y e. Fin )
165		abrexfi 7735	. . . . . . . . . . 11 |- ( y e. Fin -> { x | E. z e. y x = ( X \ z ) } e. Fin )
166	134, 165	syl5eqel 2474	. . . . . . . . . 10 |- ( y e. Fin -> ran ( z e. y |-> ( X \ z ) ) e. Fin )
167	164, 166	syl 16	. . . . . . . . 9 |- ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> ran ( z e. y |-> ( X \ z ) ) e. Fin )
168		filintn0 20447	. . . . . . . . 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 1228	. . . . . . . 8 |- ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> |^| ran ( z e. y |-> ( X \ z ) ) =/= (/) )
170	137, 169	eqnetrd 2675	. . . . . . 7 |- ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> ( X i^i |^|_ z e. y ( X \ z ) ) =/= (/) )
171		disj3 3787	. . . . . . . 8 |- ( ( X i^i |^|_ z e. y ( X \ z ) ) = (/) <-> X = ( X \ |^|_ z e. y ( X \ z ) ) )
172	171	necon3bii 2650	. . . . . . 7 |- ( ( X i^i |^|_ z e. y ( X \ z ) ) =/= (/) <-> X =/= ( X \ |^|_ z e. y ( X \ z ) ) )
173	170, 172	sylib 196	. . . . . 6 |- ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> X =/= ( X \ |^|_ z e. y ( X \ z ) ) )
174		iundif2 4310	. . . . . . 7 |- U_ z e. y ( X \ ( X \ z ) ) = ( X \ |^|_ z e. y ( X \ z ) )
175		dfss4 3657	. . . . . . . . . 10 |- ( z C_ X <-> ( X \ ( X \ z ) ) = z )
176	150, 175	sylib 196	. . . . . . . . 9 |- ( ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) /\ z e. y ) -> ( X \ ( X \ z ) ) = z )
177	176	iuneq2dv 4265	. . . . . . . 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 4296	. . . . . . . 8 |- U. y = U_ z e. y z
179	177, 178	syl6eqr 2441	. . . . . . 7 |- ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> U_ z e. y ( X \ ( X \ z ) ) = U. y )
180	174, 179	syl5eqr 2437	. . . . . 6 |- ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> ( X \ |^|_ z e. y ( X \ z ) ) = U. y )
181	173, 180	neeqtrd 2677	. . . . 5 |- ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> X =/= U. y )
182	11	adantr 463	. . . . . 6 |- ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) -> F e. ( Fil ` X ) )
183		filtop 20441	. . . . . . 7 |- ( F e. ( Fil ` X ) -> X e. F )
184		fileln0 20436	. . . . . . 7 |- ( ( F e. ( Fil ` X ) /\ X e. F ) -> X =/= (/) )
185	183, 184	mpdan 666	. . . . . 6 |- ( F e. ( Fil ` X ) -> X =/= (/) )
186	182, 185	syl 16	. . . . 5 |- ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) -> X =/= (/) )
187	122, 181, 186	pm2.61ne 2697	. . . 4 |- ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) -> X =/= U. y )
188	187	neneqd 2584	. . 3 |- ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) -> -. X = U. y )
189	188	nrexdv 2838	. 2 |- ( ph -> -. E. y e. ( ~P ( B \ F ) i^i Fin ) X = U. y )
190	118, 189	pm2.65i 173	1 |- -. ph

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   /\ wa 367   = wceq 1399   e. wcel 1826   {cab 2367   =/= wne 2577   A.wral 2732   E.wrex 2733   _Vcvv 3034   \ cdif 3386   i^i cin 3388   C_ wss 3389   (/)c0 3711   ~Pcpw 3927   {csn 3944   U.cuni 4163   |^|cint 4199   U_ciun 4243   |^|_ciin 4244   |-> cmpt 4425   dom cdm 4913   ran crn 4914   -->wf 5492   ` cfv 5496  (class class class)co 6196   Fincfn 7435   ficfi 7785   topGenctg 14845  TopOnctopon 19480   TopBasesctb 19483   Filcfil 20431   UFilcufil 20485  UFLcufl 20486   fLim cflim 20520

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-8 1828  ax-9 1830  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360  ax-rep 4478  ax-sep 4488  ax-nul 4496  ax-pow 4543  ax-pr 4601  ax-un 6491

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-eu 2222  df-mo 2223  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ne 2579  df-nel 2580  df-ral 2737  df-rex 2738  df-reu 2739  df-rab 2741  df-v 3036  df-sbc 3253  df-csb 3349  df-dif 3392  df-un 3394  df-in 3396  df-ss 3403  df-pss 3405  df-nul 3712  df-if 3858  df-pw 3929  df-sn 3945  df-pr 3947  df-tp 3949  df-op 3951  df-uni 4164  df-int 4200  df-iun 4245  df-iin 4246  df-br 4368  df-opab 4426  df-mpt 4427  df-tr 4461  df-eprel 4705  df-id 4709  df-po 4714  df-so 4715  df-fr 4752  df-we 4754  df-ord 4795  df-on 4796  df-lim 4797  df-suc 4798  df-xp 4919  df-rel 4920  df-cnv 4921  df-co 4922  df-dm 4923  df-rn 4924  df-res 4925  df-ima 4926  df-iota 5460  df-fun 5498  df-fn 5499  df-f 5500  df-f1 5501  df-fo 5502  df-f1o 5503  df-fv 5504  df-ov 6199  df-oprab 6200  df-mpt2 6201  df-om 6600  df-1st 6699  df-2nd 6700  df-recs 6960  df-rdg 6994  df-1o 7048  df-oadd 7052  df-er 7229  df-en 7436  df-dom 7437  df-fin 7439  df-fi 7786  df-topgen 14851  df-fbas 18529  df-top 19484  df-bases 19486  df-topon 19487  df-ntr 19606  df-nei 19685  df-fil 20432  df-ufil 20487  df-flim 20525

This theorem is referenced by:  alexsub  20630