Metamath Proof Explorer

Theorem hauscmplem

Description: Lemma for hauscmp . (Contributed by Mario Carneiro, 27-Nov-2013)

Ref Expression
Hypotheses hauscmp.1 
|- X = U. J
hauscmplem.2 
|- O = { y e. J | E. w e. J ( A e. w /\ ( ( cls ` J ) ` w ) C_ ( X \ y ) ) }
hauscmplem.3 
|- ( ph -> J e. Haus )
hauscmplem.4 
|- ( ph -> S C_ X )
hauscmplem.5 
|- ( ph -> ( J |`t S ) e. Comp )
hauscmplem.6 
|- ( ph -> A e. ( X \ S ) )
Assertion hauscmplem 
|- ( ph -> E. z e. J ( A e. z /\ ( ( cls ` J ) ` z ) C_ ( X \ S ) ) )

Proof

Step Hyp Ref Expression
1 hauscmp.1 
 |-  X = U. J
2 hauscmplem.2 
 |-  O = { y e. J | E. w e. J ( A e. w /\ ( ( cls ` J ) ` w ) C_ ( X \ y ) ) }
3 hauscmplem.3 
 |-  ( ph -> J e. Haus )
4 hauscmplem.4 
 |-  ( ph -> S C_ X )
5 hauscmplem.5 
 |-  ( ph -> ( J |`t S ) e. Comp )
6 hauscmplem.6 
 |-  ( ph -> A e. ( X \ S ) )
7 haustop 
 |-  ( J e. Haus -> J e. Top )
8 3 7 syl 
 |-  ( ph -> J e. Top )
9 8 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ S C_ U. x ) /\ x = (/) ) -> J e. Top )
10 1 topopn 
 |-  ( J e. Top -> X e. J )
11 9 10 syl 
 |-  ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ S C_ U. x ) /\ x = (/) ) -> X e. J )
12 6 eldifad 
 |-  ( ph -> A e. X )
13 12 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ S C_ U. x ) /\ x = (/) ) -> A e. X )
14 1 clstop 
 |-  ( J e. Top -> ( ( cls ` J ) ` X ) = X )
15 9 14 syl 
 |-  ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ S C_ U. x ) /\ x = (/) ) -> ( ( cls ` J ) ` X ) = X )
16 simplr 
 |-  ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ S C_ U. x ) /\ x = (/) ) -> S C_ U. x )
17 unieq 
 |-  ( x = (/) -> U. x = U. (/) )
18 uni0 
 |-  U. (/) = (/)
19 17 18 eqtrdi 
 |-  ( x = (/) -> U. x = (/) )
20 19 adantl 
 |-  ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ S C_ U. x ) /\ x = (/) ) -> U. x = (/) )
21 16 20 sseqtrd 
 |-  ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ S C_ U. x ) /\ x = (/) ) -> S C_ (/) )
22 ss0 
 |-  ( S C_ (/) -> S = (/) )
23 21 22 syl 
 |-  ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ S C_ U. x ) /\ x = (/) ) -> S = (/) )
24 23 difeq2d 
 |-  ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ S C_ U. x ) /\ x = (/) ) -> ( X \ S ) = ( X \ (/) ) )
25 dif0 
 |-  ( X \ (/) ) = X
26 24 25 eqtrdi 
 |-  ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ S C_ U. x ) /\ x = (/) ) -> ( X \ S ) = X )
27 15 26 eqtr4d 
 |-  ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ S C_ U. x ) /\ x = (/) ) -> ( ( cls ` J ) ` X ) = ( X \ S ) )
28 eqimss 
 |-  ( ( ( cls ` J ) ` X ) = ( X \ S ) -> ( ( cls ` J ) ` X ) C_ ( X \ S ) )
29 27 28 syl 
 |-  ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ S C_ U. x ) /\ x = (/) ) -> ( ( cls ` J ) ` X ) C_ ( X \ S ) )
30 eleq2 
 |-  ( z = X -> ( A e. z <-> A e. X ) )
31 fveq2 
 |-  ( z = X -> ( ( cls ` J ) ` z ) = ( ( cls ` J ) ` X ) )
32 31 sseq1d 
 |-  ( z = X -> ( ( ( cls ` J ) ` z ) C_ ( X \ S ) <-> ( ( cls ` J ) ` X ) C_ ( X \ S ) ) )
33 30 32 anbi12d 
 |-  ( z = X -> ( ( A e. z /\ ( ( cls ` J ) ` z ) C_ ( X \ S ) ) <-> ( A e. X /\ ( ( cls ` J ) ` X ) C_ ( X \ S ) ) ) )
34 33 rspcev 
 |-  ( ( X e. J /\ ( A e. X /\ ( ( cls ` J ) ` X ) C_ ( X \ S ) ) ) -> E. z e. J ( A e. z /\ ( ( cls ` J ) ` z ) C_ ( X \ S ) ) )
35 11 13 29 34 syl12anc 
 |-  ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ S C_ U. x ) /\ x = (/) ) -> E. z e. J ( A e. z /\ ( ( cls ` J ) ` z ) C_ ( X \ S ) ) )
36 elin 
 |-  ( x e. ( ~P O i^i Fin ) <-> ( x e. ~P O /\ x e. Fin ) )
37 id 
 |-  ( x e. Fin -> x e. Fin )
38 elpwi 
 |-  ( x e. ~P O -> x C_ O )
39 38 sseld 
 |-  ( x e. ~P O -> ( z e. x -> z e. O ) )
40 difeq2 
 |-  ( y = z -> ( X \ y ) = ( X \ z ) )
41 40 sseq2d 
 |-  ( y = z -> ( ( ( cls ` J ) ` w ) C_ ( X \ y ) <-> ( ( cls ` J ) ` w ) C_ ( X \ z ) ) )
42 41 anbi2d 
 |-  ( y = z -> ( ( A e. w /\ ( ( cls ` J ) ` w ) C_ ( X \ y ) ) <-> ( A e. w /\ ( ( cls ` J ) ` w ) C_ ( X \ z ) ) ) )
43 42 rexbidv 
 |-  ( y = z -> ( E. w e. J ( A e. w /\ ( ( cls ` J ) ` w ) C_ ( X \ y ) ) <-> E. w e. J ( A e. w /\ ( ( cls ` J ) ` w ) C_ ( X \ z ) ) ) )
44 43 2 elrab2 
 |-  ( z e. O <-> ( z e. J /\ E. w e. J ( A e. w /\ ( ( cls ` J ) ` w ) C_ ( X \ z ) ) ) )
45 44 simprbi 
 |-  ( z e. O -> E. w e. J ( A e. w /\ ( ( cls ` J ) ` w ) C_ ( X \ z ) ) )
46 39 45 syl6 
 |-  ( x e. ~P O -> ( z e. x -> E. w e. J ( A e. w /\ ( ( cls ` J ) ` w ) C_ ( X \ z ) ) ) )
47 46 ralrimiv 
 |-  ( x e. ~P O -> A. z e. x E. w e. J ( A e. w /\ ( ( cls ` J ) ` w ) C_ ( X \ z ) ) )
48 eleq2 
 |-  ( w = ( f ` z ) -> ( A e. w <-> A e. ( f ` z ) ) )
49 fveq2 
 |-  ( w = ( f ` z ) -> ( ( cls ` J ) ` w ) = ( ( cls ` J ) ` ( f ` z ) ) )
50 49 sseq1d 
 |-  ( w = ( f ` z ) -> ( ( ( cls ` J ) ` w ) C_ ( X \ z ) <-> ( ( cls ` J ) ` ( f ` z ) ) C_ ( X \ z ) ) )
51 48 50 anbi12d 
 |-  ( w = ( f ` z ) -> ( ( A e. w /\ ( ( cls ` J ) ` w ) C_ ( X \ z ) ) <-> ( A e. ( f ` z ) /\ ( ( cls ` J ) ` ( f ` z ) ) C_ ( X \ z ) ) ) )
52 51 ac6sfi 
 |-  ( ( x e. Fin /\ A. z e. x E. w e. J ( A e. w /\ ( ( cls ` J ) ` w ) C_ ( X \ z ) ) ) -> E. f ( f : x --> J /\ A. z e. x ( A e. ( f ` z ) /\ ( ( cls ` J ) ` ( f ` z ) ) C_ ( X \ z ) ) ) )
53 37 47 52 syl2anr 
 |-  ( ( x e. ~P O /\ x e. Fin ) -> E. f ( f : x --> J /\ A. z e. x ( A e. ( f ` z ) /\ ( ( cls ` J ) ` ( f ` z ) ) C_ ( X \ z ) ) ) )
54 36 53 sylbi 
 |-  ( x e. ( ~P O i^i Fin ) -> E. f ( f : x --> J /\ A. z e. x ( A e. ( f ` z ) /\ ( ( cls ` J ) ` ( f ` z ) ) C_ ( X \ z ) ) ) )
55 54 ad2antlr 
 |-  ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ ( S C_ U. x /\ x =/= (/) ) ) -> E. f ( f : x --> J /\ A. z e. x ( A e. ( f ` z ) /\ ( ( cls ` J ) ` ( f ` z ) ) C_ ( X \ z ) ) ) )
56 8 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ ( S C_ U. x /\ x =/= (/) ) ) /\ ( f : x --> J /\ A. z e. x ( A e. ( f ` z ) /\ ( ( cls ` J ) ` ( f ` z ) ) C_ ( X \ z ) ) ) ) -> J e. Top )
57 frn 
 |-  ( f : x --> J -> ran f C_ J )
58 57 ad2antrl 
 |-  ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ ( S C_ U. x /\ x =/= (/) ) ) /\ ( f : x --> J /\ A. z e. x ( A e. ( f ` z ) /\ ( ( cls ` J ) ` ( f ` z ) ) C_ ( X \ z ) ) ) ) -> ran f C_ J )
59 simprr 
 |-  ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ ( S C_ U. x /\ x =/= (/) ) ) -> x =/= (/) )
60 simpl 
 |-  ( ( f : x --> J /\ A. z e. x ( A e. ( f ` z ) /\ ( ( cls ` J ) ` ( f ` z ) ) C_ ( X \ z ) ) ) -> f : x --> J )
61 fdm 
 |-  ( f : x --> J -> dom f = x )
62 61 eqeq1d 
 |-  ( f : x --> J -> ( dom f = (/) <-> x = (/) ) )
63 dm0rn0 
 |-  ( dom f = (/) <-> ran f = (/) )
64 62 63 bitr3di 
 |-  ( f : x --> J -> ( x = (/) <-> ran f = (/) ) )
65 64 necon3bid 
 |-  ( f : x --> J -> ( x =/= (/) <-> ran f =/= (/) ) )
66 65 biimpac 
 |-  ( ( x =/= (/) /\ f : x --> J ) -> ran f =/= (/) )
67 59 60 66 syl2an 
 |-  ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ ( S C_ U. x /\ x =/= (/) ) ) /\ ( f : x --> J /\ A. z e. x ( A e. ( f ` z ) /\ ( ( cls ` J ) ` ( f ` z ) ) C_ ( X \ z ) ) ) ) -> ran f =/= (/) )
68 36 simprbi 
 |-  ( x e. ( ~P O i^i Fin ) -> x e. Fin )
69 68 ad2antlr 
 |-  ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ ( S C_ U. x /\ x =/= (/) ) ) -> x e. Fin )
70 ffn 
 |-  ( f : x --> J -> f Fn x )
71 dffn4 
 |-  ( f Fn x <-> f : x -onto-> ran f )
72 70 71 sylib 
 |-  ( f : x --> J -> f : x -onto-> ran f )
73 72 adantr 
 |-  ( ( f : x --> J /\ A. z e. x ( A e. ( f ` z ) /\ ( ( cls ` J ) ` ( f ` z ) ) C_ ( X \ z ) ) ) -> f : x -onto-> ran f )
74 fofi 
 |-  ( ( x e. Fin /\ f : x -onto-> ran f ) -> ran f e. Fin )
75 69 73 74 syl2an 
 |-  ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ ( S C_ U. x /\ x =/= (/) ) ) /\ ( f : x --> J /\ A. z e. x ( A e. ( f ` z ) /\ ( ( cls ` J ) ` ( f ` z ) ) C_ ( X \ z ) ) ) ) -> ran f e. Fin )
76 fiinopn 
 |-  ( J e. Top -> ( ( ran f C_ J /\ ran f =/= (/) /\ ran f e. Fin ) -> |^| ran f e. J ) )
77 76 imp 
 |-  ( ( J e. Top /\ ( ran f C_ J /\ ran f =/= (/) /\ ran f e. Fin ) ) -> |^| ran f e. J )
78 56 58 67 75 77 syl13anc 
 |-  ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ ( S C_ U. x /\ x =/= (/) ) ) /\ ( f : x --> J /\ A. z e. x ( A e. ( f ` z ) /\ ( ( cls ` J ) ` ( f ` z ) ) C_ ( X \ z ) ) ) ) -> |^| ran f e. J )
79 simpl 
 |-  ( ( A e. ( f ` z ) /\ ( ( cls ` J ) ` ( f ` z ) ) C_ ( X \ z ) ) -> A e. ( f ` z ) )
80 79 ralimi 
 |-  ( A. z e. x ( A e. ( f ` z ) /\ ( ( cls ` J ) ` ( f ` z ) ) C_ ( X \ z ) ) -> A. z e. x A e. ( f ` z ) )
81 80 ad2antll 
 |-  ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ ( S C_ U. x /\ x =/= (/) ) ) /\ ( f : x --> J /\ A. z e. x ( A e. ( f ` z ) /\ ( ( cls ` J ) ` ( f ` z ) ) C_ ( X \ z ) ) ) ) -> A. z e. x A e. ( f ` z ) )
82 6 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ ( S C_ U. x /\ x =/= (/) ) ) /\ ( f : x --> J /\ A. z e. x ( A e. ( f ` z ) /\ ( ( cls ` J ) ` ( f ` z ) ) C_ ( X \ z ) ) ) ) -> A e. ( X \ S ) )
83 eliin 
 |-  ( A e. ( X \ S ) -> ( A e. |^|_ z e. x ( f ` z ) <-> A. z e. x A e. ( f ` z ) ) )
84 82 83 syl 
 |-  ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ ( S C_ U. x /\ x =/= (/) ) ) /\ ( f : x --> J /\ A. z e. x ( A e. ( f ` z ) /\ ( ( cls ` J ) ` ( f ` z ) ) C_ ( X \ z ) ) ) ) -> ( A e. |^|_ z e. x ( f ` z ) <-> A. z e. x A e. ( f ` z ) ) )
85 81 84 mpbird 
 |-  ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ ( S C_ U. x /\ x =/= (/) ) ) /\ ( f : x --> J /\ A. z e. x ( A e. ( f ` z ) /\ ( ( cls ` J ) ` ( f ` z ) ) C_ ( X \ z ) ) ) ) -> A e. |^|_ z e. x ( f ` z ) )
86 70 ad2antrl 
 |-  ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ ( S C_ U. x /\ x =/= (/) ) ) /\ ( f : x --> J /\ A. z e. x ( A e. ( f ` z ) /\ ( ( cls ` J ) ` ( f ` z ) ) C_ ( X \ z ) ) ) ) -> f Fn x )
87 fnrnfv 
 |-  ( f Fn x -> ran f = { y | E. z e. x y = ( f ` z ) } )
88 87 inteqd 
 |-  ( f Fn x -> |^| ran f = |^| { y | E. z e. x y = ( f ` z ) } )
89 fvex 
 |-  ( f ` z ) e. _V
90 89 dfiin2 
 |-  |^|_ z e. x ( f ` z ) = |^| { y | E. z e. x y = ( f ` z ) }
91 88 90 eqtr4di 
 |-  ( f Fn x -> |^| ran f = |^|_ z e. x ( f ` z ) )
92 86 91 syl 
 |-  ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ ( S C_ U. x /\ x =/= (/) ) ) /\ ( f : x --> J /\ A. z e. x ( A e. ( f ` z ) /\ ( ( cls ` J ) ` ( f ` z ) ) C_ ( X \ z ) ) ) ) -> |^| ran f = |^|_ z e. x ( f ` z ) )
93 85 92 eleqtrrd 
 |-  ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ ( S C_ U. x /\ x =/= (/) ) ) /\ ( f : x --> J /\ A. z e. x ( A e. ( f ` z ) /\ ( ( cls ` J ) ` ( f ` z ) ) C_ ( X \ z ) ) ) ) -> A e. |^| ran f )
94 59 adantr 
 |-  ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ ( S C_ U. x /\ x =/= (/) ) ) /\ ( f : x --> J /\ A. z e. x ( A e. ( f ` z ) /\ ( ( cls ` J ) ` ( f ` z ) ) C_ ( X \ z ) ) ) ) -> x =/= (/) )
95 8 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ ( S C_ U. x /\ x =/= (/) ) ) /\ f : x --> J ) /\ z e. x ) -> J e. Top )
96 ffvelrn 
 |-  ( ( f : x --> J /\ z e. x ) -> ( f ` z ) e. J )
97 96 adantll 
 |-  ( ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ ( S C_ U. x /\ x =/= (/) ) ) /\ f : x --> J ) /\ z e. x ) -> ( f ` z ) e. J )
98 elssuni 
 |-  ( ( f ` z ) e. J -> ( f ` z ) C_ U. J )
99 97 98 syl 
 |-  ( ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ ( S C_ U. x /\ x =/= (/) ) ) /\ f : x --> J ) /\ z e. x ) -> ( f ` z ) C_ U. J )
100 99 1 sseqtrrdi 
 |-  ( ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ ( S C_ U. x /\ x =/= (/) ) ) /\ f : x --> J ) /\ z e. x ) -> ( f ` z ) C_ X )
101 1 clscld 
 |-  ( ( J e. Top /\ ( f ` z ) C_ X ) -> ( ( cls ` J ) ` ( f ` z ) ) e. ( Clsd ` J ) )
102 95 100 101 syl2anc 
 |-  ( ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ ( S C_ U. x /\ x =/= (/) ) ) /\ f : x --> J ) /\ z e. x ) -> ( ( cls ` J ) ` ( f ` z ) ) e. ( Clsd ` J ) )
103 102 ralrimiva 
 |-  ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ ( S C_ U. x /\ x =/= (/) ) ) /\ f : x --> J ) -> A. z e. x ( ( cls ` J ) ` ( f ` z ) ) e. ( Clsd ` J ) )
104 103 adantrr 
 |-  ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ ( S C_ U. x /\ x =/= (/) ) ) /\ ( f : x --> J /\ A. z e. x ( A e. ( f ` z ) /\ ( ( cls ` J ) ` ( f ` z ) ) C_ ( X \ z ) ) ) ) -> A. z e. x ( ( cls ` J ) ` ( f ` z ) ) e. ( Clsd ` J ) )
105 iincld 
 |-  ( ( x =/= (/) /\ A. z e. x ( ( cls ` J ) ` ( f ` z ) ) e. ( Clsd ` J ) ) -> |^|_ z e. x ( ( cls ` J ) ` ( f ` z ) ) e. ( Clsd ` J ) )
106 94 104 105 syl2anc 
 |-  ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ ( S C_ U. x /\ x =/= (/) ) ) /\ ( f : x --> J /\ A. z e. x ( A e. ( f ` z ) /\ ( ( cls ` J ) ` ( f ` z ) ) C_ ( X \ z ) ) ) ) -> |^|_ z e. x ( ( cls ` J ) ` ( f ` z ) ) e. ( Clsd ` J ) )
107 1 sscls 
 |-  ( ( J e. Top /\ ( f ` z ) C_ X ) -> ( f ` z ) C_ ( ( cls ` J ) ` ( f ` z ) ) )
108 95 100 107 syl2anc 
 |-  ( ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ ( S C_ U. x /\ x =/= (/) ) ) /\ f : x --> J ) /\ z e. x ) -> ( f ` z ) C_ ( ( cls ` J ) ` ( f ` z ) ) )
109 108 ralrimiva 
 |-  ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ ( S C_ U. x /\ x =/= (/) ) ) /\ f : x --> J ) -> A. z e. x ( f ` z ) C_ ( ( cls ` J ) ` ( f ` z ) ) )
110 ssel 
 |-  ( ( f ` z ) C_ ( ( cls ` J ) ` ( f ` z ) ) -> ( y e. ( f ` z ) -> y e. ( ( cls ` J ) ` ( f ` z ) ) ) )
111 110 ral2imi 
 |-  ( A. z e. x ( f ` z ) C_ ( ( cls ` J ) ` ( f ` z ) ) -> ( A. z e. x y e. ( f ` z ) -> A. z e. x y e. ( ( cls ` J ) ` ( f ` z ) ) ) )
112 eliin 
 |-  ( y e. _V -> ( y e. |^|_ z e. x ( f ` z ) <-> A. z e. x y e. ( f ` z ) ) )
113 112 elv 
 |-  ( y e. |^|_ z e. x ( f ` z ) <-> A. z e. x y e. ( f ` z ) )
114 eliin 
 |-  ( y e. _V -> ( y e. |^|_ z e. x ( ( cls ` J ) ` ( f ` z ) ) <-> A. z e. x y e. ( ( cls ` J ) ` ( f ` z ) ) ) )
115 114 elv 
 |-  ( y e. |^|_ z e. x ( ( cls ` J ) ` ( f ` z ) ) <-> A. z e. x y e. ( ( cls ` J ) ` ( f ` z ) ) )
116 111 113 115 3imtr4g 
 |-  ( A. z e. x ( f ` z ) C_ ( ( cls ` J ) ` ( f ` z ) ) -> ( y e. |^|_ z e. x ( f ` z ) -> y e. |^|_ z e. x ( ( cls ` J ) ` ( f ` z ) ) ) )
117 116 ssrdv 
 |-  ( A. z e. x ( f ` z ) C_ ( ( cls ` J ) ` ( f ` z ) ) -> |^|_ z e. x ( f ` z ) C_ |^|_ z e. x ( ( cls ` J ) ` ( f ` z ) ) )
118 109 117 syl 
 |-  ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ ( S C_ U. x /\ x =/= (/) ) ) /\ f : x --> J ) -> |^|_ z e. x ( f ` z ) C_ |^|_ z e. x ( ( cls ` J ) ` ( f ` z ) ) )
119 118 adantrr 
 |-  ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ ( S C_ U. x /\ x =/= (/) ) ) /\ ( f : x --> J /\ A. z e. x ( A e. ( f ` z ) /\ ( ( cls ` J ) ` ( f ` z ) ) C_ ( X \ z ) ) ) ) -> |^|_ z e. x ( f ` z ) C_ |^|_ z e. x ( ( cls ` J ) ` ( f ` z ) ) )
120 92 119 eqsstrd 
 |-  ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ ( S C_ U. x /\ x =/= (/) ) ) /\ ( f : x --> J /\ A. z e. x ( A e. ( f ` z ) /\ ( ( cls ` J ) ` ( f ` z ) ) C_ ( X \ z ) ) ) ) -> |^| ran f C_ |^|_ z e. x ( ( cls ` J ) ` ( f ` z ) ) )
121 1 clsss2 
 |-  ( ( |^|_ z e. x ( ( cls ` J ) ` ( f ` z ) ) e. ( Clsd ` J ) /\ |^| ran f C_ |^|_ z e. x ( ( cls ` J ) ` ( f ` z ) ) ) -> ( ( cls ` J ) ` |^| ran f ) C_ |^|_ z e. x ( ( cls ` J ) ` ( f ` z ) ) )
122 106 120 121 syl2anc 
 |-  ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ ( S C_ U. x /\ x =/= (/) ) ) /\ ( f : x --> J /\ A. z e. x ( A e. ( f ` z ) /\ ( ( cls ` J ) ` ( f ` z ) ) C_ ( X \ z ) ) ) ) -> ( ( cls ` J ) ` |^| ran f ) C_ |^|_ z e. x ( ( cls ` J ) ` ( f ` z ) ) )
123 ssel 
 |-  ( ( ( cls ` J ) ` ( f ` z ) ) C_ ( X \ z ) -> ( y e. ( ( cls ` J ) ` ( f ` z ) ) -> y e. ( X \ z ) ) )
124 123 adantl 
 |-  ( ( A e. ( f ` z ) /\ ( ( cls ` J ) ` ( f ` z ) ) C_ ( X \ z ) ) -> ( y e. ( ( cls ` J ) ` ( f ` z ) ) -> y e. ( X \ z ) ) )
125 124 ral2imi 
 |-  ( A. z e. x ( A e. ( f ` z ) /\ ( ( cls ` J ) ` ( f ` z ) ) C_ ( X \ z ) ) -> ( A. z e. x y e. ( ( cls ` J ) ` ( f ` z ) ) -> A. z e. x y e. ( X \ z ) ) )
126 eliin 
 |-  ( y e. _V -> ( y e. |^|_ z e. x ( X \ z ) <-> A. z e. x y e. ( X \ z ) ) )
127 126 elv 
 |-  ( y e. |^|_ z e. x ( X \ z ) <-> A. z e. x y e. ( X \ z ) )
128 125 115 127 3imtr4g 
 |-  ( A. z e. x ( A e. ( f ` z ) /\ ( ( cls ` J ) ` ( f ` z ) ) C_ ( X \ z ) ) -> ( y e. |^|_ z e. x ( ( cls ` J ) ` ( f ` z ) ) -> y e. |^|_ z e. x ( X \ z ) ) )
129 128 ssrdv 
 |-  ( A. z e. x ( A e. ( f ` z ) /\ ( ( cls ` J ) ` ( f ` z ) ) C_ ( X \ z ) ) -> |^|_ z e. x ( ( cls ` J ) ` ( f ` z ) ) C_ |^|_ z e. x ( X \ z ) )
130 129 ad2antll 
 |-  ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ ( S C_ U. x /\ x =/= (/) ) ) /\ ( f : x --> J /\ A. z e. x ( A e. ( f ` z ) /\ ( ( cls ` J ) ` ( f ` z ) ) C_ ( X \ z ) ) ) ) -> |^|_ z e. x ( ( cls ` J ) ` ( f ` z ) ) C_ |^|_ z e. x ( X \ z ) )
131 iindif2 
 |-  ( x =/= (/) -> |^|_ z e. x ( X \ z ) = ( X \ U_ z e. x z ) )
132 94 131 syl 
 |-  ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ ( S C_ U. x /\ x =/= (/) ) ) /\ ( f : x --> J /\ A. z e. x ( A e. ( f ` z ) /\ ( ( cls ` J ) ` ( f ` z ) ) C_ ( X \ z ) ) ) ) -> |^|_ z e. x ( X \ z ) = ( X \ U_ z e. x z ) )
133 simplrl 
 |-  ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ ( S C_ U. x /\ x =/= (/) ) ) /\ ( f : x --> J /\ A. z e. x ( A e. ( f ` z ) /\ ( ( cls ` J ) ` ( f ` z ) ) C_ ( X \ z ) ) ) ) -> S C_ U. x )
134 uniiun 
 |-  U. x = U_ z e. x z
135 134 sseq2i 
 |-  ( S C_ U. x <-> S C_ U_ z e. x z )
136 sscon 
 |-  ( S C_ U_ z e. x z -> ( X \ U_ z e. x z ) C_ ( X \ S ) )
137 135 136 sylbi 
 |-  ( S C_ U. x -> ( X \ U_ z e. x z ) C_ ( X \ S ) )
138 133 137 syl 
 |-  ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ ( S C_ U. x /\ x =/= (/) ) ) /\ ( f : x --> J /\ A. z e. x ( A e. ( f ` z ) /\ ( ( cls ` J ) ` ( f ` z ) ) C_ ( X \ z ) ) ) ) -> ( X \ U_ z e. x z ) C_ ( X \ S ) )
139 132 138 eqsstrd 
 |-  ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ ( S C_ U. x /\ x =/= (/) ) ) /\ ( f : x --> J /\ A. z e. x ( A e. ( f ` z ) /\ ( ( cls ` J ) ` ( f ` z ) ) C_ ( X \ z ) ) ) ) -> |^|_ z e. x ( X \ z ) C_ ( X \ S ) )
140 130 139 sstrd 
 |-  ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ ( S C_ U. x /\ x =/= (/) ) ) /\ ( f : x --> J /\ A. z e. x ( A e. ( f ` z ) /\ ( ( cls ` J ) ` ( f ` z ) ) C_ ( X \ z ) ) ) ) -> |^|_ z e. x ( ( cls ` J ) ` ( f ` z ) ) C_ ( X \ S ) )
141 122 140 sstrd 
 |-  ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ ( S C_ U. x /\ x =/= (/) ) ) /\ ( f : x --> J /\ A. z e. x ( A e. ( f ` z ) /\ ( ( cls ` J ) ` ( f ` z ) ) C_ ( X \ z ) ) ) ) -> ( ( cls ` J ) ` |^| ran f ) C_ ( X \ S ) )
142 eleq2 
 |-  ( z = |^| ran f -> ( A e. z <-> A e. |^| ran f ) )
143 fveq2 
 |-  ( z = |^| ran f -> ( ( cls ` J ) ` z ) = ( ( cls ` J ) ` |^| ran f ) )
144 143 sseq1d 
 |-  ( z = |^| ran f -> ( ( ( cls ` J ) ` z ) C_ ( X \ S ) <-> ( ( cls ` J ) ` |^| ran f ) C_ ( X \ S ) ) )
145 142 144 anbi12d 
 |-  ( z = |^| ran f -> ( ( A e. z /\ ( ( cls ` J ) ` z ) C_ ( X \ S ) ) <-> ( A e. |^| ran f /\ ( ( cls ` J ) ` |^| ran f ) C_ ( X \ S ) ) ) )
146 145 rspcev 
 |-  ( ( |^| ran f e. J /\ ( A e. |^| ran f /\ ( ( cls ` J ) ` |^| ran f ) C_ ( X \ S ) ) ) -> E. z e. J ( A e. z /\ ( ( cls ` J ) ` z ) C_ ( X \ S ) ) )
147 78 93 141 146 syl12anc 
 |-  ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ ( S C_ U. x /\ x =/= (/) ) ) /\ ( f : x --> J /\ A. z e. x ( A e. ( f ` z ) /\ ( ( cls ` J ) ` ( f ` z ) ) C_ ( X \ z ) ) ) ) -> E. z e. J ( A e. z /\ ( ( cls ` J ) ` z ) C_ ( X \ S ) ) )
148 55 147 exlimddv 
 |-  ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ ( S C_ U. x /\ x =/= (/) ) ) -> E. z e. J ( A e. z /\ ( ( cls ` J ) ` z ) C_ ( X \ S ) ) )
149 148 anassrs 
 |-  ( ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ S C_ U. x ) /\ x =/= (/) ) -> E. z e. J ( A e. z /\ ( ( cls ` J ) ` z ) C_ ( X \ S ) ) )
150 35 149 pm2.61dane 
 |-  ( ( ( ph /\ x e. ( ~P O i^i Fin ) ) /\ S C_ U. x ) -> E. z e. J ( A e. z /\ ( ( cls ` J ) ` z ) C_ ( X \ S ) ) )
151 3 adantr 
 |-  ( ( ph /\ x e. S ) -> J e. Haus )
152 4 sselda 
 |-  ( ( ph /\ x e. S ) -> x e. X )
153 12 adantr 
 |-  ( ( ph /\ x e. S ) -> A e. X )
154 id 
 |-  ( x e. S -> x e. S )
155 6 eldifbd 
 |-  ( ph -> -. A e. S )
156 nelne2 
 |-  ( ( x e. S /\ -. A e. S ) -> x =/= A )
157 154 155 156 syl2anr 
 |-  ( ( ph /\ x e. S ) -> x =/= A )
158 1 hausnei 
 |-  ( ( J e. Haus /\ ( x e. X /\ A e. X /\ x =/= A ) ) -> E. y e. J E. w e. J ( x e. y /\ A e. w /\ ( y i^i w ) = (/) ) )
159 151 152 153 157 158 syl13anc 
 |-  ( ( ph /\ x e. S ) -> E. y e. J E. w e. J ( x e. y /\ A e. w /\ ( y i^i w ) = (/) ) )
160 3anass 
 |-  ( ( x e. y /\ A e. w /\ ( y i^i w ) = (/) ) <-> ( x e. y /\ ( A e. w /\ ( y i^i w ) = (/) ) ) )
161 elssuni 
 |-  ( w e. J -> w C_ U. J )
162 161 1 sseqtrrdi 
 |-  ( w e. J -> w C_ X )
163 162 adantl 
 |-  ( ( ( ( ph /\ x e. S ) /\ y e. J ) /\ w e. J ) -> w C_ X )
164 incom 
 |-  ( y i^i w ) = ( w i^i y )
165 164 eqeq1i 
 |-  ( ( y i^i w ) = (/) <-> ( w i^i y ) = (/) )
166 reldisj 
 |-  ( w C_ X -> ( ( w i^i y ) = (/) <-> w C_ ( X \ y ) ) )
167 165 166 syl5bb 
 |-  ( w C_ X -> ( ( y i^i w ) = (/) <-> w C_ ( X \ y ) ) )
168 163 167 syl 
 |-  ( ( ( ( ph /\ x e. S ) /\ y e. J ) /\ w e. J ) -> ( ( y i^i w ) = (/) <-> w C_ ( X \ y ) ) )
169 151 7 syl 
 |-  ( ( ph /\ x e. S ) -> J e. Top )
170 1 opncld 
 |-  ( ( J e. Top /\ y e. J ) -> ( X \ y ) e. ( Clsd ` J ) )
171 169 170 sylan 
 |-  ( ( ( ph /\ x e. S ) /\ y e. J ) -> ( X \ y ) e. ( Clsd ` J ) )
172 171 adantr 
 |-  ( ( ( ( ph /\ x e. S ) /\ y e. J ) /\ w e. J ) -> ( X \ y ) e. ( Clsd ` J ) )
173 1 clsss2 
 |-  ( ( ( X \ y ) e. ( Clsd ` J ) /\ w C_ ( X \ y ) ) -> ( ( cls ` J ) ` w ) C_ ( X \ y ) )
174 173 ex 
 |-  ( ( X \ y ) e. ( Clsd ` J ) -> ( w C_ ( X \ y ) -> ( ( cls ` J ) ` w ) C_ ( X \ y ) ) )
175 172 174 syl 
 |-  ( ( ( ( ph /\ x e. S ) /\ y e. J ) /\ w e. J ) -> ( w C_ ( X \ y ) -> ( ( cls ` J ) ` w ) C_ ( X \ y ) ) )
176 168 175 sylbid 
 |-  ( ( ( ( ph /\ x e. S ) /\ y e. J ) /\ w e. J ) -> ( ( y i^i w ) = (/) -> ( ( cls ` J ) ` w ) C_ ( X \ y ) ) )
177 176 anim2d 
 |-  ( ( ( ( ph /\ x e. S ) /\ y e. J ) /\ w e. J ) -> ( ( A e. w /\ ( y i^i w ) = (/) ) -> ( A e. w /\ ( ( cls ` J ) ` w ) C_ ( X \ y ) ) ) )
178 177 anim2d 
 |-  ( ( ( ( ph /\ x e. S ) /\ y e. J ) /\ w e. J ) -> ( ( x e. y /\ ( A e. w /\ ( y i^i w ) = (/) ) ) -> ( x e. y /\ ( A e. w /\ ( ( cls ` J ) ` w ) C_ ( X \ y ) ) ) ) )
179 160 178 syl5bi 
 |-  ( ( ( ( ph /\ x e. S ) /\ y e. J ) /\ w e. J ) -> ( ( x e. y /\ A e. w /\ ( y i^i w ) = (/) ) -> ( x e. y /\ ( A e. w /\ ( ( cls ` J ) ` w ) C_ ( X \ y ) ) ) ) )
180 179 reximdva 
 |-  ( ( ( ph /\ x e. S ) /\ y e. J ) -> ( E. w e. J ( x e. y /\ A e. w /\ ( y i^i w ) = (/) ) -> E. w e. J ( x e. y /\ ( A e. w /\ ( ( cls ` J ) ` w ) C_ ( X \ y ) ) ) ) )
181 r19.42v 
 |-  ( E. w e. J ( x e. y /\ ( A e. w /\ ( ( cls ` J ) ` w ) C_ ( X \ y ) ) ) <-> ( x e. y /\ E. w e. J ( A e. w /\ ( ( cls ` J ) ` w ) C_ ( X \ y ) ) ) )
182 180 181 syl6ib 
 |-  ( ( ( ph /\ x e. S ) /\ y e. J ) -> ( E. w e. J ( x e. y /\ A e. w /\ ( y i^i w ) = (/) ) -> ( x e. y /\ E. w e. J ( A e. w /\ ( ( cls ` J ) ` w ) C_ ( X \ y ) ) ) ) )
183 182 reximdva 
 |-  ( ( ph /\ x e. S ) -> ( E. y e. J E. w e. J ( x e. y /\ A e. w /\ ( y i^i w ) = (/) ) -> E. y e. J ( x e. y /\ E. w e. J ( A e. w /\ ( ( cls ` J ) ` w ) C_ ( X \ y ) ) ) ) )
184 159 183 mpd 
 |-  ( ( ph /\ x e. S ) -> E. y e. J ( x e. y /\ E. w e. J ( A e. w /\ ( ( cls ` J ) ` w ) C_ ( X \ y ) ) ) )
185 2 unieqi 
 |-  U. O = U. { y e. J | E. w e. J ( A e. w /\ ( ( cls ` J ) ` w ) C_ ( X \ y ) ) }
186 185 eleq2i 
 |-  ( x e. U. O <-> x e. U. { y e. J | E. w e. J ( A e. w /\ ( ( cls ` J ) ` w ) C_ ( X \ y ) ) } )
187 elunirab 
 |-  ( x e. U. { y e. J | E. w e. J ( A e. w /\ ( ( cls ` J ) ` w ) C_ ( X \ y ) ) } <-> E. y e. J ( x e. y /\ E. w e. J ( A e. w /\ ( ( cls ` J ) ` w ) C_ ( X \ y ) ) ) )
188 186 187 bitri 
 |-  ( x e. U. O <-> E. y e. J ( x e. y /\ E. w e. J ( A e. w /\ ( ( cls ` J ) ` w ) C_ ( X \ y ) ) ) )
189 184 188 sylibr 
 |-  ( ( ph /\ x e. S ) -> x e. U. O )
190 189 ex 
 |-  ( ph -> ( x e. S -> x e. U. O ) )
191 190 ssrdv 
 |-  ( ph -> S C_ U. O )
192 unieq 
 |-  ( z = O -> U. z = U. O )
193 192 sseq2d 
 |-  ( z = O -> ( S C_ U. z <-> S C_ U. O ) )
194 pweq 
 |-  ( z = O -> ~P z = ~P O )
195 194 ineq1d 
 |-  ( z = O -> ( ~P z i^i Fin ) = ( ~P O i^i Fin ) )
196 195 rexeqdv 
 |-  ( z = O -> ( E. x e. ( ~P z i^i Fin ) S C_ U. x <-> E. x e. ( ~P O i^i Fin ) S C_ U. x ) )
197 193 196 imbi12d 
 |-  ( z = O -> ( ( S C_ U. z -> E. x e. ( ~P z i^i Fin ) S C_ U. x ) <-> ( S C_ U. O -> E. x e. ( ~P O i^i Fin ) S C_ U. x ) ) )
198 1 cmpsub 
 |-  ( ( J e. Top /\ S C_ X ) -> ( ( J |`t S ) e. Comp <-> A. z e. ~P J ( S C_ U. z -> E. x e. ( ~P z i^i Fin ) S C_ U. x ) ) )
199 198 biimp3a 
 |-  ( ( J e. Top /\ S C_ X /\ ( J |`t S ) e. Comp ) -> A. z e. ~P J ( S C_ U. z -> E. x e. ( ~P z i^i Fin ) S C_ U. x ) )
200 8 4 5 199 syl3anc 
 |-  ( ph -> A. z e. ~P J ( S C_ U. z -> E. x e. ( ~P z i^i Fin ) S C_ U. x ) )
201 2 ssrab3 
 |-  O C_ J
202 elpw2g 
 |-  ( J e. Haus -> ( O e. ~P J <-> O C_ J ) )
203 3 202 syl 
 |-  ( ph -> ( O e. ~P J <-> O C_ J ) )
204 201 203 mpbiri 
 |-  ( ph -> O e. ~P J )
205 197 200 204 rspcdva 
 |-  ( ph -> ( S C_ U. O -> E. x e. ( ~P O i^i Fin ) S C_ U. x ) )
206 191 205 mpd 
 |-  ( ph -> E. x e. ( ~P O i^i Fin ) S C_ U. x )
207 150 206 r19.29a 
 |-  ( ph -> E. z e. J ( A e. z /\ ( ( cls ` J ) ` z ) C_ ( X \ S ) ) )