| Step | Hyp | Ref
| Expression |
| 1 | | qtophaus.1 |
. . . 4
⊢ (𝜑 → 𝐽 ∈ Haus) |
| 2 | | haustop 23339 |
. . . 4
⊢ (𝐽 ∈ Haus → 𝐽 ∈ Top) |
| 3 | 1, 2 | syl 17 |
. . 3
⊢ (𝜑 → 𝐽 ∈ Top) |
| 4 | | qtophaus.2 |
. . . 4
⊢ (𝜑 → 𝐹:𝑋–onto→𝑌) |
| 5 | | fofn 6822 |
. . . 4
⊢ (𝐹:𝑋–onto→𝑌 → 𝐹 Fn 𝑋) |
| 6 | 4, 5 | syl 17 |
. . 3
⊢ (𝜑 → 𝐹 Fn 𝑋) |
| 7 | | qtophaus.x |
. . . 4
⊢ 𝑋 = ∪
𝐽 |
| 8 | 7 | qtoptop 23708 |
. . 3
⊢ ((𝐽 ∈ Top ∧ 𝐹 Fn 𝑋) → (𝐽 qTop 𝐹) ∈ Top) |
| 9 | 3, 6, 8 | syl2anc 584 |
. 2
⊢ (𝜑 → (𝐽 qTop 𝐹) ∈ Top) |
| 10 | | txtop 23577 |
. . . 4
⊢ (((𝐽 qTop 𝐹) ∈ Top ∧ (𝐽 qTop 𝐹) ∈ Top) → ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)) ∈ Top) |
| 11 | 9, 9, 10 | syl2anc 584 |
. . 3
⊢ (𝜑 → ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)) ∈ Top) |
| 12 | | idssxp 6067 |
. . . 4
⊢ ( I
↾ ∪ (𝐽 qTop 𝐹)) ⊆ (∪
(𝐽 qTop 𝐹) × ∪
(𝐽 qTop 𝐹)) |
| 13 | | eqid 2737 |
. . . . . 6
⊢ ∪ (𝐽
qTop 𝐹) = ∪ (𝐽
qTop 𝐹) |
| 14 | 13, 13 | txuni 23600 |
. . . . 5
⊢ (((𝐽 qTop 𝐹) ∈ Top ∧ (𝐽 qTop 𝐹) ∈ Top) → (∪ (𝐽
qTop 𝐹) × ∪ (𝐽
qTop 𝐹)) = ∪ ((𝐽
qTop 𝐹) ×t
(𝐽 qTop 𝐹))) |
| 15 | 9, 9, 14 | syl2anc 584 |
. . . 4
⊢ (𝜑 → (∪ (𝐽
qTop 𝐹) × ∪ (𝐽
qTop 𝐹)) = ∪ ((𝐽
qTop 𝐹) ×t
(𝐽 qTop 𝐹))) |
| 16 | 12, 15 | sseqtrid 4026 |
. . 3
⊢ (𝜑 → ( I ↾ ∪ (𝐽
qTop 𝐹)) ⊆ ∪ ((𝐽
qTop 𝐹) ×t
(𝐽 qTop 𝐹))) |
| 17 | 7 | qtopuni 23710 |
. . . . . . . 8
⊢ ((𝐽 ∈ Top ∧ 𝐹:𝑋–onto→𝑌) → 𝑌 = ∪ (𝐽 qTop 𝐹)) |
| 18 | 3, 4, 17 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → 𝑌 = ∪ (𝐽 qTop 𝐹)) |
| 19 | 18 | sqxpeqd 5717 |
. . . . . 6
⊢ (𝜑 → (𝑌 × 𝑌) = (∪ (𝐽 qTop 𝐹) × ∪
(𝐽 qTop 𝐹))) |
| 20 | 19, 15 | eqtr2d 2778 |
. . . . 5
⊢ (𝜑 → ∪ ((𝐽
qTop 𝐹) ×t
(𝐽 qTop 𝐹)) = (𝑌 × 𝑌)) |
| 21 | 18 | eqcomd 2743 |
. . . . . 6
⊢ (𝜑 → ∪ (𝐽
qTop 𝐹) = 𝑌) |
| 22 | 21 | reseq2d 5997 |
. . . . 5
⊢ (𝜑 → ( I ↾ ∪ (𝐽
qTop 𝐹)) = ( I ↾
𝑌)) |
| 23 | 20, 22 | difeq12d 4127 |
. . . 4
⊢ (𝜑 → (∪ ((𝐽
qTop 𝐹) ×t
(𝐽 qTop 𝐹)) ∖ ( I ↾ ∪ (𝐽
qTop 𝐹))) = ((𝑌 × 𝑌) ∖ ( I ↾ 𝑌))) |
| 24 | | qtophaus.h |
. . . . . . . . . 10
⊢ 𝐻 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) |
| 25 | | opex 5469 |
. . . . . . . . . 10
⊢
〈(𝐹‘𝑥), (𝐹‘𝑦)〉 ∈ V |
| 26 | 24, 25 | fnmpoi 8095 |
. . . . . . . . 9
⊢ 𝐻 Fn (𝑋 × 𝑋) |
| 27 | | difss 4136 |
. . . . . . . . 9
⊢ ((𝑋 × 𝑋) ∖ ∼ ) ⊆ (𝑋 × 𝑋) |
| 28 | | fvelimab 6981 |
. . . . . . . . 9
⊢ ((𝐻 Fn (𝑋 × 𝑋) ∧ ((𝑋 × 𝑋) ∖ ∼ ) ⊆ (𝑋 × 𝑋)) → (𝑐 ∈ (𝐻 “ ((𝑋 × 𝑋) ∖ ∼ )) ↔
∃𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )(𝐻‘𝑧) = 𝑐)) |
| 29 | 26, 27, 28 | mp2an 692 |
. . . . . . . 8
⊢ (𝑐 ∈ (𝐻 “ ((𝑋 × 𝑋) ∖ ∼ )) ↔
∃𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )(𝐻‘𝑧) = 𝑐) |
| 30 | | simp-4r 784 |
. . . . . . . . . . . . . . . 16
⊢
(((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = 〈𝑎, 𝑏〉) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → 𝑥 ∈ 𝑋) |
| 31 | | simplr 769 |
. . . . . . . . . . . . . . . 16
⊢
(((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = 〈𝑎, 𝑏〉) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → 𝑦 ∈ 𝑋) |
| 32 | | opelxpi 5722 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → 〈𝑥, 𝑦〉 ∈ (𝑋 × 𝑋)) |
| 33 | 30, 31, 32 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢
(((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = 〈𝑎, 𝑏〉) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → 〈𝑥, 𝑦〉 ∈ (𝑋 × 𝑋)) |
| 34 | | df-br 5144 |
. . . . . . . . . . . . . . 15
⊢ (𝑥(𝑋 × 𝑋)𝑦 ↔ 〈𝑥, 𝑦〉 ∈ (𝑋 × 𝑋)) |
| 35 | 33, 34 | sylibr 234 |
. . . . . . . . . . . . . 14
⊢
(((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = 〈𝑎, 𝑏〉) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → 𝑥(𝑋 × 𝑋)𝑦) |
| 36 | | simpllr 776 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = 〈𝑎, 𝑏〉) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → (𝐹‘𝑥) = 𝑎) |
| 37 | | simpr 484 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = 〈𝑎, 𝑏〉) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → (𝐹‘𝑦) = 𝑏) |
| 38 | 36, 37 | opeq12d 4881 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = 〈𝑎, 𝑏〉) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → 〈(𝐹‘𝑥), (𝐹‘𝑦)〉 = 〈𝑎, 𝑏〉) |
| 39 | | simp-5r 786 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = 〈𝑎, 𝑏〉) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → 𝑐 = 〈𝑎, 𝑏〉) |
| 40 | | simp-8r 792 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = 〈𝑎, 𝑏〉) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) |
| 41 | 39, 40 | eqeltrrd 2842 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = 〈𝑎, 𝑏〉) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → 〈𝑎, 𝑏〉 ∈ ((𝑌 × 𝑌) ∖ I )) |
| 42 | 38, 41 | eqeltrd 2841 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = 〈𝑎, 𝑏〉) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → 〈(𝐹‘𝑥), (𝐹‘𝑦)〉 ∈ ((𝑌 × 𝑌) ∖ I )) |
| 43 | | relxp 5703 |
. . . . . . . . . . . . . . . . . 18
⊢ Rel
(𝑌 × 𝑌) |
| 44 | | opeldifid 32612 |
. . . . . . . . . . . . . . . . . 18
⊢ (Rel
(𝑌 × 𝑌) → (〈(𝐹‘𝑥), (𝐹‘𝑦)〉 ∈ ((𝑌 × 𝑌) ∖ I ) ↔ (〈(𝐹‘𝑥), (𝐹‘𝑦)〉 ∈ (𝑌 × 𝑌) ∧ (𝐹‘𝑥) ≠ (𝐹‘𝑦)))) |
| 45 | 43, 44 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢
(〈(𝐹‘𝑥), (𝐹‘𝑦)〉 ∈ ((𝑌 × 𝑌) ∖ I ) ↔ (〈(𝐹‘𝑥), (𝐹‘𝑦)〉 ∈ (𝑌 × 𝑌) ∧ (𝐹‘𝑥) ≠ (𝐹‘𝑦))) |
| 46 | 42, 45 | sylib 218 |
. . . . . . . . . . . . . . . 16
⊢
(((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = 〈𝑎, 𝑏〉) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → (〈(𝐹‘𝑥), (𝐹‘𝑦)〉 ∈ (𝑌 × 𝑌) ∧ (𝐹‘𝑥) ≠ (𝐹‘𝑦))) |
| 47 | 46 | simprd 495 |
. . . . . . . . . . . . . . 15
⊢
(((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = 〈𝑎, 𝑏〉) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → (𝐹‘𝑥) ≠ (𝐹‘𝑦)) |
| 48 | 6 | ad8antr 740 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = 〈𝑎, 𝑏〉) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → 𝐹 Fn 𝑋) |
| 49 | | qtophaus.e |
. . . . . . . . . . . . . . . . . 18
⊢ ∼ =
(◡𝐹 ∘ 𝐹) |
| 50 | 49 | fcoinvbr 32618 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹 Fn 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥 ∼ 𝑦 ↔ (𝐹‘𝑥) = (𝐹‘𝑦))) |
| 51 | 48, 30, 31, 50 | syl3anc 1373 |
. . . . . . . . . . . . . . . 16
⊢
(((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = 〈𝑎, 𝑏〉) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → (𝑥 ∼ 𝑦 ↔ (𝐹‘𝑥) = (𝐹‘𝑦))) |
| 52 | 51 | necon3bbid 2978 |
. . . . . . . . . . . . . . 15
⊢
(((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = 〈𝑎, 𝑏〉) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → (¬ 𝑥 ∼ 𝑦 ↔ (𝐹‘𝑥) ≠ (𝐹‘𝑦))) |
| 53 | 47, 52 | mpbird 257 |
. . . . . . . . . . . . . 14
⊢
(((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = 〈𝑎, 𝑏〉) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → ¬ 𝑥 ∼ 𝑦) |
| 54 | | df-br 5144 |
. . . . . . . . . . . . . . 15
⊢ (𝑥((𝑋 × 𝑋) ∖ ∼ )𝑦 ↔ 〈𝑥, 𝑦〉 ∈ ((𝑋 × 𝑋) ∖ ∼ )) |
| 55 | | brdif 5196 |
. . . . . . . . . . . . . . 15
⊢ (𝑥((𝑋 × 𝑋) ∖ ∼ )𝑦 ↔ (𝑥(𝑋 × 𝑋)𝑦 ∧ ¬ 𝑥 ∼ 𝑦)) |
| 56 | 54, 55 | bitr3i 277 |
. . . . . . . . . . . . . 14
⊢
(〈𝑥, 𝑦〉 ∈ ((𝑋 × 𝑋) ∖ ∼ ) ↔ (𝑥(𝑋 × 𝑋)𝑦 ∧ ¬ 𝑥 ∼ 𝑦)) |
| 57 | 35, 53, 56 | sylanbrc 583 |
. . . . . . . . . . . . 13
⊢
(((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = 〈𝑎, 𝑏〉) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → 〈𝑥, 𝑦〉 ∈ ((𝑋 × 𝑋) ∖ ∼ )) |
| 58 | 24, 30, 31 | fvproj 8159 |
. . . . . . . . . . . . . 14
⊢
(((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = 〈𝑎, 𝑏〉) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → (𝐻‘〈𝑥, 𝑦〉) = 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) |
| 59 | 38, 58, 39 | 3eqtr4d 2787 |
. . . . . . . . . . . . 13
⊢
(((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = 〈𝑎, 𝑏〉) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → (𝐻‘〈𝑥, 𝑦〉) = 𝑐) |
| 60 | | fveqeq2 6915 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ((𝐻‘𝑧) = 𝑐 ↔ (𝐻‘〈𝑥, 𝑦〉) = 𝑐)) |
| 61 | 60 | rspcev 3622 |
. . . . . . . . . . . . 13
⊢
((〈𝑥, 𝑦〉 ∈ ((𝑋 × 𝑋) ∖ ∼ ) ∧ (𝐻‘〈𝑥, 𝑦〉) = 𝑐) → ∃𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )(𝐻‘𝑧) = 𝑐) |
| 62 | 57, 59, 61 | syl2anc 584 |
. . . . . . . . . . . 12
⊢
(((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = 〈𝑎, 𝑏〉) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → ∃𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )(𝐻‘𝑧) = 𝑐) |
| 63 | | fofun 6821 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹:𝑋–onto→𝑌 → Fun 𝐹) |
| 64 | 4, 63 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → Fun 𝐹) |
| 65 | 64 | ad4antr 732 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = 〈𝑎, 𝑏〉) → Fun 𝐹) |
| 66 | 65 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = 〈𝑎, 𝑏〉) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) → Fun 𝐹) |
| 67 | | simp-4r 784 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = 〈𝑎, 𝑏〉) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) → 𝑏 ∈ 𝑌) |
| 68 | | foima 6825 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹:𝑋–onto→𝑌 → (𝐹 “ 𝑋) = 𝑌) |
| 69 | 4, 68 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐹 “ 𝑋) = 𝑌) |
| 70 | 69 | ad4antr 732 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = 〈𝑎, 𝑏〉) → (𝐹 “ 𝑋) = 𝑌) |
| 71 | 70 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = 〈𝑎, 𝑏〉) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) → (𝐹 “ 𝑋) = 𝑌) |
| 72 | 67, 71 | eleqtrrd 2844 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = 〈𝑎, 𝑏〉) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) → 𝑏 ∈ (𝐹 “ 𝑋)) |
| 73 | | fvelima 6974 |
. . . . . . . . . . . . 13
⊢ ((Fun
𝐹 ∧ 𝑏 ∈ (𝐹 “ 𝑋)) → ∃𝑦 ∈ 𝑋 (𝐹‘𝑦) = 𝑏) |
| 74 | 66, 72, 73 | syl2anc 584 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = 〈𝑎, 𝑏〉) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) → ∃𝑦 ∈ 𝑋 (𝐹‘𝑦) = 𝑏) |
| 75 | 62, 74 | r19.29a 3162 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = 〈𝑎, 𝑏〉) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) → ∃𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )(𝐻‘𝑧) = 𝑐) |
| 76 | | simpllr 776 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = 〈𝑎, 𝑏〉) → 𝑎 ∈ 𝑌) |
| 77 | 76, 70 | eleqtrrd 2844 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = 〈𝑎, 𝑏〉) → 𝑎 ∈ (𝐹 “ 𝑋)) |
| 78 | | fvelima 6974 |
. . . . . . . . . . . 12
⊢ ((Fun
𝐹 ∧ 𝑎 ∈ (𝐹 “ 𝑋)) → ∃𝑥 ∈ 𝑋 (𝐹‘𝑥) = 𝑎) |
| 79 | 65, 77, 78 | syl2anc 584 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = 〈𝑎, 𝑏〉) → ∃𝑥 ∈ 𝑋 (𝐹‘𝑥) = 𝑎) |
| 80 | 75, 79 | r19.29a 3162 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = 〈𝑎, 𝑏〉) → ∃𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )(𝐻‘𝑧) = 𝑐) |
| 81 | | simpr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) → 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) |
| 82 | 81 | eldifad 3963 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) → 𝑐 ∈ (𝑌 × 𝑌)) |
| 83 | | elxp2 5709 |
. . . . . . . . . . 11
⊢ (𝑐 ∈ (𝑌 × 𝑌) ↔ ∃𝑎 ∈ 𝑌 ∃𝑏 ∈ 𝑌 𝑐 = 〈𝑎, 𝑏〉) |
| 84 | 82, 83 | sylib 218 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) → ∃𝑎 ∈ 𝑌 ∃𝑏 ∈ 𝑌 𝑐 = 〈𝑎, 𝑏〉) |
| 85 | 80, 84 | r19.29vva 3216 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) → ∃𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )(𝐻‘𝑧) = 𝑐) |
| 86 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = 〈𝑥, 𝑦〉) → 𝑧 = 〈𝑥, 𝑦〉) |
| 87 | 86 | fveq2d 6910 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = 〈𝑥, 𝑦〉) → (𝐻‘𝑧) = (𝐻‘〈𝑥, 𝑦〉)) |
| 88 | | simp-4r 784 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = 〈𝑥, 𝑦〉) → (𝐻‘𝑧) = 𝑐) |
| 89 | | simpllr 776 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = 〈𝑥, 𝑦〉) → 𝑥 ∈ 𝑋) |
| 90 | | simplr 769 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = 〈𝑥, 𝑦〉) → 𝑦 ∈ 𝑋) |
| 91 | 24, 89, 90 | fvproj 8159 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = 〈𝑥, 𝑦〉) → (𝐻‘〈𝑥, 𝑦〉) = 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) |
| 92 | 87, 88, 91 | 3eqtr3d 2785 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = 〈𝑥, 𝑦〉) → 𝑐 = 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) |
| 93 | | fof 6820 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹:𝑋–onto→𝑌 → 𝐹:𝑋⟶𝑌) |
| 94 | 4, 93 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐹:𝑋⟶𝑌) |
| 95 | 94 | ad5antr 734 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = 〈𝑥, 𝑦〉) → 𝐹:𝑋⟶𝑌) |
| 96 | 95, 89 | ffvelcdmd 7105 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = 〈𝑥, 𝑦〉) → (𝐹‘𝑥) ∈ 𝑌) |
| 97 | 95, 90 | ffvelcdmd 7105 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = 〈𝑥, 𝑦〉) → (𝐹‘𝑦) ∈ 𝑌) |
| 98 | | opelxp 5721 |
. . . . . . . . . . . . . 14
⊢
(〈(𝐹‘𝑥), (𝐹‘𝑦)〉 ∈ (𝑌 × 𝑌) ↔ ((𝐹‘𝑥) ∈ 𝑌 ∧ (𝐹‘𝑦) ∈ 𝑌)) |
| 99 | 96, 97, 98 | sylanbrc 583 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = 〈𝑥, 𝑦〉) → 〈(𝐹‘𝑥), (𝐹‘𝑦)〉 ∈ (𝑌 × 𝑌)) |
| 100 | | simp-5r 786 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = 〈𝑥, 𝑦〉) → 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) |
| 101 | 86, 100 | eqeltrrd 2842 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = 〈𝑥, 𝑦〉) → 〈𝑥, 𝑦〉 ∈ ((𝑋 × 𝑋) ∖ ∼ )) |
| 102 | 56 | simprbi 496 |
. . . . . . . . . . . . . . 15
⊢
(〈𝑥, 𝑦〉 ∈ ((𝑋 × 𝑋) ∖ ∼ ) → ¬
𝑥 ∼ 𝑦) |
| 103 | 101, 102 | syl 17 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = 〈𝑥, 𝑦〉) → ¬ 𝑥 ∼ 𝑦) |
| 104 | 6 | ad5antr 734 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = 〈𝑥, 𝑦〉) → 𝐹 Fn 𝑋) |
| 105 | 104, 89, 90, 50 | syl3anc 1373 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = 〈𝑥, 𝑦〉) → (𝑥 ∼ 𝑦 ↔ (𝐹‘𝑥) = (𝐹‘𝑦))) |
| 106 | 105 | necon3bbid 2978 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = 〈𝑥, 𝑦〉) → (¬ 𝑥 ∼ 𝑦 ↔ (𝐹‘𝑥) ≠ (𝐹‘𝑦))) |
| 107 | 103, 106 | mpbid 232 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = 〈𝑥, 𝑦〉) → (𝐹‘𝑥) ≠ (𝐹‘𝑦)) |
| 108 | 99, 107, 45 | sylanbrc 583 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = 〈𝑥, 𝑦〉) → 〈(𝐹‘𝑥), (𝐹‘𝑦)〉 ∈ ((𝑌 × 𝑌) ∖ I )) |
| 109 | 92, 108 | eqeltrd 2841 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = 〈𝑥, 𝑦〉) → 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) |
| 110 | | eldifi 4131 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ ) → 𝑧 ∈ (𝑋 × 𝑋)) |
| 111 | 110 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) → 𝑧 ∈ (𝑋 × 𝑋)) |
| 112 | | elxp2 5709 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ (𝑋 × 𝑋) ↔ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 𝑧 = 〈𝑥, 𝑦〉) |
| 113 | 111, 112 | sylib 218 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) →
∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 𝑧 = 〈𝑥, 𝑦〉) |
| 114 | 113 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) → ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 𝑧 = 〈𝑥, 𝑦〉) |
| 115 | 109, 114 | r19.29vva 3216 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) → 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) |
| 116 | 115 | r19.29an 3158 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ∃𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )(𝐻‘𝑧) = 𝑐) → 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) |
| 117 | 85, 116 | impbida 801 |
. . . . . . . 8
⊢ (𝜑 → (𝑐 ∈ ((𝑌 × 𝑌) ∖ I ) ↔ ∃𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )(𝐻‘𝑧) = 𝑐)) |
| 118 | 29, 117 | bitr4id 290 |
. . . . . . 7
⊢ (𝜑 → (𝑐 ∈ (𝐻 “ ((𝑋 × 𝑋) ∖ ∼ )) ↔ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I ))) |
| 119 | 118 | eqrdv 2735 |
. . . . . 6
⊢ (𝜑 → (𝐻 “ ((𝑋 × 𝑋) ∖ ∼ )) = ((𝑌 × 𝑌) ∖ I )) |
| 120 | | ssv 4008 |
. . . . . . 7
⊢ 𝑌 ⊆ V |
| 121 | | xpss2 5705 |
. . . . . . 7
⊢ (𝑌 ⊆ V → (𝑌 × 𝑌) ⊆ (𝑌 × V)) |
| 122 | | difres 32613 |
. . . . . . 7
⊢ ((𝑌 × 𝑌) ⊆ (𝑌 × V) → ((𝑌 × 𝑌) ∖ ( I ↾ 𝑌)) = ((𝑌 × 𝑌) ∖ I )) |
| 123 | 120, 121,
122 | mp2b 10 |
. . . . . 6
⊢ ((𝑌 × 𝑌) ∖ ( I ↾ 𝑌)) = ((𝑌 × 𝑌) ∖ I ) |
| 124 | 119, 123 | eqtr4di 2795 |
. . . . 5
⊢ (𝜑 → (𝐻 “ ((𝑋 × 𝑋) ∖ ∼ )) = ((𝑌 × 𝑌) ∖ ( I ↾ 𝑌))) |
| 125 | 7 | toptopon 22923 |
. . . . . . 7
⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋)) |
| 126 | 3, 125 | sylib 218 |
. . . . . 6
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) |
| 127 | | qtoptopon 23712 |
. . . . . . 7
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→𝑌) → (𝐽 qTop 𝐹) ∈ (TopOn‘𝑌)) |
| 128 | 126, 4, 127 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → (𝐽 qTop 𝐹) ∈ (TopOn‘𝑌)) |
| 129 | | qtophaus.3 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐽) → (𝐹 “ 𝑥) ∈ (𝐽 qTop 𝐹)) |
| 130 | 129 | ralrimiva 3146 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑥 ∈ 𝐽 (𝐹 “ 𝑥) ∈ (𝐽 qTop 𝐹)) |
| 131 | | imaeq2 6074 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝐹 “ 𝑥) = (𝐹 “ 𝑦)) |
| 132 | 131 | eleq1d 2826 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → ((𝐹 “ 𝑥) ∈ (𝐽 qTop 𝐹) ↔ (𝐹 “ 𝑦) ∈ (𝐽 qTop 𝐹))) |
| 133 | 132 | cbvralvw 3237 |
. . . . . . . 8
⊢
(∀𝑥 ∈
𝐽 (𝐹 “ 𝑥) ∈ (𝐽 qTop 𝐹) ↔ ∀𝑦 ∈ 𝐽 (𝐹 “ 𝑦) ∈ (𝐽 qTop 𝐹)) |
| 134 | 130, 133 | sylib 218 |
. . . . . . 7
⊢ (𝜑 → ∀𝑦 ∈ 𝐽 (𝐹 “ 𝑦) ∈ (𝐽 qTop 𝐹)) |
| 135 | 134 | r19.21bi 3251 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐽) → (𝐹 “ 𝑦) ∈ (𝐽 qTop 𝐹)) |
| 136 | 7, 7 | txuni 23600 |
. . . . . . . . 9
⊢ ((𝐽 ∈ Top ∧ 𝐽 ∈ Top) → (𝑋 × 𝑋) = ∪ (𝐽 ×t 𝐽)) |
| 137 | 3, 3, 136 | syl2anc 584 |
. . . . . . . 8
⊢ (𝜑 → (𝑋 × 𝑋) = ∪ (𝐽 ×t 𝐽)) |
| 138 | 137 | difeq1d 4125 |
. . . . . . 7
⊢ (𝜑 → ((𝑋 × 𝑋) ∖ ∼ ) = (∪ (𝐽
×t 𝐽)
∖ ∼ )) |
| 139 | | qtophaus.4 |
. . . . . . . 8
⊢ (𝜑 → ∼ ∈
(Clsd‘(𝐽
×t 𝐽))) |
| 140 | | txtop 23577 |
. . . . . . . . . 10
⊢ ((𝐽 ∈ Top ∧ 𝐽 ∈ Top) → (𝐽 ×t 𝐽) ∈ Top) |
| 141 | 3, 3, 140 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → (𝐽 ×t 𝐽) ∈ Top) |
| 142 | | fcoinver 32617 |
. . . . . . . . . . . . 13
⊢ (𝐹 Fn 𝑋 → (◡𝐹 ∘ 𝐹) Er 𝑋) |
| 143 | 6, 142 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (◡𝐹 ∘ 𝐹) Er 𝑋) |
| 144 | | ereq1 8752 |
. . . . . . . . . . . . 13
⊢ ( ∼ =
(◡𝐹 ∘ 𝐹) → ( ∼ Er 𝑋 ↔ (◡𝐹 ∘ 𝐹) Er 𝑋)) |
| 145 | 49, 144 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ ( ∼ Er
𝑋 ↔ (◡𝐹 ∘ 𝐹) Er 𝑋) |
| 146 | 143, 145 | sylibr 234 |
. . . . . . . . . . 11
⊢ (𝜑 → ∼ Er 𝑋) |
| 147 | | erssxp 8768 |
. . . . . . . . . . 11
⊢ ( ∼ Er
𝑋 → ∼ ⊆ (𝑋 × 𝑋)) |
| 148 | 146, 147 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ∼ ⊆ (𝑋 × 𝑋)) |
| 149 | 148, 137 | sseqtrd 4020 |
. . . . . . . . 9
⊢ (𝜑 → ∼ ⊆ ∪ (𝐽
×t 𝐽)) |
| 150 | | eqid 2737 |
. . . . . . . . . 10
⊢ ∪ (𝐽
×t 𝐽) =
∪ (𝐽 ×t 𝐽) |
| 151 | 150 | iscld2 23036 |
. . . . . . . . 9
⊢ (((𝐽 ×t 𝐽) ∈ Top ∧ ∼
⊆ ∪ (𝐽 ×t 𝐽)) → ( ∼ ∈
(Clsd‘(𝐽
×t 𝐽))
↔ (∪ (𝐽 ×t 𝐽) ∖ ∼ ) ∈ (𝐽 ×t 𝐽))) |
| 152 | 141, 149,
151 | syl2anc 584 |
. . . . . . . 8
⊢ (𝜑 → ( ∼ ∈
(Clsd‘(𝐽
×t 𝐽))
↔ (∪ (𝐽 ×t 𝐽) ∖ ∼ ) ∈ (𝐽 ×t 𝐽))) |
| 153 | 139, 152 | mpbid 232 |
. . . . . . 7
⊢ (𝜑 → (∪ (𝐽
×t 𝐽)
∖ ∼ ) ∈ (𝐽 ×t 𝐽)) |
| 154 | 138, 153 | eqeltrd 2841 |
. . . . . 6
⊢ (𝜑 → ((𝑋 × 𝑋) ∖ ∼ ) ∈ (𝐽 ×t 𝐽)) |
| 155 | 94, 94, 126, 126, 128, 128, 129, 135, 154, 24 | txomap 33833 |
. . . . 5
⊢ (𝜑 → (𝐻 “ ((𝑋 × 𝑋) ∖ ∼ )) ∈ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹))) |
| 156 | 124, 155 | eqeltrrd 2842 |
. . . 4
⊢ (𝜑 → ((𝑌 × 𝑌) ∖ ( I ↾ 𝑌)) ∈ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹))) |
| 157 | 23, 156 | eqeltrd 2841 |
. . 3
⊢ (𝜑 → (∪ ((𝐽
qTop 𝐹) ×t
(𝐽 qTop 𝐹)) ∖ ( I ↾ ∪ (𝐽
qTop 𝐹))) ∈ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹))) |
| 158 | | eqid 2737 |
. . . . 5
⊢ ∪ ((𝐽
qTop 𝐹) ×t
(𝐽 qTop 𝐹)) = ∪ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)) |
| 159 | 158 | iscld2 23036 |
. . . 4
⊢ ((((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)) ∈ Top ∧ ( I ↾ ∪ (𝐽
qTop 𝐹)) ⊆ ∪ ((𝐽
qTop 𝐹) ×t
(𝐽 qTop 𝐹))) → (( I ↾ ∪ (𝐽
qTop 𝐹)) ∈
(Clsd‘((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹))) ↔ (∪
((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)) ∖ ( I ↾ ∪ (𝐽
qTop 𝐹))) ∈ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)))) |
| 160 | 159 | biimpar 477 |
. . 3
⊢
(((((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)) ∈ Top ∧ ( I ↾ ∪ (𝐽
qTop 𝐹)) ⊆ ∪ ((𝐽
qTop 𝐹) ×t
(𝐽 qTop 𝐹))) ∧ (∪
((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)) ∖ ( I ↾ ∪ (𝐽
qTop 𝐹))) ∈ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹))) → ( I ↾ ∪ (𝐽
qTop 𝐹)) ∈
(Clsd‘((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)))) |
| 161 | 11, 16, 157, 160 | syl21anc 838 |
. 2
⊢ (𝜑 → ( I ↾ ∪ (𝐽
qTop 𝐹)) ∈
(Clsd‘((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)))) |
| 162 | 13 | hausdiag 23653 |
. 2
⊢ ((𝐽 qTop 𝐹) ∈ Haus ↔ ((𝐽 qTop 𝐹) ∈ Top ∧ ( I ↾ ∪ (𝐽
qTop 𝐹)) ∈
(Clsd‘((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹))))) |
| 163 | 9, 161, 162 | sylanbrc 583 |
1
⊢ (𝜑 → (𝐽 qTop 𝐹) ∈ Haus) |