| 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 ) |