MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  hauscmplem Structured version   Unicode version

Theorem hauscmplem 20407
Description: Lemma for hauscmp 20408. (Contributed by Mario Carneiro, 27-Nov-2013.)
Hypotheses
Ref Expression
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  ->  ( Jt  S )  e.  Comp )
hauscmplem.6  |-  ( ph  ->  A  e.  ( X 
\  S ) )
Assertion
Ref Expression
hauscmplem  |-  ( ph  ->  E. z  e.  J  ( A  e.  z  /\  ( ( cls `  J
) `  z )  C_  ( X  \  S
) ) )
Distinct variable groups:    y, w, z, A    w, J, y, z    ph, w, y, z   
w, S, y, z   
z, O    w, X, y, z
Allowed substitution hints:    O( y, w)

Proof of Theorem hauscmplem
Dummy variables  f  x are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 hauscmplem.3 . . . . . . 7  |-  ( ph  ->  J  e.  Haus )
2 haustop 20333 . . . . . . 7  |-  ( J  e.  Haus  ->  J  e. 
Top )
31, 2syl 17 . . . . . 6  |-  ( ph  ->  J  e.  Top )
43ad3antrrr 734 . . . . 5  |-  ( ( ( ( ph  /\  x  e.  ( ~P O  i^i  Fin ) )  /\  S  C_  U. x
)  /\  x  =  (/) )  ->  J  e.  Top )
5 hauscmp.1 . . . . . 6  |-  X  = 
U. J
65topopn 19922 . . . . 5  |-  ( J  e.  Top  ->  X  e.  J )
74, 6syl 17 . . . 4  |-  ( ( ( ( ph  /\  x  e.  ( ~P O  i^i  Fin ) )  /\  S  C_  U. x
)  /\  x  =  (/) )  ->  X  e.  J )
8 hauscmplem.6 . . . . . 6  |-  ( ph  ->  A  e.  ( X 
\  S ) )
98eldifad 3448 . . . . 5  |-  ( ph  ->  A  e.  X )
109ad3antrrr 734 . . . 4  |-  ( ( ( ( ph  /\  x  e.  ( ~P O  i^i  Fin ) )  /\  S  C_  U. x
)  /\  x  =  (/) )  ->  A  e.  X )
115clstop 20071 . . . . . . 7  |-  ( J  e.  Top  ->  (
( cls `  J
) `  X )  =  X )
124, 11syl 17 . . . . . 6  |-  ( ( ( ( ph  /\  x  e.  ( ~P O  i^i  Fin ) )  /\  S  C_  U. x
)  /\  x  =  (/) )  ->  ( ( cls `  J ) `  X )  =  X )
13 simplr 760 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  x  e.  ( ~P O  i^i  Fin ) )  /\  S  C_  U. x
)  /\  x  =  (/) )  ->  S  C_  U. x
)
14 unieq 4224 . . . . . . . . . . . 12  |-  ( x  =  (/)  ->  U. x  =  U. (/) )
15 uni0 4243 . . . . . . . . . . . 12  |-  U. (/)  =  (/)
1614, 15syl6eq 2479 . . . . . . . . . . 11  |-  ( x  =  (/)  ->  U. x  =  (/) )
1716adantl 467 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  x  e.  ( ~P O  i^i  Fin ) )  /\  S  C_  U. x
)  /\  x  =  (/) )  ->  U. x  =  (/) )
1813, 17sseqtrd 3500 . . . . . . . . 9  |-  ( ( ( ( ph  /\  x  e.  ( ~P O  i^i  Fin ) )  /\  S  C_  U. x
)  /\  x  =  (/) )  ->  S  C_  (/) )
19 ss0 3793 . . . . . . . . 9  |-  ( S 
C_  (/)  ->  S  =  (/) )
2018, 19syl 17 . . . . . . . 8  |-  ( ( ( ( ph  /\  x  e.  ( ~P O  i^i  Fin ) )  /\  S  C_  U. x
)  /\  x  =  (/) )  ->  S  =  (/) )
2120difeq2d 3583 . . . . . . 7  |-  ( ( ( ( ph  /\  x  e.  ( ~P O  i^i  Fin ) )  /\  S  C_  U. x
)  /\  x  =  (/) )  ->  ( X  \  S )  =  ( X  \  (/) ) )
22 dif0 3865 . . . . . . 7  |-  ( X 
\  (/) )  =  X
2321, 22syl6eq 2479 . . . . . 6  |-  ( ( ( ( ph  /\  x  e.  ( ~P O  i^i  Fin ) )  /\  S  C_  U. x
)  /\  x  =  (/) )  ->  ( X  \  S )  =  X )
2412, 23eqtr4d 2466 . . . . 5  |-  ( ( ( ( ph  /\  x  e.  ( ~P O  i^i  Fin ) )  /\  S  C_  U. x
)  /\  x  =  (/) )  ->  ( ( cls `  J ) `  X )  =  ( X  \  S ) )
25 eqimss 3516 . . . . 5  |-  ( ( ( cls `  J
) `  X )  =  ( X  \  S )  ->  (
( cls `  J
) `  X )  C_  ( X  \  S
) )
2624, 25syl 17 . . . 4  |-  ( ( ( ( ph  /\  x  e.  ( ~P O  i^i  Fin ) )  /\  S  C_  U. x
)  /\  x  =  (/) )  ->  ( ( cls `  J ) `  X )  C_  ( X  \  S ) )
27 eleq2 2495 . . . . . 6  |-  ( z  =  X  ->  ( A  e.  z  <->  A  e.  X ) )
28 fveq2 5877 . . . . . . 7  |-  ( z  =  X  ->  (
( cls `  J
) `  z )  =  ( ( cls `  J ) `  X
) )
2928sseq1d 3491 . . . . . 6  |-  ( z  =  X  ->  (
( ( cls `  J
) `  z )  C_  ( X  \  S
)  <->  ( ( cls `  J ) `  X
)  C_  ( X  \  S ) ) )
3027, 29anbi12d 715 . . . . 5  |-  ( z  =  X  ->  (
( A  e.  z  /\  ( ( cls `  J ) `  z
)  C_  ( X  \  S ) )  <->  ( A  e.  X  /\  (
( cls `  J
) `  X )  C_  ( X  \  S
) ) ) )
3130rspcev 3182 . . . 4  |-  ( ( 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
) ) )
327, 10, 26, 31syl12anc 1262 . . 3  |-  ( ( ( ( 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
) ) )
33 elin 3649 . . . . . . 7  |-  ( x  e.  ( ~P O  i^i  Fin )  <->  ( x  e.  ~P O  /\  x  e.  Fin ) )
34 id 23 . . . . . . . 8  |-  ( x  e.  Fin  ->  x  e.  Fin )
35 elpwi 3988 . . . . . . . . . . 11  |-  ( x  e.  ~P O  ->  x  C_  O )
3635sseld 3463 . . . . . . . . . 10  |-  ( x  e.  ~P O  -> 
( z  e.  x  ->  z  e.  O ) )
37 difeq2 3577 . . . . . . . . . . . . . . 15  |-  ( y  =  z  ->  ( X  \  y )  =  ( X  \  z
) )
3837sseq2d 3492 . . . . . . . . . . . . . 14  |-  ( y  =  z  ->  (
( ( cls `  J
) `  w )  C_  ( X  \  y
)  <->  ( ( cls `  J ) `  w
)  C_  ( X  \  z ) ) )
3938anbi2d 708 . . . . . . . . . . . . 13  |-  ( y  =  z  ->  (
( A  e.  w  /\  ( ( cls `  J
) `  w )  C_  ( X  \  y
) )  <->  ( A  e.  w  /\  (
( cls `  J
) `  w )  C_  ( X  \  z
) ) ) )
4039rexbidv 2939 . . . . . . . . . . . 12  |-  ( 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
) ) ) )
41 hauscmplem.2 . . . . . . . . . . . 12  |-  O  =  { y  e.  J  |  E. w  e.  J  ( A  e.  w  /\  ( ( cls `  J
) `  w )  C_  ( X  \  y
) ) }
4240, 41elrab2 3231 . . . . . . . . . . 11  |-  ( z  e.  O  <->  ( z  e.  J  /\  E. w  e.  J  ( A  e.  w  /\  (
( cls `  J
) `  w )  C_  ( X  \  z
) ) ) )
4342simprbi 465 . . . . . . . . . 10  |-  ( z  e.  O  ->  E. w  e.  J  ( A  e.  w  /\  (
( cls `  J
) `  w )  C_  ( X  \  z
) ) )
4436, 43syl6 34 . . . . . . . . 9  |-  ( x  e.  ~P O  -> 
( z  e.  x  ->  E. w  e.  J  ( A  e.  w  /\  ( ( cls `  J
) `  w )  C_  ( X  \  z
) ) ) )
4544ralrimiv 2837 . . . . . . . 8  |-  ( x  e.  ~P O  ->  A. z  e.  x  E. w  e.  J  ( A  e.  w  /\  ( ( cls `  J
) `  w )  C_  ( X  \  z
) ) )
46 eleq2 2495 . . . . . . . . . 10  |-  ( w  =  ( f `  z )  ->  ( A  e.  w  <->  A  e.  ( f `  z
) ) )
47 fveq2 5877 . . . . . . . . . . 11  |-  ( w  =  ( f `  z )  ->  (
( cls `  J
) `  w )  =  ( ( cls `  J ) `  (
f `  z )
) )
4847sseq1d 3491 . . . . . . . . . 10  |-  ( w  =  ( f `  z )  ->  (
( ( cls `  J
) `  w )  C_  ( X  \  z
)  <->  ( ( cls `  J ) `  (
f `  z )
)  C_  ( X  \  z ) ) )
4946, 48anbi12d 715 . . . . . . . . 9  |-  ( w  =  ( f `  z )  ->  (
( A  e.  w  /\  ( ( cls `  J
) `  w )  C_  ( X  \  z
) )  <->  ( A  e.  ( f `  z
)  /\  ( ( cls `  J ) `  ( f `  z
) )  C_  ( X  \  z ) ) ) )
5049ac6sfi 7817 . . . . . . . 8  |-  ( ( 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
) ) ) )
5134, 45, 50syl2anr 480 . . . . . . 7  |-  ( ( 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
) ) ) )
5233, 51sylbi 198 . . . . . 6  |-  ( 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 ) ) ) )
5352ad2antlr 731 . . . . 5  |-  ( ( ( 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
) ) ) )
543ad3antrrr 734 . . . . . . 7  |-  ( ( ( ( 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 )
55 frn 5748 . . . . . . . 8  |-  ( f : x --> J  ->  ran  f  C_  J )
5655ad2antrl 732 . . . . . . 7  |-  ( ( ( ( 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 )
57 simprr 764 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  ( ~P O  i^i  Fin ) )  /\  ( S  C_  U. x  /\  x  =/=  (/) ) )  ->  x  =/=  (/) )
58 simpl 458 . . . . . . . 8  |-  ( ( f : x --> J  /\  A. z  e.  x  ( A  e.  ( f `
 z )  /\  ( ( cls `  J
) `  ( f `  z ) )  C_  ( X  \  z
) ) )  -> 
f : x --> J )
59 dm0rn0 5066 . . . . . . . . . . 11  |-  ( dom  f  =  (/)  <->  ran  f  =  (/) )
60 fdm 5746 . . . . . . . . . . . 12  |-  ( f : x --> J  ->  dom  f  =  x
)
6160eqeq1d 2424 . . . . . . . . . . 11  |-  ( f : x --> J  -> 
( dom  f  =  (/)  <->  x  =  (/) ) )
6259, 61syl5rbbr 263 . . . . . . . . . 10  |-  ( f : x --> J  -> 
( x  =  (/)  <->  ran  f  =  (/) ) )
6362necon3bid 2682 . . . . . . . . 9  |-  ( f : x --> J  -> 
( x  =/=  (/)  <->  ran  f  =/=  (/) ) )
6463biimpac 488 . . . . . . . 8  |-  ( ( x  =/=  (/)  /\  f : x --> J )  ->  ran  f  =/=  (/) )
6557, 58, 64syl2an 479 . . . . . . 7  |-  ( ( ( ( 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  =/=  (/) )
6633simprbi 465 . . . . . . . . 9  |-  ( x  e.  ( ~P O  i^i  Fin )  ->  x  e.  Fin )
6766ad2antlr 731 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  ( ~P O  i^i  Fin ) )  /\  ( S  C_  U. x  /\  x  =/=  (/) ) )  ->  x  e.  Fin )
68 ffn 5742 . . . . . . . . . 10  |-  ( f : x --> J  -> 
f  Fn  x )
69 dffn4 5812 . . . . . . . . . 10  |-  ( f  Fn  x  <->  f :
x -onto-> ran  f )
7068, 69sylib 199 . . . . . . . . 9  |-  ( f : x --> J  -> 
f : x -onto-> ran  f )
7170adantr 466 . . . . . . . 8  |-  ( ( f : x --> J  /\  A. z  e.  x  ( A  e.  ( f `
 z )  /\  ( ( cls `  J
) `  ( f `  z ) )  C_  ( X  \  z
) ) )  -> 
f : x -onto-> ran  f )
72 fofi 7862 . . . . . . . 8  |-  ( ( x  e.  Fin  /\  f : x -onto-> ran  f
)  ->  ran  f  e. 
Fin )
7367, 71, 72syl2an 479 . . . . . . 7  |-  ( ( ( ( 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 )
74 fiinopn 19917 . . . . . . . 8  |-  ( J  e.  Top  ->  (
( ran  f  C_  J  /\  ran  f  =/=  (/)  /\  ran  f  e. 
Fin )  ->  |^| ran  f  e.  J )
)
7574imp 430 . . . . . . 7  |-  ( ( J  e.  Top  /\  ( ran  f  C_  J  /\  ran  f  =/=  (/)  /\  ran  f  e.  Fin )
)  ->  |^| ran  f  e.  J )
7654, 56, 65, 73, 75syl13anc 1266 . . . . . 6  |-  ( ( ( ( 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 )
77 simpl 458 . . . . . . . . . 10  |-  ( ( A  e.  ( f `
 z )  /\  ( ( cls `  J
) `  ( f `  z ) )  C_  ( X  \  z
) )  ->  A  e.  ( f `  z
) )
7877ralimi 2818 . . . . . . . . 9  |-  ( A. z  e.  x  ( A  e.  ( f `  z )  /\  (
( cls `  J
) `  ( f `  z ) )  C_  ( X  \  z
) )  ->  A. z  e.  x  A  e.  ( f `  z
) )
7978ad2antll 733 . . . . . . . 8  |-  ( ( ( ( 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 ) )
808ad3antrrr 734 . . . . . . . . 9  |-  ( ( ( ( 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 ) )
81 eliin 4302 . . . . . . . . 9  |-  ( A  e.  ( X  \  S )  ->  ( A  e.  |^|_ z  e.  x  ( f `  z )  <->  A. z  e.  x  A  e.  ( f `  z
) ) )
8280, 81syl 17 . . . . . . . 8  |-  ( ( ( ( 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 ) ) )
8379, 82mpbird 235 . . . . . . 7  |-  ( ( ( ( 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 )
)
8468ad2antrl 732 . . . . . . . 8  |-  ( ( ( ( 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
)
85 fnrnfv 5923 . . . . . . . . . 10  |-  ( f  Fn  x  ->  ran  f  =  { y  |  E. z  e.  x  y  =  ( f `  z ) } )
8685inteqd 4257 . . . . . . . . 9  |-  ( f  Fn  x  ->  |^| ran  f  =  |^| { y  |  E. z  e.  x  y  =  ( f `  z ) } )
87 fvex 5887 . . . . . . . . . 10  |-  ( f `
 z )  e. 
_V
8887dfiin2 4331 . . . . . . . . 9  |-  |^|_ z  e.  x  ( f `  z )  =  |^| { y  |  E. z  e.  x  y  =  ( f `  z
) }
8986, 88syl6eqr 2481 . . . . . . . 8  |-  ( f  Fn  x  ->  |^| ran  f  =  |^|_ z  e.  x  ( f `  z ) )
9084, 89syl 17 . . . . . . 7  |-  ( ( ( ( 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
) )
9183, 90eleqtrrd 2513 . . . . . 6  |-  ( ( ( ( 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 )
9257adantr 466 . . . . . . . . 9  |-  ( ( ( ( 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  =/=  (/) )
933ad4antr 736 . . . . . . . . . . . 12  |-  ( ( ( ( ( ph  /\  x  e.  ( ~P O  i^i  Fin )
)  /\  ( S  C_ 
U. x  /\  x  =/=  (/) ) )  /\  f : x --> J )  /\  z  e.  x
)  ->  J  e.  Top )
94 ffvelrn 6031 . . . . . . . . . . . . . . 15  |-  ( ( f : x --> J  /\  z  e.  x )  ->  ( f `  z
)  e.  J )
9594adantll 718 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\  x  e.  ( ~P O  i^i  Fin )
)  /\  ( S  C_ 
U. x  /\  x  =/=  (/) ) )  /\  f : x --> J )  /\  z  e.  x
)  ->  ( f `  z )  e.  J
)
96 elssuni 4245 . . . . . . . . . . . . . 14  |-  ( ( f `  z )  e.  J  ->  (
f `  z )  C_ 
U. J )
9795, 96syl 17 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\  x  e.  ( ~P O  i^i  Fin )
)  /\  ( S  C_ 
U. x  /\  x  =/=  (/) ) )  /\  f : x --> J )  /\  z  e.  x
)  ->  ( f `  z )  C_  U. J
)
9897, 5syl6sseqr 3511 . . . . . . . . . . . 12  |-  ( ( ( ( ( ph  /\  x  e.  ( ~P O  i^i  Fin )
)  /\  ( S  C_ 
U. x  /\  x  =/=  (/) ) )  /\  f : x --> J )  /\  z  e.  x
)  ->  ( f `  z )  C_  X
)
995clscld 20048 . . . . . . . . . . . 12  |-  ( ( J  e.  Top  /\  ( f `  z
)  C_  X )  ->  ( ( cls `  J
) `  ( f `  z ) )  e.  ( Clsd `  J
) )
10093, 98, 99syl2anc 665 . . . . . . . . . . 11  |-  ( ( ( ( ( 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 )
)
101100ralrimiva 2839 . . . . . . . . . 10  |-  ( ( ( ( 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
) )
102101adantrr 721 . . . . . . . . 9  |-  ( ( ( ( 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
) )
103 iincld 20040 . . . . . . . . 9  |-  ( ( x  =/=  (/)  /\  A. z  e.  x  (
( cls `  J
) `  ( f `  z ) )  e.  ( Clsd `  J
) )  ->  |^|_ z  e.  x  ( ( cls `  J ) `  ( f `  z
) )  e.  (
Clsd `  J )
)
10492, 102, 103syl2anc 665 . . . . . . . 8  |-  ( ( ( ( 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
) )
1055sscls 20057 . . . . . . . . . . . . 13  |-  ( ( J  e.  Top  /\  ( f `  z
)  C_  X )  ->  ( f `  z
)  C_  ( ( cls `  J ) `  ( f `  z
) ) )
10693, 98, 105syl2anc 665 . . . . . . . . . . . 12  |-  ( ( ( ( ( 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 ) ) )
107106ralrimiva 2839 . . . . . . . . . . 11  |-  ( ( ( ( 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
) ) )
108 ssel 3458 . . . . . . . . . . . . . 14  |-  ( ( f `  z ) 
C_  ( ( cls `  J ) `  (
f `  z )
)  ->  ( y  e.  ( f `  z
)  ->  y  e.  ( ( cls `  J
) `  ( f `  z ) ) ) )
109108ral2imi 2813 . . . . . . . . . . . . 13  |-  ( 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
) ) ) )
110 vex 3084 . . . . . . . . . . . . . 14  |-  y  e. 
_V
111 eliin 4302 . . . . . . . . . . . . . 14  |-  ( y  e.  _V  ->  (
y  e.  |^|_ z  e.  x  ( f `  z )  <->  A. z  e.  x  y  e.  ( f `  z
) ) )
112110, 111ax-mp 5 . . . . . . . . . . . . 13  |-  ( y  e.  |^|_ z  e.  x  ( f `  z
)  <->  A. z  e.  x  y  e.  ( f `  z ) )
113 eliin 4302 . . . . . . . . . . . . . 14  |-  ( y  e.  _V  ->  (
y  e.  |^|_ z  e.  x  ( ( cls `  J ) `  ( f `  z
) )  <->  A. z  e.  x  y  e.  ( ( cls `  J
) `  ( f `  z ) ) ) )
114110, 113ax-mp 5 . . . . . . . . . . . . 13  |-  ( y  e.  |^|_ z  e.  x  ( ( cls `  J
) `  ( f `  z ) )  <->  A. z  e.  x  y  e.  ( ( cls `  J
) `  ( f `  z ) ) )
115109, 112, 1143imtr4g 273 . . . . . . . . . . . 12  |-  ( 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
) ) ) )
116115ssrdv 3470 . . . . . . . . . . 11  |-  ( A. z  e.  x  (
f `  z )  C_  ( ( cls `  J
) `  ( f `  z ) )  ->  |^|_ z  e.  x  ( f `  z ) 
C_  |^|_ z  e.  x  ( ( cls `  J
) `  ( f `  z ) ) )
117107, 116syl 17 . . . . . . . . . 10  |-  ( ( ( ( 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 )
) )
118117adantrr 721 . . . . . . . . 9  |-  ( ( ( ( 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 )
) )
11990, 118eqsstrd 3498 . . . . . . . 8  |-  ( ( ( ( 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 ) ) )
1205clsss2 20074 . . . . . . . 8  |-  ( (
|^|_ 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
) ) )
121104, 119, 120syl2anc 665 . . . . . . 7  |-  ( ( ( ( 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
) ) )
122 ssel 3458 . . . . . . . . . . . . 13  |-  ( ( ( cls `  J
) `  ( f `  z ) )  C_  ( X  \  z
)  ->  ( y  e.  ( ( cls `  J
) `  ( f `  z ) )  -> 
y  e.  ( X 
\  z ) ) )
123122adantl 467 . . . . . . . . . . . 12  |-  ( ( A  e.  ( f `
 z )  /\  ( ( cls `  J
) `  ( f `  z ) )  C_  ( X  \  z
) )  ->  (
y  e.  ( ( cls `  J ) `
 ( f `  z ) )  -> 
y  e.  ( X 
\  z ) ) )
124123ral2imi 2813 . . . . . . . . . . 11  |-  ( 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
) ) )
125 eliin 4302 . . . . . . . . . . . 12  |-  ( y  e.  _V  ->  (
y  e.  |^|_ z  e.  x  ( X  \  z )  <->  A. z  e.  x  y  e.  ( X  \  z
) ) )
126110, 125ax-mp 5 . . . . . . . . . . 11  |-  ( y  e.  |^|_ z  e.  x  ( X  \  z
)  <->  A. z  e.  x  y  e.  ( X  \  z ) )
127124, 114, 1263imtr4g 273 . . . . . . . . . 10  |-  ( 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
) ) )
128127ssrdv 3470 . . . . . . . . 9  |-  ( 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 ) )
129128ad2antll 733 . . . . . . . 8  |-  ( ( ( ( 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 ) )
130 iindif2 4365 . . . . . . . . . 10  |-  ( x  =/=  (/)  ->  |^|_ z  e.  x  ( X  \ 
z )  =  ( X  \  U_ z  e.  x  z )
)
13192, 130syl 17 . . . . . . . . 9  |-  ( ( ( ( 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 ) )
132 simplrl 768 . . . . . . . . . 10  |-  ( ( ( ( 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
)
133 uniiun 4349 . . . . . . . . . . . 12  |-  U. x  =  U_ z  e.  x  z
134133sseq2i 3489 . . . . . . . . . . 11  |-  ( S 
C_  U. x  <->  S  C_  U_ z  e.  x  z )
135 sscon 3599 . . . . . . . . . . 11  |-  ( S 
C_  U_ z  e.  x  z  ->  ( X  \  U_ z  e.  x  z )  C_  ( X  \  S ) )
136134, 135sylbi 198 . . . . . . . . . 10  |-  ( S 
C_  U. x  ->  ( X  \  U_ z  e.  x  z )  C_  ( X  \  S ) )
137132, 136syl 17 . . . . . . . . 9  |-  ( ( ( ( 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 ) )
138131, 137eqsstrd 3498 . . . . . . . 8  |-  ( ( ( ( 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 ) )
139129, 138sstrd 3474 . . . . . . 7  |-  ( ( ( ( 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 ) )
140121, 139sstrd 3474 . . . . . 6  |-  ( ( ( ( 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 ) )
141 eleq2 2495 . . . . . . . 8  |-  ( z  =  |^| ran  f  ->  ( A  e.  z  <-> 
A  e.  |^| ran  f ) )
142 fveq2 5877 . . . . . . . . 9  |-  ( z  =  |^| ran  f  ->  ( ( cls `  J
) `  z )  =  ( ( cls `  J ) `  |^| ran  f ) )
143142sseq1d 3491 . . . . . . . 8  |-  ( z  =  |^| ran  f  ->  ( ( ( cls `  J ) `  z
)  C_  ( X  \  S )  <->  ( ( cls `  J ) `  |^| ran  f )  C_  ( X  \  S ) ) )
144141, 143anbi12d 715 . . . . . . 7  |-  ( z  =  |^| ran  f  ->  ( ( A  e.  z  /\  ( ( cls `  J ) `
 z )  C_  ( X  \  S ) )  <->  ( A  e. 
|^| ran  f  /\  ( ( cls `  J
) `  |^| ran  f
)  C_  ( X  \  S ) ) ) )
145144rspcev 3182 . . . . . 6  |-  ( (
|^| 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
) ) )
14676, 91, 140, 145syl12anc 1262 . . . . 5  |-  ( ( ( ( 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
) ) )
14753, 146exlimddv 1770 . . . 4  |-  ( ( ( 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
) ) )
148147anassrs 652 . . 3  |-  ( ( ( ( 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
) ) )
14932, 148pm2.61dane 2742 . 2  |-  ( ( ( 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
) ) )
1501adantr 466 . . . . . . . 8  |-  ( (
ph  /\  x  e.  S )  ->  J  e.  Haus )
151 hauscmplem.4 . . . . . . . . 9  |-  ( ph  ->  S  C_  X )
152151sselda 3464 . . . . . . . 8  |-  ( (
ph  /\  x  e.  S )  ->  x  e.  X )
1539adantr 466 . . . . . . . 8  |-  ( (
ph  /\  x  e.  S )  ->  A  e.  X )
154 id 23 . . . . . . . . 9  |-  ( x  e.  S  ->  x  e.  S )
1558eldifbd 3449 . . . . . . . . 9  |-  ( ph  ->  -.  A  e.  S
)
156 nelne2 2754 . . . . . . . . 9  |-  ( ( x  e.  S  /\  -.  A  e.  S
)  ->  x  =/=  A )
157154, 155, 156syl2anr 480 . . . . . . . 8  |-  ( (
ph  /\  x  e.  S )  ->  x  =/=  A )
1585hausnei 20330 . . . . . . . 8  |-  ( ( 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
)  =  (/) ) )
159150, 152, 153, 157, 158syl13anc 1266 . . . . . . 7  |-  ( (
ph  /\  x  e.  S )  ->  E. y  e.  J  E. w  e.  J  ( x  e.  y  /\  A  e.  w  /\  ( y  i^i  w )  =  (/) ) )
160 3anass 986 . . . . . . . . . . 11  |-  ( ( x  e.  y  /\  A  e.  w  /\  ( y  i^i  w
)  =  (/) )  <->  ( x  e.  y  /\  ( A  e.  w  /\  ( y  i^i  w
)  =  (/) ) ) )
161 elssuni 4245 . . . . . . . . . . . . . . . . 17  |-  ( w  e.  J  ->  w  C_ 
U. J )
162161, 5syl6sseqr 3511 . . . . . . . . . . . . . . . 16  |-  ( w  e.  J  ->  w  C_  X )
163162adantl 467 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  x  e.  S )  /\  y  e.  J
)  /\  w  e.  J )  ->  w  C_  X )
164 incom 3655 . . . . . . . . . . . . . . . . 17  |-  ( y  i^i  w )  =  ( w  i^i  y
)
165164eqeq1i 2429 . . . . . . . . . . . . . . . 16  |-  ( ( y  i^i  w )  =  (/)  <->  ( w  i^i  y )  =  (/) )
166 reldisj 3836 . . . . . . . . . . . . . . . 16  |-  ( w 
C_  X  ->  (
( w  i^i  y
)  =  (/)  <->  w  C_  ( X  \  y ) ) )
167165, 166syl5bb 260 . . . . . . . . . . . . . . 15  |-  ( w 
C_  X  ->  (
( y  i^i  w
)  =  (/)  <->  w  C_  ( X  \  y ) ) )
168163, 167syl 17 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  x  e.  S )  /\  y  e.  J
)  /\  w  e.  J )  ->  (
( y  i^i  w
)  =  (/)  <->  w  C_  ( X  \  y ) ) )
169150, 2syl 17 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  S )  ->  J  e.  Top )
1705opncld 20034 . . . . . . . . . . . . . . . . 17  |-  ( ( J  e.  Top  /\  y  e.  J )  ->  ( X  \  y
)  e.  ( Clsd `  J ) )
171169, 170sylan 473 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  x  e.  S )  /\  y  e.  J )  ->  ( X  \  y )  e.  ( Clsd `  J
) )
172171adantr 466 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  x  e.  S )  /\  y  e.  J
)  /\  w  e.  J )  ->  ( X  \  y )  e.  ( Clsd `  J
) )
1735clsss2 20074 . . . . . . . . . . . . . . . 16  |-  ( ( ( X  \  y
)  e.  ( Clsd `  J )  /\  w  C_  ( X  \  y
) )  ->  (
( cls `  J
) `  w )  C_  ( X  \  y
) )
174173ex 435 . . . . . . . . . . . . . . 15  |-  ( ( X  \  y )  e.  ( Clsd `  J
)  ->  ( w  C_  ( X  \  y
)  ->  ( ( cls `  J ) `  w )  C_  ( X  \  y ) ) )
175172, 174syl 17 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  x  e.  S )  /\  y  e.  J
)  /\  w  e.  J )  ->  (
w  C_  ( X  \  y )  ->  (
( cls `  J
) `  w )  C_  ( X  \  y
) ) )
176168, 175sylbid 218 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  x  e.  S )  /\  y  e.  J
)  /\  w  e.  J )  ->  (
( y  i^i  w
)  =  (/)  ->  (
( cls `  J
) `  w )  C_  ( X  \  y
) ) )
177176anim2d 567 . . . . . . . . . . . 12  |-  ( ( ( ( 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
) ) ) )
178177anim2d 567 . . . . . . . . . . 11  |-  ( ( ( ( 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
) ) ) ) )
179160, 178syl5bi 220 . . . . . . . . . 10  |-  ( ( ( ( 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
) ) ) ) )
180179reximdva 2900 . . . . . . . . 9  |-  ( ( ( 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 2983 . . . . . . . . 9  |-  ( 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
) ) ) )
182180, 181syl6ib 229 . . . . . . . 8  |-  ( ( ( 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
) ) ) ) )
183182reximdva 2900 . . . . . . 7  |-  ( (
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
) ) ) ) )
184159, 183mpd 15 . . . . . 6  |-  ( (
ph  /\  x  e.  S )  ->  E. y  e.  J  ( x  e.  y  /\  E. w  e.  J  ( A  e.  w  /\  (
( cls `  J
) `  w )  C_  ( X  \  y
) ) ) )
18541unieqi 4225 . . . . . . . 8  |-  U. O  =  U. { y  e.  J  |  E. w  e.  J  ( A  e.  w  /\  (
( cls `  J
) `  w )  C_  ( X  \  y
) ) }
186185eleq2i 2500 . . . . . . 7  |-  ( 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 4228 . . . . . . 7  |-  ( 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
) ) ) )
188186, 187bitri 252 . . . . . 6  |-  ( x  e.  U. O  <->  E. y  e.  J  ( x  e.  y  /\  E. w  e.  J  ( A  e.  w  /\  (
( cls `  J
) `  w )  C_  ( X  \  y
) ) ) )
189184, 188sylibr 215 . . . . 5  |-  ( (
ph  /\  x  e.  S )  ->  x  e.  U. O )
190189ex 435 . . . 4  |-  ( ph  ->  ( x  e.  S  ->  x  e.  U. O
) )
191190ssrdv 3470 . . 3  |-  ( ph  ->  S  C_  U. O )
192 ssrab2 3546 . . . . . 6  |-  { y  e.  J  |  E. w  e.  J  ( A  e.  w  /\  ( ( cls `  J
) `  w )  C_  ( X  \  y
) ) }  C_  J
19341, 192eqsstri 3494 . . . . 5  |-  O  C_  J
194 elpw2g 4583 . . . . . 6  |-  ( J  e.  Haus  ->  ( O  e.  ~P J  <->  O  C_  J
) )
1951, 194syl 17 . . . . 5  |-  ( ph  ->  ( O  e.  ~P J 
<->  O  C_  J )
)
196193, 195mpbiri 236 . . . 4  |-  ( ph  ->  O  e.  ~P J
)
197 hauscmplem.5 . . . . 5  |-  ( ph  ->  ( Jt  S )  e.  Comp )
1985cmpsub 20401 . . . . . 6  |-  ( ( J  e.  Top  /\  S  C_  X )  -> 
( ( Jt  S )  e.  Comp  <->  A. z  e.  ~P  J ( S  C_  U. z  ->  E. x  e.  ( ~P z  i^i 
Fin ) S  C_  U. x ) ) )
199198biimp3a 1364 . . . . 5  |-  ( ( J  e.  Top  /\  S  C_  X  /\  ( Jt  S )  e.  Comp )  ->  A. z  e.  ~P  J ( S  C_  U. z  ->  E. x  e.  ( ~P z  i^i 
Fin ) S  C_  U. x ) )
2003, 151, 197, 199syl3anc 1264 . . . 4  |-  ( ph  ->  A. z  e.  ~P  J ( S  C_  U. z  ->  E. x  e.  ( ~P z  i^i 
Fin ) S  C_  U. x ) )
201 unieq 4224 . . . . . . 7  |-  ( z  =  O  ->  U. z  =  U. O )
202201sseq2d 3492 . . . . . 6  |-  ( z  =  O  ->  ( S  C_  U. z  <->  S  C_  U. O
) )
203 pweq 3982 . . . . . . . 8  |-  ( z  =  O  ->  ~P z  =  ~P O
)
204203ineq1d 3663 . . . . . . 7  |-  ( z  =  O  ->  ( ~P z  i^i  Fin )  =  ( ~P O  i^i  Fin ) )
205204rexeqdv 3032 . . . . . 6  |-  ( 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
) )
206202, 205imbi12d 321 . . . . 5  |-  ( 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
) ) )
207206rspcva 3180 . . . 4  |-  ( ( O  e.  ~P J  /\  A. z  e.  ~P  J ( 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
) )
208196, 200, 207syl2anc 665 . . 3  |-  ( ph  ->  ( S  C_  U. O  ->  E. x  e.  ( ~P O  i^i  Fin ) S  C_  U. x
) )
209191, 208mpd 15 . 2  |-  ( ph  ->  E. x  e.  ( ~P O  i^i  Fin ) S  C_  U. x
)
210149, 209r19.29a 2970 1  |-  ( ph  ->  E. z  e.  J  ( A  e.  z  /\  ( ( cls `  J
) `  z )  C_  ( X  \  S
) ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 187    /\ wa 370    /\ w3a 982    = wceq 1437   E.wex 1659    e. wcel 1868   {cab 2407    =/= wne 2618   A.wral 2775   E.wrex 2776   {crab 2779   _Vcvv 3081    \ cdif 3433    i^i cin 3435    C_ wss 3436   (/)c0 3761   ~Pcpw 3979   U.cuni 4216   |^|cint 4252   U_ciun 4296   |^|_ciin 4297   dom cdm 4849   ran crn 4850    Fn wfn 5592   -->wf 5593   -onto->wfo 5595   ` cfv 5597  (class class class)co 6301   Fincfn 7573   ↾t crest 15306   Topctop 19903   Clsdccld 20017   clsccl 20019   Hauscha 20310   Compccmp 20387
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-rep 4533  ax-sep 4543  ax-nul 4551  ax-pow 4598  ax-pr 4656  ax-un 6593
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-reu 2782  df-rab 2784  df-v 3083  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3910  df-pw 3981  df-sn 3997  df-pr 3999  df-tp 4001  df-op 4003  df-uni 4217  df-int 4253  df-iun 4298  df-iin 4299  df-br 4421  df-opab 4480  df-mpt 4481  df-tr 4516  df-eprel 4760  df-id 4764  df-po 4770  df-so 4771  df-fr 4808  df-we 4810  df-xp 4855  df-rel 4856  df-cnv 4857  df-co 4858  df-dm 4859  df-rn 4860  df-res 4861  df-ima 4862  df-pred 5395  df-ord 5441  df-on 5442  df-lim 5443  df-suc 5444  df-iota 5561  df-fun 5599  df-fn 5600  df-f 5601  df-f1 5602  df-fo 5603  df-f1o 5604  df-fv 5605  df-ov 6304  df-oprab 6305  df-mpt2 6306  df-om 6703  df-1st 6803  df-2nd 6804  df-wrecs 7032  df-recs 7094  df-rdg 7132  df-1o 7186  df-oadd 7190  df-er 7367  df-en 7574  df-dom 7575  df-fin 7577  df-fi 7927  df-rest 15308  df-topgen 15329  df-top 19907  df-bases 19908  df-topon 19909  df-cld 20020  df-cls 20022  df-haus 20317  df-cmp 20388
This theorem is referenced by:  hauscmp  20408  hausllycmp  20495
  Copyright terms: Public domain W3C validator