Metamath Proof Explorer

Theorem kqreglem1

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

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

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. Reg ) -> ( 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. Reg ) -> ( KQ ` J ) e. Top )
6 toponss 
 |-  ( ( ( KQ ` J ) e. ( TopOn ` ran F ) /\ a e. ( KQ ` J ) ) -> a C_ ran F )
7 3 6 sylan 
 |-  ( ( ( J e. ( TopOn ` X ) /\ J e. Reg ) /\ a e. ( KQ ` J ) ) -> a C_ ran F )
8 7 sselda 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ J e. Reg ) /\ a e. ( KQ ` J ) ) /\ b e. a ) -> b e. ran F )
9 1 kqffn 
 |-  ( J e. ( TopOn ` X ) -> F Fn X )
10 9 ad3antrrr 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ J e. Reg ) /\ a e. ( KQ ` J ) ) /\ b e. a ) -> F Fn X )
11 fvelrnb 
 |-  ( F Fn X -> ( b e. ran F <-> E. z e. X ( F ` z ) = b ) )
12 10 11 syl 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ J e. Reg ) /\ a e. ( KQ ` J ) ) /\ b e. a ) -> ( b e. ran F <-> E. z e. X ( F ` z ) = b ) )
13 8 12 mpbid 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ J e. Reg ) /\ a e. ( KQ ` J ) ) /\ b e. a ) -> E. z e. X ( F ` z ) = b )
14 simpllr 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ J e. Reg ) /\ a e. ( KQ ` J ) ) /\ ( z e. X /\ ( F ` z ) e. a ) ) -> J e. Reg )
15 1 kqid 
 |-  ( J e. ( TopOn ` X ) -> F e. ( J Cn ( KQ ` J ) ) )
16 15 ad3antrrr 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ J e. Reg ) /\ a e. ( KQ ` J ) ) /\ ( z e. X /\ ( F ` z ) e. a ) ) -> F e. ( J Cn ( KQ ` J ) ) )
17 simplr 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ J e. Reg ) /\ a e. ( KQ ` J ) ) /\ ( z e. X /\ ( F ` z ) e. a ) ) -> a e. ( KQ ` J ) )
18 cnima 
 |-  ( ( F e. ( J Cn ( KQ ` J ) ) /\ a e. ( KQ ` J ) ) -> ( `' F " a ) e. J )
19 16 17 18 syl2anc 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ J e. Reg ) /\ a e. ( KQ ` J ) ) /\ ( z e. X /\ ( F ` z ) e. a ) ) -> ( `' F " a ) e. J )
20 9 adantr 
 |-  ( ( J e. ( TopOn ` X ) /\ J e. Reg ) -> F Fn X )
21 20 adantr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ J e. Reg ) /\ a e. ( KQ ` J ) ) -> F Fn X )
22 elpreima 
 |-  ( F Fn X -> ( z e. ( `' F " a ) <-> ( z e. X /\ ( F ` z ) e. a ) ) )
23 21 22 syl 
 |-  ( ( ( J e. ( TopOn ` X ) /\ J e. Reg ) /\ a e. ( KQ ` J ) ) -> ( z e. ( `' F " a ) <-> ( z e. X /\ ( F ` z ) e. a ) ) )
24 23 biimpar 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ J e. Reg ) /\ a e. ( KQ ` J ) ) /\ ( z e. X /\ ( F ` z ) e. a ) ) -> z e. ( `' F " a ) )
25 regsep 
 |-  ( ( J e. Reg /\ ( `' F " a ) e. J /\ z e. ( `' F " a ) ) -> E. w e. J ( z e. w /\ ( ( cls ` J ) ` w ) C_ ( `' F " a ) ) )
26 14 19 24 25 syl3anc 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ J e. Reg ) /\ a e. ( KQ ` J ) ) /\ ( z e. X /\ ( F ` z ) e. a ) ) -> E. w e. J ( z e. w /\ ( ( cls ` J ) ` w ) C_ ( `' F " a ) ) )
27 simp-4l 
 |-  ( ( ( ( ( J e. ( TopOn ` X ) /\ J e. Reg ) /\ a e. ( KQ ` J ) ) /\ ( z e. X /\ ( F ` z ) e. a ) ) /\ ( w e. J /\ ( z e. w /\ ( ( cls ` J ) ` w ) C_ ( `' F " a ) ) ) ) -> J e. ( TopOn ` X ) )
28 simprl 
 |-  ( ( ( ( ( J e. ( TopOn ` X ) /\ J e. Reg ) /\ a e. ( KQ ` J ) ) /\ ( z e. X /\ ( F ` z ) e. a ) ) /\ ( w e. J /\ ( z e. w /\ ( ( cls ` J ) ` w ) C_ ( `' F " a ) ) ) ) -> w e. J )
29 1 kqopn 
 |-  ( ( J e. ( TopOn ` X ) /\ w e. J ) -> ( F " w ) e. ( KQ ` J ) )
30 27 28 29 syl2anc 
 |-  ( ( ( ( ( J e. ( TopOn ` X ) /\ J e. Reg ) /\ a e. ( KQ ` J ) ) /\ ( z e. X /\ ( F ` z ) e. a ) ) /\ ( w e. J /\ ( z e. w /\ ( ( cls ` J ) ` w ) C_ ( `' F " a ) ) ) ) -> ( F " w ) e. ( KQ ` J ) )
31 simprrl 
 |-  ( ( ( ( ( J e. ( TopOn ` X ) /\ J e. Reg ) /\ a e. ( KQ ` J ) ) /\ ( z e. X /\ ( F ` z ) e. a ) ) /\ ( w e. J /\ ( z e. w /\ ( ( cls ` J ) ` w ) C_ ( `' F " a ) ) ) ) -> z e. w )
32 simplrl 
 |-  ( ( ( ( ( J e. ( TopOn ` X ) /\ J e. Reg ) /\ a e. ( KQ ` J ) ) /\ ( z e. X /\ ( F ` z ) e. a ) ) /\ ( w e. J /\ ( z e. w /\ ( ( cls ` J ) ` w ) C_ ( `' F " a ) ) ) ) -> z e. X )
33 1 kqfvima 
 |-  ( ( J e. ( TopOn ` X ) /\ w e. J /\ z e. X ) -> ( z e. w <-> ( F ` z ) e. ( F " w ) ) )
34 27 28 32 33 syl3anc 
 |-  ( ( ( ( ( J e. ( TopOn ` X ) /\ J e. Reg ) /\ a e. ( KQ ` J ) ) /\ ( z e. X /\ ( F ` z ) e. a ) ) /\ ( w e. J /\ ( z e. w /\ ( ( cls ` J ) ` w ) C_ ( `' F " a ) ) ) ) -> ( z e. w <-> ( F ` z ) e. ( F " w ) ) )
35 31 34 mpbid 
 |-  ( ( ( ( ( J e. ( TopOn ` X ) /\ J e. Reg ) /\ a e. ( KQ ` J ) ) /\ ( z e. X /\ ( F ` z ) e. a ) ) /\ ( w e. J /\ ( z e. w /\ ( ( cls ` J ) ` w ) C_ ( `' F " a ) ) ) ) -> ( F ` z ) e. ( F " w ) )
36 topontop 
 |-  ( J e. ( TopOn ` X ) -> J e. Top )
37 27 36 syl 
 |-  ( ( ( ( ( J e. ( TopOn ` X ) /\ J e. Reg ) /\ a e. ( KQ ` J ) ) /\ ( z e. X /\ ( F ` z ) e. a ) ) /\ ( w e. J /\ ( z e. w /\ ( ( cls ` J ) ` w ) C_ ( `' F " a ) ) ) ) -> J e. Top )
38 elssuni 
 |-  ( w e. J -> w C_ U. J )
39 38 ad2antrl 
 |-  ( ( ( ( ( J e. ( TopOn ` X ) /\ J e. Reg ) /\ a e. ( KQ ` J ) ) /\ ( z e. X /\ ( F ` z ) e. a ) ) /\ ( w e. J /\ ( z e. w /\ ( ( cls ` J ) ` w ) C_ ( `' F " a ) ) ) ) -> w C_ U. J )
40 eqid 
 |-  U. J = U. J
41 40 clscld 
 |-  ( ( J e. Top /\ w C_ U. J ) -> ( ( cls ` J ) ` w ) e. ( Clsd ` J ) )
42 37 39 41 syl2anc 
 |-  ( ( ( ( ( J e. ( TopOn ` X ) /\ J e. Reg ) /\ a e. ( KQ ` J ) ) /\ ( z e. X /\ ( F ` z ) e. a ) ) /\ ( w e. J /\ ( z e. w /\ ( ( cls ` J ) ` w ) C_ ( `' F " a ) ) ) ) -> ( ( cls ` J ) ` w ) e. ( Clsd ` J ) )
43 1 kqcld 
 |-  ( ( J e. ( TopOn ` X ) /\ ( ( cls ` J ) ` w ) e. ( Clsd ` J ) ) -> ( F " ( ( cls ` J ) ` w ) ) e. ( Clsd ` ( KQ ` J ) ) )
44 27 42 43 syl2anc 
 |-  ( ( ( ( ( J e. ( TopOn ` X ) /\ J e. Reg ) /\ a e. ( KQ ` J ) ) /\ ( z e. X /\ ( F ` z ) e. a ) ) /\ ( w e. J /\ ( z e. w /\ ( ( cls ` J ) ` w ) C_ ( `' F " a ) ) ) ) -> ( F " ( ( cls ` J ) ` w ) ) e. ( Clsd ` ( KQ ` J ) ) )
45 40 sscls 
 |-  ( ( J e. Top /\ w C_ U. J ) -> w C_ ( ( cls ` J ) ` w ) )
46 37 39 45 syl2anc 
 |-  ( ( ( ( ( J e. ( TopOn ` X ) /\ J e. Reg ) /\ a e. ( KQ ` J ) ) /\ ( z e. X /\ ( F ` z ) e. a ) ) /\ ( w e. J /\ ( z e. w /\ ( ( cls ` J ) ` w ) C_ ( `' F " a ) ) ) ) -> w C_ ( ( cls ` J ) ` w ) )
47 imass2 
 |-  ( w C_ ( ( cls ` J ) ` w ) -> ( F " w ) C_ ( F " ( ( cls ` J ) ` w ) ) )
48 46 47 syl 
 |-  ( ( ( ( ( J e. ( TopOn ` X ) /\ J e. Reg ) /\ a e. ( KQ ` J ) ) /\ ( z e. X /\ ( F ` z ) e. a ) ) /\ ( w e. J /\ ( z e. w /\ ( ( cls ` J ) ` w ) C_ ( `' F " a ) ) ) ) -> ( F " w ) C_ ( F " ( ( cls ` J ) ` w ) ) )
49 eqid 
 |-  U. ( KQ ` J ) = U. ( KQ ` J )
50 49 clsss2 
 |-  ( ( ( F " ( ( cls ` J ) ` w ) ) e. ( Clsd ` ( KQ ` J ) ) /\ ( F " w ) C_ ( F " ( ( cls ` J ) ` w ) ) ) -> ( ( cls ` ( KQ ` J ) ) ` ( F " w ) ) C_ ( F " ( ( cls ` J ) ` w ) ) )
51 44 48 50 syl2anc 
 |-  ( ( ( ( ( J e. ( TopOn ` X ) /\ J e. Reg ) /\ a e. ( KQ ` J ) ) /\ ( z e. X /\ ( F ` z ) e. a ) ) /\ ( w e. J /\ ( z e. w /\ ( ( cls ` J ) ` w ) C_ ( `' F " a ) ) ) ) -> ( ( cls ` ( KQ ` J ) ) ` ( F " w ) ) C_ ( F " ( ( cls ` J ) ` w ) ) )
52 20 ad3antrrr 
 |-  ( ( ( ( ( J e. ( TopOn ` X ) /\ J e. Reg ) /\ a e. ( KQ ` J ) ) /\ ( z e. X /\ ( F ` z ) e. a ) ) /\ ( w e. J /\ ( z e. w /\ ( ( cls ` J ) ` w ) C_ ( `' F " a ) ) ) ) -> F Fn X )
53 fnfun 
 |-  ( F Fn X -> Fun F )
54 52 53 syl 
 |-  ( ( ( ( ( J e. ( TopOn ` X ) /\ J e. Reg ) /\ a e. ( KQ ` J ) ) /\ ( z e. X /\ ( F ` z ) e. a ) ) /\ ( w e. J /\ ( z e. w /\ ( ( cls ` J ) ` w ) C_ ( `' F " a ) ) ) ) -> Fun F )
55 simprrr 
 |-  ( ( ( ( ( J e. ( TopOn ` X ) /\ J e. Reg ) /\ a e. ( KQ ` J ) ) /\ ( z e. X /\ ( F ` z ) e. a ) ) /\ ( w e. J /\ ( z e. w /\ ( ( cls ` J ) ` w ) C_ ( `' F " a ) ) ) ) -> ( ( cls ` J ) ` w ) C_ ( `' F " a ) )
56 funimass2 
 |-  ( ( Fun F /\ ( ( cls ` J ) ` w ) C_ ( `' F " a ) ) -> ( F " ( ( cls ` J ) ` w ) ) C_ a )
57 54 55 56 syl2anc 
 |-  ( ( ( ( ( J e. ( TopOn ` X ) /\ J e. Reg ) /\ a e. ( KQ ` J ) ) /\ ( z e. X /\ ( F ` z ) e. a ) ) /\ ( w e. J /\ ( z e. w /\ ( ( cls ` J ) ` w ) C_ ( `' F " a ) ) ) ) -> ( F " ( ( cls ` J ) ` w ) ) C_ a )
58 51 57 sstrd 
 |-  ( ( ( ( ( J e. ( TopOn ` X ) /\ J e. Reg ) /\ a e. ( KQ ` J ) ) /\ ( z e. X /\ ( F ` z ) e. a ) ) /\ ( w e. J /\ ( z e. w /\ ( ( cls ` J ) ` w ) C_ ( `' F " a ) ) ) ) -> ( ( cls ` ( KQ ` J ) ) ` ( F " w ) ) C_ a )
59 eleq2 
 |-  ( m = ( F " w ) -> ( ( F ` z ) e. m <-> ( F ` z ) e. ( F " w ) ) )
60 fveq2 
 |-  ( m = ( F " w ) -> ( ( cls ` ( KQ ` J ) ) ` m ) = ( ( cls ` ( KQ ` J ) ) ` ( F " w ) ) )
61 60 sseq1d 
 |-  ( m = ( F " w ) -> ( ( ( cls ` ( KQ ` J ) ) ` m ) C_ a <-> ( ( cls ` ( KQ ` J ) ) ` ( F " w ) ) C_ a ) )
62 59 61 anbi12d 
 |-  ( m = ( F " w ) -> ( ( ( F ` z ) e. m /\ ( ( cls ` ( KQ ` J ) ) ` m ) C_ a ) <-> ( ( F ` z ) e. ( F " w ) /\ ( ( cls ` ( KQ ` J ) ) ` ( F " w ) ) C_ a ) ) )
63 62 rspcev 
 |-  ( ( ( F " w ) e. ( KQ ` J ) /\ ( ( F ` z ) e. ( F " w ) /\ ( ( cls ` ( KQ ` J ) ) ` ( F " w ) ) C_ a ) ) -> E. m e. ( KQ ` J ) ( ( F ` z ) e. m /\ ( ( cls ` ( KQ ` J ) ) ` m ) C_ a ) )
64 30 35 58 63 syl12anc 
 |-  ( ( ( ( ( J e. ( TopOn ` X ) /\ J e. Reg ) /\ a e. ( KQ ` J ) ) /\ ( z e. X /\ ( F ` z ) e. a ) ) /\ ( w e. J /\ ( z e. w /\ ( ( cls ` J ) ` w ) C_ ( `' F " a ) ) ) ) -> E. m e. ( KQ ` J ) ( ( F ` z ) e. m /\ ( ( cls ` ( KQ ` J ) ) ` m ) C_ a ) )
65 26 64 rexlimddv 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ J e. Reg ) /\ a e. ( KQ ` J ) ) /\ ( z e. X /\ ( F ` z ) e. a ) ) -> E. m e. ( KQ ` J ) ( ( F ` z ) e. m /\ ( ( cls ` ( KQ ` J ) ) ` m ) C_ a ) )
66 65 expr 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ J e. Reg ) /\ a e. ( KQ ` J ) ) /\ z e. X ) -> ( ( F ` z ) e. a -> E. m e. ( KQ ` J ) ( ( F ` z ) e. m /\ ( ( cls ` ( KQ ` J ) ) ` m ) C_ a ) ) )
67 eleq1 
 |-  ( ( F ` z ) = b -> ( ( F ` z ) e. a <-> b e. a ) )
68 eleq1 
 |-  ( ( F ` z ) = b -> ( ( F ` z ) e. m <-> b e. m ) )
69 68 anbi1d 
 |-  ( ( F ` z ) = b -> ( ( ( F ` z ) e. m /\ ( ( cls ` ( KQ ` J ) ) ` m ) C_ a ) <-> ( b e. m /\ ( ( cls ` ( KQ ` J ) ) ` m ) C_ a ) ) )
70 69 rexbidv 
 |-  ( ( F ` z ) = b -> ( E. m e. ( KQ ` J ) ( ( F ` z ) e. m /\ ( ( cls ` ( KQ ` J ) ) ` m ) C_ a ) <-> E. m e. ( KQ ` J ) ( b e. m /\ ( ( cls ` ( KQ ` J ) ) ` m ) C_ a ) ) )
71 67 70 imbi12d 
 |-  ( ( F ` z ) = b -> ( ( ( F ` z ) e. a -> E. m e. ( KQ ` J ) ( ( F ` z ) e. m /\ ( ( cls ` ( KQ ` J ) ) ` m ) C_ a ) ) <-> ( b e. a -> E. m e. ( KQ ` J ) ( b e. m /\ ( ( cls ` ( KQ ` J ) ) ` m ) C_ a ) ) ) )
72 66 71 syl5ibcom 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ J e. Reg ) /\ a e. ( KQ ` J ) ) /\ z e. X ) -> ( ( F ` z ) = b -> ( b e. a -> E. m e. ( KQ ` J ) ( b e. m /\ ( ( cls ` ( KQ ` J ) ) ` m ) C_ a ) ) ) )
73 72 com23 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ J e. Reg ) /\ a e. ( KQ ` J ) ) /\ z e. X ) -> ( b e. a -> ( ( F ` z ) = b -> E. m e. ( KQ ` J ) ( b e. m /\ ( ( cls ` ( KQ ` J ) ) ` m ) C_ a ) ) ) )
74 73 imp 
 |-  ( ( ( ( ( J e. ( TopOn ` X ) /\ J e. Reg ) /\ a e. ( KQ ` J ) ) /\ z e. X ) /\ b e. a ) -> ( ( F ` z ) = b -> E. m e. ( KQ ` J ) ( b e. m /\ ( ( cls ` ( KQ ` J ) ) ` m ) C_ a ) ) )
75 74 an32s 
 |-  ( ( ( ( ( J e. ( TopOn ` X ) /\ J e. Reg ) /\ a e. ( KQ ` J ) ) /\ b e. a ) /\ z e. X ) -> ( ( F ` z ) = b -> E. m e. ( KQ ` J ) ( b e. m /\ ( ( cls ` ( KQ ` J ) ) ` m ) C_ a ) ) )
76 75 rexlimdva 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ J e. Reg ) /\ a e. ( KQ ` J ) ) /\ b e. a ) -> ( E. z e. X ( F ` z ) = b -> E. m e. ( KQ ` J ) ( b e. m /\ ( ( cls ` ( KQ ` J ) ) ` m ) C_ a ) ) )
77 13 76 mpd 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ J e. Reg ) /\ a e. ( KQ ` J ) ) /\ b e. a ) -> E. m e. ( KQ ` J ) ( b e. m /\ ( ( cls ` ( KQ ` J ) ) ` m ) C_ a ) )
78 77 anasss 
 |-  ( ( ( J e. ( TopOn ` X ) /\ J e. Reg ) /\ ( a e. ( KQ ` J ) /\ b e. a ) ) -> E. m e. ( KQ ` J ) ( b e. m /\ ( ( cls ` ( KQ ` J ) ) ` m ) C_ a ) )
79 78 ralrimivva 
 |-  ( ( J e. ( TopOn ` X ) /\ J e. Reg ) -> A. a e. ( KQ ` J ) A. b e. a E. m e. ( KQ ` J ) ( b e. m /\ ( ( cls ` ( KQ ` J ) ) ` m ) C_ a ) )
80 isreg 
 |-  ( ( KQ ` J ) e. Reg <-> ( ( KQ ` J ) e. Top /\ A. a e. ( KQ ` J ) A. b e. a E. m e. ( KQ ` J ) ( b e. m /\ ( ( cls ` ( KQ ` J ) ) ` m ) C_ a ) ) )
81 5 79 80 sylanbrc 
 |-  ( ( J e. ( TopOn ` X ) /\ J e. Reg ) -> ( KQ ` J ) e. Reg )