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

Theorem kqnrmlem1 20751
Description: A Kolmogorov quotient of a normal space is normal. (Contributed by Mario Carneiro, 25-Aug-2015.)
Hypothesis
Ref Expression
kqval.2  |-  F  =  ( x  e.  X  |->  { y  e.  J  |  x  e.  y } )
Assertion
Ref Expression
kqnrmlem1  |-  ( ( J  e.  (TopOn `  X )  /\  J  e.  Nrm )  ->  (KQ `  J )  e.  Nrm )
Distinct variable groups:    x, y, J    x, X, y
Allowed substitution hints:    F( x, y)

Proof of Theorem kqnrmlem1
Dummy variables  m  w  z  u are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 kqval.2 . . . . 5  |-  F  =  ( x  e.  X  |->  { y  e.  J  |  x  e.  y } )
21kqtopon 20735 . . . 4  |-  ( J  e.  (TopOn `  X
)  ->  (KQ `  J
)  e.  (TopOn `  ran  F ) )
32adantr 467 . . 3  |-  ( ( J  e.  (TopOn `  X )  /\  J  e.  Nrm )  ->  (KQ `  J )  e.  (TopOn `  ran  F ) )
4 topontop 19934 . . 3  |-  ( (KQ
`  J )  e.  (TopOn `  ran  F )  ->  (KQ `  J
)  e.  Top )
53, 4syl 17 . 2  |-  ( ( J  e.  (TopOn `  X )  /\  J  e.  Nrm )  ->  (KQ `  J )  e.  Top )
6 simplr 761 . . . . 5  |-  ( ( ( J  e.  (TopOn `  X )  /\  J  e.  Nrm )  /\  (
z  e.  (KQ `  J )  /\  w  e.  ( ( Clsd `  (KQ `  J ) )  i^i 
~P z ) ) )  ->  J  e.  Nrm )
71kqid 20736 . . . . . . 7  |-  ( J  e.  (TopOn `  X
)  ->  F  e.  ( J  Cn  (KQ `  J ) ) )
87ad2antrr 731 . . . . . 6  |-  ( ( ( J  e.  (TopOn `  X )  /\  J  e.  Nrm )  /\  (
z  e.  (KQ `  J )  /\  w  e.  ( ( Clsd `  (KQ `  J ) )  i^i 
~P z ) ) )  ->  F  e.  ( J  Cn  (KQ `  J ) ) )
9 simprl 763 . . . . . 6  |-  ( ( ( J  e.  (TopOn `  X )  /\  J  e.  Nrm )  /\  (
z  e.  (KQ `  J )  /\  w  e.  ( ( Clsd `  (KQ `  J ) )  i^i 
~P z ) ) )  ->  z  e.  (KQ `  J ) )
10 cnima 20274 . . . . . 6  |-  ( ( F  e.  ( J  Cn  (KQ `  J
) )  /\  z  e.  (KQ `  J ) )  ->  ( `' F " z )  e.  J )
118, 9, 10syl2anc 666 . . . . 5  |-  ( ( ( J  e.  (TopOn `  X )  /\  J  e.  Nrm )  /\  (
z  e.  (KQ `  J )  /\  w  e.  ( ( Clsd `  (KQ `  J ) )  i^i 
~P z ) ) )  ->  ( `' F " z )  e.  J )
12 inss1 3651 . . . . . . 7  |-  ( (
Clsd `  (KQ `  J
) )  i^i  ~P z )  C_  ( Clsd `  (KQ `  J
) )
13 simprr 765 . . . . . . 7  |-  ( ( ( J  e.  (TopOn `  X )  /\  J  e.  Nrm )  /\  (
z  e.  (KQ `  J )  /\  w  e.  ( ( Clsd `  (KQ `  J ) )  i^i 
~P z ) ) )  ->  w  e.  ( ( Clsd `  (KQ `  J ) )  i^i 
~P z ) )
1412, 13sseldi 3429 . . . . . 6  |-  ( ( ( J  e.  (TopOn `  X )  /\  J  e.  Nrm )  /\  (
z  e.  (KQ `  J )  /\  w  e.  ( ( Clsd `  (KQ `  J ) )  i^i 
~P z ) ) )  ->  w  e.  ( Clsd `  (KQ `  J
) ) )
15 cnclima 20277 . . . . . 6  |-  ( ( F  e.  ( J  Cn  (KQ `  J
) )  /\  w  e.  ( Clsd `  (KQ `  J ) ) )  ->  ( `' F " w )  e.  (
Clsd `  J )
)
168, 14, 15syl2anc 666 . . . . 5  |-  ( ( ( J  e.  (TopOn `  X )  /\  J  e.  Nrm )  /\  (
z  e.  (KQ `  J )  /\  w  e.  ( ( Clsd `  (KQ `  J ) )  i^i 
~P z ) ) )  ->  ( `' F " w )  e.  ( Clsd `  J
) )
17 inss2 3652 . . . . . . 7  |-  ( (
Clsd `  (KQ `  J
) )  i^i  ~P z )  C_  ~P z
1817, 13sseldi 3429 . . . . . 6  |-  ( ( ( J  e.  (TopOn `  X )  /\  J  e.  Nrm )  /\  (
z  e.  (KQ `  J )  /\  w  e.  ( ( Clsd `  (KQ `  J ) )  i^i 
~P z ) ) )  ->  w  e.  ~P z )
19 elpwi 3959 . . . . . 6  |-  ( w  e.  ~P z  ->  w  C_  z )
20 imass2 5203 . . . . . 6  |-  ( w 
C_  z  ->  ( `' F " w ) 
C_  ( `' F " z ) )
2118, 19, 203syl 18 . . . . 5  |-  ( ( ( J  e.  (TopOn `  X )  /\  J  e.  Nrm )  /\  (
z  e.  (KQ `  J )  /\  w  e.  ( ( Clsd `  (KQ `  J ) )  i^i 
~P z ) ) )  ->  ( `' F " w )  C_  ( `' F " z ) )
22 nrmsep3 20364 . . . . 5  |-  ( ( J  e.  Nrm  /\  ( ( `' F " z )  e.  J  /\  ( `' F "
w )  e.  (
Clsd `  J )  /\  ( `' F "
w )  C_  ( `' F " z ) ) )  ->  E. u  e.  J  ( ( `' F " w ) 
C_  u  /\  (
( cls `  J
) `  u )  C_  ( `' F "
z ) ) )
236, 11, 16, 21, 22syl13anc 1269 . . . 4  |-  ( ( ( J  e.  (TopOn `  X )  /\  J  e.  Nrm )  /\  (
z  e.  (KQ `  J )  /\  w  e.  ( ( Clsd `  (KQ `  J ) )  i^i 
~P z ) ) )  ->  E. u  e.  J  ( ( `' F " w ) 
C_  u  /\  (
( cls `  J
) `  u )  C_  ( `' F "
z ) ) )
24 simplll 767 . . . . . 6  |-  ( ( ( ( J  e.  (TopOn `  X )  /\  J  e.  Nrm )  /\  ( z  e.  (KQ `  J )  /\  w  e.  ( ( Clsd `  (KQ `  J ) )  i^i 
~P z ) ) )  /\  ( u  e.  J  /\  (
( `' F "
w )  C_  u  /\  ( ( cls `  J
) `  u )  C_  ( `' F "
z ) ) ) )  ->  J  e.  (TopOn `  X ) )
25 simprl 763 . . . . . 6  |-  ( ( ( ( J  e.  (TopOn `  X )  /\  J  e.  Nrm )  /\  ( z  e.  (KQ `  J )  /\  w  e.  ( ( Clsd `  (KQ `  J ) )  i^i 
~P z ) ) )  /\  ( u  e.  J  /\  (
( `' F "
w )  C_  u  /\  ( ( cls `  J
) `  u )  C_  ( `' F "
z ) ) ) )  ->  u  e.  J )
261kqopn 20742 . . . . . 6  |-  ( ( J  e.  (TopOn `  X )  /\  u  e.  J )  ->  ( F " u )  e.  (KQ `  J ) )
2724, 25, 26syl2anc 666 . . . . 5  |-  ( ( ( ( J  e.  (TopOn `  X )  /\  J  e.  Nrm )  /\  ( z  e.  (KQ `  J )  /\  w  e.  ( ( Clsd `  (KQ `  J ) )  i^i 
~P z ) ) )  /\  ( u  e.  J  /\  (
( `' F "
w )  C_  u  /\  ( ( cls `  J
) `  u )  C_  ( `' F "
z ) ) ) )  ->  ( F " u )  e.  (KQ
`  J ) )
28 simprrl 773 . . . . . 6  |-  ( ( ( ( J  e.  (TopOn `  X )  /\  J  e.  Nrm )  /\  ( z  e.  (KQ `  J )  /\  w  e.  ( ( Clsd `  (KQ `  J ) )  i^i 
~P z ) ) )  /\  ( u  e.  J  /\  (
( `' F "
w )  C_  u  /\  ( ( cls `  J
) `  u )  C_  ( `' F "
z ) ) ) )  ->  ( `' F " w )  C_  u )
291kqffn 20733 . . . . . . . 8  |-  ( J  e.  (TopOn `  X
)  ->  F  Fn  X )
30 fnfun 5671 . . . . . . . 8  |-  ( F  Fn  X  ->  Fun  F )
3124, 29, 303syl 18 . . . . . . 7  |-  ( ( ( ( J  e.  (TopOn `  X )  /\  J  e.  Nrm )  /\  ( z  e.  (KQ `  J )  /\  w  e.  ( ( Clsd `  (KQ `  J ) )  i^i 
~P z ) ) )  /\  ( u  e.  J  /\  (
( `' F "
w )  C_  u  /\  ( ( cls `  J
) `  u )  C_  ( `' F "
z ) ) ) )  ->  Fun  F )
3214adantr 467 . . . . . . . . 9  |-  ( ( ( ( J  e.  (TopOn `  X )  /\  J  e.  Nrm )  /\  ( z  e.  (KQ `  J )  /\  w  e.  ( ( Clsd `  (KQ `  J ) )  i^i 
~P z ) ) )  /\  ( u  e.  J  /\  (
( `' F "
w )  C_  u  /\  ( ( cls `  J
) `  u )  C_  ( `' F "
z ) ) ) )  ->  w  e.  ( Clsd `  (KQ `  J
) ) )
33 eqid 2450 . . . . . . . . . 10  |-  U. (KQ `  J )  =  U. (KQ `  J )
3433cldss 20037 . . . . . . . . 9  |-  ( w  e.  ( Clsd `  (KQ `  J ) )  ->  w  C_  U. (KQ `  J ) )
3532, 34syl 17 . . . . . . . 8  |-  ( ( ( ( J  e.  (TopOn `  X )  /\  J  e.  Nrm )  /\  ( z  e.  (KQ `  J )  /\  w  e.  ( ( Clsd `  (KQ `  J ) )  i^i 
~P z ) ) )  /\  ( u  e.  J  /\  (
( `' F "
w )  C_  u  /\  ( ( cls `  J
) `  u )  C_  ( `' F "
z ) ) ) )  ->  w  C_  U. (KQ `  J ) )
36 toponuni 19935 . . . . . . . . 9  |-  ( (KQ
`  J )  e.  (TopOn `  ran  F )  ->  ran  F  =  U. (KQ `  J ) )
3724, 2, 363syl 18 . . . . . . . 8  |-  ( ( ( ( J  e.  (TopOn `  X )  /\  J  e.  Nrm )  /\  ( z  e.  (KQ `  J )  /\  w  e.  ( ( Clsd `  (KQ `  J ) )  i^i 
~P z ) ) )  /\  ( u  e.  J  /\  (
( `' F "
w )  C_  u  /\  ( ( cls `  J
) `  u )  C_  ( `' F "
z ) ) ) )  ->  ran  F  = 
U. (KQ `  J
) )
3835, 37sseqtr4d 3468 . . . . . . 7  |-  ( ( ( ( J  e.  (TopOn `  X )  /\  J  e.  Nrm )  /\  ( z  e.  (KQ `  J )  /\  w  e.  ( ( Clsd `  (KQ `  J ) )  i^i 
~P z ) ) )  /\  ( u  e.  J  /\  (
( `' F "
w )  C_  u  /\  ( ( cls `  J
) `  u )  C_  ( `' F "
z ) ) ) )  ->  w  C_  ran  F )
39 funimass1 5654 . . . . . . 7  |-  ( ( Fun  F  /\  w  C_ 
ran  F )  -> 
( ( `' F " w )  C_  u  ->  w  C_  ( F " u ) ) )
4031, 38, 39syl2anc 666 . . . . . 6  |-  ( ( ( ( J  e.  (TopOn `  X )  /\  J  e.  Nrm )  /\  ( z  e.  (KQ `  J )  /\  w  e.  ( ( Clsd `  (KQ `  J ) )  i^i 
~P z ) ) )  /\  ( u  e.  J  /\  (
( `' F "
w )  C_  u  /\  ( ( cls `  J
) `  u )  C_  ( `' F "
z ) ) ) )  ->  ( ( `' F " w ) 
C_  u  ->  w  C_  ( F " u
) ) )
4128, 40mpd 15 . . . . 5  |-  ( ( ( ( J  e.  (TopOn `  X )  /\  J  e.  Nrm )  /\  ( z  e.  (KQ `  J )  /\  w  e.  ( ( Clsd `  (KQ `  J ) )  i^i 
~P z ) ) )  /\  ( u  e.  J  /\  (
( `' F "
w )  C_  u  /\  ( ( cls `  J
) `  u )  C_  ( `' F "
z ) ) ) )  ->  w  C_  ( F " u ) )
42 topontop 19934 . . . . . . . . . 10  |-  ( J  e.  (TopOn `  X
)  ->  J  e.  Top )
4324, 42syl 17 . . . . . . . . 9  |-  ( ( ( ( J  e.  (TopOn `  X )  /\  J  e.  Nrm )  /\  ( z  e.  (KQ `  J )  /\  w  e.  ( ( Clsd `  (KQ `  J ) )  i^i 
~P z ) ) )  /\  ( u  e.  J  /\  (
( `' F "
w )  C_  u  /\  ( ( cls `  J
) `  u )  C_  ( `' F "
z ) ) ) )  ->  J  e.  Top )
44 elssuni 4226 . . . . . . . . . 10  |-  ( u  e.  J  ->  u  C_ 
U. J )
4544ad2antrl 733 . . . . . . . . 9  |-  ( ( ( ( J  e.  (TopOn `  X )  /\  J  e.  Nrm )  /\  ( z  e.  (KQ `  J )  /\  w  e.  ( ( Clsd `  (KQ `  J ) )  i^i 
~P z ) ) )  /\  ( u  e.  J  /\  (
( `' F "
w )  C_  u  /\  ( ( cls `  J
) `  u )  C_  ( `' F "
z ) ) ) )  ->  u  C_  U. J
)
46 eqid 2450 . . . . . . . . . 10  |-  U. J  =  U. J
4746clscld 20055 . . . . . . . . 9  |-  ( ( J  e.  Top  /\  u  C_  U. J )  ->  ( ( cls `  J ) `  u
)  e.  ( Clsd `  J ) )
4843, 45, 47syl2anc 666 . . . . . . . 8  |-  ( ( ( ( J  e.  (TopOn `  X )  /\  J  e.  Nrm )  /\  ( z  e.  (KQ `  J )  /\  w  e.  ( ( Clsd `  (KQ `  J ) )  i^i 
~P z ) ) )  /\  ( u  e.  J  /\  (
( `' F "
w )  C_  u  /\  ( ( cls `  J
) `  u )  C_  ( `' F "
z ) ) ) )  ->  ( ( cls `  J ) `  u )  e.  (
Clsd `  J )
)
491kqcld 20743 . . . . . . . 8  |-  ( ( J  e.  (TopOn `  X )  /\  (
( cls `  J
) `  u )  e.  ( Clsd `  J
) )  ->  ( F " ( ( cls `  J ) `  u
) )  e.  (
Clsd `  (KQ `  J
) ) )
5024, 48, 49syl2anc 666 . . . . . . 7  |-  ( ( ( ( J  e.  (TopOn `  X )  /\  J  e.  Nrm )  /\  ( z  e.  (KQ `  J )  /\  w  e.  ( ( Clsd `  (KQ `  J ) )  i^i 
~P z ) ) )  /\  ( u  e.  J  /\  (
( `' F "
w )  C_  u  /\  ( ( cls `  J
) `  u )  C_  ( `' F "
z ) ) ) )  ->  ( F " ( ( cls `  J
) `  u )
)  e.  ( Clsd `  (KQ `  J ) ) )
5146sscls 20064 . . . . . . . . 9  |-  ( ( J  e.  Top  /\  u  C_  U. J )  ->  u  C_  (
( cls `  J
) `  u )
)
5243, 45, 51syl2anc 666 . . . . . . . 8  |-  ( ( ( ( J  e.  (TopOn `  X )  /\  J  e.  Nrm )  /\  ( z  e.  (KQ `  J )  /\  w  e.  ( ( Clsd `  (KQ `  J ) )  i^i 
~P z ) ) )  /\  ( u  e.  J  /\  (
( `' F "
w )  C_  u  /\  ( ( cls `  J
) `  u )  C_  ( `' F "
z ) ) ) )  ->  u  C_  (
( cls `  J
) `  u )
)
53 imass2 5203 . . . . . . . 8  |-  ( u 
C_  ( ( cls `  J ) `  u
)  ->  ( F " u )  C_  ( F " ( ( cls `  J ) `  u
) ) )
5452, 53syl 17 . . . . . . 7  |-  ( ( ( ( J  e.  (TopOn `  X )  /\  J  e.  Nrm )  /\  ( z  e.  (KQ `  J )  /\  w  e.  ( ( Clsd `  (KQ `  J ) )  i^i 
~P z ) ) )  /\  ( u  e.  J  /\  (
( `' F "
w )  C_  u  /\  ( ( cls `  J
) `  u )  C_  ( `' F "
z ) ) ) )  ->  ( F " u )  C_  ( F " ( ( cls `  J ) `  u
) ) )
5533clsss2 20081 . . . . . . 7  |-  ( ( ( F " (
( cls `  J
) `  u )
)  e.  ( Clsd `  (KQ `  J ) )  /\  ( F
" u )  C_  ( F " ( ( cls `  J ) `
 u ) ) )  ->  ( ( cls `  (KQ `  J
) ) `  ( F " u ) ) 
C_  ( F "
( ( cls `  J
) `  u )
) )
5650, 54, 55syl2anc 666 . . . . . 6  |-  ( ( ( ( J  e.  (TopOn `  X )  /\  J  e.  Nrm )  /\  ( z  e.  (KQ `  J )  /\  w  e.  ( ( Clsd `  (KQ `  J ) )  i^i 
~P z ) ) )  /\  ( u  e.  J  /\  (
( `' F "
w )  C_  u  /\  ( ( cls `  J
) `  u )  C_  ( `' F "
z ) ) ) )  ->  ( ( cls `  (KQ `  J
) ) `  ( F " u ) ) 
C_  ( F "
( ( cls `  J
) `  u )
) )
57 simprrr 774 . . . . . . 7  |-  ( ( ( ( J  e.  (TopOn `  X )  /\  J  e.  Nrm )  /\  ( z  e.  (KQ `  J )  /\  w  e.  ( ( Clsd `  (KQ `  J ) )  i^i 
~P z ) ) )  /\  ( u  e.  J  /\  (
( `' F "
w )  C_  u  /\  ( ( cls `  J
) `  u )  C_  ( `' F "
z ) ) ) )  ->  ( ( cls `  J ) `  u )  C_  ( `' F " z ) )
5846clsss3 20067 . . . . . . . . . 10  |-  ( ( J  e.  Top  /\  u  C_  U. J )  ->  ( ( cls `  J ) `  u
)  C_  U. J )
5943, 45, 58syl2anc 666 . . . . . . . . 9  |-  ( ( ( ( J  e.  (TopOn `  X )  /\  J  e.  Nrm )  /\  ( z  e.  (KQ `  J )  /\  w  e.  ( ( Clsd `  (KQ `  J ) )  i^i 
~P z ) ) )  /\  ( u  e.  J  /\  (
( `' F "
w )  C_  u  /\  ( ( cls `  J
) `  u )  C_  ( `' F "
z ) ) ) )  ->  ( ( cls `  J ) `  u )  C_  U. J
)
60 fndm 5673 . . . . . . . . . . 11  |-  ( F  Fn  X  ->  dom  F  =  X )
6124, 29, 603syl 18 . . . . . . . . . 10  |-  ( ( ( ( J  e.  (TopOn `  X )  /\  J  e.  Nrm )  /\  ( z  e.  (KQ `  J )  /\  w  e.  ( ( Clsd `  (KQ `  J ) )  i^i 
~P z ) ) )  /\  ( u  e.  J  /\  (
( `' F "
w )  C_  u  /\  ( ( cls `  J
) `  u )  C_  ( `' F "
z ) ) ) )  ->  dom  F  =  X )
62 toponuni 19935 . . . . . . . . . . 11  |-  ( J  e.  (TopOn `  X
)  ->  X  =  U. J )
6324, 62syl 17 . . . . . . . . . 10  |-  ( ( ( ( J  e.  (TopOn `  X )  /\  J  e.  Nrm )  /\  ( z  e.  (KQ `  J )  /\  w  e.  ( ( Clsd `  (KQ `  J ) )  i^i 
~P z ) ) )  /\  ( u  e.  J  /\  (
( `' F "
w )  C_  u  /\  ( ( cls `  J
) `  u )  C_  ( `' F "
z ) ) ) )  ->  X  =  U. J )
6461, 63eqtrd 2484 . . . . . . . . 9  |-  ( ( ( ( J  e.  (TopOn `  X )  /\  J  e.  Nrm )  /\  ( z  e.  (KQ `  J )  /\  w  e.  ( ( Clsd `  (KQ `  J ) )  i^i 
~P z ) ) )  /\  ( u  e.  J  /\  (
( `' F "
w )  C_  u  /\  ( ( cls `  J
) `  u )  C_  ( `' F "
z ) ) ) )  ->  dom  F  = 
U. J )
6559, 64sseqtr4d 3468 . . . . . . . 8  |-  ( ( ( ( J  e.  (TopOn `  X )  /\  J  e.  Nrm )  /\  ( z  e.  (KQ `  J )  /\  w  e.  ( ( Clsd `  (KQ `  J ) )  i^i 
~P z ) ) )  /\  ( u  e.  J  /\  (
( `' F "
w )  C_  u  /\  ( ( cls `  J
) `  u )  C_  ( `' F "
z ) ) ) )  ->  ( ( cls `  J ) `  u )  C_  dom  F )
66 funimass3 5996 . . . . . . . 8  |-  ( ( Fun  F  /\  (
( cls `  J
) `  u )  C_ 
dom  F )  -> 
( ( F "
( ( cls `  J
) `  u )
)  C_  z  <->  ( ( cls `  J ) `  u )  C_  ( `' F " z ) ) )
6731, 65, 66syl2anc 666 . . . . . . 7  |-  ( ( ( ( J  e.  (TopOn `  X )  /\  J  e.  Nrm )  /\  ( z  e.  (KQ `  J )  /\  w  e.  ( ( Clsd `  (KQ `  J ) )  i^i 
~P z ) ) )  /\  ( u  e.  J  /\  (
( `' F "
w )  C_  u  /\  ( ( cls `  J
) `  u )  C_  ( `' F "
z ) ) ) )  ->  ( ( F " ( ( cls `  J ) `  u
) )  C_  z  <->  ( ( cls `  J
) `  u )  C_  ( `' F "
z ) ) )
6857, 67mpbird 236 . . . . . 6  |-  ( ( ( ( J  e.  (TopOn `  X )  /\  J  e.  Nrm )  /\  ( z  e.  (KQ `  J )  /\  w  e.  ( ( Clsd `  (KQ `  J ) )  i^i 
~P z ) ) )  /\  ( u  e.  J  /\  (
( `' F "
w )  C_  u  /\  ( ( cls `  J
) `  u )  C_  ( `' F "
z ) ) ) )  ->  ( F " ( ( cls `  J
) `  u )
)  C_  z )
6956, 68sstrd 3441 . . . . 5  |-  ( ( ( ( J  e.  (TopOn `  X )  /\  J  e.  Nrm )  /\  ( z  e.  (KQ `  J )  /\  w  e.  ( ( Clsd `  (KQ `  J ) )  i^i 
~P z ) ) )  /\  ( u  e.  J  /\  (
( `' F "
w )  C_  u  /\  ( ( cls `  J
) `  u )  C_  ( `' F "
z ) ) ) )  ->  ( ( cls `  (KQ `  J
) ) `  ( F " u ) ) 
C_  z )
70 sseq2 3453 . . . . . . 7  |-  ( m  =  ( F "
u )  ->  (
w  C_  m  <->  w  C_  ( F " u ) ) )
71 fveq2 5863 . . . . . . . 8  |-  ( m  =  ( F "
u )  ->  (
( cls `  (KQ `  J ) ) `  m )  =  ( ( cls `  (KQ `  J ) ) `  ( F " u ) ) )
7271sseq1d 3458 . . . . . . 7  |-  ( m  =  ( F "
u )  ->  (
( ( cls `  (KQ `  J ) ) `  m )  C_  z  <->  ( ( cls `  (KQ `  J ) ) `  ( F " u ) )  C_  z )
)
7370, 72anbi12d 716 . . . . . 6  |-  ( m  =  ( F "
u )  ->  (
( w  C_  m  /\  ( ( cls `  (KQ `  J ) ) `  m )  C_  z
)  <->  ( w  C_  ( F " u )  /\  ( ( cls `  (KQ `  J ) ) `  ( F
" u ) ) 
C_  z ) ) )
7473rspcev 3149 . . . . 5  |-  ( ( ( F " u
)  e.  (KQ `  J )  /\  (
w  C_  ( F " u )  /\  (
( cls `  (KQ `  J ) ) `  ( F " u ) )  C_  z )
)  ->  E. m  e.  (KQ `  J ) ( w  C_  m  /\  ( ( cls `  (KQ `  J ) ) `  m )  C_  z
) )
7527, 41, 69, 74syl12anc 1265 . . . 4  |-  ( ( ( ( J  e.  (TopOn `  X )  /\  J  e.  Nrm )  /\  ( z  e.  (KQ `  J )  /\  w  e.  ( ( Clsd `  (KQ `  J ) )  i^i 
~P z ) ) )  /\  ( u  e.  J  /\  (
( `' F "
w )  C_  u  /\  ( ( cls `  J
) `  u )  C_  ( `' F "
z ) ) ) )  ->  E. m  e.  (KQ `  J ) ( w  C_  m  /\  ( ( cls `  (KQ `  J ) ) `  m )  C_  z
) )
7623, 75rexlimddv 2882 . . 3  |-  ( ( ( J  e.  (TopOn `  X )  /\  J  e.  Nrm )  /\  (
z  e.  (KQ `  J )  /\  w  e.  ( ( Clsd `  (KQ `  J ) )  i^i 
~P z ) ) )  ->  E. m  e.  (KQ `  J ) ( w  C_  m  /\  ( ( cls `  (KQ `  J ) ) `  m )  C_  z
) )
7776ralrimivva 2808 . 2  |-  ( ( J  e.  (TopOn `  X )  /\  J  e.  Nrm )  ->  A. z  e.  (KQ `  J ) A. w  e.  ( ( Clsd `  (KQ `  J ) )  i^i 
~P z ) E. m  e.  (KQ `  J ) ( w 
C_  m  /\  (
( cls `  (KQ `  J ) ) `  m )  C_  z
) )
78 isnrm 20344 . 2  |-  ( (KQ
`  J )  e. 
Nrm 
<->  ( (KQ `  J
)  e.  Top  /\  A. z  e.  (KQ `  J ) A. w  e.  ( ( Clsd `  (KQ `  J ) )  i^i 
~P z ) E. m  e.  (KQ `  J ) ( w 
C_  m  /\  (
( cls `  (KQ `  J ) ) `  m )  C_  z
) ) )
795, 77, 78sylanbrc 669 1  |-  ( ( J  e.  (TopOn `  X )  /\  J  e.  Nrm )  ->  (KQ `  J )  e.  Nrm )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188    /\ wa 371    = wceq 1443    e. wcel 1886   A.wral 2736   E.wrex 2737   {crab 2740    i^i cin 3402    C_ wss 3403   ~Pcpw 3950   U.cuni 4197    |-> cmpt 4460   `'ccnv 4832   dom cdm 4833   ran crn 4834   "cima 4836   Fun wfun 5575    Fn wfn 5576   ` cfv 5581  (class class class)co 6288   Topctop 19910  TopOnctopon 19911   Clsdccld 20024   clsccl 20026    Cn ccn 20233   Nrmcnrm 20319  KQckq 20701
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-8 1888  ax-9 1895  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430  ax-rep 4514  ax-sep 4524  ax-nul 4533  ax-pow 4580  ax-pr 4638  ax-un 6580
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 986  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-eu 2302  df-mo 2303  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ne 2623  df-ral 2741  df-rex 2742  df-reu 2743  df-rab 2745  df-v 3046  df-sbc 3267  df-csb 3363  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-nul 3731  df-if 3881  df-pw 3952  df-sn 3968  df-pr 3970  df-op 3974  df-uni 4198  df-int 4234  df-iun 4279  df-iin 4280  df-br 4402  df-opab 4461  df-mpt 4462  df-id 4748  df-xp 4839  df-rel 4840  df-cnv 4841  df-co 4842  df-dm 4843  df-rn 4844  df-res 4845  df-ima 4846  df-iota 5545  df-fun 5583  df-fn 5584  df-f 5585  df-f1 5586  df-fo 5587  df-f1o 5588  df-fv 5589  df-ov 6291  df-oprab 6292  df-mpt2 6293  df-map 7471  df-qtop 15399  df-top 19914  df-topon 19916  df-cld 20027  df-cls 20029  df-cn 20236  df-nrm 20326  df-kq 20702
This theorem is referenced by:  kqnrm  20760
  Copyright terms: Public domain W3C validator