MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  kqnrmlem1 Structured version   Visualization version   Unicode version
Theorem kqnrmlem1 21546
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 21530 . . . 4 |- ( J e. (TopOn ` X ) -> (KQ ` J ) e. (TopOn ` ran F ) )
32adantr 481 . . 3 |- ( ( J e. (TopOn ` X ) /\ J e. Nrm ) -> (KQ ` J ) e. (TopOn ` ran F ) )
4 topontop 20718 . . 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 792 . . . . 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 21531 . . . . . . 7 |- ( J e. (TopOn ` X ) -> F e. ( J Cn (KQ ` J ) ) )
87ad2antrr 762 . . . . . 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 794 . . . . . 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 21069 . . . . . 6 |- ( ( F e. ( J Cn (KQ ` J ) ) /\ z e. (KQ ` J ) ) -> ( `' F " z ) e. J )
118, 9, 10syl2anc 693 . . . . 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 3833 . . . . . . 7 |- ( ( Clsd ` (KQ ` J ) ) i^i ~P z ) C_ ( Clsd ` (KQ ` J ) )
13 simprr 796 . . . . . . 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 3601 . . . . . 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 21072 . . . . . 6 |- ( ( F e. ( J Cn (KQ ` J ) ) /\ w e. ( Clsd ` (KQ ` J ) ) ) -> ( `' F " w ) e. ( Clsd ` J ) )
168, 14, 15syl2anc 693 . . . . 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 3834 . . . . . . 7 |- ( ( Clsd ` (KQ ` J ) ) i^i ~P z ) C_ ~P z
1817, 13sseldi 3601 . . . . . 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 4168 . . . . . 6 |- ( w e. ~P z -> w C_ z )
20 imass2 5501 . . . . . 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 21159 . . . . 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 1328 . . . 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 798 . . . . . 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 794 . . . . . 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 21537 . . . . . 6 |- ( ( J e. (TopOn ` X ) /\ u e. J ) -> ( F " u ) e. (KQ ` J ) )
2724, 25, 26syl2anc 693 . . . . 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 804 . . . . . 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 21528 . . . . . . . 8 |- ( J e. (TopOn ` X ) -> F Fn X )
30 fnfun 5988 . . . . . . . 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 481 . . . . . . . . 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 2622 . . . . . . . . . 10 |- U. (KQ ` J ) = U. (KQ ` J )
3433cldss 20833 . . . . . . . . 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 20719 . . . . . . . . 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 3642 . . . . . . 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 5971 . . . . . . 7 |- ( ( Fun F /\ w C_ ran F ) -> ( ( `' F " w ) C_ u -> w C_ ( F " u ) ) )
4031, 38, 39syl2anc 693 . . . . . 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 20718 . . . . . . . . . 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 4467 . . . . . . . . . 10 |- ( u e. J -> u C_ U. J )
4544ad2antrl 764 . . . . . . . . 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 2622 . . . . . . . . . 10 |- U. J = U. J
4746clscld 20851 . . . . . . . . 9 |- ( ( J e. Top /\ u C_ U. J ) -> ( ( cls ` J ) ` u ) e. ( Clsd ` J ) )
4843, 45, 47syl2anc 693 . . . . . . . 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 21538 . . . . . . . 8 |- ( ( J e. (TopOn ` X ) /\ ( ( cls ` J ) ` u ) e. ( Clsd ` J ) ) -> ( F " ( ( cls ` J ) ` u ) ) e. ( Clsd ` (KQ ` J ) ) )
5024, 48, 49syl2anc 693 . . . . . . 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 20860 . . . . . . . . 9 |- ( ( J e. Top /\ u C_ U. J ) -> u C_ ( ( cls ` J ) ` u ) )
5243, 45, 51syl2anc 693 . . . . . . . 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 5501 . . . . . . . 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 20876 . . . . . . 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 693 . . . . . 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 805 . . . . . . 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 20863 . . . . . . . . . 10 |- ( ( J e. Top /\ u C_ U. J ) -> ( ( cls ` J ) ` u ) C_ U. J )
5943, 45, 58syl2anc 693 . . . . . . . . 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 5990 . . . . . . . . . . 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 20719 . . . . . . . . . . 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 2656 . . . . . . . . 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 3642 . . . . . . . 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 6333 . . . . . . . 8 |- ( ( Fun F /\ ( ( cls ` J ) ` u ) C_ dom F ) -> ( ( F " ( ( cls ` J ) ` u ) ) C_ z <-> ( ( cls ` J ) ` u ) C_ ( `' F " z ) ) )
6731, 65, 66syl2anc 693 . . . . . . 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 247 . . . . . 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 3613 . . . . 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 3627 . . . . . . 7 |- ( m = ( F " u ) -> ( w C_ m <-> w C_ ( F " u ) ) )
71 fveq2 6191 . . . . . . . 8 |- ( m = ( F " u ) -> ( ( cls ` (KQ ` J ) ) ` m ) = ( ( cls ` (KQ ` J ) ) ` ( F " u ) ) )
7271sseq1d 3632 . . . . . . 7 |- ( m = ( F " u ) -> ( ( ( cls ` (KQ ` J ) ) ` m ) C_ z <-> ( ( cls ` (KQ ` J ) ) ` ( F " u ) ) C_ z ) )
7370, 72anbi12d 747 . . . . . 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 3309 . . . . 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 1324 . . . 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 3035 . . 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 2971 . 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 21139 . 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 698 1 |- ( ( J e. (TopOn ` X ) /\ J e. Nrm ) -> (KQ ` J ) e. Nrm )
Colors of variables: wff setvar class
Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   = wceq 1483   e. wcel 1990   A.wral 2912   E.wrex 2913   {crab 2916   i^i cin 3573   C_ wss 3574   ~Pcpw 4158   U.cuni 4436   |-> cmpt 4729   `'ccnv 5113   dom cdm 5114   ran crn 5115   "cima 5117   Fun wfun 5882   Fn wfn 5883   ` cfv 5888  (class class class)co 6650   Topctop 20698  TopOnctopon 20715   Clsdccld 20820   clsccl 20822   Cn ccn 21028   Nrmcnrm 21114  KQckq 21496
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-iin 4523  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-map 7859  df-qtop 16167  df-top 20699  df-topon 20716  df-cld 20823  df-cls 20825  df-cn 21031  df-nrm 21121  df-kq 21497
This theorem is referenced by:  kqnrm  21555
  Copyright terms: Public domain W3C validator