| Step | Hyp | Ref
| Expression |
| 1 | | ptunhmeo.g |
. . . . 5
⊢ 𝐺 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ (𝑥 ∪ 𝑦)) |
| 2 | | vex 3484 |
. . . . . . . 8
⊢ 𝑥 ∈ V |
| 3 | | vex 3484 |
. . . . . . . 8
⊢ 𝑦 ∈ V |
| 4 | 2, 3 | op1std 8024 |
. . . . . . 7
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (1st ‘𝑧) = 𝑥) |
| 5 | 2, 3 | op2ndd 8025 |
. . . . . . 7
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (2nd ‘𝑧) = 𝑦) |
| 6 | 4, 5 | uneq12d 4169 |
. . . . . 6
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ((1st ‘𝑧) ∪ (2nd
‘𝑧)) = (𝑥 ∪ 𝑦)) |
| 7 | 6 | mpompt 7547 |
. . . . 5
⊢ (𝑧 ∈ (𝑋 × 𝑌) ↦ ((1st ‘𝑧) ∪ (2nd
‘𝑧))) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ (𝑥 ∪ 𝑦)) |
| 8 | 1, 7 | eqtr4i 2768 |
. . . 4
⊢ 𝐺 = (𝑧 ∈ (𝑋 × 𝑌) ↦ ((1st ‘𝑧) ∪ (2nd
‘𝑧))) |
| 9 | | xp1st 8046 |
. . . . . . . . . 10
⊢ (𝑧 ∈ (𝑋 × 𝑌) → (1st ‘𝑧) ∈ 𝑋) |
| 10 | 9 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑋 × 𝑌)) → (1st ‘𝑧) ∈ 𝑋) |
| 11 | | ixpeq2 8951 |
. . . . . . . . . . . . 13
⊢
(∀𝑛 ∈
𝐴 ∪ ((𝐹
↾ 𝐴)‘𝑛) = ∪
(𝐹‘𝑛) → X𝑛 ∈ 𝐴 ∪ ((𝐹 ↾ 𝐴)‘𝑛) = X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛)) |
| 12 | | fvres 6925 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ 𝐴 → ((𝐹 ↾ 𝐴)‘𝑛) = (𝐹‘𝑛)) |
| 13 | 12 | unieqd 4920 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ 𝐴 → ∪ ((𝐹 ↾ 𝐴)‘𝑛) = ∪ (𝐹‘𝑛)) |
| 14 | 11, 13 | mprg 3067 |
. . . . . . . . . . . 12
⊢ X𝑛 ∈
𝐴 ∪ ((𝐹
↾ 𝐴)‘𝑛) = X𝑛 ∈
𝐴 ∪ (𝐹‘𝑛) |
| 15 | | ptunhmeo.c |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐶 ∈ 𝑉) |
| 16 | | ssun1 4178 |
. . . . . . . . . . . . . . 15
⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵) |
| 17 | | ptunhmeo.u |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐶 = (𝐴 ∪ 𝐵)) |
| 18 | 16, 17 | sseqtrrid 4027 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐴 ⊆ 𝐶) |
| 19 | 15, 18 | ssexd 5324 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 ∈ V) |
| 20 | | ptunhmeo.f |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐹:𝐶⟶Top) |
| 21 | 20, 18 | fssresd 6775 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐹 ↾ 𝐴):𝐴⟶Top) |
| 22 | | ptunhmeo.k |
. . . . . . . . . . . . . 14
⊢ 𝐾 =
(∏t‘(𝐹 ↾ 𝐴)) |
| 23 | 22 | ptuni 23602 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ V ∧ (𝐹 ↾ 𝐴):𝐴⟶Top) → X𝑛 ∈
𝐴 ∪ ((𝐹
↾ 𝐴)‘𝑛) = ∪
𝐾) |
| 24 | 19, 21, 23 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (𝜑 → X𝑛 ∈
𝐴 ∪ ((𝐹
↾ 𝐴)‘𝑛) = ∪
𝐾) |
| 25 | 14, 24 | eqtr3id 2791 |
. . . . . . . . . . 11
⊢ (𝜑 → X𝑛 ∈
𝐴 ∪ (𝐹‘𝑛) = ∪ 𝐾) |
| 26 | | ptunhmeo.x |
. . . . . . . . . . 11
⊢ 𝑋 = ∪
𝐾 |
| 27 | 25, 26 | eqtr4di 2795 |
. . . . . . . . . 10
⊢ (𝜑 → X𝑛 ∈
𝐴 ∪ (𝐹‘𝑛) = 𝑋) |
| 28 | 27 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑋 × 𝑌)) → X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛) = 𝑋) |
| 29 | 10, 28 | eleqtrrd 2844 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑋 × 𝑌)) → (1st ‘𝑧) ∈ X𝑛 ∈
𝐴 ∪ (𝐹‘𝑛)) |
| 30 | | xp2nd 8047 |
. . . . . . . . . 10
⊢ (𝑧 ∈ (𝑋 × 𝑌) → (2nd ‘𝑧) ∈ 𝑌) |
| 31 | 30 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑋 × 𝑌)) → (2nd ‘𝑧) ∈ 𝑌) |
| 32 | 17 | eqcomd 2743 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴 ∪ 𝐵) = 𝐶) |
| 33 | | ptunhmeo.i |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅) |
| 34 | | uneqdifeq 4493 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ⊆ 𝐶 ∧ (𝐴 ∩ 𝐵) = ∅) → ((𝐴 ∪ 𝐵) = 𝐶 ↔ (𝐶 ∖ 𝐴) = 𝐵)) |
| 35 | 18, 33, 34 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐴 ∪ 𝐵) = 𝐶 ↔ (𝐶 ∖ 𝐴) = 𝐵)) |
| 36 | 32, 35 | mpbid 232 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐶 ∖ 𝐴) = 𝐵) |
| 37 | 36 | ixpeq1d 8949 |
. . . . . . . . . . 11
⊢ (𝜑 → X𝑛 ∈
(𝐶 ∖ 𝐴)∪
(𝐹‘𝑛) = X𝑛 ∈ 𝐵 ∪ (𝐹‘𝑛)) |
| 38 | | ixpeq2 8951 |
. . . . . . . . . . . . . 14
⊢
(∀𝑛 ∈
𝐵 ∪ ((𝐹
↾ 𝐵)‘𝑛) = ∪
(𝐹‘𝑛) → X𝑛 ∈ 𝐵 ∪ ((𝐹 ↾ 𝐵)‘𝑛) = X𝑛 ∈ 𝐵 ∪ (𝐹‘𝑛)) |
| 39 | | fvres 6925 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ 𝐵 → ((𝐹 ↾ 𝐵)‘𝑛) = (𝐹‘𝑛)) |
| 40 | 39 | unieqd 4920 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ 𝐵 → ∪ ((𝐹 ↾ 𝐵)‘𝑛) = ∪ (𝐹‘𝑛)) |
| 41 | 38, 40 | mprg 3067 |
. . . . . . . . . . . . 13
⊢ X𝑛 ∈
𝐵 ∪ ((𝐹
↾ 𝐵)‘𝑛) = X𝑛 ∈
𝐵 ∪ (𝐹‘𝑛) |
| 42 | | ssun2 4179 |
. . . . . . . . . . . . . . . 16
⊢ 𝐵 ⊆ (𝐴 ∪ 𝐵) |
| 43 | 42, 17 | sseqtrrid 4027 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐵 ⊆ 𝐶) |
| 44 | 15, 43 | ssexd 5324 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐵 ∈ V) |
| 45 | 20, 43 | fssresd 6775 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐹 ↾ 𝐵):𝐵⟶Top) |
| 46 | | ptunhmeo.l |
. . . . . . . . . . . . . . 15
⊢ 𝐿 =
(∏t‘(𝐹 ↾ 𝐵)) |
| 47 | 46 | ptuni 23602 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 ∈ V ∧ (𝐹 ↾ 𝐵):𝐵⟶Top) → X𝑛 ∈
𝐵 ∪ ((𝐹
↾ 𝐵)‘𝑛) = ∪
𝐿) |
| 48 | 44, 45, 47 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ (𝜑 → X𝑛 ∈
𝐵 ∪ ((𝐹
↾ 𝐵)‘𝑛) = ∪
𝐿) |
| 49 | 41, 48 | eqtr3id 2791 |
. . . . . . . . . . . 12
⊢ (𝜑 → X𝑛 ∈
𝐵 ∪ (𝐹‘𝑛) = ∪ 𝐿) |
| 50 | | ptunhmeo.y |
. . . . . . . . . . . 12
⊢ 𝑌 = ∪
𝐿 |
| 51 | 49, 50 | eqtr4di 2795 |
. . . . . . . . . . 11
⊢ (𝜑 → X𝑛 ∈
𝐵 ∪ (𝐹‘𝑛) = 𝑌) |
| 52 | 37, 51 | eqtrd 2777 |
. . . . . . . . . 10
⊢ (𝜑 → X𝑛 ∈
(𝐶 ∖ 𝐴)∪
(𝐹‘𝑛) = 𝑌) |
| 53 | 52 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑋 × 𝑌)) → X𝑛 ∈ (𝐶 ∖ 𝐴)∪ (𝐹‘𝑛) = 𝑌) |
| 54 | 31, 53 | eleqtrrd 2844 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑋 × 𝑌)) → (2nd ‘𝑧) ∈ X𝑛 ∈
(𝐶 ∖ 𝐴)∪
(𝐹‘𝑛)) |
| 55 | 18 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑋 × 𝑌)) → 𝐴 ⊆ 𝐶) |
| 56 | | undifixp 8974 |
. . . . . . . 8
⊢
(((1st ‘𝑧) ∈ X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛) ∧ (2nd ‘𝑧) ∈ X𝑛 ∈
(𝐶 ∖ 𝐴)∪
(𝐹‘𝑛) ∧ 𝐴 ⊆ 𝐶) → ((1st ‘𝑧) ∪ (2nd
‘𝑧)) ∈ X𝑛 ∈
𝐶 ∪ (𝐹‘𝑛)) |
| 57 | 29, 54, 55, 56 | syl3anc 1373 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑋 × 𝑌)) → ((1st ‘𝑧) ∪ (2nd
‘𝑧)) ∈ X𝑛 ∈
𝐶 ∪ (𝐹‘𝑛)) |
| 58 | | ixpfn 8943 |
. . . . . . 7
⊢
(((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ X𝑛 ∈
𝐶 ∪ (𝐹‘𝑛) → ((1st ‘𝑧) ∪ (2nd
‘𝑧)) Fn 𝐶) |
| 59 | 57, 58 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑋 × 𝑌)) → ((1st ‘𝑧) ∪ (2nd
‘𝑧)) Fn 𝐶) |
| 60 | | dffn5 6967 |
. . . . . 6
⊢
(((1st ‘𝑧) ∪ (2nd ‘𝑧)) Fn 𝐶 ↔ ((1st ‘𝑧) ∪ (2nd
‘𝑧)) = (𝑘 ∈ 𝐶 ↦ (((1st ‘𝑧) ∪ (2nd
‘𝑧))‘𝑘))) |
| 61 | 59, 60 | sylib 218 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑋 × 𝑌)) → ((1st ‘𝑧) ∪ (2nd
‘𝑧)) = (𝑘 ∈ 𝐶 ↦ (((1st ‘𝑧) ∪ (2nd
‘𝑧))‘𝑘))) |
| 62 | 61 | mpteq2dva 5242 |
. . . 4
⊢ (𝜑 → (𝑧 ∈ (𝑋 × 𝑌) ↦ ((1st ‘𝑧) ∪ (2nd
‘𝑧))) = (𝑧 ∈ (𝑋 × 𝑌) ↦ (𝑘 ∈ 𝐶 ↦ (((1st ‘𝑧) ∪ (2nd
‘𝑧))‘𝑘)))) |
| 63 | 8, 62 | eqtrid 2789 |
. . 3
⊢ (𝜑 → 𝐺 = (𝑧 ∈ (𝑋 × 𝑌) ↦ (𝑘 ∈ 𝐶 ↦ (((1st ‘𝑧) ∪ (2nd
‘𝑧))‘𝑘)))) |
| 64 | | ptunhmeo.j |
. . . 4
⊢ 𝐽 =
(∏t‘𝐹) |
| 65 | | pttop 23590 |
. . . . . . . 8
⊢ ((𝐴 ∈ V ∧ (𝐹 ↾ 𝐴):𝐴⟶Top) →
(∏t‘(𝐹 ↾ 𝐴)) ∈ Top) |
| 66 | 19, 21, 65 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 →
(∏t‘(𝐹 ↾ 𝐴)) ∈ Top) |
| 67 | 22, 66 | eqeltrid 2845 |
. . . . . 6
⊢ (𝜑 → 𝐾 ∈ Top) |
| 68 | 26 | toptopon 22923 |
. . . . . 6
⊢ (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘𝑋)) |
| 69 | 67, 68 | sylib 218 |
. . . . 5
⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑋)) |
| 70 | | pttop 23590 |
. . . . . . . 8
⊢ ((𝐵 ∈ V ∧ (𝐹 ↾ 𝐵):𝐵⟶Top) →
(∏t‘(𝐹 ↾ 𝐵)) ∈ Top) |
| 71 | 44, 45, 70 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 →
(∏t‘(𝐹 ↾ 𝐵)) ∈ Top) |
| 72 | 46, 71 | eqeltrid 2845 |
. . . . . 6
⊢ (𝜑 → 𝐿 ∈ Top) |
| 73 | 50 | toptopon 22923 |
. . . . . 6
⊢ (𝐿 ∈ Top ↔ 𝐿 ∈ (TopOn‘𝑌)) |
| 74 | 72, 73 | sylib 218 |
. . . . 5
⊢ (𝜑 → 𝐿 ∈ (TopOn‘𝑌)) |
| 75 | | txtopon 23599 |
. . . . 5
⊢ ((𝐾 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (TopOn‘𝑌)) → (𝐾 ×t 𝐿) ∈ (TopOn‘(𝑋 × 𝑌))) |
| 76 | 69, 74, 75 | syl2anc 584 |
. . . 4
⊢ (𝜑 → (𝐾 ×t 𝐿) ∈ (TopOn‘(𝑋 × 𝑌))) |
| 77 | 17 | eleq2d 2827 |
. . . . . . 7
⊢ (𝜑 → (𝑘 ∈ 𝐶 ↔ 𝑘 ∈ (𝐴 ∪ 𝐵))) |
| 78 | 77 | biimpa 476 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐶) → 𝑘 ∈ (𝐴 ∪ 𝐵)) |
| 79 | | elun 4153 |
. . . . . 6
⊢ (𝑘 ∈ (𝐴 ∪ 𝐵) ↔ (𝑘 ∈ 𝐴 ∨ 𝑘 ∈ 𝐵)) |
| 80 | 78, 79 | sylib 218 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐶) → (𝑘 ∈ 𝐴 ∨ 𝑘 ∈ 𝐵)) |
| 81 | | ixpfn 8943 |
. . . . . . . . . . 11
⊢
((1st ‘𝑧) ∈ X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛) → (1st ‘𝑧) Fn 𝐴) |
| 82 | 29, 81 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑋 × 𝑌)) → (1st ‘𝑧) Fn 𝐴) |
| 83 | 82 | adantlr 715 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑧 ∈ (𝑋 × 𝑌)) → (1st ‘𝑧) Fn 𝐴) |
| 84 | 51 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑋 × 𝑌)) → X𝑛 ∈ 𝐵 ∪ (𝐹‘𝑛) = 𝑌) |
| 85 | 31, 84 | eleqtrrd 2844 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑋 × 𝑌)) → (2nd ‘𝑧) ∈ X𝑛 ∈
𝐵 ∪ (𝐹‘𝑛)) |
| 86 | | ixpfn 8943 |
. . . . . . . . . . 11
⊢
((2nd ‘𝑧) ∈ X𝑛 ∈ 𝐵 ∪ (𝐹‘𝑛) → (2nd ‘𝑧) Fn 𝐵) |
| 87 | 85, 86 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑋 × 𝑌)) → (2nd ‘𝑧) Fn 𝐵) |
| 88 | 87 | adantlr 715 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑧 ∈ (𝑋 × 𝑌)) → (2nd ‘𝑧) Fn 𝐵) |
| 89 | 33 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑧 ∈ (𝑋 × 𝑌)) → (𝐴 ∩ 𝐵) = ∅) |
| 90 | | simplr 769 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑧 ∈ (𝑋 × 𝑌)) → 𝑘 ∈ 𝐴) |
| 91 | | fvun1 7000 |
. . . . . . . . 9
⊢
(((1st ‘𝑧) Fn 𝐴 ∧ (2nd ‘𝑧) Fn 𝐵 ∧ ((𝐴 ∩ 𝐵) = ∅ ∧ 𝑘 ∈ 𝐴)) → (((1st ‘𝑧) ∪ (2nd
‘𝑧))‘𝑘) = ((1st
‘𝑧)‘𝑘)) |
| 92 | 83, 88, 89, 90, 91 | syl112anc 1376 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑧 ∈ (𝑋 × 𝑌)) → (((1st ‘𝑧) ∪ (2nd
‘𝑧))‘𝑘) = ((1st
‘𝑧)‘𝑘)) |
| 93 | 92 | mpteq2dva 5242 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑧 ∈ (𝑋 × 𝑌) ↦ (((1st ‘𝑧) ∪ (2nd
‘𝑧))‘𝑘)) = (𝑧 ∈ (𝑋 × 𝑌) ↦ ((1st ‘𝑧)‘𝑘))) |
| 94 | 76 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐾 ×t 𝐿) ∈ (TopOn‘(𝑋 × 𝑌))) |
| 95 | 4 | mpompt 7547 |
. . . . . . . . 9
⊢ (𝑧 ∈ (𝑋 × 𝑌) ↦ (1st ‘𝑧)) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝑥) |
| 96 | 69 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐾 ∈ (TopOn‘𝑋)) |
| 97 | 74 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐿 ∈ (TopOn‘𝑌)) |
| 98 | 96, 97 | cnmpt1st 23676 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝑥) ∈ ((𝐾 ×t 𝐿) Cn 𝐾)) |
| 99 | 95, 98 | eqeltrid 2845 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑧 ∈ (𝑋 × 𝑌) ↦ (1st ‘𝑧)) ∈ ((𝐾 ×t 𝐿) Cn 𝐾)) |
| 100 | 19 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐴 ∈ V) |
| 101 | 21 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐹 ↾ 𝐴):𝐴⟶Top) |
| 102 | | simpr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑘 ∈ 𝐴) |
| 103 | 26, 22 | ptpjcn 23619 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ V ∧ (𝐹 ↾ 𝐴):𝐴⟶Top ∧ 𝑘 ∈ 𝐴) → (𝑓 ∈ 𝑋 ↦ (𝑓‘𝑘)) ∈ (𝐾 Cn ((𝐹 ↾ 𝐴)‘𝑘))) |
| 104 | 100, 101,
102, 103 | syl3anc 1373 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑓 ∈ 𝑋 ↦ (𝑓‘𝑘)) ∈ (𝐾 Cn ((𝐹 ↾ 𝐴)‘𝑘))) |
| 105 | | fvres 6925 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ 𝐴 → ((𝐹 ↾ 𝐴)‘𝑘) = (𝐹‘𝑘)) |
| 106 | 105 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝐹 ↾ 𝐴)‘𝑘) = (𝐹‘𝑘)) |
| 107 | 106 | oveq2d 7447 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐾 Cn ((𝐹 ↾ 𝐴)‘𝑘)) = (𝐾 Cn (𝐹‘𝑘))) |
| 108 | 104, 107 | eleqtrd 2843 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑓 ∈ 𝑋 ↦ (𝑓‘𝑘)) ∈ (𝐾 Cn (𝐹‘𝑘))) |
| 109 | | fveq1 6905 |
. . . . . . . 8
⊢ (𝑓 = (1st ‘𝑧) → (𝑓‘𝑘) = ((1st ‘𝑧)‘𝑘)) |
| 110 | 94, 99, 96, 108, 109 | cnmpt11 23671 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑧 ∈ (𝑋 × 𝑌) ↦ ((1st ‘𝑧)‘𝑘)) ∈ ((𝐾 ×t 𝐿) Cn (𝐹‘𝑘))) |
| 111 | 93, 110 | eqeltrd 2841 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑧 ∈ (𝑋 × 𝑌) ↦ (((1st ‘𝑧) ∪ (2nd
‘𝑧))‘𝑘)) ∈ ((𝐾 ×t 𝐿) Cn (𝐹‘𝑘))) |
| 112 | 82 | adantlr 715 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵) ∧ 𝑧 ∈ (𝑋 × 𝑌)) → (1st ‘𝑧) Fn 𝐴) |
| 113 | 87 | adantlr 715 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵) ∧ 𝑧 ∈ (𝑋 × 𝑌)) → (2nd ‘𝑧) Fn 𝐵) |
| 114 | 33 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵) ∧ 𝑧 ∈ (𝑋 × 𝑌)) → (𝐴 ∩ 𝐵) = ∅) |
| 115 | | simplr 769 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵) ∧ 𝑧 ∈ (𝑋 × 𝑌)) → 𝑘 ∈ 𝐵) |
| 116 | | fvun2 7001 |
. . . . . . . . 9
⊢
(((1st ‘𝑧) Fn 𝐴 ∧ (2nd ‘𝑧) Fn 𝐵 ∧ ((𝐴 ∩ 𝐵) = ∅ ∧ 𝑘 ∈ 𝐵)) → (((1st ‘𝑧) ∪ (2nd
‘𝑧))‘𝑘) = ((2nd
‘𝑧)‘𝑘)) |
| 117 | 112, 113,
114, 115, 116 | syl112anc 1376 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵) ∧ 𝑧 ∈ (𝑋 × 𝑌)) → (((1st ‘𝑧) ∪ (2nd
‘𝑧))‘𝑘) = ((2nd
‘𝑧)‘𝑘)) |
| 118 | 117 | mpteq2dva 5242 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → (𝑧 ∈ (𝑋 × 𝑌) ↦ (((1st ‘𝑧) ∪ (2nd
‘𝑧))‘𝑘)) = (𝑧 ∈ (𝑋 × 𝑌) ↦ ((2nd ‘𝑧)‘𝑘))) |
| 119 | 76 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → (𝐾 ×t 𝐿) ∈ (TopOn‘(𝑋 × 𝑌))) |
| 120 | 5 | mpompt 7547 |
. . . . . . . . 9
⊢ (𝑧 ∈ (𝑋 × 𝑌) ↦ (2nd ‘𝑧)) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝑦) |
| 121 | 69 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝐾 ∈ (TopOn‘𝑋)) |
| 122 | 74 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝐿 ∈ (TopOn‘𝑌)) |
| 123 | 121, 122 | cnmpt2nd 23677 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝑦) ∈ ((𝐾 ×t 𝐿) Cn 𝐿)) |
| 124 | 120, 123 | eqeltrid 2845 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → (𝑧 ∈ (𝑋 × 𝑌) ↦ (2nd ‘𝑧)) ∈ ((𝐾 ×t 𝐿) Cn 𝐿)) |
| 125 | 44 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝐵 ∈ V) |
| 126 | 45 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → (𝐹 ↾ 𝐵):𝐵⟶Top) |
| 127 | | simpr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝑘 ∈ 𝐵) |
| 128 | 50, 46 | ptpjcn 23619 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ V ∧ (𝐹 ↾ 𝐵):𝐵⟶Top ∧ 𝑘 ∈ 𝐵) → (𝑓 ∈ 𝑌 ↦ (𝑓‘𝑘)) ∈ (𝐿 Cn ((𝐹 ↾ 𝐵)‘𝑘))) |
| 129 | 125, 126,
127, 128 | syl3anc 1373 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → (𝑓 ∈ 𝑌 ↦ (𝑓‘𝑘)) ∈ (𝐿 Cn ((𝐹 ↾ 𝐵)‘𝑘))) |
| 130 | | fvres 6925 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ 𝐵 → ((𝐹 ↾ 𝐵)‘𝑘) = (𝐹‘𝑘)) |
| 131 | 130 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → ((𝐹 ↾ 𝐵)‘𝑘) = (𝐹‘𝑘)) |
| 132 | 131 | oveq2d 7447 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → (𝐿 Cn ((𝐹 ↾ 𝐵)‘𝑘)) = (𝐿 Cn (𝐹‘𝑘))) |
| 133 | 129, 132 | eleqtrd 2843 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → (𝑓 ∈ 𝑌 ↦ (𝑓‘𝑘)) ∈ (𝐿 Cn (𝐹‘𝑘))) |
| 134 | | fveq1 6905 |
. . . . . . . 8
⊢ (𝑓 = (2nd ‘𝑧) → (𝑓‘𝑘) = ((2nd ‘𝑧)‘𝑘)) |
| 135 | 119, 124,
122, 133, 134 | cnmpt11 23671 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → (𝑧 ∈ (𝑋 × 𝑌) ↦ ((2nd ‘𝑧)‘𝑘)) ∈ ((𝐾 ×t 𝐿) Cn (𝐹‘𝑘))) |
| 136 | 118, 135 | eqeltrd 2841 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → (𝑧 ∈ (𝑋 × 𝑌) ↦ (((1st ‘𝑧) ∪ (2nd
‘𝑧))‘𝑘)) ∈ ((𝐾 ×t 𝐿) Cn (𝐹‘𝑘))) |
| 137 | 111, 136 | jaodan 960 |
. . . . 5
⊢ ((𝜑 ∧ (𝑘 ∈ 𝐴 ∨ 𝑘 ∈ 𝐵)) → (𝑧 ∈ (𝑋 × 𝑌) ↦ (((1st ‘𝑧) ∪ (2nd
‘𝑧))‘𝑘)) ∈ ((𝐾 ×t 𝐿) Cn (𝐹‘𝑘))) |
| 138 | 80, 137 | syldan 591 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐶) → (𝑧 ∈ (𝑋 × 𝑌) ↦ (((1st ‘𝑧) ∪ (2nd
‘𝑧))‘𝑘)) ∈ ((𝐾 ×t 𝐿) Cn (𝐹‘𝑘))) |
| 139 | 64, 76, 15, 20, 138 | ptcn 23635 |
. . 3
⊢ (𝜑 → (𝑧 ∈ (𝑋 × 𝑌) ↦ (𝑘 ∈ 𝐶 ↦ (((1st ‘𝑧) ∪ (2nd
‘𝑧))‘𝑘))) ∈ ((𝐾 ×t 𝐿) Cn 𝐽)) |
| 140 | 63, 139 | eqeltrd 2841 |
. 2
⊢ (𝜑 → 𝐺 ∈ ((𝐾 ×t 𝐿) Cn 𝐽)) |
| 141 | 26, 50, 64, 22, 46, 1, 15, 20, 17, 33 | ptuncnv 23815 |
. . 3
⊢ (𝜑 → ◡𝐺 = (𝑧 ∈ ∪ 𝐽 ↦ 〈(𝑧 ↾ 𝐴), (𝑧 ↾ 𝐵)〉)) |
| 142 | | pttop 23590 |
. . . . . . 7
⊢ ((𝐶 ∈ 𝑉 ∧ 𝐹:𝐶⟶Top) →
(∏t‘𝐹) ∈ Top) |
| 143 | 15, 20, 142 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 →
(∏t‘𝐹) ∈ Top) |
| 144 | 64, 143 | eqeltrid 2845 |
. . . . 5
⊢ (𝜑 → 𝐽 ∈ Top) |
| 145 | | eqid 2737 |
. . . . . 6
⊢ ∪ 𝐽 =
∪ 𝐽 |
| 146 | 145 | toptopon 22923 |
. . . . 5
⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘∪ 𝐽)) |
| 147 | 144, 146 | sylib 218 |
. . . 4
⊢ (𝜑 → 𝐽 ∈ (TopOn‘∪ 𝐽)) |
| 148 | 145, 64, 22 | ptrescn 23647 |
. . . . 5
⊢ ((𝐶 ∈ 𝑉 ∧ 𝐹:𝐶⟶Top ∧ 𝐴 ⊆ 𝐶) → (𝑧 ∈ ∪ 𝐽 ↦ (𝑧 ↾ 𝐴)) ∈ (𝐽 Cn 𝐾)) |
| 149 | 15, 20, 18, 148 | syl3anc 1373 |
. . . 4
⊢ (𝜑 → (𝑧 ∈ ∪ 𝐽 ↦ (𝑧 ↾ 𝐴)) ∈ (𝐽 Cn 𝐾)) |
| 150 | 145, 64, 46 | ptrescn 23647 |
. . . . 5
⊢ ((𝐶 ∈ 𝑉 ∧ 𝐹:𝐶⟶Top ∧ 𝐵 ⊆ 𝐶) → (𝑧 ∈ ∪ 𝐽 ↦ (𝑧 ↾ 𝐵)) ∈ (𝐽 Cn 𝐿)) |
| 151 | 15, 20, 43, 150 | syl3anc 1373 |
. . . 4
⊢ (𝜑 → (𝑧 ∈ ∪ 𝐽 ↦ (𝑧 ↾ 𝐵)) ∈ (𝐽 Cn 𝐿)) |
| 152 | 147, 149,
151 | cnmpt1t 23673 |
. . 3
⊢ (𝜑 → (𝑧 ∈ ∪ 𝐽 ↦ 〈(𝑧 ↾ 𝐴), (𝑧 ↾ 𝐵)〉) ∈ (𝐽 Cn (𝐾 ×t 𝐿))) |
| 153 | 141, 152 | eqeltrd 2841 |
. 2
⊢ (𝜑 → ◡𝐺 ∈ (𝐽 Cn (𝐾 ×t 𝐿))) |
| 154 | | ishmeo 23767 |
. 2
⊢ (𝐺 ∈ ((𝐾 ×t 𝐿)Homeo𝐽) ↔ (𝐺 ∈ ((𝐾 ×t 𝐿) Cn 𝐽) ∧ ◡𝐺 ∈ (𝐽 Cn (𝐾 ×t 𝐿)))) |
| 155 | 140, 153,
154 | sylanbrc 583 |
1
⊢ (𝜑 → 𝐺 ∈ ((𝐾 ×t 𝐿)Homeo𝐽)) |