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 ⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } )
Assertion regr1lem2 ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ Reg ) → ( KQ ‘ 𝐽 ) ∈ Haus )

Proof

Step Hyp Ref Expression
1 kqval.2 ⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } )
2 simplll ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ Reg ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) ∧ ( 𝑎 ∈ 𝐽 ∧ ¬ ∃ 𝑚 ∈ ( KQ ‘ 𝐽 ) ∃ 𝑛 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑚 ∧ ( 𝐹 ‘ 𝑤 ) ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
3 simpllr ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ Reg ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) ∧ ( 𝑎 ∈ 𝐽 ∧ ¬ ∃ 𝑚 ∈ ( KQ ‘ 𝐽 ) ∃ 𝑛 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑚 ∧ ( 𝐹 ‘ 𝑤 ) ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) → 𝐽 ∈ Reg )
4 simplrl ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ Reg ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) ∧ ( 𝑎 ∈ 𝐽 ∧ ¬ ∃ 𝑚 ∈ ( KQ ‘ 𝐽 ) ∃ 𝑛 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑚 ∧ ( 𝐹 ‘ 𝑤 ) ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) → 𝑧 ∈ 𝑋 )
5 simplrr ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ Reg ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) ∧ ( 𝑎 ∈ 𝐽 ∧ ¬ ∃ 𝑚 ∈ ( KQ ‘ 𝐽 ) ∃ 𝑛 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑚 ∧ ( 𝐹 ‘ 𝑤 ) ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) → 𝑤 ∈ 𝑋 )
6 simprl ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ Reg ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) ∧ ( 𝑎 ∈ 𝐽 ∧ ¬ ∃ 𝑚 ∈ ( KQ ‘ 𝐽 ) ∃ 𝑛 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑚 ∧ ( 𝐹 ‘ 𝑤 ) ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) → 𝑎 ∈ 𝐽 )
7 simprr ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ Reg ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) ∧ ( 𝑎 ∈ 𝐽 ∧ ¬ ∃ 𝑚 ∈ ( KQ ‘ 𝐽 ) ∃ 𝑛 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑚 ∧ ( 𝐹 ‘ 𝑤 ) ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) → ¬ ∃ 𝑚 ∈ ( KQ ‘ 𝐽 ) ∃ 𝑛 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑚 ∧ ( 𝐹 ‘ 𝑤 ) ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) )
8 1 2 3 4 5 6 7 regr1lem ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ Reg ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) ∧ ( 𝑎 ∈ 𝐽 ∧ ¬ ∃ 𝑚 ∈ ( KQ ‘ 𝐽 ) ∃ 𝑛 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑚 ∧ ( 𝐹 ‘ 𝑤 ) ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) → ( 𝑧 ∈ 𝑎 → 𝑤 ∈ 𝑎 ) )
9 3ancoma ⊢ ( ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑚 ∧ ( 𝐹 ‘ 𝑤 ) ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ↔ ( ( 𝐹 ‘ 𝑤 ) ∈ 𝑛 ∧ ( 𝐹 ‘ 𝑧 ) ∈ 𝑚 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) )
10 incom ⊢ ( 𝑚 ∩ 𝑛 ) = ( 𝑛 ∩ 𝑚 )
11 10 eqeq1i ⊢ ( ( 𝑚 ∩ 𝑛 ) = ∅ ↔ ( 𝑛 ∩ 𝑚 ) = ∅ )
12 11 3anbi3i ⊢ ( ( ( 𝐹 ‘ 𝑤 ) ∈ 𝑛 ∧ ( 𝐹 ‘ 𝑧 ) ∈ 𝑚 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ↔ ( ( 𝐹 ‘ 𝑤 ) ∈ 𝑛 ∧ ( 𝐹 ‘ 𝑧 ) ∈ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) )
13 9 12 bitri ⊢ ( ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑚 ∧ ( 𝐹 ‘ 𝑤 ) ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ↔ ( ( 𝐹 ‘ 𝑤 ) ∈ 𝑛 ∧ ( 𝐹 ‘ 𝑧 ) ∈ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) )
14 13 2rexbii ⊢ ( ∃ 𝑚 ∈ ( KQ ‘ 𝐽 ) ∃ 𝑛 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑚 ∧ ( 𝐹 ‘ 𝑤 ) ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ↔ ∃ 𝑚 ∈ ( KQ ‘ 𝐽 ) ∃ 𝑛 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝑤 ) ∈ 𝑛 ∧ ( 𝐹 ‘ 𝑧 ) ∈ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) )
15 rexcom ⊢ ( ∃ 𝑚 ∈ ( KQ ‘ 𝐽 ) ∃ 𝑛 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝑤 ) ∈ 𝑛 ∧ ( 𝐹 ‘ 𝑧 ) ∈ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ↔ ∃ 𝑛 ∈ ( KQ ‘ 𝐽 ) ∃ 𝑚 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝑤 ) ∈ 𝑛 ∧ ( 𝐹 ‘ 𝑧 ) ∈ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) )
16 14 15 bitri ⊢ ( ∃ 𝑚 ∈ ( KQ ‘ 𝐽 ) ∃ 𝑛 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑚 ∧ ( 𝐹 ‘ 𝑤 ) ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ↔ ∃ 𝑛 ∈ ( KQ ‘ 𝐽 ) ∃ 𝑚 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝑤 ) ∈ 𝑛 ∧ ( 𝐹 ‘ 𝑧 ) ∈ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) )
17 7 16 sylnib ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ Reg ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) ∧ ( 𝑎 ∈ 𝐽 ∧ ¬ ∃ 𝑚 ∈ ( KQ ‘ 𝐽 ) ∃ 𝑛 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑚 ∧ ( 𝐹 ‘ 𝑤 ) ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) → ¬ ∃ 𝑛 ∈ ( KQ ‘ 𝐽 ) ∃ 𝑚 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝑤 ) ∈ 𝑛 ∧ ( 𝐹 ‘ 𝑧 ) ∈ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) )
18 1 2 3 5 4 6 17 regr1lem ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ Reg ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) ∧ ( 𝑎 ∈ 𝐽 ∧ ¬ ∃ 𝑚 ∈ ( KQ ‘ 𝐽 ) ∃ 𝑛 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑚 ∧ ( 𝐹 ‘ 𝑤 ) ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) → ( 𝑤 ∈ 𝑎 → 𝑧 ∈ 𝑎 ) )
19 8 18 impbid ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ Reg ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) ∧ ( 𝑎 ∈ 𝐽 ∧ ¬ ∃ 𝑚 ∈ ( KQ ‘ 𝐽 ) ∃ 𝑛 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑚 ∧ ( 𝐹 ‘ 𝑤 ) ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) → ( 𝑧 ∈ 𝑎 ↔ 𝑤 ∈ 𝑎 ) )
20 19 expr ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ Reg ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) ∧ 𝑎 ∈ 𝐽 ) → ( ¬ ∃ 𝑚 ∈ ( KQ ‘ 𝐽 ) ∃ 𝑛 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑚 ∧ ( 𝐹 ‘ 𝑤 ) ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) → ( 𝑧 ∈ 𝑎 ↔ 𝑤 ∈ 𝑎 ) ) )
21 20 ralrimdva ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ Reg ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → ( ¬ ∃ 𝑚 ∈ ( KQ ‘ 𝐽 ) ∃ 𝑛 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑚 ∧ ( 𝐹 ‘ 𝑤 ) ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) → ∀ 𝑎 ∈ 𝐽 ( 𝑧 ∈ 𝑎 ↔ 𝑤 ∈ 𝑎 ) ) )
22 1 kqfeq ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ↔ ∀ 𝑦 ∈ 𝐽 ( 𝑧 ∈ 𝑦 ↔ 𝑤 ∈ 𝑦 ) ) )
23 elequ2 ⊢ ( 𝑦 = 𝑎 → ( 𝑧 ∈ 𝑦 ↔ 𝑧 ∈ 𝑎 ) )
24 elequ2 ⊢ ( 𝑦 = 𝑎 → ( 𝑤 ∈ 𝑦 ↔ 𝑤 ∈ 𝑎 ) )
25 23 24 bibi12d ⊢ ( 𝑦 = 𝑎 → ( ( 𝑧 ∈ 𝑦 ↔ 𝑤 ∈ 𝑦 ) ↔ ( 𝑧 ∈ 𝑎 ↔ 𝑤 ∈ 𝑎 ) ) )
26 25 cbvralvw ⊢ ( ∀ 𝑦 ∈ 𝐽 ( 𝑧 ∈ 𝑦 ↔ 𝑤 ∈ 𝑦 ) ↔ ∀ 𝑎 ∈ 𝐽 ( 𝑧 ∈ 𝑎 ↔ 𝑤 ∈ 𝑎 ) )
27 22 26 bitrdi ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ↔ ∀ 𝑎 ∈ 𝐽 ( 𝑧 ∈ 𝑎 ↔ 𝑤 ∈ 𝑎 ) ) )
28 27 3expb ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ↔ ∀ 𝑎 ∈ 𝐽 ( 𝑧 ∈ 𝑎 ↔ 𝑤 ∈ 𝑎 ) ) )
29 28 adantlr ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ Reg ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ↔ ∀ 𝑎 ∈ 𝐽 ( 𝑧 ∈ 𝑎 ↔ 𝑤 ∈ 𝑎 ) ) )
30 21 29 sylibrd ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ Reg ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → ( ¬ ∃ 𝑚 ∈ ( KQ ‘ 𝐽 ) ∃ 𝑛 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑚 ∧ ( 𝐹 ‘ 𝑤 ) ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ) )
31 30 necon1ad ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ Reg ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ 𝑧 ) ≠ ( 𝐹 ‘ 𝑤 ) → ∃ 𝑚 ∈ ( KQ ‘ 𝐽 ) ∃ 𝑛 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑚 ∧ ( 𝐹 ‘ 𝑤 ) ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) )
32 31 ralrimivva ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ Reg ) → ∀ 𝑧 ∈ 𝑋 ∀ 𝑤 ∈ 𝑋 ( ( 𝐹 ‘ 𝑧 ) ≠ ( 𝐹 ‘ 𝑤 ) → ∃ 𝑚 ∈ ( KQ ‘ 𝐽 ) ∃ 𝑛 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑚 ∧ ( 𝐹 ‘ 𝑤 ) ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) )
33 1 kqffn ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐹 Fn 𝑋 )
34 33 adantr ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ Reg ) → 𝐹 Fn 𝑋 )
35 neeq1 ⊢ ( 𝑎 = ( 𝐹 ‘ 𝑧 ) → ( 𝑎 ≠ 𝑏 ↔ ( 𝐹 ‘ 𝑧 ) ≠ 𝑏 ) )
36 eleq1 ⊢ ( 𝑎 = ( 𝐹 ‘ 𝑧 ) → ( 𝑎 ∈ 𝑚 ↔ ( 𝐹 ‘ 𝑧 ) ∈ 𝑚 ) )
37 36 3anbi1d ⊢ ( 𝑎 = ( 𝐹 ‘ 𝑧 ) → ( ( 𝑎 ∈ 𝑚 ∧ 𝑏 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ↔ ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑚 ∧ 𝑏 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) )
38 37 2rexbidv ⊢ ( 𝑎 = ( 𝐹 ‘ 𝑧 ) → ( ∃ 𝑚 ∈ ( KQ ‘ 𝐽 ) ∃ 𝑛 ∈ ( KQ ‘ 𝐽 ) ( 𝑎 ∈ 𝑚 ∧ 𝑏 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ↔ ∃ 𝑚 ∈ ( KQ ‘ 𝐽 ) ∃ 𝑛 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑚 ∧ 𝑏 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) )
39 35 38 imbi12d ⊢ ( 𝑎 = ( 𝐹 ‘ 𝑧 ) → ( ( 𝑎 ≠ 𝑏 → ∃ 𝑚 ∈ ( KQ ‘ 𝐽 ) ∃ 𝑛 ∈ ( KQ ‘ 𝐽 ) ( 𝑎 ∈ 𝑚 ∧ 𝑏 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ↔ ( ( 𝐹 ‘ 𝑧 ) ≠ 𝑏 → ∃ 𝑚 ∈ ( KQ ‘ 𝐽 ) ∃ 𝑛 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑚 ∧ 𝑏 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) )
40 39 ralbidv ⊢ ( 𝑎 = ( 𝐹 ‘ 𝑧 ) → ( ∀ 𝑏 ∈ ran 𝐹 ( 𝑎 ≠ 𝑏 → ∃ 𝑚 ∈ ( KQ ‘ 𝐽 ) ∃ 𝑛 ∈ ( KQ ‘ 𝐽 ) ( 𝑎 ∈ 𝑚 ∧ 𝑏 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ↔ ∀ 𝑏 ∈ ran 𝐹 ( ( 𝐹 ‘ 𝑧 ) ≠ 𝑏 → ∃ 𝑚 ∈ ( KQ ‘ 𝐽 ) ∃ 𝑛 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑚 ∧ 𝑏 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) )
41 40 ralrn ⊢ ( 𝐹 Fn 𝑋 → ( ∀ 𝑎 ∈ ran 𝐹 ∀ 𝑏 ∈ ran 𝐹 ( 𝑎 ≠ 𝑏 → ∃ 𝑚 ∈ ( KQ ‘ 𝐽 ) ∃ 𝑛 ∈ ( KQ ‘ 𝐽 ) ( 𝑎 ∈ 𝑚 ∧ 𝑏 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ↔ ∀ 𝑧 ∈ 𝑋 ∀ 𝑏 ∈ ran 𝐹 ( ( 𝐹 ‘ 𝑧 ) ≠ 𝑏 → ∃ 𝑚 ∈ ( KQ ‘ 𝐽 ) ∃ 𝑛 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑚 ∧ 𝑏 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) )
42 neeq2 ⊢ ( 𝑏 = ( 𝐹 ‘ 𝑤 ) → ( ( 𝐹 ‘ 𝑧 ) ≠ 𝑏 ↔ ( 𝐹 ‘ 𝑧 ) ≠ ( 𝐹 ‘ 𝑤 ) ) )
43 eleq1 ⊢ ( 𝑏 = ( 𝐹 ‘ 𝑤 ) → ( 𝑏 ∈ 𝑛 ↔ ( 𝐹 ‘ 𝑤 ) ∈ 𝑛 ) )
44 43 3anbi2d ⊢ ( 𝑏 = ( 𝐹 ‘ 𝑤 ) → ( ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑚 ∧ 𝑏 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ↔ ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑚 ∧ ( 𝐹 ‘ 𝑤 ) ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) )
45 44 2rexbidv ⊢ ( 𝑏 = ( 𝐹 ‘ 𝑤 ) → ( ∃ 𝑚 ∈ ( KQ ‘ 𝐽 ) ∃ 𝑛 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑚 ∧ 𝑏 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ↔ ∃ 𝑚 ∈ ( KQ ‘ 𝐽 ) ∃ 𝑛 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑚 ∧ ( 𝐹 ‘ 𝑤 ) ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) )
46 42 45 imbi12d ⊢ ( 𝑏 = ( 𝐹 ‘ 𝑤 ) → ( ( ( 𝐹 ‘ 𝑧 ) ≠ 𝑏 → ∃ 𝑚 ∈ ( KQ ‘ 𝐽 ) ∃ 𝑛 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑚 ∧ 𝑏 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ↔ ( ( 𝐹 ‘ 𝑧 ) ≠ ( 𝐹 ‘ 𝑤 ) → ∃ 𝑚 ∈ ( KQ ‘ 𝐽 ) ∃ 𝑛 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑚 ∧ ( 𝐹 ‘ 𝑤 ) ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) )
47 46 ralrn ⊢ ( 𝐹 Fn 𝑋 → ( ∀ 𝑏 ∈ ran 𝐹 ( ( 𝐹 ‘ 𝑧 ) ≠ 𝑏 → ∃ 𝑚 ∈ ( KQ ‘ 𝐽 ) ∃ 𝑛 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑚 ∧ 𝑏 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ↔ ∀ 𝑤 ∈ 𝑋 ( ( 𝐹 ‘ 𝑧 ) ≠ ( 𝐹 ‘ 𝑤 ) → ∃ 𝑚 ∈ ( KQ ‘ 𝐽 ) ∃ 𝑛 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑚 ∧ ( 𝐹 ‘ 𝑤 ) ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) )
48 47 ralbidv ⊢ ( 𝐹 Fn 𝑋 → ( ∀ 𝑧 ∈ 𝑋 ∀ 𝑏 ∈ ran 𝐹 ( ( 𝐹 ‘ 𝑧 ) ≠ 𝑏 → ∃ 𝑚 ∈ ( KQ ‘ 𝐽 ) ∃ 𝑛 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑚 ∧ 𝑏 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ↔ ∀ 𝑧 ∈ 𝑋 ∀ 𝑤 ∈ 𝑋 ( ( 𝐹 ‘ 𝑧 ) ≠ ( 𝐹 ‘ 𝑤 ) → ∃ 𝑚 ∈ ( KQ ‘ 𝐽 ) ∃ 𝑛 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑚 ∧ ( 𝐹 ‘ 𝑤 ) ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) )
49 41 48 bitrd ⊢ ( 𝐹 Fn 𝑋 → ( ∀ 𝑎 ∈ ran 𝐹 ∀ 𝑏 ∈ ran 𝐹 ( 𝑎 ≠ 𝑏 → ∃ 𝑚 ∈ ( KQ ‘ 𝐽 ) ∃ 𝑛 ∈ ( KQ ‘ 𝐽 ) ( 𝑎 ∈ 𝑚 ∧ 𝑏 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ↔ ∀ 𝑧 ∈ 𝑋 ∀ 𝑤 ∈ 𝑋 ( ( 𝐹 ‘ 𝑧 ) ≠ ( 𝐹 ‘ 𝑤 ) → ∃ 𝑚 ∈ ( KQ ‘ 𝐽 ) ∃ 𝑛 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑚 ∧ ( 𝐹 ‘ 𝑤 ) ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) )
50 34 49 syl ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ Reg ) → ( ∀ 𝑎 ∈ ran 𝐹 ∀ 𝑏 ∈ ran 𝐹 ( 𝑎 ≠ 𝑏 → ∃ 𝑚 ∈ ( KQ ‘ 𝐽 ) ∃ 𝑛 ∈ ( KQ ‘ 𝐽 ) ( 𝑎 ∈ 𝑚 ∧ 𝑏 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ↔ ∀ 𝑧 ∈ 𝑋 ∀ 𝑤 ∈ 𝑋 ( ( 𝐹 ‘ 𝑧 ) ≠ ( 𝐹 ‘ 𝑤 ) → ∃ 𝑚 ∈ ( KQ ‘ 𝐽 ) ∃ 𝑛 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑚 ∧ ( 𝐹 ‘ 𝑤 ) ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) )
51 32 50 mpbird ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ Reg ) → ∀ 𝑎 ∈ ran 𝐹 ∀ 𝑏 ∈ ran 𝐹 ( 𝑎 ≠ 𝑏 → ∃ 𝑚 ∈ ( KQ ‘ 𝐽 ) ∃ 𝑛 ∈ ( KQ ‘ 𝐽 ) ( 𝑎 ∈ 𝑚 ∧ 𝑏 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) )
52 1 kqtopon ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( KQ ‘ 𝐽 ) ∈ ( TopOn ‘ ran 𝐹 ) )
53 52 adantr ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ Reg ) → ( KQ ‘ 𝐽 ) ∈ ( TopOn ‘ ran 𝐹 ) )
54 ishaus2 ⊢ ( ( KQ ‘ 𝐽 ) ∈ ( TopOn ‘ ran 𝐹 ) → ( ( KQ ‘ 𝐽 ) ∈ Haus ↔ ∀ 𝑎 ∈ ran 𝐹 ∀ 𝑏 ∈ ran 𝐹 ( 𝑎 ≠ 𝑏 → ∃ 𝑚 ∈ ( KQ ‘ 𝐽 ) ∃ 𝑛 ∈ ( KQ ‘ 𝐽 ) ( 𝑎 ∈ 𝑚 ∧ 𝑏 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) )
55 53 54 syl ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ Reg ) → ( ( KQ ‘ 𝐽 ) ∈ Haus ↔ ∀ 𝑎 ∈ ran 𝐹 ∀ 𝑏 ∈ ran 𝐹 ( 𝑎 ≠ 𝑏 → ∃ 𝑚 ∈ ( KQ ‘ 𝐽 ) ∃ 𝑛 ∈ ( KQ ‘ 𝐽 ) ( 𝑎 ∈ 𝑚 ∧ 𝑏 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) )
56 51 55 mpbird ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ Reg ) → ( KQ ‘ 𝐽 ) ∈ Haus )