Step | Hyp | Ref
| Expression |
1 | | xpstopnlem1.j |
. . . . . . . . . 10
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) |
2 | | xpstopnlem1.k |
. . . . . . . . . 10
⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) |
3 | | txtopon 21204 |
. . . . . . . . . 10
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌))) |
4 | 1, 2, 3 | syl2anc 691 |
. . . . . . . . 9
⊢ (𝜑 → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌))) |
5 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢
(∏t‘{〈∅, 𝐽〉}) =
(∏t‘{〈∅, 𝐽〉}) |
6 | | 0ex 4718 |
. . . . . . . . . . . . . 14
⊢ ∅
∈ V |
7 | 6 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∅ ∈
V) |
8 | 5, 7, 1 | pt1hmeo 21419 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑧 ∈ 𝑋 ↦ {〈∅, 𝑧〉}) ∈ (𝐽Homeo(∏t‘{〈∅,
𝐽〉}))) |
9 | | hmeocn 21373 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ 𝑋 ↦ {〈∅, 𝑧〉}) ∈ (𝐽Homeo(∏t‘{〈∅,
𝐽〉})) → (𝑧 ∈ 𝑋 ↦ {〈∅, 𝑧〉}) ∈ (𝐽 Cn (∏t‘{〈∅,
𝐽〉}))) |
10 | | cntop2 20855 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ 𝑋 ↦ {〈∅, 𝑧〉}) ∈ (𝐽 Cn
(∏t‘{〈∅, 𝐽〉})) →
(∏t‘{〈∅, 𝐽〉}) ∈ Top) |
11 | 8, 9, 10 | 3syl 18 |
. . . . . . . . . . 11
⊢ (𝜑 →
(∏t‘{〈∅, 𝐽〉}) ∈ Top) |
12 | | eqid 2610 |
. . . . . . . . . . . 12
⊢ ∪ (∏t‘{〈∅, 𝐽〉}) = ∪ (∏t‘{〈∅, 𝐽〉}) |
13 | 12 | toptopon 20548 |
. . . . . . . . . . 11
⊢
((∏t‘{〈∅, 𝐽〉}) ∈ Top ↔
(∏t‘{〈∅, 𝐽〉}) ∈ (TopOn‘∪ (∏t‘{〈∅, 𝐽〉}))) |
14 | 11, 13 | sylib 207 |
. . . . . . . . . 10
⊢ (𝜑 →
(∏t‘{〈∅, 𝐽〉}) ∈ (TopOn‘∪ (∏t‘{〈∅, 𝐽〉}))) |
15 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢
(∏t‘{〈1𝑜, 𝐾〉}) =
(∏t‘{〈1𝑜, 𝐾〉}) |
16 | | 1on 7454 |
. . . . . . . . . . . . . 14
⊢
1𝑜 ∈ On |
17 | 16 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 1𝑜
∈ On) |
18 | 15, 17, 2 | pt1hmeo 21419 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑧 ∈ 𝑌 ↦ {〈1𝑜, 𝑧〉}) ∈ (𝐾Homeo(∏t‘{〈1𝑜,
𝐾〉}))) |
19 | | hmeocn 21373 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ 𝑌 ↦ {〈1𝑜, 𝑧〉}) ∈ (𝐾Homeo(∏t‘{〈1𝑜,
𝐾〉})) → (𝑧 ∈ 𝑌
↦ {〈1𝑜, 𝑧〉}) ∈ (𝐾 Cn (∏t‘{〈1𝑜,
𝐾〉}))) |
20 | | cntop2 20855 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ 𝑌 ↦ {〈1𝑜, 𝑧〉}) ∈ (𝐾 Cn
(∏t‘{〈1𝑜, 𝐾〉})) →
(∏t‘{〈1𝑜, 𝐾〉}) ∈ Top) |
21 | 18, 19, 20 | 3syl 18 |
. . . . . . . . . . 11
⊢ (𝜑 →
(∏t‘{〈1𝑜, 𝐾〉}) ∈ Top) |
22 | | eqid 2610 |
. . . . . . . . . . . 12
⊢ ∪ (∏t‘{〈1𝑜,
𝐾〉}) = ∪ (∏t‘{〈1𝑜,
𝐾〉}) |
23 | 22 | toptopon 20548 |
. . . . . . . . . . 11
⊢
((∏t‘{〈1𝑜, 𝐾〉}) ∈ Top ↔
(∏t‘{〈1𝑜, 𝐾〉}) ∈ (TopOn‘∪ (∏t‘{〈1𝑜,
𝐾〉}))) |
24 | 21, 23 | sylib 207 |
. . . . . . . . . 10
⊢ (𝜑 →
(∏t‘{〈1𝑜, 𝐾〉}) ∈ (TopOn‘∪ (∏t‘{〈1𝑜,
𝐾〉}))) |
25 | | txtopon 21204 |
. . . . . . . . . 10
⊢
(((∏t‘{〈∅, 𝐽〉}) ∈ (TopOn‘∪ (∏t‘{〈∅, 𝐽〉})) ∧
(∏t‘{〈1𝑜, 𝐾〉}) ∈ (TopOn‘∪ (∏t‘{〈1𝑜,
𝐾〉}))) →
((∏t‘{〈∅, 𝐽〉}) ×t
(∏t‘{〈1𝑜, 𝐾〉})) ∈ (TopOn‘(∪ (∏t‘{〈∅, 𝐽〉}) × ∪ (∏t‘{〈1𝑜,
𝐾〉})))) |
26 | 14, 24, 25 | syl2anc 691 |
. . . . . . . . 9
⊢ (𝜑 →
((∏t‘{〈∅, 𝐽〉}) ×t
(∏t‘{〈1𝑜, 𝐾〉})) ∈ (TopOn‘(∪ (∏t‘{〈∅, 𝐽〉}) × ∪ (∏t‘{〈1𝑜,
𝐾〉})))) |
27 | | opeq2 4341 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 𝑥 → 〈∅, 𝑧〉 = 〈∅, 𝑥〉) |
28 | 27 | sneqd 4137 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑥 → {〈∅, 𝑧〉} = {〈∅, 𝑥〉}) |
29 | | eqid 2610 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ 𝑋 ↦ {〈∅, 𝑧〉}) = (𝑧 ∈ 𝑋 ↦ {〈∅, 𝑧〉}) |
30 | | snex 4835 |
. . . . . . . . . . . . . . 15
⊢
{〈∅, 𝑥〉} ∈ V |
31 | 28, 29, 30 | fvmpt 6191 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝑋 → ((𝑧 ∈ 𝑋 ↦ {〈∅, 𝑧〉})‘𝑥) = {〈∅, 𝑥〉}) |
32 | | opeq2 4341 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 𝑦 → 〈1𝑜, 𝑧〉 =
〈1𝑜, 𝑦〉) |
33 | 32 | sneqd 4137 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑦 → {〈1𝑜, 𝑧〉} =
{〈1𝑜, 𝑦〉}) |
34 | | eqid 2610 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ 𝑌 ↦ {〈1𝑜, 𝑧〉}) = (𝑧 ∈ 𝑌 ↦ {〈1𝑜, 𝑧〉}) |
35 | | snex 4835 |
. . . . . . . . . . . . . . 15
⊢
{〈1𝑜, 𝑦〉} ∈ V |
36 | 33, 34, 35 | fvmpt 6191 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ 𝑌 → ((𝑧 ∈ 𝑌 ↦ {〈1𝑜, 𝑧〉})‘𝑦) =
{〈1𝑜, 𝑦〉}) |
37 | | opeq12 4342 |
. . . . . . . . . . . . . 14
⊢ ((((𝑧 ∈ 𝑋 ↦ {〈∅, 𝑧〉})‘𝑥) = {〈∅, 𝑥〉} ∧ ((𝑧 ∈ 𝑌 ↦ {〈1𝑜, 𝑧〉})‘𝑦) =
{〈1𝑜, 𝑦〉}) → 〈((𝑧 ∈ 𝑋 ↦ {〈∅, 𝑧〉})‘𝑥), ((𝑧 ∈ 𝑌 ↦ {〈1𝑜, 𝑧〉})‘𝑦)〉 = 〈{〈∅,
𝑥〉},
{〈1𝑜, 𝑦〉}〉) |
38 | 31, 36, 37 | syl2an 493 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) → 〈((𝑧 ∈ 𝑋 ↦ {〈∅, 𝑧〉})‘𝑥), ((𝑧 ∈ 𝑌 ↦ {〈1𝑜, 𝑧〉})‘𝑦)〉 = 〈{〈∅,
𝑥〉},
{〈1𝑜, 𝑦〉}〉) |
39 | 38 | mpt2eq3ia 6618 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈((𝑧 ∈ 𝑋 ↦ {〈∅, 𝑧〉})‘𝑥), ((𝑧 ∈ 𝑌 ↦ {〈1𝑜, 𝑧〉})‘𝑦)〉) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈{〈∅, 𝑥〉},
{〈1𝑜, 𝑦〉}〉) |
40 | | toponuni 20542 |
. . . . . . . . . . . . . 14
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝐽) |
41 | 1, 40 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑋 = ∪ 𝐽) |
42 | | toponuni 20542 |
. . . . . . . . . . . . . 14
⊢ (𝐾 ∈ (TopOn‘𝑌) → 𝑌 = ∪ 𝐾) |
43 | 2, 42 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑌 = ∪ 𝐾) |
44 | | mpt2eq12 6613 |
. . . . . . . . . . . . 13
⊢ ((𝑋 = ∪
𝐽 ∧ 𝑌 = ∪ 𝐾) → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈((𝑧 ∈ 𝑋 ↦ {〈∅, 𝑧〉})‘𝑥), ((𝑧 ∈ 𝑌 ↦ {〈1𝑜, 𝑧〉})‘𝑦)〉) = (𝑥 ∈ ∪ 𝐽, 𝑦 ∈ ∪ 𝐾 ↦ 〈((𝑧 ∈ 𝑋 ↦ {〈∅, 𝑧〉})‘𝑥), ((𝑧 ∈ 𝑌 ↦ {〈1𝑜, 𝑧〉})‘𝑦)〉)) |
45 | 41, 43, 44 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈((𝑧 ∈ 𝑋 ↦ {〈∅, 𝑧〉})‘𝑥), ((𝑧 ∈ 𝑌 ↦ {〈1𝑜, 𝑧〉})‘𝑦)〉) = (𝑥 ∈ ∪ 𝐽, 𝑦 ∈ ∪ 𝐾 ↦ 〈((𝑧 ∈ 𝑋 ↦ {〈∅, 𝑧〉})‘𝑥), ((𝑧 ∈ 𝑌 ↦ {〈1𝑜, 𝑧〉})‘𝑦)〉)) |
46 | 39, 45 | syl5eqr 2658 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈{〈∅, 𝑥〉},
{〈1𝑜, 𝑦〉}〉) = (𝑥 ∈ ∪ 𝐽, 𝑦 ∈ ∪ 𝐾 ↦ 〈((𝑧 ∈ 𝑋 ↦ {〈∅, 𝑧〉})‘𝑥), ((𝑧 ∈ 𝑌 ↦ {〈1𝑜, 𝑧〉})‘𝑦)〉)) |
47 | | eqid 2610 |
. . . . . . . . . . . 12
⊢ ∪ 𝐽 =
∪ 𝐽 |
48 | | eqid 2610 |
. . . . . . . . . . . 12
⊢ ∪ 𝐾 =
∪ 𝐾 |
49 | 47, 48, 8, 18 | txhmeo 21416 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ ∪ 𝐽, 𝑦 ∈ ∪ 𝐾 ↦ 〈((𝑧 ∈ 𝑋 ↦ {〈∅, 𝑧〉})‘𝑥), ((𝑧 ∈ 𝑌 ↦ {〈1𝑜, 𝑧〉})‘𝑦)〉) ∈ ((𝐽 ×t 𝐾)Homeo((∏t‘{〈∅,
𝐽〉}) ×t
(∏t‘{〈1𝑜, 𝐾〉})))) |
50 | 46, 49 | eqeltrd 2688 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈{〈∅, 𝑥〉},
{〈1𝑜, 𝑦〉}〉) ∈ ((𝐽 ×t 𝐾)Homeo((∏t‘{〈∅,
𝐽〉}) ×t
(∏t‘{〈1𝑜, 𝐾〉})))) |
51 | | hmeocn 21373 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈{〈∅, 𝑥〉},
{〈1𝑜, 𝑦〉}〉) ∈ ((𝐽 ×t 𝐾)Homeo((∏t‘{〈∅,
𝐽〉}) ×t
(∏t‘{〈1𝑜, 𝐾〉}))) → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈{〈∅, 𝑥〉},
{〈1𝑜, 𝑦〉}〉) ∈ ((𝐽 ×t 𝐾) Cn ((∏t‘{〈∅,
𝐽〉}) ×t
(∏t‘{〈1𝑜, 𝐾〉})))) |
52 | 50, 51 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈{〈∅, 𝑥〉},
{〈1𝑜, 𝑦〉}〉) ∈ ((𝐽 ×t 𝐾) Cn
((∏t‘{〈∅, 𝐽〉}) ×t
(∏t‘{〈1𝑜, 𝐾〉})))) |
53 | | cnf2 20863 |
. . . . . . . . 9
⊢ (((𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)) ∧
((∏t‘{〈∅, 𝐽〉}) ×t
(∏t‘{〈1𝑜, 𝐾〉})) ∈ (TopOn‘(∪ (∏t‘{〈∅, 𝐽〉}) × ∪ (∏t‘{〈1𝑜,
𝐾〉}))) ∧ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈{〈∅, 𝑥〉},
{〈1𝑜, 𝑦〉}〉) ∈ ((𝐽 ×t 𝐾) Cn
((∏t‘{〈∅, 𝐽〉}) ×t
(∏t‘{〈1𝑜, 𝐾〉})))) → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈{〈∅, 𝑥〉},
{〈1𝑜, 𝑦〉}〉):(𝑋 × 𝑌)⟶(∪
(∏t‘{〈∅, 𝐽〉}) × ∪ (∏t‘{〈1𝑜,
𝐾〉}))) |
54 | 4, 26, 52, 53 | syl3anc 1318 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈{〈∅, 𝑥〉},
{〈1𝑜, 𝑦〉}〉):(𝑋 × 𝑌)⟶(∪
(∏t‘{〈∅, 𝐽〉}) × ∪ (∏t‘{〈1𝑜,
𝐾〉}))) |
55 | | eqid 2610 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈{〈∅, 𝑥〉},
{〈1𝑜, 𝑦〉}〉) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈{〈∅, 𝑥〉},
{〈1𝑜, 𝑦〉}〉) |
56 | 55 | fmpt2 7126 |
. . . . . . . 8
⊢
(∀𝑥 ∈
𝑋 ∀𝑦 ∈ 𝑌 〈{〈∅, 𝑥〉}, {〈1𝑜, 𝑦〉}〉 ∈ (∪ (∏t‘{〈∅, 𝐽〉}) × ∪ (∏t‘{〈1𝑜,
𝐾〉})) ↔ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈{〈∅, 𝑥〉},
{〈1𝑜, 𝑦〉}〉):(𝑋 × 𝑌)⟶(∪
(∏t‘{〈∅, 𝐽〉}) × ∪ (∏t‘{〈1𝑜,
𝐾〉}))) |
57 | 54, 56 | sylibr 223 |
. . . . . . 7
⊢ (𝜑 → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 〈{〈∅, 𝑥〉}, {〈1𝑜, 𝑦〉}〉 ∈ (∪ (∏t‘{〈∅, 𝐽〉}) × ∪ (∏t‘{〈1𝑜,
𝐾〉}))) |
58 | 57 | r19.21bi 2916 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ∀𝑦 ∈ 𝑌 〈{〈∅, 𝑥〉}, {〈1𝑜, 𝑦〉}〉 ∈ (∪ (∏t‘{〈∅, 𝐽〉}) × ∪ (∏t‘{〈1𝑜,
𝐾〉}))) |
59 | 58 | r19.21bi 2916 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑌) → 〈{〈∅, 𝑥〉},
{〈1𝑜, 𝑦〉}〉 ∈ (∪ (∏t‘{〈∅, 𝐽〉}) × ∪ (∏t‘{〈1𝑜,
𝐾〉}))) |
60 | 59 | anasss 677 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → 〈{〈∅, 𝑥〉},
{〈1𝑜, 𝑦〉}〉 ∈ (∪ (∏t‘{〈∅, 𝐽〉}) × ∪ (∏t‘{〈1𝑜,
𝐾〉}))) |
61 | | eqidd 2611 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈{〈∅, 𝑥〉},
{〈1𝑜, 𝑦〉}〉) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈{〈∅, 𝑥〉},
{〈1𝑜, 𝑦〉}〉)) |
62 | | vex 3176 |
. . . . . . . . 9
⊢ 𝑥 ∈ V |
63 | | vex 3176 |
. . . . . . . . 9
⊢ 𝑦 ∈ V |
64 | 62, 63 | op1std 7069 |
. . . . . . . 8
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (1st ‘𝑧) = 𝑥) |
65 | 62, 63 | op2ndd 7070 |
. . . . . . . 8
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (2nd ‘𝑧) = 𝑦) |
66 | 64, 65 | uneq12d 3730 |
. . . . . . 7
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ((1st ‘𝑧) ∪ (2nd
‘𝑧)) = (𝑥 ∪ 𝑦)) |
67 | 66 | mpt2mpt 6650 |
. . . . . 6
⊢ (𝑧 ∈ (∪ (∏t‘{〈∅, 𝐽〉}) × ∪ (∏t‘{〈1𝑜,
𝐾〉})) ↦
((1st ‘𝑧)
∪ (2nd ‘𝑧))) = (𝑥 ∈ ∪
(∏t‘{〈∅, 𝐽〉}), 𝑦 ∈ ∪
(∏t‘{〈1𝑜, 𝐾〉}) ↦ (𝑥 ∪ 𝑦)) |
68 | 67 | eqcomi 2619 |
. . . . 5
⊢ (𝑥 ∈ ∪ (∏t‘{〈∅, 𝐽〉}), 𝑦 ∈ ∪
(∏t‘{〈1𝑜, 𝐾〉}) ↦ (𝑥 ∪ 𝑦)) = (𝑧 ∈ (∪
(∏t‘{〈∅, 𝐽〉}) × ∪ (∏t‘{〈1𝑜,
𝐾〉})) ↦
((1st ‘𝑧)
∪ (2nd ‘𝑧))) |
69 | 68 | a1i 11 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ ∪
(∏t‘{〈∅, 𝐽〉}), 𝑦 ∈ ∪
(∏t‘{〈1𝑜, 𝐾〉}) ↦ (𝑥 ∪ 𝑦)) = (𝑧 ∈ (∪
(∏t‘{〈∅, 𝐽〉}) × ∪ (∏t‘{〈1𝑜,
𝐾〉})) ↦
((1st ‘𝑧)
∪ (2nd ‘𝑧)))) |
70 | 30, 35 | op1std 7069 |
. . . . . 6
⊢ (𝑧 = 〈{〈∅, 𝑥〉},
{〈1𝑜, 𝑦〉}〉 → (1st
‘𝑧) = {〈∅,
𝑥〉}) |
71 | 30, 35 | op2ndd 7070 |
. . . . . 6
⊢ (𝑧 = 〈{〈∅, 𝑥〉},
{〈1𝑜, 𝑦〉}〉 → (2nd
‘𝑧) =
{〈1𝑜, 𝑦〉}) |
72 | 70, 71 | uneq12d 3730 |
. . . . 5
⊢ (𝑧 = 〈{〈∅, 𝑥〉},
{〈1𝑜, 𝑦〉}〉 → ((1st
‘𝑧) ∪
(2nd ‘𝑧))
= ({〈∅, 𝑥〉}
∪ {〈1𝑜, 𝑦〉})) |
73 | | xpscg 16041 |
. . . . . . 7
⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V) → ◡({𝑥} +𝑐 {𝑦}) = {〈∅, 𝑥〉, 〈1𝑜, 𝑦〉}) |
74 | 62, 63, 73 | mp2an 704 |
. . . . . 6
⊢ ◡({𝑥} +𝑐 {𝑦}) = {〈∅, 𝑥〉, 〈1𝑜, 𝑦〉} |
75 | | df-pr 4128 |
. . . . . 6
⊢
{〈∅, 𝑥〉, 〈1𝑜, 𝑦〉} = ({〈∅, 𝑥〉} ∪
{〈1𝑜, 𝑦〉}) |
76 | 74, 75 | eqtri 2632 |
. . . . 5
⊢ ◡({𝑥} +𝑐 {𝑦}) = ({〈∅, 𝑥〉} ∪ {〈1𝑜,
𝑦〉}) |
77 | 72, 76 | syl6eqr 2662 |
. . . 4
⊢ (𝑧 = 〈{〈∅, 𝑥〉},
{〈1𝑜, 𝑦〉}〉 → ((1st
‘𝑧) ∪
(2nd ‘𝑧))
= ◡({𝑥} +𝑐 {𝑦})) |
78 | 60, 61, 69, 77 | fmpt2co 7147 |
. . 3
⊢ (𝜑 → ((𝑥 ∈ ∪
(∏t‘{〈∅, 𝐽〉}), 𝑦 ∈ ∪
(∏t‘{〈1𝑜, 𝐾〉}) ↦ (𝑥 ∪ 𝑦)) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈{〈∅, 𝑥〉},
{〈1𝑜, 𝑦〉}〉)) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))) |
79 | | xpstopnlem1.f |
. . 3
⊢ 𝐹 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) |
80 | 78, 79 | syl6reqr 2663 |
. 2
⊢ (𝜑 → 𝐹 = ((𝑥 ∈ ∪
(∏t‘{〈∅, 𝐽〉}), 𝑦 ∈ ∪
(∏t‘{〈1𝑜, 𝐾〉}) ↦ (𝑥 ∪ 𝑦)) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈{〈∅, 𝑥〉},
{〈1𝑜, 𝑦〉}〉))) |
81 | | eqid 2610 |
. . . . 5
⊢ ∪ (∏t‘(◡({𝐽} +𝑐 {𝐾}) ↾ {∅})) = ∪ (∏t‘(◡({𝐽} +𝑐 {𝐾}) ↾ {∅})) |
82 | | eqid 2610 |
. . . . 5
⊢ ∪ (∏t‘(◡({𝐽} +𝑐 {𝐾}) ↾ {1𝑜})) = ∪ (∏t‘(◡({𝐽} +𝑐 {𝐾}) ↾
{1𝑜})) |
83 | | eqid 2610 |
. . . . 5
⊢
(∏t‘◡({𝐽} +𝑐 {𝐾})) = (∏t‘◡({𝐽} +𝑐 {𝐾})) |
84 | | eqid 2610 |
. . . . 5
⊢
(∏t‘(◡({𝐽} +𝑐 {𝐾}) ↾ {∅})) =
(∏t‘(◡({𝐽} +𝑐 {𝐾}) ↾
{∅})) |
85 | | eqid 2610 |
. . . . 5
⊢
(∏t‘(◡({𝐽} +𝑐 {𝐾}) ↾ {1𝑜})) =
(∏t‘(◡({𝐽} +𝑐 {𝐾}) ↾
{1𝑜})) |
86 | | eqid 2610 |
. . . . 5
⊢ (𝑥 ∈ ∪ (∏t‘(◡({𝐽} +𝑐 {𝐾}) ↾ {∅})), 𝑦 ∈ ∪
(∏t‘(◡({𝐽} +𝑐 {𝐾}) ↾
{1𝑜})) ↦ (𝑥 ∪ 𝑦)) = (𝑥 ∈ ∪
(∏t‘(◡({𝐽} +𝑐 {𝐾}) ↾ {∅})), 𝑦 ∈ ∪ (∏t‘(◡({𝐽} +𝑐 {𝐾}) ↾ {1𝑜})) ↦
(𝑥 ∪ 𝑦)) |
87 | | 2on 7455 |
. . . . . 6
⊢
2𝑜 ∈ On |
88 | 87 | a1i 11 |
. . . . 5
⊢ (𝜑 → 2𝑜
∈ On) |
89 | | topontop 20541 |
. . . . . . 7
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top) |
90 | 1, 89 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐽 ∈ Top) |
91 | | topontop 20541 |
. . . . . . 7
⊢ (𝐾 ∈ (TopOn‘𝑌) → 𝐾 ∈ Top) |
92 | 2, 91 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐾 ∈ Top) |
93 | | xpscf 16049 |
. . . . . 6
⊢ (◡({𝐽} +𝑐 {𝐾}):2𝑜⟶Top ↔
(𝐽 ∈ Top ∧ 𝐾 ∈ Top)) |
94 | 90, 92, 93 | sylanbrc 695 |
. . . . 5
⊢ (𝜑 → ◡({𝐽} +𝑐 {𝐾}):2𝑜⟶Top) |
95 | | df2o3 7460 |
. . . . . . 7
⊢
2𝑜 = {∅,
1𝑜} |
96 | | df-pr 4128 |
. . . . . . 7
⊢ {∅,
1𝑜} = ({∅} ∪
{1𝑜}) |
97 | 95, 96 | eqtri 2632 |
. . . . . 6
⊢
2𝑜 = ({∅} ∪
{1𝑜}) |
98 | 97 | a1i 11 |
. . . . 5
⊢ (𝜑 → 2𝑜 =
({∅} ∪ {1𝑜})) |
99 | | 1n0 7462 |
. . . . . . 7
⊢
1𝑜 ≠ ∅ |
100 | 99 | necomi 2836 |
. . . . . 6
⊢ ∅
≠ 1𝑜 |
101 | | disjsn2 4193 |
. . . . . 6
⊢ (∅
≠ 1𝑜 → ({∅} ∩ {1𝑜}) =
∅) |
102 | 100, 101 | mp1i 13 |
. . . . 5
⊢ (𝜑 → ({∅} ∩
{1𝑜}) = ∅) |
103 | 81, 82, 83, 84, 85, 86, 88, 94, 98, 102 | ptunhmeo 21421 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ ∪
(∏t‘(◡({𝐽} +𝑐 {𝐾}) ↾ {∅})), 𝑦 ∈ ∪ (∏t‘(◡({𝐽} +𝑐 {𝐾}) ↾ {1𝑜})) ↦
(𝑥 ∪ 𝑦)) ∈ (((∏t‘(◡({𝐽} +𝑐 {𝐾}) ↾ {∅})) ×t
(∏t‘(◡({𝐽} +𝑐 {𝐾}) ↾
{1𝑜})))Homeo(∏t‘◡({𝐽} +𝑐 {𝐾})))) |
104 | | xpscfn 16042 |
. . . . . . . . . 10
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → ◡({𝐽} +𝑐 {𝐾}) Fn
2𝑜) |
105 | 1, 2, 104 | syl2anc 691 |
. . . . . . . . 9
⊢ (𝜑 → ◡({𝐽} +𝑐 {𝐾}) Fn
2𝑜) |
106 | 6 | prid1 4241 |
. . . . . . . . . 10
⊢ ∅
∈ {∅, 1𝑜} |
107 | 106, 95 | eleqtrri 2687 |
. . . . . . . . 9
⊢ ∅
∈ 2𝑜 |
108 | | fnressn 6330 |
. . . . . . . . 9
⊢ ((◡({𝐽} +𝑐 {𝐾}) Fn 2𝑜 ∧ ∅
∈ 2𝑜) → (◡({𝐽} +𝑐 {𝐾}) ↾ {∅}) = {〈∅,
(◡({𝐽} +𝑐 {𝐾})‘∅)〉}) |
109 | 105, 107,
108 | sylancl 693 |
. . . . . . . 8
⊢ (𝜑 → (◡({𝐽} +𝑐 {𝐾}) ↾ {∅}) = {〈∅,
(◡({𝐽} +𝑐 {𝐾})‘∅)〉}) |
110 | | xpsc0 16043 |
. . . . . . . . . . 11
⊢ (𝐽 ∈ (TopOn‘𝑋) → (◡({𝐽} +𝑐 {𝐾})‘∅) = 𝐽) |
111 | 1, 110 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (◡({𝐽} +𝑐 {𝐾})‘∅) = 𝐽) |
112 | 111 | opeq2d 4347 |
. . . . . . . . 9
⊢ (𝜑 → 〈∅, (◡({𝐽} +𝑐 {𝐾})‘∅)〉 = 〈∅,
𝐽〉) |
113 | 112 | sneqd 4137 |
. . . . . . . 8
⊢ (𝜑 → {〈∅, (◡({𝐽} +𝑐 {𝐾})‘∅)〉} = {〈∅,
𝐽〉}) |
114 | 109, 113 | eqtrd 2644 |
. . . . . . 7
⊢ (𝜑 → (◡({𝐽} +𝑐 {𝐾}) ↾ {∅}) = {〈∅,
𝐽〉}) |
115 | 114 | fveq2d 6107 |
. . . . . 6
⊢ (𝜑 →
(∏t‘(◡({𝐽} +𝑐 {𝐾}) ↾ {∅})) =
(∏t‘{〈∅, 𝐽〉})) |
116 | 115 | unieqd 4382 |
. . . . 5
⊢ (𝜑 → ∪ (∏t‘(◡({𝐽} +𝑐 {𝐾}) ↾ {∅})) = ∪ (∏t‘{〈∅, 𝐽〉})) |
117 | 16 | elexi 3186 |
. . . . . . . . . . 11
⊢
1𝑜 ∈ V |
118 | 117 | prid2 4242 |
. . . . . . . . . 10
⊢
1𝑜 ∈ {∅,
1𝑜} |
119 | 118, 95 | eleqtrri 2687 |
. . . . . . . . 9
⊢
1𝑜 ∈ 2𝑜 |
120 | | fnressn 6330 |
. . . . . . . . 9
⊢ ((◡({𝐽} +𝑐 {𝐾}) Fn 2𝑜 ∧
1𝑜 ∈ 2𝑜) → (◡({𝐽} +𝑐 {𝐾}) ↾ {1𝑜}) =
{〈1𝑜, (◡({𝐽} +𝑐 {𝐾})‘1𝑜)〉}) |
121 | 105, 119,
120 | sylancl 693 |
. . . . . . . 8
⊢ (𝜑 → (◡({𝐽} +𝑐 {𝐾}) ↾ {1𝑜}) =
{〈1𝑜, (◡({𝐽} +𝑐 {𝐾})‘1𝑜)〉}) |
122 | | xpsc1 16044 |
. . . . . . . . . . 11
⊢ (𝐾 ∈ (TopOn‘𝑌) → (◡({𝐽} +𝑐 {𝐾})‘1𝑜) = 𝐾) |
123 | 2, 122 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (◡({𝐽} +𝑐 {𝐾})‘1𝑜) = 𝐾) |
124 | 123 | opeq2d 4347 |
. . . . . . . . 9
⊢ (𝜑 →
〈1𝑜, (◡({𝐽} +𝑐 {𝐾})‘1𝑜)〉 =
〈1𝑜, 𝐾〉) |
125 | 124 | sneqd 4137 |
. . . . . . . 8
⊢ (𝜑 →
{〈1𝑜, (◡({𝐽} +𝑐 {𝐾})‘1𝑜)〉} =
{〈1𝑜, 𝐾〉}) |
126 | 121, 125 | eqtrd 2644 |
. . . . . . 7
⊢ (𝜑 → (◡({𝐽} +𝑐 {𝐾}) ↾ {1𝑜}) =
{〈1𝑜, 𝐾〉}) |
127 | 126 | fveq2d 6107 |
. . . . . 6
⊢ (𝜑 →
(∏t‘(◡({𝐽} +𝑐 {𝐾}) ↾
{1𝑜})) =
(∏t‘{〈1𝑜, 𝐾〉})) |
128 | 127 | unieqd 4382 |
. . . . 5
⊢ (𝜑 → ∪ (∏t‘(◡({𝐽} +𝑐 {𝐾}) ↾ {1𝑜})) = ∪ (∏t‘{〈1𝑜,
𝐾〉})) |
129 | | eqidd 2611 |
. . . . 5
⊢ (𝜑 → (𝑥 ∪ 𝑦) = (𝑥 ∪ 𝑦)) |
130 | 116, 128,
129 | mpt2eq123dv 6615 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ ∪
(∏t‘(◡({𝐽} +𝑐 {𝐾}) ↾ {∅})), 𝑦 ∈ ∪ (∏t‘(◡({𝐽} +𝑐 {𝐾}) ↾ {1𝑜})) ↦
(𝑥 ∪ 𝑦)) = (𝑥 ∈ ∪
(∏t‘{〈∅, 𝐽〉}), 𝑦 ∈ ∪
(∏t‘{〈1𝑜, 𝐾〉}) ↦ (𝑥 ∪ 𝑦))) |
131 | 115, 127 | oveq12d 6567 |
. . . . 5
⊢ (𝜑 →
((∏t‘(◡({𝐽} +𝑐 {𝐾}) ↾ {∅}))
×t (∏t‘(◡({𝐽} +𝑐 {𝐾}) ↾ {1𝑜}))) =
((∏t‘{〈∅, 𝐽〉}) ×t
(∏t‘{〈1𝑜, 𝐾〉}))) |
132 | 131 | oveq1d 6564 |
. . . 4
⊢ (𝜑 →
(((∏t‘(◡({𝐽} +𝑐 {𝐾}) ↾ {∅}))
×t (∏t‘(◡({𝐽} +𝑐 {𝐾}) ↾
{1𝑜})))Homeo(∏t‘◡({𝐽} +𝑐 {𝐾}))) =
(((∏t‘{〈∅, 𝐽〉}) ×t
(∏t‘{〈1𝑜, 𝐾〉}))Homeo(∏t‘◡({𝐽} +𝑐 {𝐾})))) |
133 | 103, 130,
132 | 3eltr3d 2702 |
. . 3
⊢ (𝜑 → (𝑥 ∈ ∪
(∏t‘{〈∅, 𝐽〉}), 𝑦 ∈ ∪
(∏t‘{〈1𝑜, 𝐾〉}) ↦ (𝑥 ∪ 𝑦)) ∈
(((∏t‘{〈∅, 𝐽〉}) ×t
(∏t‘{〈1𝑜, 𝐾〉}))Homeo(∏t‘◡({𝐽} +𝑐 {𝐾})))) |
134 | | hmeoco 21385 |
. . 3
⊢ (((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈{〈∅, 𝑥〉},
{〈1𝑜, 𝑦〉}〉) ∈ ((𝐽 ×t 𝐾)Homeo((∏t‘{〈∅,
𝐽〉}) ×t
(∏t‘{〈1𝑜, 𝐾〉}))) ∧ (𝑥 ∈ ∪
(∏t‘{〈∅, 𝐽〉}), 𝑦 ∈ ∪
(∏t‘{〈1𝑜, 𝐾〉}) ↦ (𝑥 ∪ 𝑦)) ∈
(((∏t‘{〈∅, 𝐽〉}) ×t
(∏t‘{〈1𝑜, 𝐾〉}))Homeo(∏t‘◡({𝐽} +𝑐 {𝐾})))) → ((𝑥 ∈ ∪
(∏t‘{〈∅, 𝐽〉}), 𝑦 ∈ ∪
(∏t‘{〈1𝑜, 𝐾〉}) ↦ (𝑥 ∪ 𝑦)) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈{〈∅, 𝑥〉},
{〈1𝑜, 𝑦〉}〉)) ∈ ((𝐽 ×t 𝐾)Homeo(∏t‘◡({𝐽} +𝑐 {𝐾})))) |
135 | 50, 133, 134 | syl2anc 691 |
. 2
⊢ (𝜑 → ((𝑥 ∈ ∪
(∏t‘{〈∅, 𝐽〉}), 𝑦 ∈ ∪
(∏t‘{〈1𝑜, 𝐾〉}) ↦ (𝑥 ∪ 𝑦)) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈{〈∅, 𝑥〉},
{〈1𝑜, 𝑦〉}〉)) ∈ ((𝐽 ×t 𝐾)Homeo(∏t‘◡({𝐽} +𝑐 {𝐾})))) |
136 | 80, 135 | eqeltrd 2688 |
1
⊢ (𝜑 → 𝐹 ∈ ((𝐽 ×t 𝐾)Homeo(∏t‘◡({𝐽} +𝑐 {𝐾})))) |