Metamath Proof Explorer

Theorem alexsublem

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

Ref Expression
Hypotheses 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 alexsublem 
|- -. ph

Proof

Step Hyp Ref Expression
1 alexsub.1 
 |-  ( ph -> X e. UFL )
2 alexsub.2 
 |-  ( ph -> X = U. B )
3 alexsub.3 
 |-  ( ph -> J = ( topGen ` ( fi ` B ) ) )
4 alexsub.4 
 |-  ( ( ph /\ ( x C_ B /\ X = U. x ) ) -> E. y e. ( ~P x i^i Fin ) X = U. y )
5 alexsub.5 
 |-  ( ph -> F e. ( UFil ` X ) )
6 alexsub.6 
 |-  ( ph -> ( J fLim F ) = (/) )
7 eldif 
 |-  ( x e. ( X \ U. ( B \ F ) ) <-> ( x e. X /\ -. x e. U. ( B \ F ) ) )
8 3 eleq2d 
 |-  ( ph -> ( y e. J <-> y e. ( topGen ` ( fi ` B ) ) ) )
9 8 anbi1d 
 |-  ( ph -> ( ( y e. J /\ x e. y ) <-> ( y e. ( topGen ` ( fi ` B ) ) /\ x e. y ) ) )
10 9 biimpa 
 |-  ( ( ph /\ ( y e. J /\ x e. y ) ) -> ( y e. ( topGen ` ( fi ` B ) ) /\ x e. y ) )
11 10 adantlr 
 |-  ( ( ( ph /\ ( x e. X /\ -. x e. U. ( B \ F ) ) ) /\ ( y e. J /\ x e. y ) ) -> ( y e. ( topGen ` ( fi ` B ) ) /\ x e. y ) )
12 tg2 
 |-  ( ( y e. ( topGen ` ( fi ` B ) ) /\ x e. y ) -> E. z e. ( fi ` B ) ( x e. z /\ z C_ y ) )
13 11 12 syl 
 |-  ( ( ( 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 ) )
14 ufilfil 
 |-  ( F e. ( UFil ` X ) -> F e. ( Fil ` X ) )
15 5 14 syl 
 |-  ( ph -> F e. ( Fil ` X ) )
16 15 ad3antrrr 
 |-  ( ( ( ( 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 ) )
17 5 elfvexd 
 |-  ( ph -> X e. _V )
18 2 17 eqeltrrd 
 |-  ( ph -> U. B e. _V )
19 uniexb 
 |-  ( B e. _V <-> U. B e. _V )
20 18 19 sylibr 
 |-  ( ph -> B e. _V )
21 elfi2 
 |-  ( B e. _V -> ( z e. ( fi ` B ) <-> E. y e. ( ( ~P B i^i Fin ) \ { (/) } ) z = |^| y ) )
22 20 21 syl 
 |-  ( ph -> ( z e. ( fi ` B ) <-> E. y e. ( ( ~P B i^i Fin ) \ { (/) } ) z = |^| y ) )
23 22 adantr 
 |-  ( ( ph /\ ( x e. X /\ -. x e. U. ( B \ F ) ) ) -> ( z e. ( fi ` B ) <-> E. y e. ( ( ~P B i^i Fin ) \ { (/) } ) z = |^| y ) )
24 15 ad2antrr 
 |-  ( ( ( ph /\ ( x e. X /\ -. x e. U. ( B \ F ) ) ) /\ ( y e. ( ( ~P B i^i Fin ) \ { (/) } ) /\ x e. |^| y ) ) -> F e. ( Fil ` X ) )
25 simplrr 
 |-  ( ( ( 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 ) )
26 intss1 
 |-  ( z e. y -> |^| y C_ z )
27 26 adantl 
 |-  ( ( ( y e. ( ( ~P B i^i Fin ) \ { (/) } ) /\ x e. |^| y ) /\ z e. y ) -> |^| y C_ z )
28 simplr 
 |-  ( ( ( y e. ( ( ~P B i^i Fin ) \ { (/) } ) /\ x e. |^| y ) /\ z e. y ) -> x e. |^| y )
29 27 28 sseldd 
 |-  ( ( ( y e. ( ( ~P B i^i Fin ) \ { (/) } ) /\ x e. |^| y ) /\ z e. y ) -> x e. z )
30 29 ad2antlr 
 |-  ( ( ( ( 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 )
31 eldifsn 
 |-  ( y e. ( ( ~P B i^i Fin ) \ { (/) } ) <-> ( y e. ( ~P B i^i Fin ) /\ y =/= (/) ) )
32 31 simplbi 
 |-  ( y e. ( ( ~P B i^i Fin ) \ { (/) } ) -> y e. ( ~P B i^i Fin ) )
33 32 ad2antrl 
 |-  ( ( ( 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 ) )
34 elfpw 
 |-  ( y e. ( ~P B i^i Fin ) <-> ( y C_ B /\ y e. Fin ) )
35 34 simplbi 
 |-  ( y e. ( ~P B i^i Fin ) -> y C_ B )
36 33 35 syl 
 |-  ( ( ( ph /\ ( x e. X /\ -. x e. U. ( B \ F ) ) ) /\ ( y e. ( ( ~P B i^i Fin ) \ { (/) } ) /\ x e. |^| y ) ) -> y C_ B )
37 36 sselda 
 |-  ( ( ( ( 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 )
38 37 anasss 
 |-  ( ( ( 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 )
39 38 anim1i 
 |-  ( ( ( ( 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 ) )
40 eldif 
 |-  ( z e. ( B \ F ) <-> ( z e. B /\ -. z e. F ) )
41 39 40 sylibr 
 |-  ( ( ( ( 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 ) )
42 elunii 
 |-  ( ( x e. z /\ z e. ( B \ F ) ) -> x e. U. ( B \ F ) )
43 30 41 42 syl2anc 
 |-  ( ( ( ( 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 ) )
44 43 ex 
 |-  ( ( ( 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 ) ) )
45 25 44 mt3d 
 |-  ( ( ( 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 )
46 45 expr 
 |-  ( ( ( 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 ) )
47 46 ssrdv 
 |-  ( ( ( ph /\ ( x e. X /\ -. x e. U. ( B \ F ) ) ) /\ ( y e. ( ( ~P B i^i Fin ) \ { (/) } ) /\ x e. |^| y ) ) -> y C_ F )
48 eldifsni 
 |-  ( y e. ( ( ~P B i^i Fin ) \ { (/) } ) -> y =/= (/) )
49 48 ad2antrl 
 |-  ( ( ( ph /\ ( x e. X /\ -. x e. U. ( B \ F ) ) ) /\ ( y e. ( ( ~P B i^i Fin ) \ { (/) } ) /\ x e. |^| y ) ) -> y =/= (/) )
50 elinel2 
 |-  ( y e. ( ~P B i^i Fin ) -> y e. Fin )
51 33 50 syl 
 |-  ( ( ( ph /\ ( x e. X /\ -. x e. U. ( B \ F ) ) ) /\ ( y e. ( ( ~P B i^i Fin ) \ { (/) } ) /\ x e. |^| y ) ) -> y e. Fin )
52 elfir 
 |-  ( ( F e. ( Fil ` X ) /\ ( y C_ F /\ y =/= (/) /\ y e. Fin ) ) -> |^| y e. ( fi ` F ) )
53 24 47 49 51 52 syl13anc 
 |-  ( ( ( ph /\ ( x e. X /\ -. x e. U. ( B \ F ) ) ) /\ ( y e. ( ( ~P B i^i Fin ) \ { (/) } ) /\ x e. |^| y ) ) -> |^| y e. ( fi ` F ) )
54 filfi 
 |-  ( F e. ( Fil ` X ) -> ( fi ` F ) = F )
55 24 54 syl 
 |-  ( ( ( ph /\ ( x e. X /\ -. x e. U. ( B \ F ) ) ) /\ ( y e. ( ( ~P B i^i Fin ) \ { (/) } ) /\ x e. |^| y ) ) -> ( fi ` F ) = F )
56 53 55 eleqtrd 
 |-  ( ( ( ph /\ ( x e. X /\ -. x e. U. ( B \ F ) ) ) /\ ( y e. ( ( ~P B i^i Fin ) \ { (/) } ) /\ x e. |^| y ) ) -> |^| y e. F )
57 56 expr 
 |-  ( ( ( ph /\ ( x e. X /\ -. x e. U. ( B \ F ) ) ) /\ y e. ( ( ~P B i^i Fin ) \ { (/) } ) ) -> ( x e. |^| y -> |^| y e. F ) )
58 eleq2 
 |-  ( z = |^| y -> ( x e. z <-> x e. |^| y ) )
59 eleq1 
 |-  ( z = |^| y -> ( z e. F <-> |^| y e. F ) )
60 58 59 imbi12d 
 |-  ( z = |^| y -> ( ( x e. z -> z e. F ) <-> ( x e. |^| y -> |^| y e. F ) ) )
61 57 60 syl5ibrcom 
 |-  ( ( ( ph /\ ( x e. X /\ -. x e. U. ( B \ F ) ) ) /\ y e. ( ( ~P B i^i Fin ) \ { (/) } ) ) -> ( z = |^| y -> ( x e. z -> z e. F ) ) )
62 61 rexlimdva 
 |-  ( ( 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 ) ) )
63 23 62 sylbid 
 |-  ( ( ph /\ ( x e. X /\ -. x e. U. ( B \ F ) ) ) -> ( z e. ( fi ` B ) -> ( x e. z -> z e. F ) ) )
64 63 imp32 
 |-  ( ( ( ph /\ ( x e. X /\ -. x e. U. ( B \ F ) ) ) /\ ( z e. ( fi ` B ) /\ x e. z ) ) -> z e. F )
65 64 adantrrr 
 |-  ( ( ( ph /\ ( x e. X /\ -. x e. U. ( B \ F ) ) ) /\ ( z e. ( fi ` B ) /\ ( x e. z /\ z C_ y ) ) ) -> z e. F )
66 65 adantlr 
 |-  ( ( ( ( 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 )
67 elssuni 
 |-  ( y e. J -> y C_ U. J )
68 67 ad2antrl 
 |-  ( ( ( ph /\ ( x e. X /\ -. x e. U. ( B \ F ) ) ) /\ ( y e. J /\ x e. y ) ) -> y C_ U. J )
69 fibas 
 |-  ( fi ` B ) e. TopBases
70 tgtopon 
 |-  ( ( fi ` B ) e. TopBases -> ( topGen ` ( fi ` B ) ) e. ( TopOn ` U. ( fi ` B ) ) )
71 69 70 ax-mp 
 |-  ( topGen ` ( fi ` B ) ) e. ( TopOn ` U. ( fi ` B ) )
72 3 71 eqeltrdi 
 |-  ( ph -> J e. ( TopOn ` U. ( fi ` B ) ) )
73 fiuni 
 |-  ( B e. _V -> U. B = U. ( fi ` B ) )
74 20 73 syl 
 |-  ( ph -> U. B = U. ( fi ` B ) )
75 2 74 eqtrd 
 |-  ( ph -> X = U. ( fi ` B ) )
76 75 fveq2d 
 |-  ( ph -> ( TopOn ` X ) = ( TopOn ` U. ( fi ` B ) ) )
77 72 76 eleqtrrd 
 |-  ( ph -> J e. ( TopOn ` X ) )
78 toponuni 
 |-  ( J e. ( TopOn ` X ) -> X = U. J )
79 77 78 syl 
 |-  ( ph -> X = U. J )
80 79 ad2antrr 
 |-  ( ( ( ph /\ ( x e. X /\ -. x e. U. ( B \ F ) ) ) /\ ( y e. J /\ x e. y ) ) -> X = U. J )
81 68 80 sseqtrrd 
 |-  ( ( ( ph /\ ( x e. X /\ -. x e. U. ( B \ F ) ) ) /\ ( y e. J /\ x e. y ) ) -> y C_ X )
82 81 adantr 
 |-  ( ( ( ( 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 )
83 simprrr 
 |-  ( ( ( ( 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 )
84 filss 
 |-  ( ( F e. ( Fil ` X ) /\ ( z e. F /\ y C_ X /\ z C_ y ) ) -> y e. F )
85 16 66 82 83 84 syl13anc 
 |-  ( ( ( ( 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 )
86 13 85 rexlimddv 
 |-  ( ( ( ph /\ ( x e. X /\ -. x e. U. ( B \ F ) ) ) /\ ( y e. J /\ x e. y ) ) -> y e. F )
87 86 expr 
 |-  ( ( ( ph /\ ( x e. X /\ -. x e. U. ( B \ F ) ) ) /\ y e. J ) -> ( x e. y -> y e. F ) )
88 87 ralrimiva 
 |-  ( ( ph /\ ( x e. X /\ -. x e. U. ( B \ F ) ) ) -> A. y e. J ( x e. y -> y e. F ) )
89 88 expr 
 |-  ( ( ph /\ x e. X ) -> ( -. x e. U. ( B \ F ) -> A. y e. J ( x e. y -> y e. F ) ) )
90 89 imdistanda 
 |-  ( ph -> ( ( x e. X /\ -. x e. U. ( B \ F ) ) -> ( x e. X /\ A. y e. J ( x e. y -> y e. F ) ) ) )
91 7 90 syl5bi 
 |-  ( ph -> ( x e. ( X \ U. ( B \ F ) ) -> ( x e. X /\ A. y e. J ( x e. y -> y e. F ) ) ) )
92 flimopn 
 |-  ( ( 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 ) ) ) )
93 77 15 92 syl2anc 
 |-  ( ph -> ( x e. ( J fLim F ) <-> ( x e. X /\ A. y e. J ( x e. y -> y e. F ) ) ) )
94 91 93 sylibrd 
 |-  ( ph -> ( x e. ( X \ U. ( B \ F ) ) -> x e. ( J fLim F ) ) )
95 94 ssrdv 
 |-  ( ph -> ( X \ U. ( B \ F ) ) C_ ( J fLim F ) )
96 sseq0 
 |-  ( ( ( X \ U. ( B \ F ) ) C_ ( J fLim F ) /\ ( J fLim F ) = (/) ) -> ( X \ U. ( B \ F ) ) = (/) )
97 95 6 96 syl2anc 
 |-  ( ph -> ( X \ U. ( B \ F ) ) = (/) )
98 ssdif0 
 |-  ( X C_ U. ( B \ F ) <-> ( X \ U. ( B \ F ) ) = (/) )
99 97 98 sylibr 
 |-  ( ph -> X C_ U. ( B \ F ) )
100 difss 
 |-  ( B \ F ) C_ B
101 100 unissi 
 |-  U. ( B \ F ) C_ U. B
102 101 2 sseqtrrid 
 |-  ( ph -> U. ( B \ F ) C_ X )
103 99 102 eqssd 
 |-  ( ph -> X = U. ( B \ F ) )
104 103 100 jctil 
 |-  ( ph -> ( ( B \ F ) C_ B /\ X = U. ( B \ F ) ) )
105 difexg 
 |-  ( B e. _V -> ( B \ F ) e. _V )
106 20 105 syl 
 |-  ( ph -> ( B \ F ) e. _V )
107 106 adantr 
 |-  ( ( ph /\ ( ( B \ F ) C_ B /\ X = U. ( B \ F ) ) ) -> ( B \ F ) e. _V )
108 sseq1 
 |-  ( x = ( B \ F ) -> ( x C_ B <-> ( B \ F ) C_ B ) )
109 unieq 
 |-  ( x = ( B \ F ) -> U. x = U. ( B \ F ) )
110 109 eqeq2d 
 |-  ( x = ( B \ F ) -> ( X = U. x <-> X = U. ( B \ F ) ) )
111 108 110 anbi12d 
 |-  ( x = ( B \ F ) -> ( ( x C_ B /\ X = U. x ) <-> ( ( B \ F ) C_ B /\ X = U. ( B \ F ) ) ) )
112 111 anbi2d 
 |-  ( x = ( B \ F ) -> ( ( ph /\ ( x C_ B /\ X = U. x ) ) <-> ( ph /\ ( ( B \ F ) C_ B /\ X = U. ( B \ F ) ) ) ) )
113 pweq 
 |-  ( x = ( B \ F ) -> ~P x = ~P ( B \ F ) )
114 113 ineq1d 
 |-  ( x = ( B \ F ) -> ( ~P x i^i Fin ) = ( ~P ( B \ F ) i^i Fin ) )
115 114 rexeqdv 
 |-  ( 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 ) )
116 112 115 imbi12d 
 |-  ( 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 ) ) )
117 116 4 vtoclg 
 |-  ( ( 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 ) )
118 107 117 mpcom 
 |-  ( ( ph /\ ( ( B \ F ) C_ B /\ X = U. ( B \ F ) ) ) -> E. y e. ( ~P ( B \ F ) i^i Fin ) X = U. y )
119 104 118 mpdan 
 |-  ( ph -> E. y e. ( ~P ( B \ F ) i^i Fin ) X = U. y )
120 unieq 
 |-  ( y = (/) -> U. y = U. (/) )
121 uni0 
 |-  U. (/) = (/)
122 120 121 eqtrdi 
 |-  ( y = (/) -> U. y = (/) )
123 122 neeq2d 
 |-  ( y = (/) -> ( X =/= U. y <-> X =/= (/) ) )
124 difssd 
 |-  ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) -> ( X \ z ) C_ X )
125 124 ralrimivw 
 |-  ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) -> A. z e. y ( X \ z ) C_ X )
126 riinn0 
 |-  ( ( A. z e. y ( X \ z ) C_ X /\ y =/= (/) ) -> ( X i^i |^|_ z e. y ( X \ z ) ) = |^|_ z e. y ( X \ z ) )
127 125 126 sylan 
 |-  ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> ( X i^i |^|_ z e. y ( X \ z ) ) = |^|_ z e. y ( X \ z ) )
128 17 ad2antrr 
 |-  ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> X e. _V )
129 difexg 
 |-  ( X e. _V -> ( X \ z ) e. _V )
130 128 129 syl 
 |-  ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> ( X \ z ) e. _V )
131 130 ralrimivw 
 |-  ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> A. z e. y ( X \ z ) e. _V )
132 dfiin2g 
 |-  ( A. z e. y ( X \ z ) e. _V -> |^|_ z e. y ( X \ z ) = |^| { x | E. z e. y x = ( X \ z ) } )
133 131 132 syl 
 |-  ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> |^|_ z e. y ( X \ z ) = |^| { x | E. z e. y x = ( X \ z ) } )
134 eqid 
 |-  ( z e. y |-> ( X \ z ) ) = ( z e. y |-> ( X \ z ) )
135 134 rnmpt 
 |-  ran ( z e. y |-> ( X \ z ) ) = { x | E. z e. y x = ( X \ z ) }
136 135 inteqi 
 |-  |^| ran ( z e. y |-> ( X \ z ) ) = |^| { x | E. z e. y x = ( X \ z ) }
137 133 136 eqtr4di 
 |-  ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> |^|_ z e. y ( X \ z ) = |^| ran ( z e. y |-> ( X \ z ) ) )
138 127 137 eqtrd 
 |-  ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> ( X i^i |^|_ z e. y ( X \ z ) ) = |^| ran ( z e. y |-> ( X \ z ) ) )
139 15 ad2antrr 
 |-  ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> F e. ( Fil ` X ) )
140 elfpw 
 |-  ( y e. ( ~P ( B \ F ) i^i Fin ) <-> ( y C_ ( B \ F ) /\ y e. Fin ) )
141 140 simplbi 
 |-  ( y e. ( ~P ( B \ F ) i^i Fin ) -> y C_ ( B \ F ) )
142 141 ad2antlr 
 |-  ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> y C_ ( B \ F ) )
143 142 sselda 
 |-  ( ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) /\ z e. y ) -> z e. ( B \ F ) )
144 143 eldifbd 
 |-  ( ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) /\ z e. y ) -> -. z e. F )
145 5 ad3antrrr 
 |-  ( ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) /\ z e. y ) -> F e. ( UFil ` X ) )
146 142 difss2d 
 |-  ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> y C_ B )
147 146 sselda 
 |-  ( ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) /\ z e. y ) -> z e. B )
148 elssuni 
 |-  ( z e. B -> z C_ U. B )
149 147 148 syl 
 |-  ( ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) /\ z e. y ) -> z C_ U. B )
150 2 ad3antrrr 
 |-  ( ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) /\ z e. y ) -> X = U. B )
151 149 150 sseqtrrd 
 |-  ( ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) /\ z e. y ) -> z C_ X )
152 ufilb 
 |-  ( ( F e. ( UFil ` X ) /\ z C_ X ) -> ( -. z e. F <-> ( X \ z ) e. F ) )
153 145 151 152 syl2anc 
 |-  ( ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) /\ z e. y ) -> ( -. z e. F <-> ( X \ z ) e. F ) )
154 144 153 mpbid 
 |-  ( ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) /\ z e. y ) -> ( X \ z ) e. F )
155 154 fmpttd 
 |-  ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> ( z e. y |-> ( X \ z ) ) : y --> F )
156 155 frnd 
 |-  ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> ran ( z e. y |-> ( X \ z ) ) C_ F )
157 134 154 dmmptd 
 |-  ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> dom ( z e. y |-> ( X \ z ) ) = y )
158 simpr 
 |-  ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> y =/= (/) )
159 157 158 eqnetrd 
 |-  ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> dom ( z e. y |-> ( X \ z ) ) =/= (/) )
160 dm0rn0 
 |-  ( dom ( z e. y |-> ( X \ z ) ) = (/) <-> ran ( z e. y |-> ( X \ z ) ) = (/) )
161 160 necon3bii 
 |-  ( dom ( z e. y |-> ( X \ z ) ) =/= (/) <-> ran ( z e. y |-> ( X \ z ) ) =/= (/) )
162 159 161 sylib 
 |-  ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> ran ( z e. y |-> ( X \ z ) ) =/= (/) )
163 elinel2 
 |-  ( y e. ( ~P ( B \ F ) i^i Fin ) -> y e. Fin )
164 163 ad2antlr 
 |-  ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> y e. Fin )
165 abrexfi 
 |-  ( y e. Fin -> { x | E. z e. y x = ( X \ z ) } e. Fin )
166 135 165 eqeltrid 
 |-  ( y e. Fin -> ran ( z e. y |-> ( X \ z ) ) e. Fin )
167 164 166 syl 
 |-  ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> ran ( z e. y |-> ( X \ z ) ) e. Fin )
168 filintn0 
 |-  ( ( 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 139 156 162 167 168 syl13anc 
 |-  ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> |^| ran ( z e. y |-> ( X \ z ) ) =/= (/) )
170 138 169 eqnetrd 
 |-  ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> ( X i^i |^|_ z e. y ( X \ z ) ) =/= (/) )
171 disj3 
 |-  ( ( X i^i |^|_ z e. y ( X \ z ) ) = (/) <-> X = ( X \ |^|_ z e. y ( X \ z ) ) )
172 171 necon3bii 
 |-  ( ( X i^i |^|_ z e. y ( X \ z ) ) =/= (/) <-> X =/= ( X \ |^|_ z e. y ( X \ z ) ) )
173 170 172 sylib 
 |-  ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> X =/= ( X \ |^|_ z e. y ( X \ z ) ) )
174 iundif2 
 |-  U_ z e. y ( X \ ( X \ z ) ) = ( X \ |^|_ z e. y ( X \ z ) )
175 dfss4 
 |-  ( z C_ X <-> ( X \ ( X \ z ) ) = z )
176 151 175 sylib 
 |-  ( ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) /\ z e. y ) -> ( X \ ( X \ z ) ) = z )
177 176 iuneq2dv 
 |-  ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> U_ z e. y ( X \ ( X \ z ) ) = U_ z e. y z )
178 uniiun 
 |-  U. y = U_ z e. y z
179 177 178 eqtr4di 
 |-  ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> U_ z e. y ( X \ ( X \ z ) ) = U. y )
180 174 179 eqtr3id 
 |-  ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> ( X \ |^|_ z e. y ( X \ z ) ) = U. y )
181 173 180 neeqtrd 
 |-  ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> X =/= U. y )
182 15 adantr 
 |-  ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) -> F e. ( Fil ` X ) )
183 filtop 
 |-  ( F e. ( Fil ` X ) -> X e. F )
184 fileln0 
 |-  ( ( F e. ( Fil ` X ) /\ X e. F ) -> X =/= (/) )
185 182 183 184 syl2anc2 
 |-  ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) -> X =/= (/) )
186 123 181 185 pm2.61ne 
 |-  ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) -> X =/= U. y )
187 186 neneqd 
 |-  ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) -> -. X = U. y )
188 187 nrexdv 
 |-  ( ph -> -. E. y e. ( ~P ( B \ F ) i^i Fin ) X = U. y )
189 119 188 pm2.65i 
 |-  -. ph