Metamath Proof Explorer

Theorem kqnrmlem2

Description: If the Kolmogorov quotient of a space is normal then so is the original space. (Contributed by Mario Carneiro, 25-Aug-2015)

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

Proof

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