| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | xpstopnlem1.f | . . 3
⊢ 𝐹 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}) | 
| 2 |  | xpstopnlem1.j | . . . . . . . . . 10
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) | 
| 3 |  | xpstopnlem1.k | . . . . . . . . . 10
⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) | 
| 4 |  | txtopon 23600 | . . . . . . . . . 10
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌))) | 
| 5 | 2, 3, 4 | syl2anc 584 | . . . . . . . . 9
⊢ (𝜑 → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌))) | 
| 6 |  | eqid 2736 | . . . . . . . . . . . . 13
⊢
(∏t‘{〈∅, 𝐽〉}) =
(∏t‘{〈∅, 𝐽〉}) | 
| 7 |  | 0ex 5306 | . . . . . . . . . . . . . 14
⊢ ∅
∈ V | 
| 8 | 7 | a1i 11 | . . . . . . . . . . . . 13
⊢ (𝜑 → ∅ ∈
V) | 
| 9 | 6, 8, 2 | pt1hmeo 23815 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑧 ∈ 𝑋 ↦ {〈∅, 𝑧〉}) ∈ (𝐽Homeo(∏t‘{〈∅,
𝐽〉}))) | 
| 10 |  | hmeocn 23769 | . . . . . . . . . . . 12
⊢ ((𝑧 ∈ 𝑋 ↦ {〈∅, 𝑧〉}) ∈ (𝐽Homeo(∏t‘{〈∅,
𝐽〉})) → (𝑧 ∈ 𝑋 ↦ {〈∅, 𝑧〉}) ∈ (𝐽 Cn (∏t‘{〈∅,
𝐽〉}))) | 
| 11 |  | cntop2 23250 | . . . . . . . . . . . 12
⊢ ((𝑧 ∈ 𝑋 ↦ {〈∅, 𝑧〉}) ∈ (𝐽 Cn
(∏t‘{〈∅, 𝐽〉})) →
(∏t‘{〈∅, 𝐽〉}) ∈ Top) | 
| 12 | 9, 10, 11 | 3syl 18 | . . . . . . . . . . 11
⊢ (𝜑 →
(∏t‘{〈∅, 𝐽〉}) ∈ Top) | 
| 13 |  | toptopon2 22925 | . . . . . . . . . . 11
⊢
((∏t‘{〈∅, 𝐽〉}) ∈ Top ↔
(∏t‘{〈∅, 𝐽〉}) ∈ (TopOn‘∪ (∏t‘{〈∅, 𝐽〉}))) | 
| 14 | 12, 13 | sylib 218 | . . . . . . . . . 10
⊢ (𝜑 →
(∏t‘{〈∅, 𝐽〉}) ∈ (TopOn‘∪ (∏t‘{〈∅, 𝐽〉}))) | 
| 15 |  | eqid 2736 | . . . . . . . . . . . . 13
⊢
(∏t‘{〈1o, 𝐾〉}) =
(∏t‘{〈1o, 𝐾〉}) | 
| 16 |  | 1on 8519 | . . . . . . . . . . . . . 14
⊢
1o ∈ On | 
| 17 | 16 | a1i 11 | . . . . . . . . . . . . 13
⊢ (𝜑 → 1o ∈
On) | 
| 18 | 15, 17, 3 | pt1hmeo 23815 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑧 ∈ 𝑌 ↦ {〈1o, 𝑧〉}) ∈ (𝐾Homeo(∏t‘{〈1o,
𝐾〉}))) | 
| 19 |  | hmeocn 23769 | . . . . . . . . . . . 12
⊢ ((𝑧 ∈ 𝑌 ↦ {〈1o, 𝑧〉}) ∈ (𝐾Homeo(∏t‘{〈1o,
𝐾〉})) → (𝑧 ∈ 𝑌 ↦ {〈1o, 𝑧〉}) ∈ (𝐾 Cn (∏t‘{〈1o,
𝐾〉}))) | 
| 20 |  | cntop2 23250 | . . . . . . . . . . . 12
⊢ ((𝑧 ∈ 𝑌 ↦ {〈1o, 𝑧〉}) ∈ (𝐾 Cn
(∏t‘{〈1o, 𝐾〉})) →
(∏t‘{〈1o, 𝐾〉}) ∈ Top) | 
| 21 | 18, 19, 20 | 3syl 18 | . . . . . . . . . . 11
⊢ (𝜑 →
(∏t‘{〈1o, 𝐾〉}) ∈ Top) | 
| 22 |  | toptopon2 22925 | . . . . . . . . . . 11
⊢
((∏t‘{〈1o, 𝐾〉}) ∈ Top ↔
(∏t‘{〈1o, 𝐾〉}) ∈ (TopOn‘∪ (∏t‘{〈1o, 𝐾〉}))) | 
| 23 | 21, 22 | sylib 218 | . . . . . . . . . 10
⊢ (𝜑 →
(∏t‘{〈1o, 𝐾〉}) ∈ (TopOn‘∪ (∏t‘{〈1o, 𝐾〉}))) | 
| 24 |  | txtopon 23600 | . . . . . . . . . 10
⊢
(((∏t‘{〈∅, 𝐽〉}) ∈ (TopOn‘∪ (∏t‘{〈∅, 𝐽〉})) ∧
(∏t‘{〈1o, 𝐾〉}) ∈ (TopOn‘∪ (∏t‘{〈1o, 𝐾〉}))) →
((∏t‘{〈∅, 𝐽〉}) ×t
(∏t‘{〈1o, 𝐾〉})) ∈ (TopOn‘(∪ (∏t‘{〈∅, 𝐽〉}) × ∪ (∏t‘{〈1o, 𝐾〉})))) | 
| 25 | 14, 23, 24 | syl2anc 584 | . . . . . . . . 9
⊢ (𝜑 →
((∏t‘{〈∅, 𝐽〉}) ×t
(∏t‘{〈1o, 𝐾〉})) ∈ (TopOn‘(∪ (∏t‘{〈∅, 𝐽〉}) × ∪ (∏t‘{〈1o, 𝐾〉})))) | 
| 26 |  | opeq2 4873 | . . . . . . . . . . . . . . . 16
⊢ (𝑧 = 𝑥 → 〈∅, 𝑧〉 = 〈∅, 𝑥〉) | 
| 27 | 26 | sneqd 4637 | . . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑥 → {〈∅, 𝑧〉} = {〈∅, 𝑥〉}) | 
| 28 |  | eqid 2736 | . . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ 𝑋 ↦ {〈∅, 𝑧〉}) = (𝑧 ∈ 𝑋 ↦ {〈∅, 𝑧〉}) | 
| 29 |  | snex 5435 | . . . . . . . . . . . . . . 15
⊢
{〈∅, 𝑥〉} ∈ V | 
| 30 | 27, 28, 29 | fvmpt 7015 | . . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝑋 → ((𝑧 ∈ 𝑋 ↦ {〈∅, 𝑧〉})‘𝑥) = {〈∅, 𝑥〉}) | 
| 31 |  | opeq2 4873 | . . . . . . . . . . . . . . . 16
⊢ (𝑧 = 𝑦 → 〈1o, 𝑧〉 = 〈1o,
𝑦〉) | 
| 32 | 31 | sneqd 4637 | . . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑦 → {〈1o, 𝑧〉} = {〈1o,
𝑦〉}) | 
| 33 |  | eqid 2736 | . . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ 𝑌 ↦ {〈1o, 𝑧〉}) = (𝑧 ∈ 𝑌 ↦ {〈1o, 𝑧〉}) | 
| 34 |  | snex 5435 | . . . . . . . . . . . . . . 15
⊢
{〈1o, 𝑦〉} ∈ V | 
| 35 | 32, 33, 34 | fvmpt 7015 | . . . . . . . . . . . . . 14
⊢ (𝑦 ∈ 𝑌 → ((𝑧 ∈ 𝑌 ↦ {〈1o, 𝑧〉})‘𝑦) = {〈1o, 𝑦〉}) | 
| 36 |  | opeq12 4874 | . . . . . . . . . . . . . 14
⊢ ((((𝑧 ∈ 𝑋 ↦ {〈∅, 𝑧〉})‘𝑥) = {〈∅, 𝑥〉} ∧ ((𝑧 ∈ 𝑌 ↦ {〈1o, 𝑧〉})‘𝑦) = {〈1o, 𝑦〉}) → 〈((𝑧 ∈ 𝑋 ↦ {〈∅, 𝑧〉})‘𝑥), ((𝑧 ∈ 𝑌 ↦ {〈1o, 𝑧〉})‘𝑦)〉 = 〈{〈∅,
𝑥〉},
{〈1o, 𝑦〉}〉) | 
| 37 | 30, 35, 36 | syl2an 596 | . . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) → 〈((𝑧 ∈ 𝑋 ↦ {〈∅, 𝑧〉})‘𝑥), ((𝑧 ∈ 𝑌 ↦ {〈1o, 𝑧〉})‘𝑦)〉 = 〈{〈∅,
𝑥〉},
{〈1o, 𝑦〉}〉) | 
| 38 | 37 | mpoeq3ia 7512 | . . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈((𝑧 ∈ 𝑋 ↦ {〈∅, 𝑧〉})‘𝑥), ((𝑧 ∈ 𝑌 ↦ {〈1o, 𝑧〉})‘𝑦)〉) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈{〈∅, 𝑥〉}, {〈1o,
𝑦〉}〉) | 
| 39 |  | toponuni 22921 | . . . . . . . . . . . . . 14
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝐽) | 
| 40 | 2, 39 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝑋 = ∪ 𝐽) | 
| 41 |  | toponuni 22921 | . . . . . . . . . . . . . 14
⊢ (𝐾 ∈ (TopOn‘𝑌) → 𝑌 = ∪ 𝐾) | 
| 42 | 3, 41 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝑌 = ∪ 𝐾) | 
| 43 |  | mpoeq12 7507 | . . . . . . . . . . . . 13
⊢ ((𝑋 = ∪
𝐽 ∧ 𝑌 = ∪ 𝐾) → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈((𝑧 ∈ 𝑋 ↦ {〈∅, 𝑧〉})‘𝑥), ((𝑧 ∈ 𝑌 ↦ {〈1o, 𝑧〉})‘𝑦)〉) = (𝑥 ∈ ∪ 𝐽, 𝑦 ∈ ∪ 𝐾 ↦ 〈((𝑧 ∈ 𝑋 ↦ {〈∅, 𝑧〉})‘𝑥), ((𝑧 ∈ 𝑌 ↦ {〈1o, 𝑧〉})‘𝑦)〉)) | 
| 44 | 40, 42, 43 | syl2anc 584 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈((𝑧 ∈ 𝑋 ↦ {〈∅, 𝑧〉})‘𝑥), ((𝑧 ∈ 𝑌 ↦ {〈1o, 𝑧〉})‘𝑦)〉) = (𝑥 ∈ ∪ 𝐽, 𝑦 ∈ ∪ 𝐾 ↦ 〈((𝑧 ∈ 𝑋 ↦ {〈∅, 𝑧〉})‘𝑥), ((𝑧 ∈ 𝑌 ↦ {〈1o, 𝑧〉})‘𝑦)〉)) | 
| 45 | 38, 44 | eqtr3id 2790 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈{〈∅, 𝑥〉}, {〈1o,
𝑦〉}〉) = (𝑥 ∈ ∪ 𝐽,
𝑦 ∈ ∪ 𝐾
↦ 〈((𝑧 ∈
𝑋 ↦ {〈∅,
𝑧〉})‘𝑥), ((𝑧 ∈ 𝑌 ↦ {〈1o, 𝑧〉})‘𝑦)〉)) | 
| 46 |  | eqid 2736 | . . . . . . . . . . . 12
⊢ ∪ 𝐽 =
∪ 𝐽 | 
| 47 |  | eqid 2736 | . . . . . . . . . . . 12
⊢ ∪ 𝐾 =
∪ 𝐾 | 
| 48 | 46, 47, 9, 18 | txhmeo 23812 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ ∪ 𝐽, 𝑦 ∈ ∪ 𝐾 ↦ 〈((𝑧 ∈ 𝑋 ↦ {〈∅, 𝑧〉})‘𝑥), ((𝑧 ∈ 𝑌 ↦ {〈1o, 𝑧〉})‘𝑦)〉) ∈ ((𝐽 ×t 𝐾)Homeo((∏t‘{〈∅,
𝐽〉}) ×t
(∏t‘{〈1o, 𝐾〉})))) | 
| 49 | 45, 48 | eqeltrd 2840 | . . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈{〈∅, 𝑥〉}, {〈1o,
𝑦〉}〉) ∈
((𝐽 ×t
𝐾)Homeo((∏t‘{〈∅,
𝐽〉}) ×t
(∏t‘{〈1o, 𝐾〉})))) | 
| 50 |  | hmeocn 23769 | . . . . . . . . . 10
⊢ ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈{〈∅, 𝑥〉}, {〈1o,
𝑦〉}〉) ∈
((𝐽 ×t
𝐾)Homeo((∏t‘{〈∅,
𝐽〉}) ×t
(∏t‘{〈1o, 𝐾〉}))) → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈{〈∅, 𝑥〉}, {〈1o, 𝑦〉}〉) ∈ ((𝐽 ×t 𝐾) Cn
((∏t‘{〈∅, 𝐽〉}) ×t
(∏t‘{〈1o, 𝐾〉})))) | 
| 51 | 49, 50 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈{〈∅, 𝑥〉}, {〈1o,
𝑦〉}〉) ∈
((𝐽 ×t
𝐾) Cn
((∏t‘{〈∅, 𝐽〉}) ×t
(∏t‘{〈1o, 𝐾〉})))) | 
| 52 |  | cnf2 23258 | . . . . . . . . 9
⊢ (((𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)) ∧
((∏t‘{〈∅, 𝐽〉}) ×t
(∏t‘{〈1o, 𝐾〉})) ∈ (TopOn‘(∪ (∏t‘{〈∅, 𝐽〉}) × ∪ (∏t‘{〈1o, 𝐾〉}))) ∧ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈{〈∅, 𝑥〉}, {〈1o,
𝑦〉}〉) ∈
((𝐽 ×t
𝐾) Cn
((∏t‘{〈∅, 𝐽〉}) ×t
(∏t‘{〈1o, 𝐾〉})))) → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈{〈∅, 𝑥〉}, {〈1o,
𝑦〉}〉):(𝑋 × 𝑌)⟶(∪
(∏t‘{〈∅, 𝐽〉}) × ∪ (∏t‘{〈1o, 𝐾〉}))) | 
| 53 | 5, 25, 51, 52 | syl3anc 1372 | . . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈{〈∅, 𝑥〉}, {〈1o,
𝑦〉}〉):(𝑋 × 𝑌)⟶(∪
(∏t‘{〈∅, 𝐽〉}) × ∪ (∏t‘{〈1o, 𝐾〉}))) | 
| 54 |  | eqid 2736 | . . . . . . . . 9
⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈{〈∅, 𝑥〉}, {〈1o,
𝑦〉}〉) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈{〈∅, 𝑥〉}, {〈1o,
𝑦〉}〉) | 
| 55 | 54 | fmpo 8094 | . . . . . . . 8
⊢
(∀𝑥 ∈
𝑋 ∀𝑦 ∈ 𝑌 〈{〈∅, 𝑥〉}, {〈1o, 𝑦〉}〉 ∈ (∪ (∏t‘{〈∅, 𝐽〉}) × ∪ (∏t‘{〈1o, 𝐾〉})) ↔ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈{〈∅, 𝑥〉}, {〈1o,
𝑦〉}〉):(𝑋 × 𝑌)⟶(∪
(∏t‘{〈∅, 𝐽〉}) × ∪ (∏t‘{〈1o, 𝐾〉}))) | 
| 56 | 53, 55 | sylibr 234 | . . . . . . 7
⊢ (𝜑 → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 〈{〈∅, 𝑥〉}, {〈1o, 𝑦〉}〉 ∈ (∪ (∏t‘{〈∅, 𝐽〉}) × ∪ (∏t‘{〈1o, 𝐾〉}))) | 
| 57 | 56 | r19.21bi 3250 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ∀𝑦 ∈ 𝑌 〈{〈∅, 𝑥〉}, {〈1o, 𝑦〉}〉 ∈ (∪ (∏t‘{〈∅, 𝐽〉}) × ∪ (∏t‘{〈1o, 𝐾〉}))) | 
| 58 | 57 | r19.21bi 3250 | . . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑌) → 〈{〈∅, 𝑥〉}, {〈1o,
𝑦〉}〉 ∈
(∪ (∏t‘{〈∅, 𝐽〉}) × ∪ (∏t‘{〈1o, 𝐾〉}))) | 
| 59 | 58 | anasss 466 | . . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → 〈{〈∅, 𝑥〉}, {〈1o,
𝑦〉}〉 ∈
(∪ (∏t‘{〈∅, 𝐽〉}) × ∪ (∏t‘{〈1o, 𝐾〉}))) | 
| 60 |  | eqidd 2737 | . . . 4
⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈{〈∅, 𝑥〉}, {〈1o,
𝑦〉}〉) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈{〈∅, 𝑥〉}, {〈1o,
𝑦〉}〉)) | 
| 61 |  | vex 3483 | . . . . . . . . 9
⊢ 𝑥 ∈ V | 
| 62 |  | vex 3483 | . . . . . . . . 9
⊢ 𝑦 ∈ V | 
| 63 | 61, 62 | op1std 8025 | . . . . . . . 8
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (1st ‘𝑧) = 𝑥) | 
| 64 | 61, 62 | op2ndd 8026 | . . . . . . . 8
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (2nd ‘𝑧) = 𝑦) | 
| 65 | 63, 64 | uneq12d 4168 | . . . . . . 7
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ((1st ‘𝑧) ∪ (2nd
‘𝑧)) = (𝑥 ∪ 𝑦)) | 
| 66 | 65 | mpompt 7548 | . . . . . 6
⊢ (𝑧 ∈ (∪ (∏t‘{〈∅, 𝐽〉}) × ∪ (∏t‘{〈1o, 𝐾〉})) ↦
((1st ‘𝑧)
∪ (2nd ‘𝑧))) = (𝑥 ∈ ∪
(∏t‘{〈∅, 𝐽〉}), 𝑦 ∈ ∪
(∏t‘{〈1o, 𝐾〉}) ↦ (𝑥 ∪ 𝑦)) | 
| 67 | 66 | eqcomi 2745 | . . . . 5
⊢ (𝑥 ∈ ∪ (∏t‘{〈∅, 𝐽〉}), 𝑦 ∈ ∪
(∏t‘{〈1o, 𝐾〉}) ↦ (𝑥 ∪ 𝑦)) = (𝑧 ∈ (∪
(∏t‘{〈∅, 𝐽〉}) × ∪ (∏t‘{〈1o, 𝐾〉})) ↦
((1st ‘𝑧)
∪ (2nd ‘𝑧))) | 
| 68 | 67 | a1i 11 | . . . 4
⊢ (𝜑 → (𝑥 ∈ ∪
(∏t‘{〈∅, 𝐽〉}), 𝑦 ∈ ∪
(∏t‘{〈1o, 𝐾〉}) ↦ (𝑥 ∪ 𝑦)) = (𝑧 ∈ (∪
(∏t‘{〈∅, 𝐽〉}) × ∪ (∏t‘{〈1o, 𝐾〉})) ↦
((1st ‘𝑧)
∪ (2nd ‘𝑧)))) | 
| 69 | 29, 34 | op1std 8025 | . . . . . 6
⊢ (𝑧 = 〈{〈∅, 𝑥〉}, {〈1o,
𝑦〉}〉 →
(1st ‘𝑧) =
{〈∅, 𝑥〉}) | 
| 70 | 29, 34 | op2ndd 8026 | . . . . . 6
⊢ (𝑧 = 〈{〈∅, 𝑥〉}, {〈1o,
𝑦〉}〉 →
(2nd ‘𝑧) =
{〈1o, 𝑦〉}) | 
| 71 | 69, 70 | uneq12d 4168 | . . . . 5
⊢ (𝑧 = 〈{〈∅, 𝑥〉}, {〈1o,
𝑦〉}〉 →
((1st ‘𝑧)
∪ (2nd ‘𝑧)) = ({〈∅, 𝑥〉} ∪ {〈1o, 𝑦〉})) | 
| 72 |  | df-pr 4628 | . . . . 5
⊢
{〈∅, 𝑥〉, 〈1o, 𝑦〉} = ({〈∅, 𝑥〉} ∪
{〈1o, 𝑦〉}) | 
| 73 | 71, 72 | eqtr4di 2794 | . . . 4
⊢ (𝑧 = 〈{〈∅, 𝑥〉}, {〈1o,
𝑦〉}〉 →
((1st ‘𝑧)
∪ (2nd ‘𝑧)) = {〈∅, 𝑥〉, 〈1o, 𝑦〉}) | 
| 74 | 59, 60, 68, 73 | fmpoco 8121 | . . 3
⊢ (𝜑 → ((𝑥 ∈ ∪
(∏t‘{〈∅, 𝐽〉}), 𝑦 ∈ ∪
(∏t‘{〈1o, 𝐾〉}) ↦ (𝑥 ∪ 𝑦)) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈{〈∅, 𝑥〉}, {〈1o,
𝑦〉}〉)) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉})) | 
| 75 | 1, 74 | eqtr4id 2795 | . 2
⊢ (𝜑 → 𝐹 = ((𝑥 ∈ ∪
(∏t‘{〈∅, 𝐽〉}), 𝑦 ∈ ∪
(∏t‘{〈1o, 𝐾〉}) ↦ (𝑥 ∪ 𝑦)) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈{〈∅, 𝑥〉}, {〈1o,
𝑦〉}〉))) | 
| 76 |  | eqid 2736 | . . . . 5
⊢ ∪ (∏t‘({〈∅, 𝐽〉, 〈1o,
𝐾〉} ↾
{∅})) = ∪
(∏t‘({〈∅, 𝐽〉, 〈1o, 𝐾〉} ↾
{∅})) | 
| 77 |  | eqid 2736 | . . . . 5
⊢ ∪ (∏t‘({〈∅, 𝐽〉, 〈1o,
𝐾〉} ↾
{1o})) = ∪
(∏t‘({〈∅, 𝐽〉, 〈1o, 𝐾〉} ↾
{1o})) | 
| 78 |  | eqid 2736 | . . . . 5
⊢
(∏t‘{〈∅, 𝐽〉, 〈1o, 𝐾〉}) =
(∏t‘{〈∅, 𝐽〉, 〈1o, 𝐾〉}) | 
| 79 |  | eqid 2736 | . . . . 5
⊢
(∏t‘({〈∅, 𝐽〉, 〈1o, 𝐾〉} ↾ {∅})) =
(∏t‘({〈∅, 𝐽〉, 〈1o, 𝐾〉} ↾
{∅})) | 
| 80 |  | eqid 2736 | . . . . 5
⊢
(∏t‘({〈∅, 𝐽〉, 〈1o, 𝐾〉} ↾
{1o})) = (∏t‘({〈∅, 𝐽〉, 〈1o,
𝐾〉} ↾
{1o})) | 
| 81 |  | eqid 2736 | . . . . 5
⊢ (𝑥 ∈ ∪ (∏t‘({〈∅, 𝐽〉, 〈1o,
𝐾〉} ↾
{∅})), 𝑦 ∈ ∪ (∏t‘({〈∅, 𝐽〉, 〈1o,
𝐾〉} ↾
{1o})) ↦ (𝑥 ∪ 𝑦)) = (𝑥 ∈ ∪
(∏t‘({〈∅, 𝐽〉, 〈1o, 𝐾〉} ↾ {∅})),
𝑦 ∈ ∪ (∏t‘({〈∅, 𝐽〉, 〈1o,
𝐾〉} ↾
{1o})) ↦ (𝑥 ∪ 𝑦)) | 
| 82 |  | 2on 8521 | . . . . . 6
⊢
2o ∈ On | 
| 83 | 82 | a1i 11 | . . . . 5
⊢ (𝜑 → 2o ∈
On) | 
| 84 |  | topontop 22920 | . . . . . . 7
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top) | 
| 85 | 2, 84 | syl 17 | . . . . . 6
⊢ (𝜑 → 𝐽 ∈ Top) | 
| 86 |  | topontop 22920 | . . . . . . 7
⊢ (𝐾 ∈ (TopOn‘𝑌) → 𝐾 ∈ Top) | 
| 87 | 3, 86 | syl 17 | . . . . . 6
⊢ (𝜑 → 𝐾 ∈ Top) | 
| 88 |  | xpscf 17611 | . . . . . 6
⊢
({〈∅, 𝐽〉, 〈1o, 𝐾〉}:2o⟶Top
↔ (𝐽 ∈ Top ∧
𝐾 ∈
Top)) | 
| 89 | 85, 87, 88 | sylanbrc 583 | . . . . 5
⊢ (𝜑 → {〈∅, 𝐽〉, 〈1o,
𝐾〉}:2o⟶Top) | 
| 90 |  | df2o3 8515 | . . . . . . 7
⊢
2o = {∅, 1o} | 
| 91 |  | df-pr 4628 | . . . . . . 7
⊢ {∅,
1o} = ({∅} ∪ {1o}) | 
| 92 | 90, 91 | eqtri 2764 | . . . . . 6
⊢
2o = ({∅} ∪ {1o}) | 
| 93 | 92 | a1i 11 | . . . . 5
⊢ (𝜑 → 2o = ({∅}
∪ {1o})) | 
| 94 |  | 1n0 8527 | . . . . . . 7
⊢
1o ≠ ∅ | 
| 95 | 94 | necomi 2994 | . . . . . 6
⊢ ∅
≠ 1o | 
| 96 |  | disjsn2 4711 | . . . . . 6
⊢ (∅
≠ 1o → ({∅} ∩ {1o}) =
∅) | 
| 97 | 95, 96 | mp1i 13 | . . . . 5
⊢ (𝜑 → ({∅} ∩
{1o}) = ∅) | 
| 98 | 76, 77, 78, 79, 80, 81, 83, 89, 93, 97 | ptunhmeo 23817 | . . . 4
⊢ (𝜑 → (𝑥 ∈ ∪
(∏t‘({〈∅, 𝐽〉, 〈1o, 𝐾〉} ↾ {∅})),
𝑦 ∈ ∪ (∏t‘({〈∅, 𝐽〉, 〈1o,
𝐾〉} ↾
{1o})) ↦ (𝑥 ∪ 𝑦)) ∈
(((∏t‘({〈∅, 𝐽〉, 〈1o, 𝐾〉} ↾ {∅}))
×t (∏t‘({〈∅, 𝐽〉, 〈1o,
𝐾〉} ↾
{1o})))Homeo(∏t‘{〈∅, 𝐽〉, 〈1o,
𝐾〉}))) | 
| 99 |  | fnpr2o 17603 | . . . . . . . . . 10
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → {〈∅, 𝐽〉, 〈1o, 𝐾〉} Fn
2o) | 
| 100 | 2, 3, 99 | syl2anc 584 | . . . . . . . . 9
⊢ (𝜑 → {〈∅, 𝐽〉, 〈1o,
𝐾〉} Fn
2o) | 
| 101 | 7 | prid1 4761 | . . . . . . . . . 10
⊢ ∅
∈ {∅, 1o} | 
| 102 | 101, 90 | eleqtrri 2839 | . . . . . . . . 9
⊢ ∅
∈ 2o | 
| 103 |  | fnressn 7177 | . . . . . . . . 9
⊢
(({〈∅, 𝐽〉, 〈1o, 𝐾〉} Fn 2o ∧
∅ ∈ 2o) → ({〈∅, 𝐽〉, 〈1o, 𝐾〉} ↾ {∅}) =
{〈∅, ({〈∅, 𝐽〉, 〈1o, 𝐾〉}‘∅)〉}) | 
| 104 | 100, 102,
103 | sylancl 586 | . . . . . . . 8
⊢ (𝜑 → ({〈∅, 𝐽〉, 〈1o,
𝐾〉} ↾ {∅})
= {〈∅, ({〈∅, 𝐽〉, 〈1o, 𝐾〉}‘∅)〉}) | 
| 105 |  | fvpr0o 17605 | . . . . . . . . . . 11
⊢ (𝐽 ∈ (TopOn‘𝑋) → ({〈∅, 𝐽〉, 〈1o,
𝐾〉}‘∅) =
𝐽) | 
| 106 | 2, 105 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → ({〈∅, 𝐽〉, 〈1o,
𝐾〉}‘∅) =
𝐽) | 
| 107 | 106 | opeq2d 4879 | . . . . . . . . 9
⊢ (𝜑 → 〈∅,
({〈∅, 𝐽〉,
〈1o, 𝐾〉}‘∅)〉 =
〈∅, 𝐽〉) | 
| 108 | 107 | sneqd 4637 | . . . . . . . 8
⊢ (𝜑 → {〈∅,
({〈∅, 𝐽〉,
〈1o, 𝐾〉}‘∅)〉} =
{〈∅, 𝐽〉}) | 
| 109 | 104, 108 | eqtrd 2776 | . . . . . . 7
⊢ (𝜑 → ({〈∅, 𝐽〉, 〈1o,
𝐾〉} ↾ {∅})
= {〈∅, 𝐽〉}) | 
| 110 | 109 | fveq2d 6909 | . . . . . 6
⊢ (𝜑 →
(∏t‘({〈∅, 𝐽〉, 〈1o, 𝐾〉} ↾ {∅})) =
(∏t‘{〈∅, 𝐽〉})) | 
| 111 | 110 | unieqd 4919 | . . . . 5
⊢ (𝜑 → ∪ (∏t‘({〈∅, 𝐽〉, 〈1o,
𝐾〉} ↾
{∅})) = ∪
(∏t‘{〈∅, 𝐽〉})) | 
| 112 |  | 1oex 8517 | . . . . . . . . . . 11
⊢
1o ∈ V | 
| 113 | 112 | prid2 4762 | . . . . . . . . . 10
⊢
1o ∈ {∅, 1o} | 
| 114 | 113, 90 | eleqtrri 2839 | . . . . . . . . 9
⊢
1o ∈ 2o | 
| 115 |  | fnressn 7177 | . . . . . . . . 9
⊢
(({〈∅, 𝐽〉, 〈1o, 𝐾〉} Fn 2o ∧
1o ∈ 2o) → ({〈∅, 𝐽〉, 〈1o, 𝐾〉} ↾ {1o})
= {〈1o, ({〈∅, 𝐽〉, 〈1o, 𝐾〉}‘1o)〉}) | 
| 116 | 100, 114,
115 | sylancl 586 | . . . . . . . 8
⊢ (𝜑 → ({〈∅, 𝐽〉, 〈1o,
𝐾〉} ↾
{1o}) = {〈1o, ({〈∅, 𝐽〉, 〈1o, 𝐾〉}‘1o)〉}) | 
| 117 |  | fvpr1o 17606 | . . . . . . . . . . 11
⊢ (𝐾 ∈ (TopOn‘𝑌) → ({〈∅, 𝐽〉, 〈1o,
𝐾〉}‘1o) = 𝐾) | 
| 118 | 3, 117 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → ({〈∅, 𝐽〉, 〈1o,
𝐾〉}‘1o) = 𝐾) | 
| 119 | 118 | opeq2d 4879 | . . . . . . . . 9
⊢ (𝜑 → 〈1o,
({〈∅, 𝐽〉,
〈1o, 𝐾〉}‘1o)〉 =
〈1o, 𝐾〉) | 
| 120 | 119 | sneqd 4637 | . . . . . . . 8
⊢ (𝜑 → {〈1o,
({〈∅, 𝐽〉,
〈1o, 𝐾〉}‘1o)〉} =
{〈1o, 𝐾〉}) | 
| 121 | 116, 120 | eqtrd 2776 | . . . . . . 7
⊢ (𝜑 → ({〈∅, 𝐽〉, 〈1o,
𝐾〉} ↾
{1o}) = {〈1o, 𝐾〉}) | 
| 122 | 121 | fveq2d 6909 | . . . . . 6
⊢ (𝜑 →
(∏t‘({〈∅, 𝐽〉, 〈1o, 𝐾〉} ↾
{1o})) = (∏t‘{〈1o, 𝐾〉})) | 
| 123 | 122 | unieqd 4919 | . . . . 5
⊢ (𝜑 → ∪ (∏t‘({〈∅, 𝐽〉, 〈1o,
𝐾〉} ↾
{1o})) = ∪
(∏t‘{〈1o, 𝐾〉})) | 
| 124 |  | eqidd 2737 | . . . . 5
⊢ (𝜑 → (𝑥 ∪ 𝑦) = (𝑥 ∪ 𝑦)) | 
| 125 | 111, 123,
124 | mpoeq123dv 7509 | . . . 4
⊢ (𝜑 → (𝑥 ∈ ∪
(∏t‘({〈∅, 𝐽〉, 〈1o, 𝐾〉} ↾ {∅})),
𝑦 ∈ ∪ (∏t‘({〈∅, 𝐽〉, 〈1o,
𝐾〉} ↾
{1o})) ↦ (𝑥 ∪ 𝑦)) = (𝑥 ∈ ∪
(∏t‘{〈∅, 𝐽〉}), 𝑦 ∈ ∪
(∏t‘{〈1o, 𝐾〉}) ↦ (𝑥 ∪ 𝑦))) | 
| 126 | 110, 122 | oveq12d 7450 | . . . . 5
⊢ (𝜑 →
((∏t‘({〈∅, 𝐽〉, 〈1o, 𝐾〉} ↾ {∅}))
×t (∏t‘({〈∅, 𝐽〉, 〈1o,
𝐾〉} ↾
{1o}))) = ((∏t‘{〈∅, 𝐽〉}) ×t
(∏t‘{〈1o, 𝐾〉}))) | 
| 127 | 126 | oveq1d 7447 | . . . 4
⊢ (𝜑 →
(((∏t‘({〈∅, 𝐽〉, 〈1o, 𝐾〉} ↾ {∅}))
×t (∏t‘({〈∅, 𝐽〉, 〈1o,
𝐾〉} ↾
{1o})))Homeo(∏t‘{〈∅, 𝐽〉, 〈1o,
𝐾〉})) =
(((∏t‘{〈∅, 𝐽〉}) ×t
(∏t‘{〈1o, 𝐾〉}))Homeo(∏t‘{〈∅,
𝐽〉, 〈1o, 𝐾〉}))) | 
| 128 | 98, 125, 127 | 3eltr3d 2854 | . . 3
⊢ (𝜑 → (𝑥 ∈ ∪
(∏t‘{〈∅, 𝐽〉}), 𝑦 ∈ ∪
(∏t‘{〈1o, 𝐾〉}) ↦ (𝑥 ∪ 𝑦)) ∈
(((∏t‘{〈∅, 𝐽〉}) ×t
(∏t‘{〈1o, 𝐾〉}))Homeo(∏t‘{〈∅,
𝐽〉, 〈1o, 𝐾〉}))) | 
| 129 |  | hmeoco 23781 | . . 3
⊢ (((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈{〈∅, 𝑥〉}, {〈1o,
𝑦〉}〉) ∈
((𝐽 ×t
𝐾)Homeo((∏t‘{〈∅,
𝐽〉}) ×t
(∏t‘{〈1o, 𝐾〉}))) ∧ (𝑥 ∈ ∪
(∏t‘{〈∅, 𝐽〉}), 𝑦 ∈ ∪
(∏t‘{〈1o, 𝐾〉}) ↦ (𝑥 ∪ 𝑦)) ∈
(((∏t‘{〈∅, 𝐽〉}) ×t
(∏t‘{〈1o, 𝐾〉}))Homeo(∏t‘{〈∅,
𝐽〉, 〈1o, 𝐾〉}))) → ((𝑥 ∈ ∪
(∏t‘{〈∅, 𝐽〉}), 𝑦 ∈ ∪
(∏t‘{〈1o, 𝐾〉}) ↦ (𝑥 ∪ 𝑦)) ∘ (𝑥 ∈ 𝑋, 𝑦
∈ 𝑌 ↦ 〈{〈∅,
𝑥〉}, {〈1o, 𝑦〉}〉)) ∈ ((𝐽 ×t 𝐾)Homeo(∏t‘{〈∅, 𝐽〉, 〈1o, 𝐾〉}))) | 
| 130 | 49, 128, 129 | syl2anc 584 | . 2
⊢ (𝜑 → ((𝑥 ∈ ∪
(∏t‘{〈∅, 𝐽〉}), 𝑦 ∈ ∪
(∏t‘{〈1o, 𝐾〉}) ↦ (𝑥 ∪ 𝑦)) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈{〈∅, 𝑥〉}, {〈1o,
𝑦〉}〉)) ∈
((𝐽 ×t
𝐾)Homeo(∏t‘{〈∅,
𝐽〉, 〈1o,
𝐾〉}))) | 
| 131 | 75, 130 | eqeltrd 2840 | 1
⊢ (𝜑 → 𝐹 ∈ ((𝐽 ×t 𝐾)Homeo(∏t‘{〈∅,
𝐽〉, 〈1o,
𝐾〉}))) |