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 X y J | x y
Assertion regr1lem2 J TopOn X J Reg KQ J Haus

Proof

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