Step |
Hyp |
Ref |
Expression |
1 |
|
xpstopnlem1.f |
⊢ 𝐹 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { 〈 ∅ , 𝑥 〉 , 〈 1o , 𝑦 〉 } ) |
2 |
|
xpstopnlem1.j |
⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) |
3 |
|
xpstopnlem1.k |
⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) |
4 |
|
txtopon |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝐽 ×t 𝐾 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) ) |
5 |
2 3 4
|
syl2anc |
⊢ ( 𝜑 → ( 𝐽 ×t 𝐾 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) ) |
6 |
|
eqid |
⊢ ( ∏t ‘ { 〈 ∅ , 𝐽 〉 } ) = ( ∏t ‘ { 〈 ∅ , 𝐽 〉 } ) |
7 |
|
0ex |
⊢ ∅ ∈ V |
8 |
7
|
a1i |
⊢ ( 𝜑 → ∅ ∈ V ) |
9 |
6 8 2
|
pt1hmeo |
⊢ ( 𝜑 → ( 𝑧 ∈ 𝑋 ↦ { 〈 ∅ , 𝑧 〉 } ) ∈ ( 𝐽 Homeo ( ∏t ‘ { 〈 ∅ , 𝐽 〉 } ) ) ) |
10 |
|
hmeocn |
⊢ ( ( 𝑧 ∈ 𝑋 ↦ { 〈 ∅ , 𝑧 〉 } ) ∈ ( 𝐽 Homeo ( ∏t ‘ { 〈 ∅ , 𝐽 〉 } ) ) → ( 𝑧 ∈ 𝑋 ↦ { 〈 ∅ , 𝑧 〉 } ) ∈ ( 𝐽 Cn ( ∏t ‘ { 〈 ∅ , 𝐽 〉 } ) ) ) |
11 |
|
cntop2 |
⊢ ( ( 𝑧 ∈ 𝑋 ↦ { 〈 ∅ , 𝑧 〉 } ) ∈ ( 𝐽 Cn ( ∏t ‘ { 〈 ∅ , 𝐽 〉 } ) ) → ( ∏t ‘ { 〈 ∅ , 𝐽 〉 } ) ∈ Top ) |
12 |
9 10 11
|
3syl |
⊢ ( 𝜑 → ( ∏t ‘ { 〈 ∅ , 𝐽 〉 } ) ∈ Top ) |
13 |
|
toptopon2 |
⊢ ( ( ∏t ‘ { 〈 ∅ , 𝐽 〉 } ) ∈ Top ↔ ( ∏t ‘ { 〈 ∅ , 𝐽 〉 } ) ∈ ( TopOn ‘ ∪ ( ∏t ‘ { 〈 ∅ , 𝐽 〉 } ) ) ) |
14 |
12 13
|
sylib |
⊢ ( 𝜑 → ( ∏t ‘ { 〈 ∅ , 𝐽 〉 } ) ∈ ( TopOn ‘ ∪ ( ∏t ‘ { 〈 ∅ , 𝐽 〉 } ) ) ) |
15 |
|
eqid |
⊢ ( ∏t ‘ { 〈 1o , 𝐾 〉 } ) = ( ∏t ‘ { 〈 1o , 𝐾 〉 } ) |
16 |
|
1on |
⊢ 1o ∈ On |
17 |
16
|
a1i |
⊢ ( 𝜑 → 1o ∈ On ) |
18 |
15 17 3
|
pt1hmeo |
⊢ ( 𝜑 → ( 𝑧 ∈ 𝑌 ↦ { 〈 1o , 𝑧 〉 } ) ∈ ( 𝐾 Homeo ( ∏t ‘ { 〈 1o , 𝐾 〉 } ) ) ) |
19 |
|
hmeocn |
⊢ ( ( 𝑧 ∈ 𝑌 ↦ { 〈 1o , 𝑧 〉 } ) ∈ ( 𝐾 Homeo ( ∏t ‘ { 〈 1o , 𝐾 〉 } ) ) → ( 𝑧 ∈ 𝑌 ↦ { 〈 1o , 𝑧 〉 } ) ∈ ( 𝐾 Cn ( ∏t ‘ { 〈 1o , 𝐾 〉 } ) ) ) |
20 |
|
cntop2 |
⊢ ( ( 𝑧 ∈ 𝑌 ↦ { 〈 1o , 𝑧 〉 } ) ∈ ( 𝐾 Cn ( ∏t ‘ { 〈 1o , 𝐾 〉 } ) ) → ( ∏t ‘ { 〈 1o , 𝐾 〉 } ) ∈ Top ) |
21 |
18 19 20
|
3syl |
⊢ ( 𝜑 → ( ∏t ‘ { 〈 1o , 𝐾 〉 } ) ∈ Top ) |
22 |
|
toptopon2 |
⊢ ( ( ∏t ‘ { 〈 1o , 𝐾 〉 } ) ∈ Top ↔ ( ∏t ‘ { 〈 1o , 𝐾 〉 } ) ∈ ( TopOn ‘ ∪ ( ∏t ‘ { 〈 1o , 𝐾 〉 } ) ) ) |
23 |
21 22
|
sylib |
⊢ ( 𝜑 → ( ∏t ‘ { 〈 1o , 𝐾 〉 } ) ∈ ( TopOn ‘ ∪ ( ∏t ‘ { 〈 1o , 𝐾 〉 } ) ) ) |
24 |
|
txtopon |
⊢ ( ( ( ∏t ‘ { 〈 ∅ , 𝐽 〉 } ) ∈ ( TopOn ‘ ∪ ( ∏t ‘ { 〈 ∅ , 𝐽 〉 } ) ) ∧ ( ∏t ‘ { 〈 1o , 𝐾 〉 } ) ∈ ( TopOn ‘ ∪ ( ∏t ‘ { 〈 1o , 𝐾 〉 } ) ) ) → ( ( ∏t ‘ { 〈 ∅ , 𝐽 〉 } ) ×t ( ∏t ‘ { 〈 1o , 𝐾 〉 } ) ) ∈ ( TopOn ‘ ( ∪ ( ∏t ‘ { 〈 ∅ , 𝐽 〉 } ) × ∪ ( ∏t ‘ { 〈 1o , 𝐾 〉 } ) ) ) ) |
25 |
14 23 24
|
syl2anc |
⊢ ( 𝜑 → ( ( ∏t ‘ { 〈 ∅ , 𝐽 〉 } ) ×t ( ∏t ‘ { 〈 1o , 𝐾 〉 } ) ) ∈ ( TopOn ‘ ( ∪ ( ∏t ‘ { 〈 ∅ , 𝐽 〉 } ) × ∪ ( ∏t ‘ { 〈 1o , 𝐾 〉 } ) ) ) ) |
26 |
|
opeq2 |
⊢ ( 𝑧 = 𝑥 → 〈 ∅ , 𝑧 〉 = 〈 ∅ , 𝑥 〉 ) |
27 |
26
|
sneqd |
⊢ ( 𝑧 = 𝑥 → { 〈 ∅ , 𝑧 〉 } = { 〈 ∅ , 𝑥 〉 } ) |
28 |
|
eqid |
⊢ ( 𝑧 ∈ 𝑋 ↦ { 〈 ∅ , 𝑧 〉 } ) = ( 𝑧 ∈ 𝑋 ↦ { 〈 ∅ , 𝑧 〉 } ) |
29 |
|
snex |
⊢ { 〈 ∅ , 𝑥 〉 } ∈ V |
30 |
27 28 29
|
fvmpt |
⊢ ( 𝑥 ∈ 𝑋 → ( ( 𝑧 ∈ 𝑋 ↦ { 〈 ∅ , 𝑧 〉 } ) ‘ 𝑥 ) = { 〈 ∅ , 𝑥 〉 } ) |
31 |
|
opeq2 |
⊢ ( 𝑧 = 𝑦 → 〈 1o , 𝑧 〉 = 〈 1o , 𝑦 〉 ) |
32 |
31
|
sneqd |
⊢ ( 𝑧 = 𝑦 → { 〈 1o , 𝑧 〉 } = { 〈 1o , 𝑦 〉 } ) |
33 |
|
eqid |
⊢ ( 𝑧 ∈ 𝑌 ↦ { 〈 1o , 𝑧 〉 } ) = ( 𝑧 ∈ 𝑌 ↦ { 〈 1o , 𝑧 〉 } ) |
34 |
|
snex |
⊢ { 〈 1o , 𝑦 〉 } ∈ V |
35 |
32 33 34
|
fvmpt |
⊢ ( 𝑦 ∈ 𝑌 → ( ( 𝑧 ∈ 𝑌 ↦ { 〈 1o , 𝑧 〉 } ) ‘ 𝑦 ) = { 〈 1o , 𝑦 〉 } ) |
36 |
|
opeq12 |
⊢ ( ( ( ( 𝑧 ∈ 𝑋 ↦ { 〈 ∅ , 𝑧 〉 } ) ‘ 𝑥 ) = { 〈 ∅ , 𝑥 〉 } ∧ ( ( 𝑧 ∈ 𝑌 ↦ { 〈 1o , 𝑧 〉 } ) ‘ 𝑦 ) = { 〈 1o , 𝑦 〉 } ) → 〈 ( ( 𝑧 ∈ 𝑋 ↦ { 〈 ∅ , 𝑧 〉 } ) ‘ 𝑥 ) , ( ( 𝑧 ∈ 𝑌 ↦ { 〈 1o , 𝑧 〉 } ) ‘ 𝑦 ) 〉 = 〈 { 〈 ∅ , 𝑥 〉 } , { 〈 1o , 𝑦 〉 } 〉 ) |
37 |
30 35 36
|
syl2an |
⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) → 〈 ( ( 𝑧 ∈ 𝑋 ↦ { 〈 ∅ , 𝑧 〉 } ) ‘ 𝑥 ) , ( ( 𝑧 ∈ 𝑌 ↦ { 〈 1o , 𝑧 〉 } ) ‘ 𝑦 ) 〉 = 〈 { 〈 ∅ , 𝑥 〉 } , { 〈 1o , 𝑦 〉 } 〉 ) |
38 |
37
|
mpoeq3ia |
⊢ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 〈 ( ( 𝑧 ∈ 𝑋 ↦ { 〈 ∅ , 𝑧 〉 } ) ‘ 𝑥 ) , ( ( 𝑧 ∈ 𝑌 ↦ { 〈 1o , 𝑧 〉 } ) ‘ 𝑦 ) 〉 ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 〈 { 〈 ∅ , 𝑥 〉 } , { 〈 1o , 𝑦 〉 } 〉 ) |
39 |
|
toponuni |
⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 ) |
40 |
2 39
|
syl |
⊢ ( 𝜑 → 𝑋 = ∪ 𝐽 ) |
41 |
|
toponuni |
⊢ ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) → 𝑌 = ∪ 𝐾 ) |
42 |
3 41
|
syl |
⊢ ( 𝜑 → 𝑌 = ∪ 𝐾 ) |
43 |
|
mpoeq12 |
⊢ ( ( 𝑋 = ∪ 𝐽 ∧ 𝑌 = ∪ 𝐾 ) → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 〈 ( ( 𝑧 ∈ 𝑋 ↦ { 〈 ∅ , 𝑧 〉 } ) ‘ 𝑥 ) , ( ( 𝑧 ∈ 𝑌 ↦ { 〈 1o , 𝑧 〉 } ) ‘ 𝑦 ) 〉 ) = ( 𝑥 ∈ ∪ 𝐽 , 𝑦 ∈ ∪ 𝐾 ↦ 〈 ( ( 𝑧 ∈ 𝑋 ↦ { 〈 ∅ , 𝑧 〉 } ) ‘ 𝑥 ) , ( ( 𝑧 ∈ 𝑌 ↦ { 〈 1o , 𝑧 〉 } ) ‘ 𝑦 ) 〉 ) ) |
44 |
40 42 43
|
syl2anc |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 〈 ( ( 𝑧 ∈ 𝑋 ↦ { 〈 ∅ , 𝑧 〉 } ) ‘ 𝑥 ) , ( ( 𝑧 ∈ 𝑌 ↦ { 〈 1o , 𝑧 〉 } ) ‘ 𝑦 ) 〉 ) = ( 𝑥 ∈ ∪ 𝐽 , 𝑦 ∈ ∪ 𝐾 ↦ 〈 ( ( 𝑧 ∈ 𝑋 ↦ { 〈 ∅ , 𝑧 〉 } ) ‘ 𝑥 ) , ( ( 𝑧 ∈ 𝑌 ↦ { 〈 1o , 𝑧 〉 } ) ‘ 𝑦 ) 〉 ) ) |
45 |
38 44
|
syl5eqr |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 〈 { 〈 ∅ , 𝑥 〉 } , { 〈 1o , 𝑦 〉 } 〉 ) = ( 𝑥 ∈ ∪ 𝐽 , 𝑦 ∈ ∪ 𝐾 ↦ 〈 ( ( 𝑧 ∈ 𝑋 ↦ { 〈 ∅ , 𝑧 〉 } ) ‘ 𝑥 ) , ( ( 𝑧 ∈ 𝑌 ↦ { 〈 1o , 𝑧 〉 } ) ‘ 𝑦 ) 〉 ) ) |
46 |
|
eqid |
⊢ ∪ 𝐽 = ∪ 𝐽 |
47 |
|
eqid |
⊢ ∪ 𝐾 = ∪ 𝐾 |
48 |
46 47 9 18
|
txhmeo |
⊢ ( 𝜑 → ( 𝑥 ∈ ∪ 𝐽 , 𝑦 ∈ ∪ 𝐾 ↦ 〈 ( ( 𝑧 ∈ 𝑋 ↦ { 〈 ∅ , 𝑧 〉 } ) ‘ 𝑥 ) , ( ( 𝑧 ∈ 𝑌 ↦ { 〈 1o , 𝑧 〉 } ) ‘ 𝑦 ) 〉 ) ∈ ( ( 𝐽 ×t 𝐾 ) Homeo ( ( ∏t ‘ { 〈 ∅ , 𝐽 〉 } ) ×t ( ∏t ‘ { 〈 1o , 𝐾 〉 } ) ) ) ) |
49 |
45 48
|
eqeltrd |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 〈 { 〈 ∅ , 𝑥 〉 } , { 〈 1o , 𝑦 〉 } 〉 ) ∈ ( ( 𝐽 ×t 𝐾 ) Homeo ( ( ∏t ‘ { 〈 ∅ , 𝐽 〉 } ) ×t ( ∏t ‘ { 〈 1o , 𝐾 〉 } ) ) ) ) |
50 |
|
hmeocn |
⊢ ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 〈 { 〈 ∅ , 𝑥 〉 } , { 〈 1o , 𝑦 〉 } 〉 ) ∈ ( ( 𝐽 ×t 𝐾 ) Homeo ( ( ∏t ‘ { 〈 ∅ , 𝐽 〉 } ) ×t ( ∏t ‘ { 〈 1o , 𝐾 〉 } ) ) ) → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 〈 { 〈 ∅ , 𝑥 〉 } , { 〈 1o , 𝑦 〉 } 〉 ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn ( ( ∏t ‘ { 〈 ∅ , 𝐽 〉 } ) ×t ( ∏t ‘ { 〈 1o , 𝐾 〉 } ) ) ) ) |
51 |
49 50
|
syl |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 〈 { 〈 ∅ , 𝑥 〉 } , { 〈 1o , 𝑦 〉 } 〉 ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn ( ( ∏t ‘ { 〈 ∅ , 𝐽 〉 } ) ×t ( ∏t ‘ { 〈 1o , 𝐾 〉 } ) ) ) ) |
52 |
|
cnf2 |
⊢ ( ( ( 𝐽 ×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 |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 〈 { 〈 ∅ , 𝑥 〉 } , { 〈 1o , 𝑦 〉 } 〉 ) : ( 𝑋 × 𝑌 ) ⟶ ( ∪ ( ∏t ‘ { 〈 ∅ , 𝐽 〉 } ) × ∪ ( ∏t ‘ { 〈 1o , 𝐾 〉 } ) ) ) |
54 |
|
eqid |
⊢ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 〈 { 〈 ∅ , 𝑥 〉 } , { 〈 1o , 𝑦 〉 } 〉 ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 〈 { 〈 ∅ , 𝑥 〉 } , { 〈 1o , 𝑦 〉 } 〉 ) |
55 |
54
|
fmpo |
⊢ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 〈 { 〈 ∅ , 𝑥 〉 } , { 〈 1o , 𝑦 〉 } 〉 ∈ ( ∪ ( ∏t ‘ { 〈 ∅ , 𝐽 〉 } ) × ∪ ( ∏t ‘ { 〈 1o , 𝐾 〉 } ) ) ↔ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 〈 { 〈 ∅ , 𝑥 〉 } , { 〈 1o , 𝑦 〉 } 〉 ) : ( 𝑋 × 𝑌 ) ⟶ ( ∪ ( ∏t ‘ { 〈 ∅ , 𝐽 〉 } ) × ∪ ( ∏t ‘ { 〈 1o , 𝐾 〉 } ) ) ) |
56 |
53 55
|
sylibr |
⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 〈 { 〈 ∅ , 𝑥 〉 } , { 〈 1o , 𝑦 〉 } 〉 ∈ ( ∪ ( ∏t ‘ { 〈 ∅ , 𝐽 〉 } ) × ∪ ( ∏t ‘ { 〈 1o , 𝐾 〉 } ) ) ) |
57 |
56
|
r19.21bi |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ∀ 𝑦 ∈ 𝑌 〈 { 〈 ∅ , 𝑥 〉 } , { 〈 1o , 𝑦 〉 } 〉 ∈ ( ∪ ( ∏t ‘ { 〈 ∅ , 𝐽 〉 } ) × ∪ ( ∏t ‘ { 〈 1o , 𝐾 〉 } ) ) ) |
58 |
57
|
r19.21bi |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑌 ) → 〈 { 〈 ∅ , 𝑥 〉 } , { 〈 1o , 𝑦 〉 } 〉 ∈ ( ∪ ( ∏t ‘ { 〈 ∅ , 𝐽 〉 } ) × ∪ ( ∏t ‘ { 〈 1o , 𝐾 〉 } ) ) ) |
59 |
58
|
anasss |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ) → 〈 { 〈 ∅ , 𝑥 〉 } , { 〈 1o , 𝑦 〉 } 〉 ∈ ( ∪ ( ∏t ‘ { 〈 ∅ , 𝐽 〉 } ) × ∪ ( ∏t ‘ { 〈 1o , 𝐾 〉 } ) ) ) |
60 |
|
eqidd |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 〈 { 〈 ∅ , 𝑥 〉 } , { 〈 1o , 𝑦 〉 } 〉 ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 〈 { 〈 ∅ , 𝑥 〉 } , { 〈 1o , 𝑦 〉 } 〉 ) ) |
61 |
|
vex |
⊢ 𝑥 ∈ V |
62 |
|
vex |
⊢ 𝑦 ∈ V |
63 |
61 62
|
op1std |
⊢ ( 𝑧 = 〈 𝑥 , 𝑦 〉 → ( 1st ‘ 𝑧 ) = 𝑥 ) |
64 |
61 62
|
op2ndd |
⊢ ( 𝑧 = 〈 𝑥 , 𝑦 〉 → ( 2nd ‘ 𝑧 ) = 𝑦 ) |
65 |
63 64
|
uneq12d |
⊢ ( 𝑧 = 〈 𝑥 , 𝑦 〉 → ( ( 1st ‘ 𝑧 ) ∪ ( 2nd ‘ 𝑧 ) ) = ( 𝑥 ∪ 𝑦 ) ) |
66 |
65
|
mpompt |
⊢ ( 𝑧 ∈ ( ∪ ( ∏t ‘ { 〈 ∅ , 𝐽 〉 } ) × ∪ ( ∏t ‘ { 〈 1o , 𝐾 〉 } ) ) ↦ ( ( 1st ‘ 𝑧 ) ∪ ( 2nd ‘ 𝑧 ) ) ) = ( 𝑥 ∈ ∪ ( ∏t ‘ { 〈 ∅ , 𝐽 〉 } ) , 𝑦 ∈ ∪ ( ∏t ‘ { 〈 1o , 𝐾 〉 } ) ↦ ( 𝑥 ∪ 𝑦 ) ) |
67 |
66
|
eqcomi |
⊢ ( 𝑥 ∈ ∪ ( ∏t ‘ { 〈 ∅ , 𝐽 〉 } ) , 𝑦 ∈ ∪ ( ∏t ‘ { 〈 1o , 𝐾 〉 } ) ↦ ( 𝑥 ∪ 𝑦 ) ) = ( 𝑧 ∈ ( ∪ ( ∏t ‘ { 〈 ∅ , 𝐽 〉 } ) × ∪ ( ∏t ‘ { 〈 1o , 𝐾 〉 } ) ) ↦ ( ( 1st ‘ 𝑧 ) ∪ ( 2nd ‘ 𝑧 ) ) ) |
68 |
67
|
a1i |
⊢ ( 𝜑 → ( 𝑥 ∈ ∪ ( ∏t ‘ { 〈 ∅ , 𝐽 〉 } ) , 𝑦 ∈ ∪ ( ∏t ‘ { 〈 1o , 𝐾 〉 } ) ↦ ( 𝑥 ∪ 𝑦 ) ) = ( 𝑧 ∈ ( ∪ ( ∏t ‘ { 〈 ∅ , 𝐽 〉 } ) × ∪ ( ∏t ‘ { 〈 1o , 𝐾 〉 } ) ) ↦ ( ( 1st ‘ 𝑧 ) ∪ ( 2nd ‘ 𝑧 ) ) ) ) |
69 |
29 34
|
op1std |
⊢ ( 𝑧 = 〈 { 〈 ∅ , 𝑥 〉 } , { 〈 1o , 𝑦 〉 } 〉 → ( 1st ‘ 𝑧 ) = { 〈 ∅ , 𝑥 〉 } ) |
70 |
29 34
|
op2ndd |
⊢ ( 𝑧 = 〈 { 〈 ∅ , 𝑥 〉 } , { 〈 1o , 𝑦 〉 } 〉 → ( 2nd ‘ 𝑧 ) = { 〈 1o , 𝑦 〉 } ) |
71 |
69 70
|
uneq12d |
⊢ ( 𝑧 = 〈 { 〈 ∅ , 𝑥 〉 } , { 〈 1o , 𝑦 〉 } 〉 → ( ( 1st ‘ 𝑧 ) ∪ ( 2nd ‘ 𝑧 ) ) = ( { 〈 ∅ , 𝑥 〉 } ∪ { 〈 1o , 𝑦 〉 } ) ) |
72 |
|
df-pr |
⊢ { 〈 ∅ , 𝑥 〉 , 〈 1o , 𝑦 〉 } = ( { 〈 ∅ , 𝑥 〉 } ∪ { 〈 1o , 𝑦 〉 } ) |
73 |
71 72
|
eqtr4di |
⊢ ( 𝑧 = 〈 { 〈 ∅ , 𝑥 〉 } , { 〈 1o , 𝑦 〉 } 〉 → ( ( 1st ‘ 𝑧 ) ∪ ( 2nd ‘ 𝑧 ) ) = { 〈 ∅ , 𝑥 〉 , 〈 1o , 𝑦 〉 } ) |
74 |
59 60 68 73
|
fmpoco |
⊢ ( 𝜑 → ( ( 𝑥 ∈ ∪ ( ∏t ‘ { 〈 ∅ , 𝐽 〉 } ) , 𝑦 ∈ ∪ ( ∏t ‘ { 〈 1o , 𝐾 〉 } ) ↦ ( 𝑥 ∪ 𝑦 ) ) ∘ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 〈 { 〈 ∅ , 𝑥 〉 } , { 〈 1o , 𝑦 〉 } 〉 ) ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { 〈 ∅ , 𝑥 〉 , 〈 1o , 𝑦 〉 } ) ) |
75 |
1 74
|
eqtr4id |
⊢ ( 𝜑 → 𝐹 = ( ( 𝑥 ∈ ∪ ( ∏t ‘ { 〈 ∅ , 𝐽 〉 } ) , 𝑦 ∈ ∪ ( ∏t ‘ { 〈 1o , 𝐾 〉 } ) ↦ ( 𝑥 ∪ 𝑦 ) ) ∘ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 〈 { 〈 ∅ , 𝑥 〉 } , { 〈 1o , 𝑦 〉 } 〉 ) ) ) |
76 |
|
eqid |
⊢ ∪ ( ∏t ‘ ( { 〈 ∅ , 𝐽 〉 , 〈 1o , 𝐾 〉 } ↾ { ∅ } ) ) = ∪ ( ∏t ‘ ( { 〈 ∅ , 𝐽 〉 , 〈 1o , 𝐾 〉 } ↾ { ∅ } ) ) |
77 |
|
eqid |
⊢ ∪ ( ∏t ‘ ( { 〈 ∅ , 𝐽 〉 , 〈 1o , 𝐾 〉 } ↾ { 1o } ) ) = ∪ ( ∏t ‘ ( { 〈 ∅ , 𝐽 〉 , 〈 1o , 𝐾 〉 } ↾ { 1o } ) ) |
78 |
|
eqid |
⊢ ( ∏t ‘ { 〈 ∅ , 𝐽 〉 , 〈 1o , 𝐾 〉 } ) = ( ∏t ‘ { 〈 ∅ , 𝐽 〉 , 〈 1o , 𝐾 〉 } ) |
79 |
|
eqid |
⊢ ( ∏t ‘ ( { 〈 ∅ , 𝐽 〉 , 〈 1o , 𝐾 〉 } ↾ { ∅ } ) ) = ( ∏t ‘ ( { 〈 ∅ , 𝐽 〉 , 〈 1o , 𝐾 〉 } ↾ { ∅ } ) ) |
80 |
|
eqid |
⊢ ( ∏t ‘ ( { 〈 ∅ , 𝐽 〉 , 〈 1o , 𝐾 〉 } ↾ { 1o } ) ) = ( ∏t ‘ ( { 〈 ∅ , 𝐽 〉 , 〈 1o , 𝐾 〉 } ↾ { 1o } ) ) |
81 |
|
eqid |
⊢ ( 𝑥 ∈ ∪ ( ∏t ‘ ( { 〈 ∅ , 𝐽 〉 , 〈 1o , 𝐾 〉 } ↾ { ∅ } ) ) , 𝑦 ∈ ∪ ( ∏t ‘ ( { 〈 ∅ , 𝐽 〉 , 〈 1o , 𝐾 〉 } ↾ { 1o } ) ) ↦ ( 𝑥 ∪ 𝑦 ) ) = ( 𝑥 ∈ ∪ ( ∏t ‘ ( { 〈 ∅ , 𝐽 〉 , 〈 1o , 𝐾 〉 } ↾ { ∅ } ) ) , 𝑦 ∈ ∪ ( ∏t ‘ ( { 〈 ∅ , 𝐽 〉 , 〈 1o , 𝐾 〉 } ↾ { 1o } ) ) ↦ ( 𝑥 ∪ 𝑦 ) ) |
82 |
|
2on |
⊢ 2o ∈ On |
83 |
82
|
a1i |
⊢ ( 𝜑 → 2o ∈ On ) |
84 |
|
topontop |
⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐽 ∈ Top ) |
85 |
2 84
|
syl |
⊢ ( 𝜑 → 𝐽 ∈ Top ) |
86 |
|
topontop |
⊢ ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) → 𝐾 ∈ Top ) |
87 |
3 86
|
syl |
⊢ ( 𝜑 → 𝐾 ∈ Top ) |
88 |
|
xpscf |
⊢ ( { 〈 ∅ , 𝐽 〉 , 〈 1o , 𝐾 〉 } : 2o ⟶ Top ↔ ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ) |
89 |
85 87 88
|
sylanbrc |
⊢ ( 𝜑 → { 〈 ∅ , 𝐽 〉 , 〈 1o , 𝐾 〉 } : 2o ⟶ Top ) |
90 |
|
df2o3 |
⊢ 2o = { ∅ , 1o } |
91 |
|
df-pr |
⊢ { ∅ , 1o } = ( { ∅ } ∪ { 1o } ) |
92 |
90 91
|
eqtri |
⊢ 2o = ( { ∅ } ∪ { 1o } ) |
93 |
92
|
a1i |
⊢ ( 𝜑 → 2o = ( { ∅ } ∪ { 1o } ) ) |
94 |
|
1n0 |
⊢ 1o ≠ ∅ |
95 |
94
|
necomi |
⊢ ∅ ≠ 1o |
96 |
|
disjsn2 |
⊢ ( ∅ ≠ 1o → ( { ∅ } ∩ { 1o } ) = ∅ ) |
97 |
95 96
|
mp1i |
⊢ ( 𝜑 → ( { ∅ } ∩ { 1o } ) = ∅ ) |
98 |
76 77 78 79 80 81 83 89 93 97
|
ptunhmeo |
⊢ ( 𝜑 → ( 𝑥 ∈ ∪ ( ∏t ‘ ( { 〈 ∅ , 𝐽 〉 , 〈 1o , 𝐾 〉 } ↾ { ∅ } ) ) , 𝑦 ∈ ∪ ( ∏t ‘ ( { 〈 ∅ , 𝐽 〉 , 〈 1o , 𝐾 〉 } ↾ { 1o } ) ) ↦ ( 𝑥 ∪ 𝑦 ) ) ∈ ( ( ( ∏t ‘ ( { 〈 ∅ , 𝐽 〉 , 〈 1o , 𝐾 〉 } ↾ { ∅ } ) ) ×t ( ∏t ‘ ( { 〈 ∅ , 𝐽 〉 , 〈 1o , 𝐾 〉 } ↾ { 1o } ) ) ) Homeo ( ∏t ‘ { 〈 ∅ , 𝐽 〉 , 〈 1o , 𝐾 〉 } ) ) ) |
99 |
|
fnpr2o |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → { 〈 ∅ , 𝐽 〉 , 〈 1o , 𝐾 〉 } Fn 2o ) |
100 |
2 3 99
|
syl2anc |
⊢ ( 𝜑 → { 〈 ∅ , 𝐽 〉 , 〈 1o , 𝐾 〉 } Fn 2o ) |
101 |
7
|
prid1 |
⊢ ∅ ∈ { ∅ , 1o } |
102 |
101 90
|
eleqtrri |
⊢ ∅ ∈ 2o |
103 |
|
fnressn |
⊢ ( ( { 〈 ∅ , 𝐽 〉 , 〈 1o , 𝐾 〉 } Fn 2o ∧ ∅ ∈ 2o ) → ( { 〈 ∅ , 𝐽 〉 , 〈 1o , 𝐾 〉 } ↾ { ∅ } ) = { 〈 ∅ , ( { 〈 ∅ , 𝐽 〉 , 〈 1o , 𝐾 〉 } ‘ ∅ ) 〉 } ) |
104 |
100 102 103
|
sylancl |
⊢ ( 𝜑 → ( { 〈 ∅ , 𝐽 〉 , 〈 1o , 𝐾 〉 } ↾ { ∅ } ) = { 〈 ∅ , ( { 〈 ∅ , 𝐽 〉 , 〈 1o , 𝐾 〉 } ‘ ∅ ) 〉 } ) |
105 |
|
fvpr0o |
⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( { 〈 ∅ , 𝐽 〉 , 〈 1o , 𝐾 〉 } ‘ ∅ ) = 𝐽 ) |
106 |
2 105
|
syl |
⊢ ( 𝜑 → ( { 〈 ∅ , 𝐽 〉 , 〈 1o , 𝐾 〉 } ‘ ∅ ) = 𝐽 ) |
107 |
106
|
opeq2d |
⊢ ( 𝜑 → 〈 ∅ , ( { 〈 ∅ , 𝐽 〉 , 〈 1o , 𝐾 〉 } ‘ ∅ ) 〉 = 〈 ∅ , 𝐽 〉 ) |
108 |
107
|
sneqd |
⊢ ( 𝜑 → { 〈 ∅ , ( { 〈 ∅ , 𝐽 〉 , 〈 1o , 𝐾 〉 } ‘ ∅ ) 〉 } = { 〈 ∅ , 𝐽 〉 } ) |
109 |
104 108
|
eqtrd |
⊢ ( 𝜑 → ( { 〈 ∅ , 𝐽 〉 , 〈 1o , 𝐾 〉 } ↾ { ∅ } ) = { 〈 ∅ , 𝐽 〉 } ) |
110 |
109
|
fveq2d |
⊢ ( 𝜑 → ( ∏t ‘ ( { 〈 ∅ , 𝐽 〉 , 〈 1o , 𝐾 〉 } ↾ { ∅ } ) ) = ( ∏t ‘ { 〈 ∅ , 𝐽 〉 } ) ) |
111 |
110
|
unieqd |
⊢ ( 𝜑 → ∪ ( ∏t ‘ ( { 〈 ∅ , 𝐽 〉 , 〈 1o , 𝐾 〉 } ↾ { ∅ } ) ) = ∪ ( ∏t ‘ { 〈 ∅ , 𝐽 〉 } ) ) |
112 |
|
1oex |
⊢ 1o ∈ V |
113 |
112
|
prid2 |
⊢ 1o ∈ { ∅ , 1o } |
114 |
113 90
|
eleqtrri |
⊢ 1o ∈ 2o |
115 |
|
fnressn |
⊢ ( ( { 〈 ∅ , 𝐽 〉 , 〈 1o , 𝐾 〉 } Fn 2o ∧ 1o ∈ 2o ) → ( { 〈 ∅ , 𝐽 〉 , 〈 1o , 𝐾 〉 } ↾ { 1o } ) = { 〈 1o , ( { 〈 ∅ , 𝐽 〉 , 〈 1o , 𝐾 〉 } ‘ 1o ) 〉 } ) |
116 |
100 114 115
|
sylancl |
⊢ ( 𝜑 → ( { 〈 ∅ , 𝐽 〉 , 〈 1o , 𝐾 〉 } ↾ { 1o } ) = { 〈 1o , ( { 〈 ∅ , 𝐽 〉 , 〈 1o , 𝐾 〉 } ‘ 1o ) 〉 } ) |
117 |
|
fvpr1o |
⊢ ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) → ( { 〈 ∅ , 𝐽 〉 , 〈 1o , 𝐾 〉 } ‘ 1o ) = 𝐾 ) |
118 |
3 117
|
syl |
⊢ ( 𝜑 → ( { 〈 ∅ , 𝐽 〉 , 〈 1o , 𝐾 〉 } ‘ 1o ) = 𝐾 ) |
119 |
118
|
opeq2d |
⊢ ( 𝜑 → 〈 1o , ( { 〈 ∅ , 𝐽 〉 , 〈 1o , 𝐾 〉 } ‘ 1o ) 〉 = 〈 1o , 𝐾 〉 ) |
120 |
119
|
sneqd |
⊢ ( 𝜑 → { 〈 1o , ( { 〈 ∅ , 𝐽 〉 , 〈 1o , 𝐾 〉 } ‘ 1o ) 〉 } = { 〈 1o , 𝐾 〉 } ) |
121 |
116 120
|
eqtrd |
⊢ ( 𝜑 → ( { 〈 ∅ , 𝐽 〉 , 〈 1o , 𝐾 〉 } ↾ { 1o } ) = { 〈 1o , 𝐾 〉 } ) |
122 |
121
|
fveq2d |
⊢ ( 𝜑 → ( ∏t ‘ ( { 〈 ∅ , 𝐽 〉 , 〈 1o , 𝐾 〉 } ↾ { 1o } ) ) = ( ∏t ‘ { 〈 1o , 𝐾 〉 } ) ) |
123 |
122
|
unieqd |
⊢ ( 𝜑 → ∪ ( ∏t ‘ ( { 〈 ∅ , 𝐽 〉 , 〈 1o , 𝐾 〉 } ↾ { 1o } ) ) = ∪ ( ∏t ‘ { 〈 1o , 𝐾 〉 } ) ) |
124 |
|
eqidd |
⊢ ( 𝜑 → ( 𝑥 ∪ 𝑦 ) = ( 𝑥 ∪ 𝑦 ) ) |
125 |
111 123 124
|
mpoeq123dv |
⊢ ( 𝜑 → ( 𝑥 ∈ ∪ ( ∏t ‘ ( { 〈 ∅ , 𝐽 〉 , 〈 1o , 𝐾 〉 } ↾ { ∅ } ) ) , 𝑦 ∈ ∪ ( ∏t ‘ ( { 〈 ∅ , 𝐽 〉 , 〈 1o , 𝐾 〉 } ↾ { 1o } ) ) ↦ ( 𝑥 ∪ 𝑦 ) ) = ( 𝑥 ∈ ∪ ( ∏t ‘ { 〈 ∅ , 𝐽 〉 } ) , 𝑦 ∈ ∪ ( ∏t ‘ { 〈 1o , 𝐾 〉 } ) ↦ ( 𝑥 ∪ 𝑦 ) ) ) |
126 |
110 122
|
oveq12d |
⊢ ( 𝜑 → ( ( ∏t ‘ ( { 〈 ∅ , 𝐽 〉 , 〈 1o , 𝐾 〉 } ↾ { ∅ } ) ) ×t ( ∏t ‘ ( { 〈 ∅ , 𝐽 〉 , 〈 1o , 𝐾 〉 } ↾ { 1o } ) ) ) = ( ( ∏t ‘ { 〈 ∅ , 𝐽 〉 } ) ×t ( ∏t ‘ { 〈 1o , 𝐾 〉 } ) ) ) |
127 |
126
|
oveq1d |
⊢ ( 𝜑 → ( ( ( ∏t ‘ ( { 〈 ∅ , 𝐽 〉 , 〈 1o , 𝐾 〉 } ↾ { ∅ } ) ) ×t ( ∏t ‘ ( { 〈 ∅ , 𝐽 〉 , 〈 1o , 𝐾 〉 } ↾ { 1o } ) ) ) Homeo ( ∏t ‘ { 〈 ∅ , 𝐽 〉 , 〈 1o , 𝐾 〉 } ) ) = ( ( ( ∏t ‘ { 〈 ∅ , 𝐽 〉 } ) ×t ( ∏t ‘ { 〈 1o , 𝐾 〉 } ) ) Homeo ( ∏t ‘ { 〈 ∅ , 𝐽 〉 , 〈 1o , 𝐾 〉 } ) ) ) |
128 |
98 125 127
|
3eltr3d |
⊢ ( 𝜑 → ( 𝑥 ∈ ∪ ( ∏t ‘ { 〈 ∅ , 𝐽 〉 } ) , 𝑦 ∈ ∪ ( ∏t ‘ { 〈 1o , 𝐾 〉 } ) ↦ ( 𝑥 ∪ 𝑦 ) ) ∈ ( ( ( ∏t ‘ { 〈 ∅ , 𝐽 〉 } ) ×t ( ∏t ‘ { 〈 1o , 𝐾 〉 } ) ) Homeo ( ∏t ‘ { 〈 ∅ , 𝐽 〉 , 〈 1o , 𝐾 〉 } ) ) ) |
129 |
|
hmeoco |
⊢ ( ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 〈 { 〈 ∅ , 𝑥 〉 } , { 〈 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 |
⊢ ( 𝜑 → ( ( 𝑥 ∈ ∪ ( ∏t ‘ { 〈 ∅ , 𝐽 〉 } ) , 𝑦 ∈ ∪ ( ∏t ‘ { 〈 1o , 𝐾 〉 } ) ↦ ( 𝑥 ∪ 𝑦 ) ) ∘ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 〈 { 〈 ∅ , 𝑥 〉 } , { 〈 1o , 𝑦 〉 } 〉 ) ) ∈ ( ( 𝐽 ×t 𝐾 ) Homeo ( ∏t ‘ { 〈 ∅ , 𝐽 〉 , 〈 1o , 𝐾 〉 } ) ) ) |
131 |
75 130
|
eqeltrd |
⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐽 ×t 𝐾 ) Homeo ( ∏t ‘ { 〈 ∅ , 𝐽 〉 , 〈 1o , 𝐾 〉 } ) ) ) |