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 20 difexd 
 |-  ( ph -> ( B \ F ) e. _V )
106 105 adantr 
 |-  ( ( ph /\ ( ( B \ F ) C_ B /\ X = U. ( B \ F ) ) ) -> ( B \ F ) e. _V )
107 sseq1 
 |-  ( x = ( B \ F ) -> ( x C_ B <-> ( B \ F ) C_ B ) )
108 unieq 
 |-  ( x = ( B \ F ) -> U. x = U. ( B \ F ) )
109 108 eqeq2d 
 |-  ( x = ( B \ F ) -> ( X = U. x <-> X = U. ( B \ F ) ) )
110 107 109 anbi12d 
 |-  ( x = ( B \ F ) -> ( ( x C_ B /\ X = U. x ) <-> ( ( B \ F ) C_ B /\ X = U. ( B \ F ) ) ) )
111 110 anbi2d 
 |-  ( x = ( B \ F ) -> ( ( ph /\ ( x C_ B /\ X = U. x ) ) <-> ( ph /\ ( ( B \ F ) C_ B /\ X = U. ( B \ F ) ) ) ) )
112 pweq 
 |-  ( x = ( B \ F ) -> ~P x = ~P ( B \ F ) )
113 112 ineq1d 
 |-  ( x = ( B \ F ) -> ( ~P x i^i Fin ) = ( ~P ( B \ F ) i^i Fin ) )
114 113 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 ) )
115 111 114 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 ) ) )
116 115 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 ) )
117 106 116 mpcom 
 |-  ( ( ph /\ ( ( B \ F ) C_ B /\ X = U. ( B \ F ) ) ) -> E. y e. ( ~P ( B \ F ) i^i Fin ) X = U. y )
118 104 117 mpdan 
 |-  ( ph -> E. y e. ( ~P ( B \ F ) i^i Fin ) X = U. y )
119 unieq 
 |-  ( y = (/) -> U. y = U. (/) )
120 uni0 
 |-  U. (/) = (/)
121 119 120 eqtrdi 
 |-  ( y = (/) -> U. y = (/) )
122 121 neeq2d 
 |-  ( y = (/) -> ( X =/= U. y <-> X =/= (/) ) )
123 difssd 
 |-  ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) -> ( X \ z ) C_ X )
124 123 ralrimivw 
 |-  ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) -> A. z e. y ( X \ z ) C_ X )
125 riinn0 
 |-  ( ( 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 
 |-  ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> ( X i^i |^|_ z e. y ( X \ z ) ) = |^|_ z e. y ( X \ z ) )
127 17 ad2antrr 
 |-  ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> X e. _V )
128 127 difexd 
 |-  ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> ( X \ z ) e. _V )
129 128 ralrimivw 
 |-  ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> A. z e. y ( X \ z ) e. _V )
130 dfiin2g 
 |-  ( A. z e. y ( X \ z ) e. _V -> |^|_ z e. y ( X \ z ) = |^| { x | E. z e. y x = ( X \ z ) } )
131 129 130 syl 
 |-  ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> |^|_ z e. y ( X \ z ) = |^| { x | E. z e. y x = ( X \ z ) } )
132 eqid 
 |-  ( z e. y |-> ( X \ z ) ) = ( z e. y |-> ( X \ z ) )
133 132 rnmpt 
 |-  ran ( z e. y |-> ( X \ z ) ) = { x | E. z e. y x = ( X \ z ) }
134 133 inteqi 
 |-  |^| ran ( z e. y |-> ( X \ z ) ) = |^| { x | E. z e. y x = ( X \ z ) }
135 131 134 eqtr4di 
 |-  ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> |^|_ z e. y ( X \ z ) = |^| ran ( z e. y |-> ( X \ z ) ) )
136 126 135 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 ) ) )
137 15 ad2antrr 
 |-  ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> F e. ( Fil ` X ) )
138 elfpw 
 |-  ( y e. ( ~P ( B \ F ) i^i Fin ) <-> ( y C_ ( B \ F ) /\ y e. Fin ) )
139 138 simplbi 
 |-  ( y e. ( ~P ( B \ F ) i^i Fin ) -> y C_ ( B \ F ) )
140 139 ad2antlr 
 |-  ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> y C_ ( B \ F ) )
141 140 sselda 
 |-  ( ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) /\ z e. y ) -> z e. ( B \ F ) )
142 141 eldifbd 
 |-  ( ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) /\ z e. y ) -> -. z e. F )
143 5 ad3antrrr 
 |-  ( ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) /\ z e. y ) -> F e. ( UFil ` X ) )
144 140 difss2d 
 |-  ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> y C_ B )
145 144 sselda 
 |-  ( ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) /\ z e. y ) -> z e. B )
146 elssuni 
 |-  ( z e. B -> z C_ U. B )
147 145 146 syl 
 |-  ( ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) /\ z e. y ) -> z C_ U. B )
148 2 ad3antrrr 
 |-  ( ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) /\ z e. y ) -> X = U. B )
149 147 148 sseqtrrd 
 |-  ( ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) /\ z e. y ) -> z C_ X )
150 ufilb 
 |-  ( ( F e. ( UFil ` X ) /\ z C_ X ) -> ( -. z e. F <-> ( X \ z ) e. F ) )
151 143 149 150 syl2anc 
 |-  ( ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) /\ z e. y ) -> ( -. z e. F <-> ( X \ z ) e. F ) )
152 142 151 mpbid 
 |-  ( ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) /\ z e. y ) -> ( X \ z ) e. F )
153 152 fmpttd 
 |-  ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> ( z e. y |-> ( X \ z ) ) : y --> F )
154 153 frnd 
 |-  ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> ran ( z e. y |-> ( X \ z ) ) C_ F )
155 132 152 dmmptd 
 |-  ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> dom ( z e. y |-> ( X \ z ) ) = y )
156 simpr 
 |-  ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> y =/= (/) )
157 155 156 eqnetrd 
 |-  ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> dom ( z e. y |-> ( X \ z ) ) =/= (/) )
158 dm0rn0 
 |-  ( dom ( z e. y |-> ( X \ z ) ) = (/) <-> ran ( z e. y |-> ( X \ z ) ) = (/) )
159 158 necon3bii 
 |-  ( dom ( z e. y |-> ( X \ z ) ) =/= (/) <-> ran ( z e. y |-> ( X \ z ) ) =/= (/) )
160 157 159 sylib 
 |-  ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> ran ( z e. y |-> ( X \ z ) ) =/= (/) )
161 elinel2 
 |-  ( y e. ( ~P ( B \ F ) i^i Fin ) -> y e. Fin )
162 161 ad2antlr 
 |-  ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> y e. Fin )
163 abrexfi 
 |-  ( y e. Fin -> { x | E. z e. y x = ( X \ z ) } e. Fin )
164 133 163 eqeltrid 
 |-  ( y e. Fin -> ran ( z e. y |-> ( X \ z ) ) e. Fin )
165 162 164 syl 
 |-  ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> ran ( z e. y |-> ( X \ z ) ) e. Fin )
166 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 ) ) =/= (/) )
167 137 154 160 165 166 syl13anc 
 |-  ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> |^| ran ( z e. y |-> ( X \ z ) ) =/= (/) )
168 136 167 eqnetrd 
 |-  ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> ( X i^i |^|_ z e. y ( X \ z ) ) =/= (/) )
169 disj3 
 |-  ( ( X i^i |^|_ z e. y ( X \ z ) ) = (/) <-> X = ( X \ |^|_ z e. y ( X \ z ) ) )
170 169 necon3bii 
 |-  ( ( X i^i |^|_ z e. y ( X \ z ) ) =/= (/) <-> X =/= ( X \ |^|_ z e. y ( X \ z ) ) )
171 168 170 sylib 
 |-  ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> X =/= ( X \ |^|_ z e. y ( X \ z ) ) )
172 iundif2 
 |-  U_ z e. y ( X \ ( X \ z ) ) = ( X \ |^|_ z e. y ( X \ z ) )
173 dfss4 
 |-  ( z C_ X <-> ( X \ ( X \ z ) ) = z )
174 149 173 sylib 
 |-  ( ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) /\ z e. y ) -> ( X \ ( X \ z ) ) = z )
175 174 iuneq2dv 
 |-  ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> U_ z e. y ( X \ ( X \ z ) ) = U_ z e. y z )
176 uniiun 
 |-  U. y = U_ z e. y z
177 175 176 eqtr4di 
 |-  ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> U_ z e. y ( X \ ( X \ z ) ) = U. y )
178 172 177 eqtr3id 
 |-  ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> ( X \ |^|_ z e. y ( X \ z ) ) = U. y )
179 171 178 neeqtrd 
 |-  ( ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) /\ y =/= (/) ) -> X =/= U. y )
180 15 adantr 
 |-  ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) -> F e. ( Fil ` X ) )
181 filtop 
 |-  ( F e. ( Fil ` X ) -> X e. F )
182 fileln0 
 |-  ( ( F e. ( Fil ` X ) /\ X e. F ) -> X =/= (/) )
183 180 181 182 syl2anc2 
 |-  ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) -> X =/= (/) )
184 122 179 183 pm2.61ne 
 |-  ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) -> X =/= U. y )
185 184 neneqd 
 |-  ( ( ph /\ y e. ( ~P ( B \ F ) i^i Fin ) ) -> -. X = U. y )
186 185 nrexdv 
 |-  ( ph -> -. E. y e. ( ~P ( B \ F ) i^i Fin ) X = U. y )
187 118 186 pm2.65i 
 |-  -. ph