Metamath Proof Explorer

Theorem kqreglem2

Description: If the Kolmogorov quotient of a space is regular 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 kqreglem2 
|- ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Reg ) -> J e. Reg )

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. Reg ) -> J e. Top )
4 simplr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Reg ) /\ ( z e. J /\ w e. z ) ) -> ( KQ ` J ) e. Reg )
5 simpll 
 |-  ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Reg ) /\ ( z e. J /\ w e. z ) ) -> J e. ( TopOn ` X ) )
6 simprl 
 |-  ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Reg ) /\ ( z e. J /\ w e. 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. Reg ) /\ ( z e. J /\ w e. z ) ) -> ( F " z ) e. ( KQ ` J ) )
9 simprr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Reg ) /\ ( z e. J /\ w e. z ) ) -> w e. z )
10 toponss 
 |-  ( ( J e. ( TopOn ` X ) /\ z e. J ) -> z C_ X )
11 5 6 10 syl2anc 
 |-  ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Reg ) /\ ( z e. J /\ w e. z ) ) -> z C_ X )
12 11 9 sseldd 
 |-  ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Reg ) /\ ( z e. J /\ w e. z ) ) -> w e. X )
13 1 kqfvima 
 |-  ( ( J e. ( TopOn ` X ) /\ z e. J /\ w e. X ) -> ( w e. z <-> ( F ` w ) e. ( F " z ) ) )
14 5 6 12 13 syl3anc 
 |-  ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Reg ) /\ ( z e. J /\ w e. z ) ) -> ( w e. z <-> ( F ` w ) e. ( F " z ) ) )
15 9 14 mpbid 
 |-  ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Reg ) /\ ( z e. J /\ w e. z ) ) -> ( F ` w ) e. ( F " z ) )
16 regsep 
 |-  ( ( ( KQ ` J ) e. Reg /\ ( F " z ) e. ( KQ ` J ) /\ ( F ` w ) e. ( F " z ) ) -> E. n e. ( KQ ` J ) ( ( F ` w ) e. n /\ ( ( cls ` ( KQ ` J ) ) ` n ) C_ ( F " z ) ) )
17 4 8 15 16 syl3anc 
 |-  ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Reg ) /\ ( z e. J /\ w e. z ) ) -> E. n e. ( KQ ` J ) ( ( F ` w ) e. n /\ ( ( cls ` ( KQ ` J ) ) ` n ) C_ ( F " z ) ) )
18 5 adantr 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Reg ) /\ ( z e. J /\ w e. z ) ) /\ ( n e. ( KQ ` J ) /\ ( ( F ` w ) e. n /\ ( ( cls ` ( KQ ` J ) ) ` n ) C_ ( F " z ) ) ) ) -> J e. ( TopOn ` X ) )
19 1 kqid 
 |-  ( J e. ( TopOn ` X ) -> F e. ( J Cn ( KQ ` J ) ) )
20 18 19 syl 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Reg ) /\ ( z e. J /\ w e. z ) ) /\ ( n e. ( KQ ` J ) /\ ( ( F ` w ) e. n /\ ( ( cls ` ( KQ ` J ) ) ` n ) C_ ( F " z ) ) ) ) -> F e. ( J Cn ( KQ ` J ) ) )
21 simprl 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Reg ) /\ ( z e. J /\ w e. z ) ) /\ ( n e. ( KQ ` J ) /\ ( ( F ` w ) e. n /\ ( ( cls ` ( KQ ` J ) ) ` n ) C_ ( F " z ) ) ) ) -> n e. ( KQ ` J ) )
22 cnima 
 |-  ( ( F e. ( J Cn ( KQ ` J ) ) /\ n e. ( KQ ` J ) ) -> ( `' F " n ) e. J )
23 20 21 22 syl2anc 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Reg ) /\ ( z e. J /\ w e. z ) ) /\ ( n e. ( KQ ` J ) /\ ( ( F ` w ) e. n /\ ( ( cls ` ( KQ ` J ) ) ` n ) C_ ( F " z ) ) ) ) -> ( `' F " n ) e. J )
24 12 adantr 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Reg ) /\ ( z e. J /\ w e. z ) ) /\ ( n e. ( KQ ` J ) /\ ( ( F ` w ) e. n /\ ( ( cls ` ( KQ ` J ) ) ` n ) C_ ( F " z ) ) ) ) -> w e. X )
25 simprrl 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Reg ) /\ ( z e. J /\ w e. z ) ) /\ ( n e. ( KQ ` J ) /\ ( ( F ` w ) e. n /\ ( ( cls ` ( KQ ` J ) ) ` n ) C_ ( F " z ) ) ) ) -> ( F ` w ) e. n )
26 1 kqffn 
 |-  ( J e. ( TopOn ` X ) -> F Fn X )
27 elpreima 
 |-  ( F Fn X -> ( w e. ( `' F " n ) <-> ( w e. X /\ ( F ` w ) e. n ) ) )
28 18 26 27 3syl 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Reg ) /\ ( z e. J /\ w e. z ) ) /\ ( n e. ( KQ ` J ) /\ ( ( F ` w ) e. n /\ ( ( cls ` ( KQ ` J ) ) ` n ) C_ ( F " z ) ) ) ) -> ( w e. ( `' F " n ) <-> ( w e. X /\ ( F ` w ) e. n ) ) )
29 24 25 28 mpbir2and 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Reg ) /\ ( z e. J /\ w e. z ) ) /\ ( n e. ( KQ ` J ) /\ ( ( F ` w ) e. n /\ ( ( cls ` ( KQ ` J ) ) ` n ) C_ ( F " z ) ) ) ) -> w e. ( `' F " n ) )
30 1 kqtopon 
 |-  ( J e. ( TopOn ` X ) -> ( KQ ` J ) e. ( TopOn ` ran F ) )
31 topontop 
 |-  ( ( KQ ` J ) e. ( TopOn ` ran F ) -> ( KQ ` J ) e. Top )
32 18 30 31 3syl 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Reg ) /\ ( z e. J /\ w e. z ) ) /\ ( n e. ( KQ ` J ) /\ ( ( F ` w ) e. n /\ ( ( cls ` ( KQ ` J ) ) ` n ) C_ ( F " z ) ) ) ) -> ( KQ ` J ) e. Top )
33 elssuni 
 |-  ( n e. ( KQ ` J ) -> n C_ U. ( KQ ` J ) )
34 33 ad2antrl 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Reg ) /\ ( z e. J /\ w e. z ) ) /\ ( n e. ( KQ ` J ) /\ ( ( F ` w ) e. n /\ ( ( cls ` ( KQ ` J ) ) ` n ) C_ ( F " z ) ) ) ) -> n C_ U. ( KQ ` J ) )
35 eqid 
 |-  U. ( KQ ` J ) = U. ( KQ ` J )
36 35 clscld 
 |-  ( ( ( KQ ` J ) e. Top /\ n C_ U. ( KQ ` J ) ) -> ( ( cls ` ( KQ ` J ) ) ` n ) e. ( Clsd ` ( KQ ` J ) ) )
37 32 34 36 syl2anc 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Reg ) /\ ( z e. J /\ w e. z ) ) /\ ( n e. ( KQ ` J ) /\ ( ( F ` w ) e. n /\ ( ( cls ` ( KQ ` J ) ) ` n ) C_ ( F " z ) ) ) ) -> ( ( cls ` ( KQ ` J ) ) ` n ) e. ( Clsd ` ( KQ ` J ) ) )
38 cnclima 
 |-  ( ( F e. ( J Cn ( KQ ` J ) ) /\ ( ( cls ` ( KQ ` J ) ) ` n ) e. ( Clsd ` ( KQ ` J ) ) ) -> ( `' F " ( ( cls ` ( KQ ` J ) ) ` n ) ) e. ( Clsd ` J ) )
39 20 37 38 syl2anc 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Reg ) /\ ( z e. J /\ w e. z ) ) /\ ( n e. ( KQ ` J ) /\ ( ( F ` w ) e. n /\ ( ( cls ` ( KQ ` J ) ) ` n ) C_ ( F " z ) ) ) ) -> ( `' F " ( ( cls ` ( KQ ` J ) ) ` n ) ) e. ( Clsd ` J ) )
40 35 sscls 
 |-  ( ( ( KQ ` J ) e. Top /\ n C_ U. ( KQ ` J ) ) -> n C_ ( ( cls ` ( KQ ` J ) ) ` n ) )
41 32 34 40 syl2anc 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Reg ) /\ ( z e. J /\ w e. z ) ) /\ ( n e. ( KQ ` J ) /\ ( ( F ` w ) e. n /\ ( ( cls ` ( KQ ` J ) ) ` n ) C_ ( F " z ) ) ) ) -> n C_ ( ( cls ` ( KQ ` J ) ) ` n ) )
42 imass2 
 |-  ( n C_ ( ( cls ` ( KQ ` J ) ) ` n ) -> ( `' F " n ) C_ ( `' F " ( ( cls ` ( KQ ` J ) ) ` n ) ) )
43 41 42 syl 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Reg ) /\ ( z e. J /\ w e. z ) ) /\ ( n e. ( KQ ` J ) /\ ( ( F ` w ) e. n /\ ( ( cls ` ( KQ ` J ) ) ` n ) C_ ( F " z ) ) ) ) -> ( `' F " n ) C_ ( `' F " ( ( cls ` ( KQ ` J ) ) ` n ) ) )
44 eqid 
 |-  U. J = U. J
45 44 clsss2 
 |-  ( ( ( `' F " ( ( cls ` ( KQ ` J ) ) ` n ) ) e. ( Clsd ` J ) /\ ( `' F " n ) C_ ( `' F " ( ( cls ` ( KQ ` J ) ) ` n ) ) ) -> ( ( cls ` J ) ` ( `' F " n ) ) C_ ( `' F " ( ( cls ` ( KQ ` J ) ) ` n ) ) )
46 39 43 45 syl2anc 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Reg ) /\ ( z e. J /\ w e. z ) ) /\ ( n e. ( KQ ` J ) /\ ( ( F ` w ) e. n /\ ( ( cls ` ( KQ ` J ) ) ` n ) C_ ( F " z ) ) ) ) -> ( ( cls ` J ) ` ( `' F " n ) ) C_ ( `' F " ( ( cls ` ( KQ ` J ) ) ` n ) ) )
47 simprrr 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Reg ) /\ ( z e. J /\ w e. z ) ) /\ ( n e. ( KQ ` J ) /\ ( ( F ` w ) e. n /\ ( ( cls ` ( KQ ` J ) ) ` n ) C_ ( F " z ) ) ) ) -> ( ( cls ` ( KQ ` J ) ) ` n ) C_ ( F " z ) )
48 imass2 
 |-  ( ( ( cls ` ( KQ ` J ) ) ` n ) C_ ( F " z ) -> ( `' F " ( ( cls ` ( KQ ` J ) ) ` n ) ) C_ ( `' F " ( F " z ) ) )
49 47 48 syl 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Reg ) /\ ( z e. J /\ w e. z ) ) /\ ( n e. ( KQ ` J ) /\ ( ( F ` w ) e. n /\ ( ( cls ` ( KQ ` J ) ) ` n ) C_ ( F " z ) ) ) ) -> ( `' F " ( ( cls ` ( KQ ` J ) ) ` n ) ) C_ ( `' F " ( F " z ) ) )
50 6 adantr 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Reg ) /\ ( z e. J /\ w e. z ) ) /\ ( n e. ( KQ ` J ) /\ ( ( F ` w ) e. n /\ ( ( cls ` ( KQ ` J ) ) ` n ) C_ ( F " z ) ) ) ) -> z e. J )
51 1 kqsat 
 |-  ( ( J e. ( TopOn ` X ) /\ z e. J ) -> ( `' F " ( F " z ) ) = z )
52 18 50 51 syl2anc 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Reg ) /\ ( z e. J /\ w e. z ) ) /\ ( n e. ( KQ ` J ) /\ ( ( F ` w ) e. n /\ ( ( cls ` ( KQ ` J ) ) ` n ) C_ ( F " z ) ) ) ) -> ( `' F " ( F " z ) ) = z )
53 49 52 sseqtrd 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Reg ) /\ ( z e. J /\ w e. z ) ) /\ ( n e. ( KQ ` J ) /\ ( ( F ` w ) e. n /\ ( ( cls ` ( KQ ` J ) ) ` n ) C_ ( F " z ) ) ) ) -> ( `' F " ( ( cls ` ( KQ ` J ) ) ` n ) ) C_ z )
54 46 53 sstrd 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Reg ) /\ ( z e. J /\ w e. z ) ) /\ ( n e. ( KQ ` J ) /\ ( ( F ` w ) e. n /\ ( ( cls ` ( KQ ` J ) ) ` n ) C_ ( F " z ) ) ) ) -> ( ( cls ` J ) ` ( `' F " n ) ) C_ z )
55 eleq2 
 |-  ( m = ( `' F " n ) -> ( w e. m <-> w e. ( `' F " n ) ) )
56 fveq2 
 |-  ( m = ( `' F " n ) -> ( ( cls ` J ) ` m ) = ( ( cls ` J ) ` ( `' F " n ) ) )
57 56 sseq1d 
 |-  ( m = ( `' F " n ) -> ( ( ( cls ` J ) ` m ) C_ z <-> ( ( cls ` J ) ` ( `' F " n ) ) C_ z ) )
58 55 57 anbi12d 
 |-  ( m = ( `' F " n ) -> ( ( w e. m /\ ( ( cls ` J ) ` m ) C_ z ) <-> ( w e. ( `' F " n ) /\ ( ( cls ` J ) ` ( `' F " n ) ) C_ z ) ) )
59 58 rspcev 
 |-  ( ( ( `' F " n ) e. J /\ ( w e. ( `' F " n ) /\ ( ( cls ` J ) ` ( `' F " n ) ) C_ z ) ) -> E. m e. J ( w e. m /\ ( ( cls ` J ) ` m ) C_ z ) )
60 23 29 54 59 syl12anc 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Reg ) /\ ( z e. J /\ w e. z ) ) /\ ( n e. ( KQ ` J ) /\ ( ( F ` w ) e. n /\ ( ( cls ` ( KQ ` J ) ) ` n ) C_ ( F " z ) ) ) ) -> E. m e. J ( w e. m /\ ( ( cls ` J ) ` m ) C_ z ) )
61 17 60 rexlimddv 
 |-  ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Reg ) /\ ( z e. J /\ w e. z ) ) -> E. m e. J ( w e. m /\ ( ( cls ` J ) ` m ) C_ z ) )
62 61 ralrimivva 
 |-  ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Reg ) -> A. z e. J A. w e. z E. m e. J ( w e. m /\ ( ( cls ` J ) ` m ) C_ z ) )
63 isreg 
 |-  ( J e. Reg <-> ( J e. Top /\ A. z e. J A. w e. z E. m e. J ( w e. m /\ ( ( cls ` J ) ` m ) C_ z ) ) )
64 3 62 63 sylanbrc 
 |-  ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Reg ) -> J e. Reg )