Step | Hyp | Ref
| Expression |
1 | | qtophaus.1 |
. . . 4
⊢ (𝜑 → 𝐽 ∈ Haus) |
2 | | haustop 20945 |
. . . 4
⊢ (𝐽 ∈ Haus → 𝐽 ∈ Top) |
3 | 1, 2 | syl 17 |
. . 3
⊢ (𝜑 → 𝐽 ∈ Top) |
4 | | qtophaus.2 |
. . . 4
⊢ (𝜑 → 𝐹:𝑋–onto→𝑌) |
5 | | fofn 6030 |
. . . 4
⊢ (𝐹:𝑋–onto→𝑌 → 𝐹 Fn 𝑋) |
6 | 4, 5 | syl 17 |
. . 3
⊢ (𝜑 → 𝐹 Fn 𝑋) |
7 | | qtophaus.x |
. . . 4
⊢ 𝑋 = ∪
𝐽 |
8 | 7 | qtoptop 21313 |
. . 3
⊢ ((𝐽 ∈ Top ∧ 𝐹 Fn 𝑋) → (𝐽 qTop 𝐹) ∈ Top) |
9 | 3, 6, 8 | syl2anc 691 |
. 2
⊢ (𝜑 → (𝐽 qTop 𝐹) ∈ Top) |
10 | | txtop 21182 |
. . . 4
⊢ (((𝐽 qTop 𝐹) ∈ Top ∧ (𝐽 qTop 𝐹) ∈ Top) → ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)) ∈ Top) |
11 | 9, 9, 10 | syl2anc 691 |
. . 3
⊢ (𝜑 → ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)) ∈ Top) |
12 | | idssxp 28811 |
. . . 4
⊢ ( I
↾ ∪ (𝐽 qTop 𝐹)) ⊆ (∪
(𝐽 qTop 𝐹) × ∪
(𝐽 qTop 𝐹)) |
13 | | eqid 2610 |
. . . . . 6
⊢ ∪ (𝐽
qTop 𝐹) = ∪ (𝐽
qTop 𝐹) |
14 | 13, 13 | txuni 21205 |
. . . . 5
⊢ (((𝐽 qTop 𝐹) ∈ Top ∧ (𝐽 qTop 𝐹) ∈ Top) → (∪ (𝐽
qTop 𝐹) × ∪ (𝐽
qTop 𝐹)) = ∪ ((𝐽
qTop 𝐹) ×t
(𝐽 qTop 𝐹))) |
15 | 9, 9, 14 | syl2anc 691 |
. . . 4
⊢ (𝜑 → (∪ (𝐽
qTop 𝐹) × ∪ (𝐽
qTop 𝐹)) = ∪ ((𝐽
qTop 𝐹) ×t
(𝐽 qTop 𝐹))) |
16 | 12, 15 | syl5sseq 3616 |
. . 3
⊢ (𝜑 → ( I ↾ ∪ (𝐽
qTop 𝐹)) ⊆ ∪ ((𝐽
qTop 𝐹) ×t
(𝐽 qTop 𝐹))) |
17 | 7 | qtopuni 21315 |
. . . . . . . 8
⊢ ((𝐽 ∈ Top ∧ 𝐹:𝑋–onto→𝑌) → 𝑌 = ∪ (𝐽 qTop 𝐹)) |
18 | 3, 4, 17 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 → 𝑌 = ∪ (𝐽 qTop 𝐹)) |
19 | 18 | sqxpeqd 5065 |
. . . . . 6
⊢ (𝜑 → (𝑌 × 𝑌) = (∪ (𝐽 qTop 𝐹) × ∪
(𝐽 qTop 𝐹))) |
20 | 19, 15 | eqtr2d 2645 |
. . . . 5
⊢ (𝜑 → ∪ ((𝐽
qTop 𝐹) ×t
(𝐽 qTop 𝐹)) = (𝑌 × 𝑌)) |
21 | 18 | eqcomd 2616 |
. . . . . 6
⊢ (𝜑 → ∪ (𝐽
qTop 𝐹) = 𝑌) |
22 | 21 | reseq2d 5317 |
. . . . 5
⊢ (𝜑 → ( I ↾ ∪ (𝐽
qTop 𝐹)) = ( I ↾
𝑌)) |
23 | 20, 22 | difeq12d 3691 |
. . . 4
⊢ (𝜑 → (∪ ((𝐽
qTop 𝐹) ×t
(𝐽 qTop 𝐹)) ∖ ( I ↾ ∪ (𝐽
qTop 𝐹))) = ((𝑌 × 𝑌) ∖ ( I ↾ 𝑌))) |
24 | | simp-4r 803 |
. . . . . . . . . . . . . . . 16
⊢
(((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = 〈𝑎, 𝑏〉) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → 𝑥 ∈ 𝑋) |
25 | | simplr 788 |
. . . . . . . . . . . . . . . 16
⊢
(((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = 〈𝑎, 𝑏〉) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → 𝑦 ∈ 𝑋) |
26 | | opelxpi 5072 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → 〈𝑥, 𝑦〉 ∈ (𝑋 × 𝑋)) |
27 | 24, 25, 26 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢
(((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = 〈𝑎, 𝑏〉) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → 〈𝑥, 𝑦〉 ∈ (𝑋 × 𝑋)) |
28 | | df-br 4584 |
. . . . . . . . . . . . . . 15
⊢ (𝑥(𝑋 × 𝑋)𝑦 ↔ 〈𝑥, 𝑦〉 ∈ (𝑋 × 𝑋)) |
29 | 27, 28 | sylibr 223 |
. . . . . . . . . . . . . 14
⊢
(((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = 〈𝑎, 𝑏〉) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → 𝑥(𝑋 × 𝑋)𝑦) |
30 | | simpllr 795 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = 〈𝑎, 𝑏〉) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → (𝐹‘𝑥) = 𝑎) |
31 | | simpr 476 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = 〈𝑎, 𝑏〉) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → (𝐹‘𝑦) = 𝑏) |
32 | 30, 31 | opeq12d 4348 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = 〈𝑎, 𝑏〉) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → 〈(𝐹‘𝑥), (𝐹‘𝑦)〉 = 〈𝑎, 𝑏〉) |
33 | | simp-5r 805 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = 〈𝑎, 𝑏〉) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → 𝑐 = 〈𝑎, 𝑏〉) |
34 | | simp-8r 811 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = 〈𝑎, 𝑏〉) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) |
35 | 33, 34 | eqeltrrd 2689 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = 〈𝑎, 𝑏〉) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → 〈𝑎, 𝑏〉 ∈ ((𝑌 × 𝑌) ∖ I )) |
36 | 32, 35 | eqeltrd 2688 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = 〈𝑎, 𝑏〉) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → 〈(𝐹‘𝑥), (𝐹‘𝑦)〉 ∈ ((𝑌 × 𝑌) ∖ I )) |
37 | | relxp 5150 |
. . . . . . . . . . . . . . . . . 18
⊢ Rel
(𝑌 × 𝑌) |
38 | | opeldifid 28794 |
. . . . . . . . . . . . . . . . . 18
⊢ (Rel
(𝑌 × 𝑌) → (〈(𝐹‘𝑥), (𝐹‘𝑦)〉 ∈ ((𝑌 × 𝑌) ∖ I ) ↔ (〈(𝐹‘𝑥), (𝐹‘𝑦)〉 ∈ (𝑌 × 𝑌) ∧ (𝐹‘𝑥) ≠ (𝐹‘𝑦)))) |
39 | 37, 38 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢
(〈(𝐹‘𝑥), (𝐹‘𝑦)〉 ∈ ((𝑌 × 𝑌) ∖ I ) ↔ (〈(𝐹‘𝑥), (𝐹‘𝑦)〉 ∈ (𝑌 × 𝑌) ∧ (𝐹‘𝑥) ≠ (𝐹‘𝑦))) |
40 | 36, 39 | sylib 207 |
. . . . . . . . . . . . . . . 16
⊢
(((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = 〈𝑎, 𝑏〉) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → (〈(𝐹‘𝑥), (𝐹‘𝑦)〉 ∈ (𝑌 × 𝑌) ∧ (𝐹‘𝑥) ≠ (𝐹‘𝑦))) |
41 | 40 | simprd 478 |
. . . . . . . . . . . . . . 15
⊢
(((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = 〈𝑎, 𝑏〉) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → (𝐹‘𝑥) ≠ (𝐹‘𝑦)) |
42 | 6 | ad8antr 772 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = 〈𝑎, 𝑏〉) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → 𝐹 Fn 𝑋) |
43 | | qtophaus.e |
. . . . . . . . . . . . . . . . . 18
⊢ ∼ =
(◡𝐹 ∘ 𝐹) |
44 | 43 | fcoinvbr 28799 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹 Fn 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥 ∼ 𝑦 ↔ (𝐹‘𝑥) = (𝐹‘𝑦))) |
45 | 42, 24, 25, 44 | syl3anc 1318 |
. . . . . . . . . . . . . . . 16
⊢
(((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = 〈𝑎, 𝑏〉) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → (𝑥 ∼ 𝑦 ↔ (𝐹‘𝑥) = (𝐹‘𝑦))) |
46 | 45 | necon3bbid 2819 |
. . . . . . . . . . . . . . 15
⊢
(((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = 〈𝑎, 𝑏〉) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → (¬ 𝑥 ∼ 𝑦 ↔ (𝐹‘𝑥) ≠ (𝐹‘𝑦))) |
47 | 41, 46 | mpbird 246 |
. . . . . . . . . . . . . 14
⊢
(((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = 〈𝑎, 𝑏〉) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → ¬ 𝑥 ∼ 𝑦) |
48 | | df-br 4584 |
. . . . . . . . . . . . . . 15
⊢ (𝑥((𝑋 × 𝑋) ∖ ∼ )𝑦 ↔ 〈𝑥, 𝑦〉 ∈ ((𝑋 × 𝑋) ∖ ∼ )) |
49 | | brdif 4635 |
. . . . . . . . . . . . . . 15
⊢ (𝑥((𝑋 × 𝑋) ∖ ∼ )𝑦 ↔ (𝑥(𝑋 × 𝑋)𝑦 ∧ ¬ 𝑥 ∼ 𝑦)) |
50 | 48, 49 | bitr3i 265 |
. . . . . . . . . . . . . 14
⊢
(〈𝑥, 𝑦〉 ∈ ((𝑋 × 𝑋) ∖ ∼ ) ↔ (𝑥(𝑋 × 𝑋)𝑦 ∧ ¬ 𝑥 ∼ 𝑦)) |
51 | 29, 47, 50 | sylanbrc 695 |
. . . . . . . . . . . . 13
⊢
(((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = 〈𝑎, 𝑏〉) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → 〈𝑥, 𝑦〉 ∈ ((𝑋 × 𝑋) ∖ ∼ )) |
52 | | qtophaus.h |
. . . . . . . . . . . . . . 15
⊢ 𝐻 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) |
53 | 52, 24, 25 | fvproj 29227 |
. . . . . . . . . . . . . 14
⊢
(((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = 〈𝑎, 𝑏〉) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → (𝐻‘〈𝑥, 𝑦〉) = 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) |
54 | 32, 53, 33 | 3eqtr4d 2654 |
. . . . . . . . . . . . 13
⊢
(((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = 〈𝑎, 𝑏〉) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → (𝐻‘〈𝑥, 𝑦〉) = 𝑐) |
55 | | fveq2 6103 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (𝐻‘𝑧) = (𝐻‘〈𝑥, 𝑦〉)) |
56 | 55 | eqeq1d 2612 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ((𝐻‘𝑧) = 𝑐 ↔ (𝐻‘〈𝑥, 𝑦〉) = 𝑐)) |
57 | 56 | rspcev 3282 |
. . . . . . . . . . . . 13
⊢
((〈𝑥, 𝑦〉 ∈ ((𝑋 × 𝑋) ∖ ∼ ) ∧ (𝐻‘〈𝑥, 𝑦〉) = 𝑐) → ∃𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )(𝐻‘𝑧) = 𝑐) |
58 | 51, 54, 57 | syl2anc 691 |
. . . . . . . . . . . 12
⊢
(((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = 〈𝑎, 𝑏〉) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → ∃𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )(𝐻‘𝑧) = 𝑐) |
59 | | fofun 6029 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹:𝑋–onto→𝑌 → Fun 𝐹) |
60 | 4, 59 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → Fun 𝐹) |
61 | 60 | ad4antr 764 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = 〈𝑎, 𝑏〉) → Fun 𝐹) |
62 | 61 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = 〈𝑎, 𝑏〉) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) → Fun 𝐹) |
63 | | simp-4r 803 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = 〈𝑎, 𝑏〉) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) → 𝑏 ∈ 𝑌) |
64 | | foima 6033 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹:𝑋–onto→𝑌 → (𝐹 “ 𝑋) = 𝑌) |
65 | 4, 64 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐹 “ 𝑋) = 𝑌) |
66 | 65 | ad4antr 764 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = 〈𝑎, 𝑏〉) → (𝐹 “ 𝑋) = 𝑌) |
67 | 66 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = 〈𝑎, 𝑏〉) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) → (𝐹 “ 𝑋) = 𝑌) |
68 | 63, 67 | eleqtrrd 2691 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = 〈𝑎, 𝑏〉) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) → 𝑏 ∈ (𝐹 “ 𝑋)) |
69 | | fvelima 6158 |
. . . . . . . . . . . . 13
⊢ ((Fun
𝐹 ∧ 𝑏 ∈ (𝐹 “ 𝑋)) → ∃𝑦 ∈ 𝑋 (𝐹‘𝑦) = 𝑏) |
70 | 62, 68, 69 | syl2anc 691 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = 〈𝑎, 𝑏〉) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) → ∃𝑦 ∈ 𝑋 (𝐹‘𝑦) = 𝑏) |
71 | 58, 70 | r19.29a 3060 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = 〈𝑎, 𝑏〉) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) → ∃𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )(𝐻‘𝑧) = 𝑐) |
72 | | simpllr 795 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = 〈𝑎, 𝑏〉) → 𝑎 ∈ 𝑌) |
73 | 72, 66 | eleqtrrd 2691 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = 〈𝑎, 𝑏〉) → 𝑎 ∈ (𝐹 “ 𝑋)) |
74 | | fvelima 6158 |
. . . . . . . . . . . 12
⊢ ((Fun
𝐹 ∧ 𝑎 ∈ (𝐹 “ 𝑋)) → ∃𝑥 ∈ 𝑋 (𝐹‘𝑥) = 𝑎) |
75 | 61, 73, 74 | syl2anc 691 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = 〈𝑎, 𝑏〉) → ∃𝑥 ∈ 𝑋 (𝐹‘𝑥) = 𝑎) |
76 | 71, 75 | r19.29a 3060 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = 〈𝑎, 𝑏〉) → ∃𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )(𝐻‘𝑧) = 𝑐) |
77 | | simpr 476 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) → 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) |
78 | 77 | eldifad 3552 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) → 𝑐 ∈ (𝑌 × 𝑌)) |
79 | | elxp2 5056 |
. . . . . . . . . . 11
⊢ (𝑐 ∈ (𝑌 × 𝑌) ↔ ∃𝑎 ∈ 𝑌 ∃𝑏 ∈ 𝑌 𝑐 = 〈𝑎, 𝑏〉) |
80 | 78, 79 | sylib 207 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) → ∃𝑎 ∈ 𝑌 ∃𝑏 ∈ 𝑌 𝑐 = 〈𝑎, 𝑏〉) |
81 | 76, 80 | r19.29vva 3062 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) → ∃𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )(𝐻‘𝑧) = 𝑐) |
82 | | simpr 476 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = 〈𝑥, 𝑦〉) → 𝑧 = 〈𝑥, 𝑦〉) |
83 | 82 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = 〈𝑥, 𝑦〉) → (𝐻‘𝑧) = (𝐻‘〈𝑥, 𝑦〉)) |
84 | | simp-4r 803 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = 〈𝑥, 𝑦〉) → (𝐻‘𝑧) = 𝑐) |
85 | | simpllr 795 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = 〈𝑥, 𝑦〉) → 𝑥 ∈ 𝑋) |
86 | | simplr 788 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = 〈𝑥, 𝑦〉) → 𝑦 ∈ 𝑋) |
87 | 52, 85, 86 | fvproj 29227 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = 〈𝑥, 𝑦〉) → (𝐻‘〈𝑥, 𝑦〉) = 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) |
88 | 83, 84, 87 | 3eqtr3d 2652 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = 〈𝑥, 𝑦〉) → 𝑐 = 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) |
89 | | fof 6028 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹:𝑋–onto→𝑌 → 𝐹:𝑋⟶𝑌) |
90 | 4, 89 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐹:𝑋⟶𝑌) |
91 | 90 | ad5antr 766 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = 〈𝑥, 𝑦〉) → 𝐹:𝑋⟶𝑌) |
92 | 91, 85 | ffvelrnd 6268 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = 〈𝑥, 𝑦〉) → (𝐹‘𝑥) ∈ 𝑌) |
93 | 91, 86 | ffvelrnd 6268 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = 〈𝑥, 𝑦〉) → (𝐹‘𝑦) ∈ 𝑌) |
94 | | opelxp 5070 |
. . . . . . . . . . . . . 14
⊢
(〈(𝐹‘𝑥), (𝐹‘𝑦)〉 ∈ (𝑌 × 𝑌) ↔ ((𝐹‘𝑥) ∈ 𝑌 ∧ (𝐹‘𝑦) ∈ 𝑌)) |
95 | 92, 93, 94 | sylanbrc 695 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = 〈𝑥, 𝑦〉) → 〈(𝐹‘𝑥), (𝐹‘𝑦)〉 ∈ (𝑌 × 𝑌)) |
96 | | simp-5r 805 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = 〈𝑥, 𝑦〉) → 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) |
97 | 82, 96 | eqeltrrd 2689 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = 〈𝑥, 𝑦〉) → 〈𝑥, 𝑦〉 ∈ ((𝑋 × 𝑋) ∖ ∼ )) |
98 | 50 | simprbi 479 |
. . . . . . . . . . . . . . 15
⊢
(〈𝑥, 𝑦〉 ∈ ((𝑋 × 𝑋) ∖ ∼ ) → ¬
𝑥 ∼ 𝑦) |
99 | 97, 98 | syl 17 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = 〈𝑥, 𝑦〉) → ¬ 𝑥 ∼ 𝑦) |
100 | 6 | ad5antr 766 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = 〈𝑥, 𝑦〉) → 𝐹 Fn 𝑋) |
101 | 100, 85, 86, 44 | syl3anc 1318 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = 〈𝑥, 𝑦〉) → (𝑥 ∼ 𝑦 ↔ (𝐹‘𝑥) = (𝐹‘𝑦))) |
102 | 101 | necon3bbid 2819 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = 〈𝑥, 𝑦〉) → (¬ 𝑥 ∼ 𝑦 ↔ (𝐹‘𝑥) ≠ (𝐹‘𝑦))) |
103 | 99, 102 | mpbid 221 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = 〈𝑥, 𝑦〉) → (𝐹‘𝑥) ≠ (𝐹‘𝑦)) |
104 | 95, 103, 39 | sylanbrc 695 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = 〈𝑥, 𝑦〉) → 〈(𝐹‘𝑥), (𝐹‘𝑦)〉 ∈ ((𝑌 × 𝑌) ∖ I )) |
105 | 88, 104 | eqeltrd 2688 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = 〈𝑥, 𝑦〉) → 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) |
106 | | eldifi 3694 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ ) → 𝑧 ∈ (𝑋 × 𝑋)) |
107 | 106 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) → 𝑧 ∈ (𝑋 × 𝑋)) |
108 | | elxp2 5056 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ (𝑋 × 𝑋) ↔ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 𝑧 = 〈𝑥, 𝑦〉) |
109 | 107, 108 | sylib 207 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) →
∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 𝑧 = 〈𝑥, 𝑦〉) |
110 | 109 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) → ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 𝑧 = 〈𝑥, 𝑦〉) |
111 | 105, 110 | r19.29vva 3062 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) → 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) |
112 | 111 | r19.29an 3059 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ∃𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )(𝐻‘𝑧) = 𝑐) → 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) |
113 | 81, 112 | impbida 873 |
. . . . . . . 8
⊢ (𝜑 → (𝑐 ∈ ((𝑌 × 𝑌) ∖ I ) ↔ ∃𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )(𝐻‘𝑧) = 𝑐)) |
114 | | opex 4859 |
. . . . . . . . . 10
⊢
〈(𝐹‘𝑥), (𝐹‘𝑦)〉 ∈ V |
115 | 52, 114 | fnmpt2i 7128 |
. . . . . . . . 9
⊢ 𝐻 Fn (𝑋 × 𝑋) |
116 | | difss 3699 |
. . . . . . . . 9
⊢ ((𝑋 × 𝑋) ∖ ∼ ) ⊆ (𝑋 × 𝑋) |
117 | | fvelimab 6163 |
. . . . . . . . 9
⊢ ((𝐻 Fn (𝑋 × 𝑋) ∧ ((𝑋 × 𝑋) ∖ ∼ ) ⊆ (𝑋 × 𝑋)) → (𝑐 ∈ (𝐻 “ ((𝑋 × 𝑋) ∖ ∼ )) ↔
∃𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )(𝐻‘𝑧) = 𝑐)) |
118 | 115, 116,
117 | mp2an 704 |
. . . . . . . 8
⊢ (𝑐 ∈ (𝐻 “ ((𝑋 × 𝑋) ∖ ∼ )) ↔
∃𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )(𝐻‘𝑧) = 𝑐) |
119 | 113, 118 | syl6rbbr 278 |
. . . . . . 7
⊢ (𝜑 → (𝑐 ∈ (𝐻 “ ((𝑋 × 𝑋) ∖ ∼ )) ↔ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I ))) |
120 | 119 | eqrdv 2608 |
. . . . . 6
⊢ (𝜑 → (𝐻 “ ((𝑋 × 𝑋) ∖ ∼ )) = ((𝑌 × 𝑌) ∖ I )) |
121 | | ssv 3588 |
. . . . . . 7
⊢ 𝑌 ⊆ V |
122 | | xpss2 5152 |
. . . . . . 7
⊢ (𝑌 ⊆ V → (𝑌 × 𝑌) ⊆ (𝑌 × V)) |
123 | | difres 28795 |
. . . . . . 7
⊢ ((𝑌 × 𝑌) ⊆ (𝑌 × V) → ((𝑌 × 𝑌) ∖ ( I ↾ 𝑌)) = ((𝑌 × 𝑌) ∖ I )) |
124 | 121, 122,
123 | mp2b 10 |
. . . . . 6
⊢ ((𝑌 × 𝑌) ∖ ( I ↾ 𝑌)) = ((𝑌 × 𝑌) ∖ I ) |
125 | 120, 124 | syl6eqr 2662 |
. . . . 5
⊢ (𝜑 → (𝐻 “ ((𝑋 × 𝑋) ∖ ∼ )) = ((𝑌 × 𝑌) ∖ ( I ↾ 𝑌))) |
126 | 7 | toptopon 20548 |
. . . . . . 7
⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋)) |
127 | 3, 126 | sylib 207 |
. . . . . 6
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) |
128 | | qtoptopon 21317 |
. . . . . . 7
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→𝑌) → (𝐽 qTop 𝐹) ∈ (TopOn‘𝑌)) |
129 | 127, 4, 128 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 → (𝐽 qTop 𝐹) ∈ (TopOn‘𝑌)) |
130 | | qtophaus.3 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐽) → (𝐹 “ 𝑥) ∈ (𝐽 qTop 𝐹)) |
131 | 130 | ralrimiva 2949 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑥 ∈ 𝐽 (𝐹 “ 𝑥) ∈ (𝐽 qTop 𝐹)) |
132 | | imaeq2 5381 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝐹 “ 𝑥) = (𝐹 “ 𝑦)) |
133 | 132 | eleq1d 2672 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → ((𝐹 “ 𝑥) ∈ (𝐽 qTop 𝐹) ↔ (𝐹 “ 𝑦) ∈ (𝐽 qTop 𝐹))) |
134 | 133 | cbvralv 3147 |
. . . . . . . 8
⊢
(∀𝑥 ∈
𝐽 (𝐹 “ 𝑥) ∈ (𝐽 qTop 𝐹) ↔ ∀𝑦 ∈ 𝐽 (𝐹 “ 𝑦) ∈ (𝐽 qTop 𝐹)) |
135 | 131, 134 | sylib 207 |
. . . . . . 7
⊢ (𝜑 → ∀𝑦 ∈ 𝐽 (𝐹 “ 𝑦) ∈ (𝐽 qTop 𝐹)) |
136 | 135 | r19.21bi 2916 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐽) → (𝐹 “ 𝑦) ∈ (𝐽 qTop 𝐹)) |
137 | 7, 7 | txuni 21205 |
. . . . . . . . 9
⊢ ((𝐽 ∈ Top ∧ 𝐽 ∈ Top) → (𝑋 × 𝑋) = ∪ (𝐽 ×t 𝐽)) |
138 | 3, 3, 137 | syl2anc 691 |
. . . . . . . 8
⊢ (𝜑 → (𝑋 × 𝑋) = ∪ (𝐽 ×t 𝐽)) |
139 | 138 | difeq1d 3689 |
. . . . . . 7
⊢ (𝜑 → ((𝑋 × 𝑋) ∖ ∼ ) = (∪ (𝐽
×t 𝐽)
∖ ∼ )) |
140 | | qtophaus.4 |
. . . . . . . 8
⊢ (𝜑 → ∼ ∈
(Clsd‘(𝐽
×t 𝐽))) |
141 | | txtop 21182 |
. . . . . . . . . 10
⊢ ((𝐽 ∈ Top ∧ 𝐽 ∈ Top) → (𝐽 ×t 𝐽) ∈ Top) |
142 | 3, 3, 141 | syl2anc 691 |
. . . . . . . . 9
⊢ (𝜑 → (𝐽 ×t 𝐽) ∈ Top) |
143 | | fcoinver 28798 |
. . . . . . . . . . . . 13
⊢ (𝐹 Fn 𝑋 → (◡𝐹 ∘ 𝐹) Er 𝑋) |
144 | 6, 143 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (◡𝐹 ∘ 𝐹) Er 𝑋) |
145 | | ereq1 7636 |
. . . . . . . . . . . . 13
⊢ ( ∼ =
(◡𝐹 ∘ 𝐹) → ( ∼ Er 𝑋 ↔ (◡𝐹 ∘ 𝐹) Er 𝑋)) |
146 | 43, 145 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ ( ∼ Er
𝑋 ↔ (◡𝐹 ∘ 𝐹) Er 𝑋) |
147 | 144, 146 | sylibr 223 |
. . . . . . . . . . 11
⊢ (𝜑 → ∼ Er 𝑋) |
148 | | erssxp 7652 |
. . . . . . . . . . 11
⊢ ( ∼ Er
𝑋 → ∼ ⊆ (𝑋 × 𝑋)) |
149 | 147, 148 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ∼ ⊆ (𝑋 × 𝑋)) |
150 | 149, 138 | sseqtrd 3604 |
. . . . . . . . 9
⊢ (𝜑 → ∼ ⊆ ∪ (𝐽
×t 𝐽)) |
151 | | eqid 2610 |
. . . . . . . . . 10
⊢ ∪ (𝐽
×t 𝐽) =
∪ (𝐽 ×t 𝐽) |
152 | 151 | iscld2 20642 |
. . . . . . . . 9
⊢ (((𝐽 ×t 𝐽) ∈ Top ∧ ∼
⊆ ∪ (𝐽 ×t 𝐽)) → ( ∼ ∈
(Clsd‘(𝐽
×t 𝐽))
↔ (∪ (𝐽 ×t 𝐽) ∖ ∼ ) ∈ (𝐽 ×t 𝐽))) |
153 | 142, 150,
152 | syl2anc 691 |
. . . . . . . 8
⊢ (𝜑 → ( ∼ ∈
(Clsd‘(𝐽
×t 𝐽))
↔ (∪ (𝐽 ×t 𝐽) ∖ ∼ ) ∈ (𝐽 ×t 𝐽))) |
154 | 140, 153 | mpbid 221 |
. . . . . . 7
⊢ (𝜑 → (∪ (𝐽
×t 𝐽)
∖ ∼ ) ∈ (𝐽 ×t 𝐽)) |
155 | 139, 154 | eqeltrd 2688 |
. . . . . 6
⊢ (𝜑 → ((𝑋 × 𝑋) ∖ ∼ ) ∈ (𝐽 ×t 𝐽)) |
156 | 90, 90, 127, 127, 129, 129, 130, 136, 155, 52 | txomap 29229 |
. . . . 5
⊢ (𝜑 → (𝐻 “ ((𝑋 × 𝑋) ∖ ∼ )) ∈ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹))) |
157 | 125, 156 | eqeltrrd 2689 |
. . . 4
⊢ (𝜑 → ((𝑌 × 𝑌) ∖ ( I ↾ 𝑌)) ∈ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹))) |
158 | 23, 157 | eqeltrd 2688 |
. . 3
⊢ (𝜑 → (∪ ((𝐽
qTop 𝐹) ×t
(𝐽 qTop 𝐹)) ∖ ( I ↾ ∪ (𝐽
qTop 𝐹))) ∈ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹))) |
159 | | eqid 2610 |
. . . . 5
⊢ ∪ ((𝐽
qTop 𝐹) ×t
(𝐽 qTop 𝐹)) = ∪ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)) |
160 | 159 | iscld2 20642 |
. . . 4
⊢ ((((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)) ∈ Top ∧ ( I ↾ ∪ (𝐽
qTop 𝐹)) ⊆ ∪ ((𝐽
qTop 𝐹) ×t
(𝐽 qTop 𝐹))) → (( I ↾ ∪ (𝐽
qTop 𝐹)) ∈
(Clsd‘((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹))) ↔ (∪
((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)) ∖ ( I ↾ ∪ (𝐽
qTop 𝐹))) ∈ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)))) |
161 | 160 | biimpar 501 |
. . 3
⊢
(((((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)) ∈ Top ∧ ( I ↾ ∪ (𝐽
qTop 𝐹)) ⊆ ∪ ((𝐽
qTop 𝐹) ×t
(𝐽 qTop 𝐹))) ∧ (∪
((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)) ∖ ( I ↾ ∪ (𝐽
qTop 𝐹))) ∈ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹))) → ( I ↾ ∪ (𝐽
qTop 𝐹)) ∈
(Clsd‘((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)))) |
162 | 11, 16, 158, 161 | syl21anc 1317 |
. 2
⊢ (𝜑 → ( I ↾ ∪ (𝐽
qTop 𝐹)) ∈
(Clsd‘((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)))) |
163 | 13 | hausdiag 21258 |
. 2
⊢ ((𝐽 qTop 𝐹) ∈ Haus ↔ ((𝐽 qTop 𝐹) ∈ Top ∧ ( I ↾ ∪ (𝐽
qTop 𝐹)) ∈
(Clsd‘((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹))))) |
164 | 9, 162, 163 | sylanbrc 695 |
1
⊢ (𝜑 → (𝐽 qTop 𝐹) ∈ Haus) |