This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem regr1lem2

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

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

Proof

Step Hyp Ref Expression
1 kqval.2 
 |-  F = ( x e. X |-> { y e. J | x e. y } )
2 simplll 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ J e. Reg ) /\ ( z e. X /\ w e. X ) ) /\ ( a e. J /\ -. E. m e. ( KQ ` J ) E. n e. ( KQ ` J ) ( ( F ` z ) e. m /\ ( F ` w ) e. n /\ ( m i^i n ) = (/) ) ) ) -> J e. ( TopOn ` X ) )
3 simpllr 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ J e. Reg ) /\ ( z e. X /\ w e. X ) ) /\ ( a e. J /\ -. E. m e. ( KQ ` J ) E. n e. ( KQ ` J ) ( ( F ` z ) e. m /\ ( F ` w ) e. n /\ ( m i^i n ) = (/) ) ) ) -> J e. Reg )
4 simplrl 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ J e. Reg ) /\ ( z e. X /\ w e. X ) ) /\ ( a e. J /\ -. E. m e. ( KQ ` J ) E. n e. ( KQ ` J ) ( ( F ` z ) e. m /\ ( F ` w ) e. n /\ ( m i^i n ) = (/) ) ) ) -> z e. X )
5 simplrr 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ J e. Reg ) /\ ( z e. X /\ w e. X ) ) /\ ( a e. J /\ -. E. m e. ( KQ ` J ) E. n e. ( KQ ` J ) ( ( F ` z ) e. m /\ ( F ` w ) e. n /\ ( m i^i n ) = (/) ) ) ) -> w e. X )
6 simprl 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ J e. Reg ) /\ ( z e. X /\ w e. X ) ) /\ ( a e. J /\ -. E. m e. ( KQ ` J ) E. n e. ( KQ ` J ) ( ( F ` z ) e. m /\ ( F ` w ) e. n /\ ( m i^i n ) = (/) ) ) ) -> a e. J )
7 simprr 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ J e. Reg ) /\ ( z e. X /\ w e. X ) ) /\ ( a e. J /\ -. E. m e. ( KQ ` J ) E. n e. ( KQ ` J ) ( ( F ` z ) e. m /\ ( F ` w ) e. n /\ ( m i^i n ) = (/) ) ) ) -> -. E. m e. ( KQ ` J ) E. n e. ( KQ ` J ) ( ( F ` z ) e. m /\ ( F ` w ) e. n /\ ( m i^i n ) = (/) ) )
8 1 2 3 4 5 6 7 regr1lem 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ J e. Reg ) /\ ( z e. X /\ w e. X ) ) /\ ( a e. J /\ -. E. m e. ( KQ ` J ) E. n e. ( KQ ` J ) ( ( F ` z ) e. m /\ ( F ` w ) e. n /\ ( m i^i n ) = (/) ) ) ) -> ( z e. a -> w e. a ) )
9 3ancoma 
 |-  ( ( ( F ` z ) e. m /\ ( F ` w ) e. n /\ ( m i^i n ) = (/) ) <-> ( ( F ` w ) e. n /\ ( F ` z ) e. m /\ ( m i^i n ) = (/) ) )
10 incom 
 |-  ( m i^i n ) = ( n i^i m )
11 10 eqeq1i 
 |-  ( ( m i^i n ) = (/) <-> ( n i^i m ) = (/) )
12 11 3anbi3i 
 |-  ( ( ( F ` w ) e. n /\ ( F ` z ) e. m /\ ( m i^i n ) = (/) ) <-> ( ( F ` w ) e. n /\ ( F ` z ) e. m /\ ( n i^i m ) = (/) ) )
13 9 12 bitri 
 |-  ( ( ( F ` z ) e. m /\ ( F ` w ) e. n /\ ( m i^i n ) = (/) ) <-> ( ( F ` w ) e. n /\ ( F ` z ) e. m /\ ( n i^i m ) = (/) ) )
14 13 2rexbii 
 |-  ( E. m e. ( KQ ` J ) E. n e. ( KQ ` J ) ( ( F ` z ) e. m /\ ( F ` w ) e. n /\ ( m i^i n ) = (/) ) <-> E. m e. ( KQ ` J ) E. n e. ( KQ ` J ) ( ( F ` w ) e. n /\ ( F ` z ) e. m /\ ( n i^i m ) = (/) ) )
15 rexcom 
 |-  ( E. m e. ( KQ ` J ) E. n e. ( KQ ` J ) ( ( F ` w ) e. n /\ ( F ` z ) e. m /\ ( n i^i m ) = (/) ) <-> E. n e. ( KQ ` J ) E. m e. ( KQ ` J ) ( ( F ` w ) e. n /\ ( F ` z ) e. m /\ ( n i^i m ) = (/) ) )
16 14 15 bitri 
 |-  ( E. m e. ( KQ ` J ) E. n e. ( KQ ` J ) ( ( F ` z ) e. m /\ ( F ` w ) e. n /\ ( m i^i n ) = (/) ) <-> E. n e. ( KQ ` J ) E. m e. ( KQ ` J ) ( ( F ` w ) e. n /\ ( F ` z ) e. m /\ ( n i^i m ) = (/) ) )
17 7 16 sylnib 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ J e. Reg ) /\ ( z e. X /\ w e. X ) ) /\ ( a e. J /\ -. E. m e. ( KQ ` J ) E. n e. ( KQ ` J ) ( ( F ` z ) e. m /\ ( F ` w ) e. n /\ ( m i^i n ) = (/) ) ) ) -> -. E. n e. ( KQ ` J ) E. m e. ( KQ ` J ) ( ( F ` w ) e. n /\ ( F ` z ) e. m /\ ( n i^i m ) = (/) ) )
18 1 2 3 5 4 6 17 regr1lem 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ J e. Reg ) /\ ( z e. X /\ w e. X ) ) /\ ( a e. J /\ -. E. m e. ( KQ ` J ) E. n e. ( KQ ` J ) ( ( F ` z ) e. m /\ ( F ` w ) e. n /\ ( m i^i n ) = (/) ) ) ) -> ( w e. a -> z e. a ) )
19 8 18 impbid 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ J e. Reg ) /\ ( z e. X /\ w e. X ) ) /\ ( a e. J /\ -. E. m e. ( KQ ` J ) E. n e. ( KQ ` J ) ( ( F ` z ) e. m /\ ( F ` w ) e. n /\ ( m i^i n ) = (/) ) ) ) -> ( z e. a <-> w e. a ) )
20 19 expr 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ J e. Reg ) /\ ( z e. X /\ w e. X ) ) /\ a e. J ) -> ( -. E. m e. ( KQ ` J ) E. n e. ( KQ ` J ) ( ( F ` z ) e. m /\ ( F ` w ) e. n /\ ( m i^i n ) = (/) ) -> ( z e. a <-> w e. a ) ) )
21 20 ralrimdva 
 |-  ( ( ( J e. ( TopOn ` X ) /\ J e. Reg ) /\ ( z e. X /\ w e. X ) ) -> ( -. E. m e. ( KQ ` J ) E. n e. ( KQ ` J ) ( ( F ` z ) e. m /\ ( F ` w ) e. n /\ ( m i^i n ) = (/) ) -> A. a e. J ( z e. a <-> w e. a ) ) )
22 1 kqfeq 
 |-  ( ( J e. ( TopOn ` X ) /\ z e. X /\ w e. X ) -> ( ( F ` z ) = ( F ` w ) <-> A. y e. J ( z e. y <-> w e. y ) ) )
23 elequ2 
 |-  ( y = a -> ( z e. y <-> z e. a ) )
24 elequ2 
 |-  ( y = a -> ( w e. y <-> w e. a ) )
25 23 24 bibi12d 
 |-  ( y = a -> ( ( z e. y <-> w e. y ) <-> ( z e. a <-> w e. a ) ) )
26 25 cbvralvw 
 |-  ( A. y e. J ( z e. y <-> w e. y ) <-> A. a e. J ( z e. a <-> w e. a ) )
27 22 26 bitrdi 
 |-  ( ( J e. ( TopOn ` X ) /\ z e. X /\ w e. X ) -> ( ( F ` z ) = ( F ` w ) <-> A. a e. J ( z e. a <-> w e. a ) ) )
28 27 3expb 
 |-  ( ( J e. ( TopOn ` X ) /\ ( z e. X /\ w e. X ) ) -> ( ( F ` z ) = ( F ` w ) <-> A. a e. J ( z e. a <-> w e. a ) ) )
29 28 adantlr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ J e. Reg ) /\ ( z e. X /\ w e. X ) ) -> ( ( F ` z ) = ( F ` w ) <-> A. a e. J ( z e. a <-> w e. a ) ) )
30 21 29 sylibrd 
 |-  ( ( ( J e. ( TopOn ` X ) /\ J e. Reg ) /\ ( z e. X /\ w e. X ) ) -> ( -. E. m e. ( KQ ` J ) E. n e. ( KQ ` J ) ( ( F ` z ) e. m /\ ( F ` w ) e. n /\ ( m i^i n ) = (/) ) -> ( F ` z ) = ( F ` w ) ) )
31 30 necon1ad 
 |-  ( ( ( J e. ( TopOn ` X ) /\ J e. Reg ) /\ ( z e. X /\ w e. X ) ) -> ( ( F ` z ) =/= ( F ` w ) -> E. m e. ( KQ ` J ) E. n e. ( KQ ` J ) ( ( F ` z ) e. m /\ ( F ` w ) e. n /\ ( m i^i n ) = (/) ) ) )
32 31 ralrimivva 
 |-  ( ( J e. ( TopOn ` X ) /\ J e. Reg ) -> A. z e. X A. w e. X ( ( F ` z ) =/= ( F ` w ) -> E. m e. ( KQ ` J ) E. n e. ( KQ ` J ) ( ( F ` z ) e. m /\ ( F ` w ) e. n /\ ( m i^i n ) = (/) ) ) )
33 1 kqffn 
 |-  ( J e. ( TopOn ` X ) -> F Fn X )
34 33 adantr 
 |-  ( ( J e. ( TopOn ` X ) /\ J e. Reg ) -> F Fn X )
35 neeq1 
 |-  ( a = ( F ` z ) -> ( a =/= b <-> ( F ` z ) =/= b ) )
36 eleq1 
 |-  ( a = ( F ` z ) -> ( a e. m <-> ( F ` z ) e. m ) )
37 36 3anbi1d 
 |-  ( a = ( F ` z ) -> ( ( a e. m /\ b e. n /\ ( m i^i n ) = (/) ) <-> ( ( F ` z ) e. m /\ b e. n /\ ( m i^i n ) = (/) ) ) )
38 37 2rexbidv 
 |-  ( a = ( F ` z ) -> ( E. m e. ( KQ ` J ) E. n e. ( KQ ` J ) ( a e. m /\ b e. n /\ ( m i^i n ) = (/) ) <-> E. m e. ( KQ ` J ) E. n e. ( KQ ` J ) ( ( F ` z ) e. m /\ b e. n /\ ( m i^i n ) = (/) ) ) )
39 35 38 imbi12d 
 |-  ( a = ( F ` z ) -> ( ( a =/= b -> E. m e. ( KQ ` J ) E. n e. ( KQ ` J ) ( a e. m /\ b e. n /\ ( m i^i n ) = (/) ) ) <-> ( ( F ` z ) =/= b -> E. m e. ( KQ ` J ) E. n e. ( KQ ` J ) ( ( F ` z ) e. m /\ b e. n /\ ( m i^i n ) = (/) ) ) ) )
40 39 ralbidv 
 |-  ( a = ( F ` z ) -> ( A. b e. ran F ( a =/= b -> E. m e. ( KQ ` J ) E. n e. ( KQ ` J ) ( a e. m /\ b e. n /\ ( m i^i n ) = (/) ) ) <-> A. b e. ran F ( ( F ` z ) =/= b -> E. m e. ( KQ ` J ) E. n e. ( KQ ` J ) ( ( F ` z ) e. m /\ b e. n /\ ( m i^i n ) = (/) ) ) ) )
41 40 ralrn 
 |-  ( F Fn X -> ( A. a e. ran F A. b e. ran F ( a =/= b -> E. m e. ( KQ ` J ) E. n e. ( KQ ` J ) ( a e. m /\ b e. n /\ ( m i^i n ) = (/) ) ) <-> A. z e. X A. b e. ran F ( ( F ` z ) =/= b -> E. m e. ( KQ ` J ) E. n e. ( KQ ` J ) ( ( F ` z ) e. m /\ b e. n /\ ( m i^i n ) = (/) ) ) ) )
42 neeq2 
 |-  ( b = ( F ` w ) -> ( ( F ` z ) =/= b <-> ( F ` z ) =/= ( F ` w ) ) )
43 eleq1 
 |-  ( b = ( F ` w ) -> ( b e. n <-> ( F ` w ) e. n ) )
44 43 3anbi2d 
 |-  ( b = ( F ` w ) -> ( ( ( F ` z ) e. m /\ b e. n /\ ( m i^i n ) = (/) ) <-> ( ( F ` z ) e. m /\ ( F ` w ) e. n /\ ( m i^i n ) = (/) ) ) )
45 44 2rexbidv 
 |-  ( b = ( F ` w ) -> ( E. m e. ( KQ ` J ) E. n e. ( KQ ` J ) ( ( F ` z ) e. m /\ b e. n /\ ( m i^i n ) = (/) ) <-> E. m e. ( KQ ` J ) E. n e. ( KQ ` J ) ( ( F ` z ) e. m /\ ( F ` w ) e. n /\ ( m i^i n ) = (/) ) ) )
46 42 45 imbi12d 
 |-  ( b = ( F ` w ) -> ( ( ( F ` z ) =/= b -> E. m e. ( KQ ` J ) E. n e. ( KQ ` J ) ( ( F ` z ) e. m /\ b e. n /\ ( m i^i n ) = (/) ) ) <-> ( ( F ` z ) =/= ( F ` w ) -> E. m e. ( KQ ` J ) E. n e. ( KQ ` J ) ( ( F ` z ) e. m /\ ( F ` w ) e. n /\ ( m i^i n ) = (/) ) ) ) )
47 46 ralrn 
 |-  ( F Fn X -> ( A. b e. ran F ( ( F ` z ) =/= b -> E. m e. ( KQ ` J ) E. n e. ( KQ ` J ) ( ( F ` z ) e. m /\ b e. n /\ ( m i^i n ) = (/) ) ) <-> A. w e. X ( ( F ` z ) =/= ( F ` w ) -> E. m e. ( KQ ` J ) E. n e. ( KQ ` J ) ( ( F ` z ) e. m /\ ( F ` w ) e. n /\ ( m i^i n ) = (/) ) ) ) )
48 47 ralbidv 
 |-  ( F Fn X -> ( A. z e. X A. b e. ran F ( ( F ` z ) =/= b -> E. m e. ( KQ ` J ) E. n e. ( KQ ` J ) ( ( F ` z ) e. m /\ b e. n /\ ( m i^i n ) = (/) ) ) <-> A. z e. X A. w e. X ( ( F ` z ) =/= ( F ` w ) -> E. m e. ( KQ ` J ) E. n e. ( KQ ` J ) ( ( F ` z ) e. m /\ ( F ` w ) e. n /\ ( m i^i n ) = (/) ) ) ) )
49 41 48 bitrd 
 |-  ( F Fn X -> ( A. a e. ran F A. b e. ran F ( a =/= b -> E. m e. ( KQ ` J ) E. n e. ( KQ ` J ) ( a e. m /\ b e. n /\ ( m i^i n ) = (/) ) ) <-> A. z e. X A. w e. X ( ( F ` z ) =/= ( F ` w ) -> E. m e. ( KQ ` J ) E. n e. ( KQ ` J ) ( ( F ` z ) e. m /\ ( F ` w ) e. n /\ ( m i^i n ) = (/) ) ) ) )
50 34 49 syl 
 |-  ( ( J e. ( TopOn ` X ) /\ J e. Reg ) -> ( A. a e. ran F A. b e. ran F ( a =/= b -> E. m e. ( KQ ` J ) E. n e. ( KQ ` J ) ( a e. m /\ b e. n /\ ( m i^i n ) = (/) ) ) <-> A. z e. X A. w e. X ( ( F ` z ) =/= ( F ` w ) -> E. m e. ( KQ ` J ) E. n e. ( KQ ` J ) ( ( F ` z ) e. m /\ ( F ` w ) e. n /\ ( m i^i n ) = (/) ) ) ) )
51 32 50 mpbird 
 |-  ( ( J e. ( TopOn ` X ) /\ J e. Reg ) -> A. a e. ran F A. b e. ran F ( a =/= b -> E. m e. ( KQ ` J ) E. n e. ( KQ ` J ) ( a e. m /\ b e. n /\ ( m i^i n ) = (/) ) ) )
52 1 kqtopon 
 |-  ( J e. ( TopOn ` X ) -> ( KQ ` J ) e. ( TopOn ` ran F ) )
53 52 adantr 
 |-  ( ( J e. ( TopOn ` X ) /\ J e. Reg ) -> ( KQ ` J ) e. ( TopOn ` ran F ) )
54 ishaus2 
 |-  ( ( KQ ` J ) e. ( TopOn ` ran F ) -> ( ( KQ ` J ) e. Haus <-> A. a e. ran F A. b e. ran F ( a =/= b -> E. m e. ( KQ ` J ) E. n e. ( KQ ` J ) ( a e. m /\ b e. n /\ ( m i^i n ) = (/) ) ) ) )
55 53 54 syl 
 |-  ( ( J e. ( TopOn ` X ) /\ J e. Reg ) -> ( ( KQ ` J ) e. Haus <-> A. a e. ran F A. b e. ran F ( a =/= b -> E. m e. ( KQ ` J ) E. n e. ( KQ ` J ) ( a e. m /\ b e. n /\ ( m i^i n ) = (/) ) ) ) )
56 51 55 mpbird 
 |-  ( ( J e. ( TopOn ` X ) /\ J e. Reg ) -> ( KQ ` J ) e. Haus )