Step | Hyp | Ref
| Expression |
1 | | xpstopnlem1.j |
. . . . . . . . . 10
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) |
2 | | xpstopnlem1.k |
. . . . . . . . . 10
⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) |
3 | | txtopon 21918 |
. . . . . . . . . 10
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌))) |
4 | 1, 2, 3 | syl2anc 576 |
. . . . . . . . 9
⊢ (𝜑 → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌))) |
5 | | eqid 2771 |
. . . . . . . . . . . . 13
⊢
(∏t‘{〈∅, 𝐽〉}) =
(∏t‘{〈∅, 𝐽〉}) |
6 | | 0ex 5064 |
. . . . . . . . . . . . . 14
⊢ ∅
∈ V |
7 | 6 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∅ ∈
V) |
8 | 5, 7, 1 | pt1hmeo 22133 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑧 ∈ 𝑋 ↦ {〈∅, 𝑧〉}) ∈ (𝐽Homeo(∏t‘{〈∅,
𝐽〉}))) |
9 | | hmeocn 22087 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ 𝑋 ↦ {〈∅, 𝑧〉}) ∈ (𝐽Homeo(∏t‘{〈∅,
𝐽〉})) → (𝑧 ∈ 𝑋 ↦ {〈∅, 𝑧〉}) ∈ (𝐽 Cn (∏t‘{〈∅,
𝐽〉}))) |
10 | | cntop2 21568 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ 𝑋 ↦ {〈∅, 𝑧〉}) ∈ (𝐽 Cn
(∏t‘{〈∅, 𝐽〉})) →
(∏t‘{〈∅, 𝐽〉}) ∈ Top) |
11 | 8, 9, 10 | 3syl 18 |
. . . . . . . . . . 11
⊢ (𝜑 →
(∏t‘{〈∅, 𝐽〉}) ∈ Top) |
12 | | toptopon2 21245 |
. . . . . . . . . . 11
⊢
((∏t‘{〈∅, 𝐽〉}) ∈ Top ↔
(∏t‘{〈∅, 𝐽〉}) ∈ (TopOn‘∪ (∏t‘{〈∅, 𝐽〉}))) |
13 | 11, 12 | sylib 210 |
. . . . . . . . . 10
⊢ (𝜑 →
(∏t‘{〈∅, 𝐽〉}) ∈ (TopOn‘∪ (∏t‘{〈∅, 𝐽〉}))) |
14 | | eqid 2771 |
. . . . . . . . . . . . 13
⊢
(∏t‘{〈1o, 𝐾〉}) =
(∏t‘{〈1o, 𝐾〉}) |
15 | | 1on 7910 |
. . . . . . . . . . . . . 14
⊢
1o ∈ On |
16 | 15 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 1o ∈
On) |
17 | 14, 16, 2 | pt1hmeo 22133 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑧 ∈ 𝑌 ↦ {〈1o, 𝑧〉}) ∈ (𝐾Homeo(∏t‘{〈1o,
𝐾〉}))) |
18 | | hmeocn 22087 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ 𝑌 ↦ {〈1o, 𝑧〉}) ∈ (𝐾Homeo(∏t‘{〈1o,
𝐾〉})) → (𝑧 ∈ 𝑌 ↦ {〈1o, 𝑧〉}) ∈ (𝐾 Cn (∏t‘{〈1o,
𝐾〉}))) |
19 | | cntop2 21568 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ 𝑌 ↦ {〈1o, 𝑧〉}) ∈ (𝐾 Cn
(∏t‘{〈1o, 𝐾〉})) →
(∏t‘{〈1o, 𝐾〉}) ∈ Top) |
20 | 17, 18, 19 | 3syl 18 |
. . . . . . . . . . 11
⊢ (𝜑 →
(∏t‘{〈1o, 𝐾〉}) ∈ Top) |
21 | | toptopon2 21245 |
. . . . . . . . . . 11
⊢
((∏t‘{〈1o, 𝐾〉}) ∈ Top ↔
(∏t‘{〈1o, 𝐾〉}) ∈ (TopOn‘∪ (∏t‘{〈1o, 𝐾〉}))) |
22 | 20, 21 | sylib 210 |
. . . . . . . . . 10
⊢ (𝜑 →
(∏t‘{〈1o, 𝐾〉}) ∈ (TopOn‘∪ (∏t‘{〈1o, 𝐾〉}))) |
23 | | txtopon 21918 |
. . . . . . . . . 10
⊢
(((∏t‘{〈∅, 𝐽〉}) ∈ (TopOn‘∪ (∏t‘{〈∅, 𝐽〉})) ∧
(∏t‘{〈1o, 𝐾〉}) ∈ (TopOn‘∪ (∏t‘{〈1o, 𝐾〉}))) →
((∏t‘{〈∅, 𝐽〉}) ×t
(∏t‘{〈1o, 𝐾〉})) ∈ (TopOn‘(∪ (∏t‘{〈∅, 𝐽〉}) × ∪ (∏t‘{〈1o, 𝐾〉})))) |
24 | 13, 22, 23 | syl2anc 576 |
. . . . . . . . 9
⊢ (𝜑 →
((∏t‘{〈∅, 𝐽〉}) ×t
(∏t‘{〈1o, 𝐾〉})) ∈ (TopOn‘(∪ (∏t‘{〈∅, 𝐽〉}) × ∪ (∏t‘{〈1o, 𝐾〉})))) |
25 | | opeq2 4674 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 𝑥 → 〈∅, 𝑧〉 = 〈∅, 𝑥〉) |
26 | 25 | sneqd 4447 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑥 → {〈∅, 𝑧〉} = {〈∅, 𝑥〉}) |
27 | | eqid 2771 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ 𝑋 ↦ {〈∅, 𝑧〉}) = (𝑧 ∈ 𝑋 ↦ {〈∅, 𝑧〉}) |
28 | | snex 5184 |
. . . . . . . . . . . . . . 15
⊢
{〈∅, 𝑥〉} ∈ V |
29 | 26, 27, 28 | fvmpt 6593 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝑋 → ((𝑧 ∈ 𝑋 ↦ {〈∅, 𝑧〉})‘𝑥) = {〈∅, 𝑥〉}) |
30 | | opeq2 4674 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 𝑦 → 〈1o, 𝑧〉 = 〈1o,
𝑦〉) |
31 | 30 | sneqd 4447 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑦 → {〈1o, 𝑧〉} = {〈1o,
𝑦〉}) |
32 | | eqid 2771 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ 𝑌 ↦ {〈1o, 𝑧〉}) = (𝑧 ∈ 𝑌 ↦ {〈1o, 𝑧〉}) |
33 | | snex 5184 |
. . . . . . . . . . . . . . 15
⊢
{〈1o, 𝑦〉} ∈ V |
34 | 31, 32, 33 | fvmpt 6593 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ 𝑌 → ((𝑧 ∈ 𝑌 ↦ {〈1o, 𝑧〉})‘𝑦) = {〈1o, 𝑦〉}) |
35 | | opeq12 4675 |
. . . . . . . . . . . . . 14
⊢ ((((𝑧 ∈ 𝑋 ↦ {〈∅, 𝑧〉})‘𝑥) = {〈∅, 𝑥〉} ∧ ((𝑧 ∈ 𝑌 ↦ {〈1o, 𝑧〉})‘𝑦) = {〈1o, 𝑦〉}) → 〈((𝑧 ∈ 𝑋 ↦ {〈∅, 𝑧〉})‘𝑥), ((𝑧 ∈ 𝑌 ↦ {〈1o, 𝑧〉})‘𝑦)〉 = 〈{〈∅,
𝑥〉},
{〈1o, 𝑦〉}〉) |
36 | 29, 34, 35 | syl2an 587 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) → 〈((𝑧 ∈ 𝑋 ↦ {〈∅, 𝑧〉})‘𝑥), ((𝑧 ∈ 𝑌 ↦ {〈1o, 𝑧〉})‘𝑦)〉 = 〈{〈∅,
𝑥〉},
{〈1o, 𝑦〉}〉) |
37 | 36 | mpoeq3ia 7048 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈((𝑧 ∈ 𝑋 ↦ {〈∅, 𝑧〉})‘𝑥), ((𝑧 ∈ 𝑌 ↦ {〈1o, 𝑧〉})‘𝑦)〉) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈{〈∅, 𝑥〉}, {〈1o,
𝑦〉}〉) |
38 | | toponuni 21241 |
. . . . . . . . . . . . . 14
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝐽) |
39 | 1, 38 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑋 = ∪ 𝐽) |
40 | | toponuni 21241 |
. . . . . . . . . . . . . 14
⊢ (𝐾 ∈ (TopOn‘𝑌) → 𝑌 = ∪ 𝐾) |
41 | 2, 40 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑌 = ∪ 𝐾) |
42 | | mpoeq12 7043 |
. . . . . . . . . . . . 13
⊢ ((𝑋 = ∪
𝐽 ∧ 𝑌 = ∪ 𝐾) → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈((𝑧 ∈ 𝑋 ↦ {〈∅, 𝑧〉})‘𝑥), ((𝑧 ∈ 𝑌 ↦ {〈1o, 𝑧〉})‘𝑦)〉) = (𝑥 ∈ ∪ 𝐽, 𝑦 ∈ ∪ 𝐾 ↦ 〈((𝑧 ∈ 𝑋 ↦ {〈∅, 𝑧〉})‘𝑥), ((𝑧 ∈ 𝑌 ↦ {〈1o, 𝑧〉})‘𝑦)〉)) |
43 | 39, 41, 42 | syl2anc 576 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈((𝑧 ∈ 𝑋 ↦ {〈∅, 𝑧〉})‘𝑥), ((𝑧 ∈ 𝑌 ↦ {〈1o, 𝑧〉})‘𝑦)〉) = (𝑥 ∈ ∪ 𝐽, 𝑦 ∈ ∪ 𝐾 ↦ 〈((𝑧 ∈ 𝑋 ↦ {〈∅, 𝑧〉})‘𝑥), ((𝑧 ∈ 𝑌 ↦ {〈1o, 𝑧〉})‘𝑦)〉)) |
44 | 37, 43 | syl5eqr 2821 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈{〈∅, 𝑥〉}, {〈1o,
𝑦〉}〉) = (𝑥 ∈ ∪ 𝐽,
𝑦 ∈ ∪ 𝐾
↦ 〈((𝑧 ∈
𝑋 ↦ {〈∅,
𝑧〉})‘𝑥), ((𝑧 ∈ 𝑌 ↦ {〈1o, 𝑧〉})‘𝑦)〉)) |
45 | | eqid 2771 |
. . . . . . . . . . . 12
⊢ ∪ 𝐽 =
∪ 𝐽 |
46 | | eqid 2771 |
. . . . . . . . . . . 12
⊢ ∪ 𝐾 =
∪ 𝐾 |
47 | 45, 46, 8, 17 | txhmeo 22130 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ ∪ 𝐽, 𝑦 ∈ ∪ 𝐾 ↦ 〈((𝑧 ∈ 𝑋 ↦ {〈∅, 𝑧〉})‘𝑥), ((𝑧 ∈ 𝑌 ↦ {〈1o, 𝑧〉})‘𝑦)〉) ∈ ((𝐽 ×t 𝐾)Homeo((∏t‘{〈∅,
𝐽〉}) ×t
(∏t‘{〈1o, 𝐾〉})))) |
48 | 44, 47 | eqeltrd 2859 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈{〈∅, 𝑥〉}, {〈1o,
𝑦〉}〉) ∈
((𝐽 ×t
𝐾)Homeo((∏t‘{〈∅,
𝐽〉}) ×t
(∏t‘{〈1o, 𝐾〉})))) |
49 | | hmeocn 22087 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈{〈∅, 𝑥〉}, {〈1o,
𝑦〉}〉) ∈
((𝐽 ×t
𝐾)Homeo((∏t‘{〈∅,
𝐽〉}) ×t
(∏t‘{〈1o, 𝐾〉}))) → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈{〈∅, 𝑥〉}, {〈1o, 𝑦〉}〉) ∈ ((𝐽 ×t 𝐾) Cn
((∏t‘{〈∅, 𝐽〉}) ×t
(∏t‘{〈1o, 𝐾〉})))) |
50 | 48, 49 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈{〈∅, 𝑥〉}, {〈1o,
𝑦〉}〉) ∈
((𝐽 ×t
𝐾) Cn
((∏t‘{〈∅, 𝐽〉}) ×t
(∏t‘{〈1o, 𝐾〉})))) |
51 | | cnf2 21576 |
. . . . . . . . 9
⊢ (((𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)) ∧
((∏t‘{〈∅, 𝐽〉}) ×t
(∏t‘{〈1o, 𝐾〉})) ∈ (TopOn‘(∪ (∏t‘{〈∅, 𝐽〉}) × ∪ (∏t‘{〈1o, 𝐾〉}))) ∧ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈{〈∅, 𝑥〉}, {〈1o,
𝑦〉}〉) ∈
((𝐽 ×t
𝐾) Cn
((∏t‘{〈∅, 𝐽〉}) ×t
(∏t‘{〈1o, 𝐾〉})))) → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈{〈∅, 𝑥〉}, {〈1o,
𝑦〉}〉):(𝑋 × 𝑌)⟶(∪
(∏t‘{〈∅, 𝐽〉}) × ∪ (∏t‘{〈1o, 𝐾〉}))) |
52 | 4, 24, 50, 51 | syl3anc 1352 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈{〈∅, 𝑥〉}, {〈1o,
𝑦〉}〉):(𝑋 × 𝑌)⟶(∪
(∏t‘{〈∅, 𝐽〉}) × ∪ (∏t‘{〈1o, 𝐾〉}))) |
53 | | eqid 2771 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈{〈∅, 𝑥〉}, {〈1o,
𝑦〉}〉) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈{〈∅, 𝑥〉}, {〈1o,
𝑦〉}〉) |
54 | 53 | fmpo 7572 |
. . . . . . . 8
⊢
(∀𝑥 ∈
𝑋 ∀𝑦 ∈ 𝑌 〈{〈∅, 𝑥〉}, {〈1o, 𝑦〉}〉 ∈ (∪ (∏t‘{〈∅, 𝐽〉}) × ∪ (∏t‘{〈1o, 𝐾〉})) ↔ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈{〈∅, 𝑥〉}, {〈1o,
𝑦〉}〉):(𝑋 × 𝑌)⟶(∪
(∏t‘{〈∅, 𝐽〉}) × ∪ (∏t‘{〈1o, 𝐾〉}))) |
55 | 52, 54 | sylibr 226 |
. . . . . . 7
⊢ (𝜑 → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 〈{〈∅, 𝑥〉}, {〈1o, 𝑦〉}〉 ∈ (∪ (∏t‘{〈∅, 𝐽〉}) × ∪ (∏t‘{〈1o, 𝐾〉}))) |
56 | 55 | r19.21bi 3151 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ∀𝑦 ∈ 𝑌 〈{〈∅, 𝑥〉}, {〈1o, 𝑦〉}〉 ∈ (∪ (∏t‘{〈∅, 𝐽〉}) × ∪ (∏t‘{〈1o, 𝐾〉}))) |
57 | 56 | r19.21bi 3151 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑌) → 〈{〈∅, 𝑥〉}, {〈1o,
𝑦〉}〉 ∈
(∪ (∏t‘{〈∅, 𝐽〉}) × ∪ (∏t‘{〈1o, 𝐾〉}))) |
58 | 57 | anasss 459 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → 〈{〈∅, 𝑥〉}, {〈1o,
𝑦〉}〉 ∈
(∪ (∏t‘{〈∅, 𝐽〉}) × ∪ (∏t‘{〈1o, 𝐾〉}))) |
59 | | eqidd 2772 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈{〈∅, 𝑥〉}, {〈1o,
𝑦〉}〉) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈{〈∅, 𝑥〉}, {〈1o,
𝑦〉}〉)) |
60 | | vex 3411 |
. . . . . . . . 9
⊢ 𝑥 ∈ V |
61 | | vex 3411 |
. . . . . . . . 9
⊢ 𝑦 ∈ V |
62 | 60, 61 | op1std 7509 |
. . . . . . . 8
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (1st ‘𝑧) = 𝑥) |
63 | 60, 61 | op2ndd 7510 |
. . . . . . . 8
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (2nd ‘𝑧) = 𝑦) |
64 | 62, 63 | uneq12d 4022 |
. . . . . . 7
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ((1st ‘𝑧) ∪ (2nd
‘𝑧)) = (𝑥 ∪ 𝑦)) |
65 | 64 | mpompt 7080 |
. . . . . 6
⊢ (𝑧 ∈ (∪ (∏t‘{〈∅, 𝐽〉}) × ∪ (∏t‘{〈1o, 𝐾〉})) ↦
((1st ‘𝑧)
∪ (2nd ‘𝑧))) = (𝑥 ∈ ∪
(∏t‘{〈∅, 𝐽〉}), 𝑦 ∈ ∪
(∏t‘{〈1o, 𝐾〉}) ↦ (𝑥 ∪ 𝑦)) |
66 | 65 | eqcomi 2780 |
. . . . 5
⊢ (𝑥 ∈ ∪ (∏t‘{〈∅, 𝐽〉}), 𝑦 ∈ ∪
(∏t‘{〈1o, 𝐾〉}) ↦ (𝑥 ∪ 𝑦)) = (𝑧 ∈ (∪
(∏t‘{〈∅, 𝐽〉}) × ∪ (∏t‘{〈1o, 𝐾〉})) ↦
((1st ‘𝑧)
∪ (2nd ‘𝑧))) |
67 | 66 | a1i 11 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ ∪
(∏t‘{〈∅, 𝐽〉}), 𝑦 ∈ ∪
(∏t‘{〈1o, 𝐾〉}) ↦ (𝑥 ∪ 𝑦)) = (𝑧 ∈ (∪
(∏t‘{〈∅, 𝐽〉}) × ∪ (∏t‘{〈1o, 𝐾〉})) ↦
((1st ‘𝑧)
∪ (2nd ‘𝑧)))) |
68 | 28, 33 | op1std 7509 |
. . . . . 6
⊢ (𝑧 = 〈{〈∅, 𝑥〉}, {〈1o,
𝑦〉}〉 →
(1st ‘𝑧) =
{〈∅, 𝑥〉}) |
69 | 28, 33 | op2ndd 7510 |
. . . . . 6
⊢ (𝑧 = 〈{〈∅, 𝑥〉}, {〈1o,
𝑦〉}〉 →
(2nd ‘𝑧) =
{〈1o, 𝑦〉}) |
70 | 68, 69 | uneq12d 4022 |
. . . . 5
⊢ (𝑧 = 〈{〈∅, 𝑥〉}, {〈1o,
𝑦〉}〉 →
((1st ‘𝑧)
∪ (2nd ‘𝑧)) = ({〈∅, 𝑥〉} ∪ {〈1o, 𝑦〉})) |
71 | | xpscg 16685 |
. . . . . . 7
⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V) → ◡({𝑥} +𝑐 {𝑦}) = {〈∅, 𝑥〉, 〈1o, 𝑦〉}) |
72 | 71 | el2v 3415 |
. . . . . 6
⊢ ◡({𝑥} +𝑐 {𝑦}) = {〈∅, 𝑥〉, 〈1o, 𝑦〉} |
73 | | df-pr 4438 |
. . . . . 6
⊢
{〈∅, 𝑥〉, 〈1o, 𝑦〉} = ({〈∅, 𝑥〉} ∪
{〈1o, 𝑦〉}) |
74 | 72, 73 | eqtri 2795 |
. . . . 5
⊢ ◡({𝑥} +𝑐 {𝑦}) = ({〈∅, 𝑥〉} ∪ {〈1o, 𝑦〉}) |
75 | 70, 74 | syl6eqr 2825 |
. . . 4
⊢ (𝑧 = 〈{〈∅, 𝑥〉}, {〈1o,
𝑦〉}〉 →
((1st ‘𝑧)
∪ (2nd ‘𝑧)) = ◡({𝑥} +𝑐 {𝑦})) |
76 | 58, 59, 67, 75 | fmpoco 7596 |
. . 3
⊢ (𝜑 → ((𝑥 ∈ ∪
(∏t‘{〈∅, 𝐽〉}), 𝑦 ∈ ∪
(∏t‘{〈1o, 𝐾〉}) ↦ (𝑥 ∪ 𝑦)) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈{〈∅, 𝑥〉}, {〈1o,
𝑦〉}〉)) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))) |
77 | | xpstopnlem1.f |
. . 3
⊢ 𝐹 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) |
78 | 76, 77 | syl6reqr 2826 |
. 2
⊢ (𝜑 → 𝐹 = ((𝑥 ∈ ∪
(∏t‘{〈∅, 𝐽〉}), 𝑦 ∈ ∪
(∏t‘{〈1o, 𝐾〉}) ↦ (𝑥 ∪ 𝑦)) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈{〈∅, 𝑥〉}, {〈1o,
𝑦〉}〉))) |
79 | | eqid 2771 |
. . . . 5
⊢ ∪ (∏t‘(◡({𝐽} +𝑐 {𝐾}) ↾ {∅})) = ∪ (∏t‘(◡({𝐽} +𝑐 {𝐾}) ↾ {∅})) |
80 | | eqid 2771 |
. . . . 5
⊢ ∪ (∏t‘(◡({𝐽} +𝑐 {𝐾}) ↾ {1o})) = ∪ (∏t‘(◡({𝐽} +𝑐 {𝐾}) ↾
{1o})) |
81 | | eqid 2771 |
. . . . 5
⊢
(∏t‘◡({𝐽} +𝑐 {𝐾})) = (∏t‘◡({𝐽} +𝑐 {𝐾})) |
82 | | eqid 2771 |
. . . . 5
⊢
(∏t‘(◡({𝐽} +𝑐 {𝐾}) ↾ {∅})) =
(∏t‘(◡({𝐽} +𝑐 {𝐾}) ↾
{∅})) |
83 | | eqid 2771 |
. . . . 5
⊢
(∏t‘(◡({𝐽} +𝑐 {𝐾}) ↾ {1o})) =
(∏t‘(◡({𝐽} +𝑐 {𝐾}) ↾
{1o})) |
84 | | eqid 2771 |
. . . . 5
⊢ (𝑥 ∈ ∪ (∏t‘(◡({𝐽} +𝑐 {𝐾}) ↾ {∅})), 𝑦 ∈ ∪
(∏t‘(◡({𝐽} +𝑐 {𝐾}) ↾ {1o}))
↦ (𝑥 ∪ 𝑦)) = (𝑥 ∈ ∪
(∏t‘(◡({𝐽} +𝑐 {𝐾}) ↾ {∅})), 𝑦 ∈ ∪ (∏t‘(◡({𝐽} +𝑐 {𝐾}) ↾ {1o})) ↦ (𝑥 ∪ 𝑦)) |
85 | | 2on 7912 |
. . . . . 6
⊢
2o ∈ On |
86 | 85 | a1i 11 |
. . . . 5
⊢ (𝜑 → 2o ∈
On) |
87 | | topontop 21240 |
. . . . . . 7
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top) |
88 | 1, 87 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐽 ∈ Top) |
89 | | topontop 21240 |
. . . . . . 7
⊢ (𝐾 ∈ (TopOn‘𝑌) → 𝐾 ∈ Top) |
90 | 2, 89 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐾 ∈ Top) |
91 | | xpscfcda 16699 |
. . . . . 6
⊢ (◡({𝐽} +𝑐 {𝐾}):2o⟶Top ↔ (𝐽 ∈ Top ∧ 𝐾 ∈ Top)) |
92 | 88, 90, 91 | sylanbrc 575 |
. . . . 5
⊢ (𝜑 → ◡({𝐽} +𝑐 {𝐾}):2o⟶Top) |
93 | | df2o3 7917 |
. . . . . . 7
⊢
2o = {∅, 1o} |
94 | | df-pr 4438 |
. . . . . . 7
⊢ {∅,
1o} = ({∅} ∪ {1o}) |
95 | 93, 94 | eqtri 2795 |
. . . . . 6
⊢
2o = ({∅} ∪ {1o}) |
96 | 95 | a1i 11 |
. . . . 5
⊢ (𝜑 → 2o = ({∅}
∪ {1o})) |
97 | | 1n0 7919 |
. . . . . . 7
⊢
1o ≠ ∅ |
98 | 97 | necomi 3014 |
. . . . . 6
⊢ ∅
≠ 1o |
99 | | disjsn2 4518 |
. . . . . 6
⊢ (∅
≠ 1o → ({∅} ∩ {1o}) =
∅) |
100 | 98, 99 | mp1i 13 |
. . . . 5
⊢ (𝜑 → ({∅} ∩
{1o}) = ∅) |
101 | 79, 80, 81, 82, 83, 84, 86, 92, 96, 100 | ptunhmeo 22135 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ ∪
(∏t‘(◡({𝐽} +𝑐 {𝐾}) ↾ {∅})), 𝑦 ∈ ∪ (∏t‘(◡({𝐽} +𝑐 {𝐾}) ↾ {1o})) ↦ (𝑥 ∪ 𝑦)) ∈ (((∏t‘(◡({𝐽} +𝑐 {𝐾}) ↾ {∅})) ×t
(∏t‘(◡({𝐽} +𝑐 {𝐾}) ↾
{1o})))Homeo(∏t‘◡({𝐽} +𝑐 {𝐾})))) |
102 | | xpscfn 16686 |
. . . . . . . . . 10
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → ◡({𝐽} +𝑐 {𝐾}) Fn 2o) |
103 | 1, 2, 102 | syl2anc 576 |
. . . . . . . . 9
⊢ (𝜑 → ◡({𝐽} +𝑐 {𝐾}) Fn 2o) |
104 | 6 | prid1 4568 |
. . . . . . . . . 10
⊢ ∅
∈ {∅, 1o} |
105 | 104, 93 | eleqtrri 2858 |
. . . . . . . . 9
⊢ ∅
∈ 2o |
106 | | fnressn 6741 |
. . . . . . . . 9
⊢ ((◡({𝐽} +𝑐 {𝐾}) Fn 2o ∧ ∅ ∈
2o) → (◡({𝐽} +𝑐 {𝐾}) ↾ {∅}) =
{〈∅, (◡({𝐽} +𝑐 {𝐾})‘∅)〉}) |
107 | 103, 105,
106 | sylancl 578 |
. . . . . . . 8
⊢ (𝜑 → (◡({𝐽} +𝑐 {𝐾}) ↾ {∅}) = {〈∅,
(◡({𝐽} +𝑐 {𝐾})‘∅)〉}) |
108 | | xpsc0 16689 |
. . . . . . . . . . 11
⊢ (𝐽 ∈ (TopOn‘𝑋) → (◡({𝐽} +𝑐 {𝐾})‘∅) = 𝐽) |
109 | 1, 108 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (◡({𝐽} +𝑐 {𝐾})‘∅) = 𝐽) |
110 | 109 | opeq2d 4680 |
. . . . . . . . 9
⊢ (𝜑 → 〈∅, (◡({𝐽} +𝑐 {𝐾})‘∅)〉 = 〈∅,
𝐽〉) |
111 | 110 | sneqd 4447 |
. . . . . . . 8
⊢ (𝜑 → {〈∅, (◡({𝐽} +𝑐 {𝐾})‘∅)〉} = {〈∅,
𝐽〉}) |
112 | 107, 111 | eqtrd 2807 |
. . . . . . 7
⊢ (𝜑 → (◡({𝐽} +𝑐 {𝐾}) ↾ {∅}) = {〈∅,
𝐽〉}) |
113 | 112 | fveq2d 6500 |
. . . . . 6
⊢ (𝜑 →
(∏t‘(◡({𝐽} +𝑐 {𝐾}) ↾ {∅})) =
(∏t‘{〈∅, 𝐽〉})) |
114 | 113 | unieqd 4718 |
. . . . 5
⊢ (𝜑 → ∪ (∏t‘(◡({𝐽} +𝑐 {𝐾}) ↾ {∅})) = ∪ (∏t‘{〈∅, 𝐽〉})) |
115 | | 1oex 7911 |
. . . . . . . . . . 11
⊢
1o ∈ V |
116 | 115 | prid2 4569 |
. . . . . . . . . 10
⊢
1o ∈ {∅, 1o} |
117 | 116, 93 | eleqtrri 2858 |
. . . . . . . . 9
⊢
1o ∈ 2o |
118 | | fnressn 6741 |
. . . . . . . . 9
⊢ ((◡({𝐽} +𝑐 {𝐾}) Fn 2o ∧ 1o
∈ 2o) → (◡({𝐽} +𝑐 {𝐾}) ↾ {1o}) =
{〈1o, (◡({𝐽} +𝑐 {𝐾})‘1o)〉}) |
119 | 103, 117,
118 | sylancl 578 |
. . . . . . . 8
⊢ (𝜑 → (◡({𝐽} +𝑐 {𝐾}) ↾ {1o}) =
{〈1o, (◡({𝐽} +𝑐 {𝐾})‘1o)〉}) |
120 | | xpsc1 16690 |
. . . . . . . . . . 11
⊢ (𝐾 ∈ (TopOn‘𝑌) → (◡({𝐽} +𝑐 {𝐾})‘1o) = 𝐾) |
121 | 2, 120 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (◡({𝐽} +𝑐 {𝐾})‘1o) = 𝐾) |
122 | 121 | opeq2d 4680 |
. . . . . . . . 9
⊢ (𝜑 → 〈1o,
(◡({𝐽} +𝑐 {𝐾})‘1o)〉 =
〈1o, 𝐾〉) |
123 | 122 | sneqd 4447 |
. . . . . . . 8
⊢ (𝜑 → {〈1o,
(◡({𝐽} +𝑐 {𝐾})‘1o)〉} =
{〈1o, 𝐾〉}) |
124 | 119, 123 | eqtrd 2807 |
. . . . . . 7
⊢ (𝜑 → (◡({𝐽} +𝑐 {𝐾}) ↾ {1o}) =
{〈1o, 𝐾〉}) |
125 | 124 | fveq2d 6500 |
. . . . . 6
⊢ (𝜑 →
(∏t‘(◡({𝐽} +𝑐 {𝐾}) ↾ {1o})) =
(∏t‘{〈1o, 𝐾〉})) |
126 | 125 | unieqd 4718 |
. . . . 5
⊢ (𝜑 → ∪ (∏t‘(◡({𝐽} +𝑐 {𝐾}) ↾ {1o})) = ∪ (∏t‘{〈1o, 𝐾〉})) |
127 | | eqidd 2772 |
. . . . 5
⊢ (𝜑 → (𝑥 ∪ 𝑦) = (𝑥 ∪ 𝑦)) |
128 | 114, 126,
127 | mpoeq123dv 7045 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ ∪
(∏t‘(◡({𝐽} +𝑐 {𝐾}) ↾ {∅})), 𝑦 ∈ ∪ (∏t‘(◡({𝐽} +𝑐 {𝐾}) ↾ {1o})) ↦ (𝑥 ∪ 𝑦)) = (𝑥 ∈ ∪
(∏t‘{〈∅, 𝐽〉}), 𝑦 ∈ ∪
(∏t‘{〈1o, 𝐾〉}) ↦ (𝑥 ∪ 𝑦))) |
129 | 113, 125 | oveq12d 6992 |
. . . . 5
⊢ (𝜑 →
((∏t‘(◡({𝐽} +𝑐 {𝐾}) ↾ {∅}))
×t (∏t‘(◡({𝐽} +𝑐 {𝐾}) ↾ {1o}))) =
((∏t‘{〈∅, 𝐽〉}) ×t
(∏t‘{〈1o, 𝐾〉}))) |
130 | 129 | oveq1d 6989 |
. . . 4
⊢ (𝜑 →
(((∏t‘(◡({𝐽} +𝑐 {𝐾}) ↾ {∅}))
×t (∏t‘(◡({𝐽} +𝑐 {𝐾}) ↾
{1o})))Homeo(∏t‘◡({𝐽} +𝑐 {𝐾}))) =
(((∏t‘{〈∅, 𝐽〉}) ×t
(∏t‘{〈1o, 𝐾〉}))Homeo(∏t‘◡({𝐽} +𝑐 {𝐾})))) |
131 | 101, 128,
130 | 3eltr3d 2873 |
. . 3
⊢ (𝜑 → (𝑥 ∈ ∪
(∏t‘{〈∅, 𝐽〉}), 𝑦 ∈ ∪
(∏t‘{〈1o, 𝐾〉}) ↦ (𝑥 ∪ 𝑦)) ∈
(((∏t‘{〈∅, 𝐽〉}) ×t
(∏t‘{〈1o, 𝐾〉}))Homeo(∏t‘◡({𝐽} +𝑐 {𝐾})))) |
132 | | hmeoco 22099 |
. . 3
⊢ (((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈{〈∅, 𝑥〉}, {〈1o,
𝑦〉}〉) ∈
((𝐽 ×t
𝐾)Homeo((∏t‘{〈∅,
𝐽〉}) ×t
(∏t‘{〈1o, 𝐾〉}))) ∧ (𝑥 ∈ ∪
(∏t‘{〈∅, 𝐽〉}), 𝑦 ∈ ∪
(∏t‘{〈1o, 𝐾〉}) ↦ (𝑥 ∪ 𝑦)) ∈
(((∏t‘{〈∅, 𝐽〉}) ×t
(∏t‘{〈1o, 𝐾〉}))Homeo(∏t‘◡({𝐽} +𝑐 {𝐾})))) → ((𝑥 ∈ ∪
(∏t‘{〈∅, 𝐽〉}), 𝑦 ∈ ∪
(∏t‘{〈1o, 𝐾〉}) ↦ (𝑥 ∪ 𝑦)) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈{〈∅, 𝑥〉}, {〈1o, 𝑦〉}〉)) ∈ ((𝐽 ×t 𝐾)Homeo(∏t‘◡({𝐽} +𝑐 {𝐾})))) |
133 | 48, 131, 132 | syl2anc 576 |
. 2
⊢ (𝜑 → ((𝑥 ∈ ∪
(∏t‘{〈∅, 𝐽〉}), 𝑦 ∈ ∪
(∏t‘{〈1o, 𝐾〉}) ↦ (𝑥 ∪ 𝑦)) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈{〈∅, 𝑥〉}, {〈1o,
𝑦〉}〉)) ∈
((𝐽 ×t
𝐾)Homeo(∏t‘◡({𝐽} +𝑐 {𝐾})))) |
134 | 78, 133 | eqeltrd 2859 |
1
⊢ (𝜑 → 𝐹 ∈ ((𝐽 ×t 𝐾)Homeo(∏t‘◡({𝐽} +𝑐 {𝐾})))) |