Metamath Proof Explorer

Theorem kqnrmlem1

Description: A Kolmogorov quotient of a normal space is normal. (Contributed by Mario Carneiro, 25-Aug-2015)

Ref Expression
Hypothesis kqval.2 
|- F = ( x e. X |-> { y e. J | x e. y } )
Assertion kqnrmlem1 
|- ( ( J e. ( TopOn ` X ) /\ J e. Nrm ) -> ( KQ ` J ) e. Nrm )

Proof

Step Hyp Ref Expression
1 kqval.2 
 |-  F = ( x e. X |-> { y e. J | x e. y } )
2 1 kqtopon 
 |-  ( J e. ( TopOn ` X ) -> ( KQ ` J ) e. ( TopOn ` ran F ) )
3 2 adantr 
 |-  ( ( J e. ( TopOn ` X ) /\ J e. Nrm ) -> ( KQ ` J ) e. ( TopOn ` ran F ) )
4 topontop 
 |-  ( ( KQ ` J ) e. ( TopOn ` ran F ) -> ( KQ ` J ) e. Top )
5 3 4 syl 
 |-  ( ( J e. ( TopOn ` X ) /\ J e. Nrm ) -> ( KQ ` J ) e. Top )
6 simplr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ J e. Nrm ) /\ ( z e. ( KQ ` J ) /\ w e. ( ( Clsd ` ( KQ ` J ) ) i^i ~P z ) ) ) -> J e. Nrm )
7 1 kqid 
 |-  ( J e. ( TopOn ` X ) -> F e. ( J Cn ( KQ ` J ) ) )
8 7 ad2antrr 
 |-  ( ( ( 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 
 |-  ( ( ( 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 
 |-  ( ( F e. ( J Cn ( KQ ` J ) ) /\ z e. ( KQ ` J ) ) -> ( `' F " z ) e. J )
11 8 9 10 syl2anc 
 |-  ( ( ( 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 simprr 
 |-  ( ( ( 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 ) )
13 12 elin1d 
 |-  ( ( ( 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 ) ) )
14 cnclima 
 |-  ( ( F e. ( J Cn ( KQ ` J ) ) /\ w e. ( Clsd ` ( KQ ` J ) ) ) -> ( `' F " w ) e. ( Clsd ` J ) )
15 8 13 14 syl2anc 
 |-  ( ( ( 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 ) )
16 12 elin2d 
 |-  ( ( ( J e. ( TopOn ` X ) /\ J e. Nrm ) /\ ( z e. ( KQ ` J ) /\ w e. ( ( Clsd ` ( KQ ` J ) ) i^i ~P z ) ) ) -> w e. ~P z )
17 elpwi 
 |-  ( w e. ~P z -> w C_ z )
18 imass2 
 |-  ( w C_ z -> ( `' F " w ) C_ ( `' F " z ) )
19 16 17 18 3syl 
 |-  ( ( ( 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 ) )
20 nrmsep3 
 |-  ( ( 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 ) ) )
21 6 11 15 19 20 syl13anc 
 |-  ( ( ( 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 ) ) )
22 simplll 
 |-  ( ( ( ( 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 ) )
23 simprl 
 |-  ( ( ( ( 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 )
24 1 kqopn 
 |-  ( ( J e. ( TopOn ` X ) /\ u e. J ) -> ( F " u ) e. ( KQ ` J ) )
25 22 23 24 syl2anc 
 |-  ( ( ( ( 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 ) )
26 simprrl 
 |-  ( ( ( ( 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 )
27 1 kqffn 
 |-  ( J e. ( TopOn ` X ) -> F Fn X )
28 fnfun 
 |-  ( F Fn X -> Fun F )
29 22 27 28 3syl 
 |-  ( ( ( ( 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 )
30 13 adantr 
 |-  ( ( ( ( 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 ) ) )
31 eqid 
 |-  U. ( KQ ` J ) = U. ( KQ ` J )
32 31 cldss 
 |-  ( w e. ( Clsd ` ( KQ ` J ) ) -> w C_ U. ( KQ ` J ) )
33 30 32 syl 
 |-  ( ( ( ( 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 ) )
34 toponuni 
 |-  ( ( KQ ` J ) e. ( TopOn ` ran F ) -> ran F = U. ( KQ ` J ) )
35 22 2 34 3syl 
 |-  ( ( ( ( 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 ) )
36 33 35 sseqtrrd 
 |-  ( ( ( ( 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 )
37 funimass1 
 |-  ( ( Fun F /\ w C_ ran F ) -> ( ( `' F " w ) C_ u -> w C_ ( F " u ) ) )
38 29 36 37 syl2anc 
 |-  ( ( ( ( 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 ) ) )
39 26 38 mpd 
 |-  ( ( ( ( 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 ) )
40 topontop 
 |-  ( J e. ( TopOn ` X ) -> J e. Top )
41 22 40 syl 
 |-  ( ( ( ( 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 )
42 elssuni 
 |-  ( u e. J -> u C_ U. J )
43 42 ad2antrl 
 |-  ( ( ( ( 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 )
44 eqid 
 |-  U. J = U. J
45 44 clscld 
 |-  ( ( J e. Top /\ u C_ U. J ) -> ( ( cls ` J ) ` u ) e. ( Clsd ` J ) )
46 41 43 45 syl2anc 
 |-  ( ( ( ( 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 ) )
47 1 kqcld 
 |-  ( ( J e. ( TopOn ` X ) /\ ( ( cls ` J ) ` u ) e. ( Clsd ` J ) ) -> ( F " ( ( cls ` J ) ` u ) ) e. ( Clsd ` ( KQ ` J ) ) )
48 22 46 47 syl2anc 
 |-  ( ( ( ( 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 ) ) )
49 44 sscls 
 |-  ( ( J e. Top /\ u C_ U. J ) -> u C_ ( ( cls ` J ) ` u ) )
50 41 43 49 syl2anc 
 |-  ( ( ( ( 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 ) )
51 imass2 
 |-  ( u C_ ( ( cls ` J ) ` u ) -> ( F " u ) C_ ( F " ( ( cls ` J ) ` u ) ) )
52 50 51 syl 
 |-  ( ( ( ( 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 ) ) )
53 31 clsss2 
 |-  ( ( ( 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 ) ) )
54 48 52 53 syl2anc 
 |-  ( ( ( ( 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 ) ) )
55 simprrr 
 |-  ( ( ( ( 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 ) )
56 44 clsss3 
 |-  ( ( J e. Top /\ u C_ U. J ) -> ( ( cls ` J ) ` u ) C_ U. J )
57 41 43 56 syl2anc 
 |-  ( ( ( ( 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 )
58 fndm 
 |-  ( F Fn X -> dom F = X )
59 22 27 58 3syl 
 |-  ( ( ( ( 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 )
60 toponuni 
 |-  ( J e. ( TopOn ` X ) -> X = U. J )
61 22 60 syl 
 |-  ( ( ( ( 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 )
62 59 61 eqtrd 
 |-  ( ( ( ( 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 )
63 57 62 sseqtrrd 
 |-  ( ( ( ( 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 )
64 funimass3 
 |-  ( ( Fun F /\ ( ( cls ` J ) ` u ) C_ dom F ) -> ( ( F " ( ( cls ` J ) ` u ) ) C_ z <-> ( ( cls ` J ) ` u ) C_ ( `' F " z ) ) )
65 29 63 64 syl2anc 
 |-  ( ( ( ( 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 ) ) )
66 55 65 mpbird 
 |-  ( ( ( ( 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 )
67 54 66 sstrd 
 |-  ( ( ( ( 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 )
68 sseq2 
 |-  ( m = ( F " u ) -> ( w C_ m <-> w C_ ( F " u ) ) )
69 fveq2 
 |-  ( m = ( F " u ) -> ( ( cls ` ( KQ ` J ) ) ` m ) = ( ( cls ` ( KQ ` J ) ) ` ( F " u ) ) )
70 69 sseq1d 
 |-  ( m = ( F " u ) -> ( ( ( cls ` ( KQ ` J ) ) ` m ) C_ z <-> ( ( cls ` ( KQ ` J ) ) ` ( F " u ) ) C_ z ) )
71 68 70 anbi12d 
 |-  ( m = ( F " u ) -> ( ( w C_ m /\ ( ( cls ` ( KQ ` J ) ) ` m ) C_ z ) <-> ( w C_ ( F " u ) /\ ( ( cls ` ( KQ ` J ) ) ` ( F " u ) ) C_ z ) ) )
72 71 rspcev 
 |-  ( ( ( 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 ) )
73 25 39 67 72 syl12anc 
 |-  ( ( ( ( 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 ) )
74 21 73 rexlimddv 
 |-  ( ( ( 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 ) )
75 74 ralrimivva 
 |-  ( ( 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 ) )
76 isnrm 
 |-  ( ( 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 ) ) )
77 5 75 76 sylanbrc 
 |-  ( ( J e. ( TopOn ` X ) /\ J e. Nrm ) -> ( KQ ` J ) e. Nrm )