Step | Hyp | Ref
| Expression |
1 | | prdstmdd.y |
. . 3
⊢ 𝑌 = (𝑆Xs𝑅) |
2 | | prdstmdd.i |
. . 3
⊢ (𝜑 → 𝐼 ∈ 𝑊) |
3 | | prdstmdd.s |
. . 3
⊢ (𝜑 → 𝑆 ∈ 𝑉) |
4 | | prdstmdd.r |
. . . 4
⊢ (𝜑 → 𝑅:𝐼⟶TopMnd) |
5 | | tmdmnd 22819 |
. . . . 5
⊢ (𝑥 ∈ TopMnd → 𝑥 ∈ Mnd) |
6 | 5 | ssriv 3879 |
. . . 4
⊢ TopMnd
⊆ Mnd |
7 | | fss 6515 |
. . . 4
⊢ ((𝑅:𝐼⟶TopMnd ∧ TopMnd ⊆ Mnd)
→ 𝑅:𝐼⟶Mnd) |
8 | 4, 6, 7 | sylancl 589 |
. . 3
⊢ (𝜑 → 𝑅:𝐼⟶Mnd) |
9 | 1, 2, 3, 8 | prdsmndd 18053 |
. 2
⊢ (𝜑 → 𝑌 ∈ Mnd) |
10 | | tmdtps 22820 |
. . . . 5
⊢ (𝑥 ∈ TopMnd → 𝑥 ∈ TopSp) |
11 | 10 | ssriv 3879 |
. . . 4
⊢ TopMnd
⊆ TopSp |
12 | | fss 6515 |
. . . 4
⊢ ((𝑅:𝐼⟶TopMnd ∧ TopMnd ⊆ TopSp)
→ 𝑅:𝐼⟶TopSp) |
13 | 4, 11, 12 | sylancl 589 |
. . 3
⊢ (𝜑 → 𝑅:𝐼⟶TopSp) |
14 | 1, 3, 2, 13 | prdstps 22373 |
. 2
⊢ (𝜑 → 𝑌 ∈ TopSp) |
15 | | eqid 2738 |
. . . . . . 7
⊢
(Base‘𝑌) =
(Base‘𝑌) |
16 | 3 | 3ad2ant1 1134 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ (Base‘𝑌) ∧ 𝑔 ∈ (Base‘𝑌)) → 𝑆 ∈ 𝑉) |
17 | 2 | 3ad2ant1 1134 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ (Base‘𝑌) ∧ 𝑔 ∈ (Base‘𝑌)) → 𝐼 ∈ 𝑊) |
18 | 4 | ffnd 6499 |
. . . . . . . 8
⊢ (𝜑 → 𝑅 Fn 𝐼) |
19 | 18 | 3ad2ant1 1134 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ (Base‘𝑌) ∧ 𝑔 ∈ (Base‘𝑌)) → 𝑅 Fn 𝐼) |
20 | | simp2 1138 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ (Base‘𝑌) ∧ 𝑔 ∈ (Base‘𝑌)) → 𝑓 ∈ (Base‘𝑌)) |
21 | | simp3 1139 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ (Base‘𝑌) ∧ 𝑔 ∈ (Base‘𝑌)) → 𝑔 ∈ (Base‘𝑌)) |
22 | | eqid 2738 |
. . . . . . 7
⊢
(+g‘𝑌) = (+g‘𝑌) |
23 | 1, 15, 16, 17, 19, 20, 21, 22 | prdsplusgval 16842 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓 ∈ (Base‘𝑌) ∧ 𝑔 ∈ (Base‘𝑌)) → (𝑓(+g‘𝑌)𝑔) = (𝑘 ∈ 𝐼 ↦ ((𝑓‘𝑘)(+g‘(𝑅‘𝑘))(𝑔‘𝑘)))) |
24 | 23 | mpoeq3dva 7239 |
. . . . 5
⊢ (𝜑 → (𝑓 ∈ (Base‘𝑌), 𝑔 ∈ (Base‘𝑌) ↦ (𝑓(+g‘𝑌)𝑔)) = (𝑓 ∈ (Base‘𝑌), 𝑔 ∈ (Base‘𝑌) ↦ (𝑘 ∈ 𝐼 ↦ ((𝑓‘𝑘)(+g‘(𝑅‘𝑘))(𝑔‘𝑘))))) |
25 | | eqid 2738 |
. . . . . 6
⊢
(+𝑓‘𝑌) = (+𝑓‘𝑌) |
26 | 15, 22, 25 | plusffval 17967 |
. . . . 5
⊢
(+𝑓‘𝑌) = (𝑓 ∈ (Base‘𝑌), 𝑔 ∈ (Base‘𝑌) ↦ (𝑓(+g‘𝑌)𝑔)) |
27 | | vex 3401 |
. . . . . . . . . 10
⊢ 𝑓 ∈ V |
28 | | vex 3401 |
. . . . . . . . . 10
⊢ 𝑔 ∈ V |
29 | 27, 28 | op1std 7717 |
. . . . . . . . 9
⊢ (𝑧 = 〈𝑓, 𝑔〉 → (1st ‘𝑧) = 𝑓) |
30 | 29 | fveq1d 6670 |
. . . . . . . 8
⊢ (𝑧 = 〈𝑓, 𝑔〉 → ((1st ‘𝑧)‘𝑘) = (𝑓‘𝑘)) |
31 | 27, 28 | op2ndd 7718 |
. . . . . . . . 9
⊢ (𝑧 = 〈𝑓, 𝑔〉 → (2nd ‘𝑧) = 𝑔) |
32 | 31 | fveq1d 6670 |
. . . . . . . 8
⊢ (𝑧 = 〈𝑓, 𝑔〉 → ((2nd ‘𝑧)‘𝑘) = (𝑔‘𝑘)) |
33 | 30, 32 | oveq12d 7182 |
. . . . . . 7
⊢ (𝑧 = 〈𝑓, 𝑔〉 → (((1st ‘𝑧)‘𝑘)(+g‘(𝑅‘𝑘))((2nd ‘𝑧)‘𝑘)) = ((𝑓‘𝑘)(+g‘(𝑅‘𝑘))(𝑔‘𝑘))) |
34 | 33 | mpteq2dv 5123 |
. . . . . 6
⊢ (𝑧 = 〈𝑓, 𝑔〉 → (𝑘 ∈ 𝐼 ↦ (((1st ‘𝑧)‘𝑘)(+g‘(𝑅‘𝑘))((2nd ‘𝑧)‘𝑘))) = (𝑘 ∈ 𝐼 ↦ ((𝑓‘𝑘)(+g‘(𝑅‘𝑘))(𝑔‘𝑘)))) |
35 | 34 | mpompt 7274 |
. . . . 5
⊢ (𝑧 ∈ ((Base‘𝑌) × (Base‘𝑌)) ↦ (𝑘 ∈ 𝐼 ↦ (((1st ‘𝑧)‘𝑘)(+g‘(𝑅‘𝑘))((2nd ‘𝑧)‘𝑘)))) = (𝑓 ∈ (Base‘𝑌), 𝑔 ∈ (Base‘𝑌) ↦ (𝑘 ∈ 𝐼 ↦ ((𝑓‘𝑘)(+g‘(𝑅‘𝑘))(𝑔‘𝑘)))) |
36 | 24, 26, 35 | 3eqtr4g 2798 |
. . . 4
⊢ (𝜑 →
(+𝑓‘𝑌) = (𝑧 ∈ ((Base‘𝑌) × (Base‘𝑌)) ↦ (𝑘 ∈ 𝐼 ↦ (((1st ‘𝑧)‘𝑘)(+g‘(𝑅‘𝑘))((2nd ‘𝑧)‘𝑘))))) |
37 | | eqid 2738 |
. . . . 5
⊢
(∏t‘(TopOpen ∘ 𝑅)) = (∏t‘(TopOpen
∘ 𝑅)) |
38 | | eqid 2738 |
. . . . . . . 8
⊢
(TopOpen‘𝑌) =
(TopOpen‘𝑌) |
39 | 15, 38 | istps 21678 |
. . . . . . 7
⊢ (𝑌 ∈ TopSp ↔
(TopOpen‘𝑌) ∈
(TopOn‘(Base‘𝑌))) |
40 | 14, 39 | sylib 221 |
. . . . . 6
⊢ (𝜑 → (TopOpen‘𝑌) ∈
(TopOn‘(Base‘𝑌))) |
41 | | txtopon 22335 |
. . . . . 6
⊢
(((TopOpen‘𝑌)
∈ (TopOn‘(Base‘𝑌)) ∧ (TopOpen‘𝑌) ∈ (TopOn‘(Base‘𝑌))) → ((TopOpen‘𝑌) ×t
(TopOpen‘𝑌)) ∈
(TopOn‘((Base‘𝑌) × (Base‘𝑌)))) |
42 | 40, 40, 41 | syl2anc 587 |
. . . . 5
⊢ (𝜑 → ((TopOpen‘𝑌) ×t
(TopOpen‘𝑌)) ∈
(TopOn‘((Base‘𝑌) × (Base‘𝑌)))) |
43 | | topnfn 16795 |
. . . . . . . 8
⊢ TopOpen
Fn V |
44 | | ssv 3899 |
. . . . . . . 8
⊢ TopSp
⊆ V |
45 | | fnssres 6453 |
. . . . . . . 8
⊢ ((TopOpen
Fn V ∧ TopSp ⊆ V) → (TopOpen ↾ TopSp) Fn
TopSp) |
46 | 43, 44, 45 | mp2an 692 |
. . . . . . 7
⊢ (TopOpen
↾ TopSp) Fn TopSp |
47 | | fvres 6687 |
. . . . . . . . 9
⊢ (𝑥 ∈ TopSp → ((TopOpen
↾ TopSp)‘𝑥) =
(TopOpen‘𝑥)) |
48 | | eqid 2738 |
. . . . . . . . . 10
⊢
(TopOpen‘𝑥) =
(TopOpen‘𝑥) |
49 | 48 | tpstop 21681 |
. . . . . . . . 9
⊢ (𝑥 ∈ TopSp →
(TopOpen‘𝑥) ∈
Top) |
50 | 47, 49 | eqeltrd 2833 |
. . . . . . . 8
⊢ (𝑥 ∈ TopSp → ((TopOpen
↾ TopSp)‘𝑥)
∈ Top) |
51 | 50 | rgen 3063 |
. . . . . . 7
⊢
∀𝑥 ∈
TopSp ((TopOpen ↾ TopSp)‘𝑥) ∈ Top |
52 | | ffnfv 6886 |
. . . . . . 7
⊢ ((TopOpen
↾ TopSp):TopSp⟶Top ↔ ((TopOpen ↾ TopSp) Fn TopSp ∧
∀𝑥 ∈ TopSp
((TopOpen ↾ TopSp)‘𝑥) ∈ Top)) |
53 | 46, 51, 52 | mpbir2an 711 |
. . . . . 6
⊢ (TopOpen
↾ TopSp):TopSp⟶Top |
54 | | fco2 6525 |
. . . . . 6
⊢
(((TopOpen ↾ TopSp):TopSp⟶Top ∧ 𝑅:𝐼⟶TopSp) → (TopOpen ∘ 𝑅):𝐼⟶Top) |
55 | 53, 13, 54 | sylancr 590 |
. . . . 5
⊢ (𝜑 → (TopOpen ∘ 𝑅):𝐼⟶Top) |
56 | 33 | mpompt 7274 |
. . . . . 6
⊢ (𝑧 ∈ ((Base‘𝑌) × (Base‘𝑌)) ↦ (((1st
‘𝑧)‘𝑘)(+g‘(𝑅‘𝑘))((2nd ‘𝑧)‘𝑘))) = (𝑓 ∈ (Base‘𝑌), 𝑔 ∈ (Base‘𝑌) ↦ ((𝑓‘𝑘)(+g‘(𝑅‘𝑘))(𝑔‘𝑘))) |
57 | | eqid 2738 |
. . . . . . . 8
⊢
(TopOpen‘(𝑅‘𝑘)) = (TopOpen‘(𝑅‘𝑘)) |
58 | | eqid 2738 |
. . . . . . . 8
⊢
(+g‘(𝑅‘𝑘)) = (+g‘(𝑅‘𝑘)) |
59 | 4 | ffvelrnda 6855 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝑅‘𝑘) ∈ TopMnd) |
60 | 40 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (TopOpen‘𝑌) ∈ (TopOn‘(Base‘𝑌))) |
61 | 60, 60 | cnmpt1st 22412 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝑓 ∈ (Base‘𝑌), 𝑔 ∈ (Base‘𝑌) ↦ 𝑓) ∈ (((TopOpen‘𝑌) ×t (TopOpen‘𝑌)) Cn (TopOpen‘𝑌))) |
62 | 1, 3, 2, 18, 38 | prdstopn 22372 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (TopOpen‘𝑌) =
(∏t‘(TopOpen ∘ 𝑅))) |
63 | 62 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (TopOpen‘𝑌) = (∏t‘(TopOpen
∘ 𝑅))) |
64 | 63, 60 | eqeltrrd 2834 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (∏t‘(TopOpen
∘ 𝑅)) ∈
(TopOn‘(Base‘𝑌))) |
65 | | toponuni 21658 |
. . . . . . . . . . . . 13
⊢
((∏t‘(TopOpen ∘ 𝑅)) ∈ (TopOn‘(Base‘𝑌)) → (Base‘𝑌) = ∪
(∏t‘(TopOpen ∘ 𝑅))) |
66 | 64, 65 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (Base‘𝑌) = ∪
(∏t‘(TopOpen ∘ 𝑅))) |
67 | 66 | mpteq1d 5116 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝑥 ∈ (Base‘𝑌) ↦ (𝑥‘𝑘)) = (𝑥 ∈ ∪
(∏t‘(TopOpen ∘ 𝑅)) ↦ (𝑥‘𝑘))) |
68 | 2 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → 𝐼 ∈ 𝑊) |
69 | 55 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (TopOpen ∘ 𝑅):𝐼⟶Top) |
70 | | simpr 488 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → 𝑘 ∈ 𝐼) |
71 | | eqid 2738 |
. . . . . . . . . . . . 13
⊢ ∪ (∏t‘(TopOpen ∘ 𝑅)) = ∪ (∏t‘(TopOpen ∘ 𝑅)) |
72 | 71, 37 | ptpjcn 22355 |
. . . . . . . . . . . 12
⊢ ((𝐼 ∈ 𝑊 ∧ (TopOpen ∘ 𝑅):𝐼⟶Top ∧ 𝑘 ∈ 𝐼) → (𝑥 ∈ ∪
(∏t‘(TopOpen ∘ 𝑅)) ↦ (𝑥‘𝑘)) ∈ ((∏t‘(TopOpen
∘ 𝑅)) Cn ((TopOpen
∘ 𝑅)‘𝑘))) |
73 | 68, 69, 70, 72 | syl3anc 1372 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝑥 ∈ ∪
(∏t‘(TopOpen ∘ 𝑅)) ↦ (𝑥‘𝑘)) ∈ ((∏t‘(TopOpen
∘ 𝑅)) Cn ((TopOpen
∘ 𝑅)‘𝑘))) |
74 | 67, 73 | eqeltrd 2833 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝑥 ∈ (Base‘𝑌) ↦ (𝑥‘𝑘)) ∈ ((∏t‘(TopOpen
∘ 𝑅)) Cn ((TopOpen
∘ 𝑅)‘𝑘))) |
75 | 63 | eqcomd 2744 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (∏t‘(TopOpen
∘ 𝑅)) =
(TopOpen‘𝑌)) |
76 | | fvco3 6761 |
. . . . . . . . . . . 12
⊢ ((𝑅:𝐼⟶TopMnd ∧ 𝑘 ∈ 𝐼) → ((TopOpen ∘ 𝑅)‘𝑘) = (TopOpen‘(𝑅‘𝑘))) |
77 | 4, 76 | sylan 583 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → ((TopOpen ∘ 𝑅)‘𝑘) = (TopOpen‘(𝑅‘𝑘))) |
78 | 75, 77 | oveq12d 7182 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → ((∏t‘(TopOpen
∘ 𝑅)) Cn ((TopOpen
∘ 𝑅)‘𝑘)) = ((TopOpen‘𝑌) Cn (TopOpen‘(𝑅‘𝑘)))) |
79 | 74, 78 | eleqtrd 2835 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝑥 ∈ (Base‘𝑌) ↦ (𝑥‘𝑘)) ∈ ((TopOpen‘𝑌) Cn (TopOpen‘(𝑅‘𝑘)))) |
80 | | fveq1 6667 |
. . . . . . . . 9
⊢ (𝑥 = 𝑓 → (𝑥‘𝑘) = (𝑓‘𝑘)) |
81 | 60, 60, 61, 60, 79, 80 | cnmpt21 22415 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝑓 ∈ (Base‘𝑌), 𝑔 ∈ (Base‘𝑌) ↦ (𝑓‘𝑘)) ∈ (((TopOpen‘𝑌) ×t (TopOpen‘𝑌)) Cn (TopOpen‘(𝑅‘𝑘)))) |
82 | 60, 60 | cnmpt2nd 22413 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝑓 ∈ (Base‘𝑌), 𝑔 ∈ (Base‘𝑌) ↦ 𝑔) ∈ (((TopOpen‘𝑌) ×t (TopOpen‘𝑌)) Cn (TopOpen‘𝑌))) |
83 | | fveq1 6667 |
. . . . . . . . 9
⊢ (𝑥 = 𝑔 → (𝑥‘𝑘) = (𝑔‘𝑘)) |
84 | 60, 60, 82, 60, 79, 83 | cnmpt21 22415 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝑓 ∈ (Base‘𝑌), 𝑔 ∈ (Base‘𝑌) ↦ (𝑔‘𝑘)) ∈ (((TopOpen‘𝑌) ×t (TopOpen‘𝑌)) Cn (TopOpen‘(𝑅‘𝑘)))) |
85 | 57, 58, 59, 60, 60, 81, 84 | cnmpt2plusg 22832 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝑓 ∈ (Base‘𝑌), 𝑔 ∈ (Base‘𝑌) ↦ ((𝑓‘𝑘)(+g‘(𝑅‘𝑘))(𝑔‘𝑘))) ∈ (((TopOpen‘𝑌) ×t (TopOpen‘𝑌)) Cn (TopOpen‘(𝑅‘𝑘)))) |
86 | 77 | oveq2d 7180 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (((TopOpen‘𝑌) ×t (TopOpen‘𝑌)) Cn ((TopOpen ∘ 𝑅)‘𝑘)) = (((TopOpen‘𝑌) ×t (TopOpen‘𝑌)) Cn (TopOpen‘(𝑅‘𝑘)))) |
87 | 85, 86 | eleqtrrd 2836 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝑓 ∈ (Base‘𝑌), 𝑔 ∈ (Base‘𝑌) ↦ ((𝑓‘𝑘)(+g‘(𝑅‘𝑘))(𝑔‘𝑘))) ∈ (((TopOpen‘𝑌) ×t (TopOpen‘𝑌)) Cn ((TopOpen ∘ 𝑅)‘𝑘))) |
88 | 56, 87 | eqeltrid 2837 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝑧 ∈ ((Base‘𝑌) × (Base‘𝑌)) ↦ (((1st ‘𝑧)‘𝑘)(+g‘(𝑅‘𝑘))((2nd ‘𝑧)‘𝑘))) ∈ (((TopOpen‘𝑌) ×t (TopOpen‘𝑌)) Cn ((TopOpen ∘ 𝑅)‘𝑘))) |
89 | 37, 42, 2, 55, 88 | ptcn 22371 |
. . . 4
⊢ (𝜑 → (𝑧 ∈ ((Base‘𝑌) × (Base‘𝑌)) ↦ (𝑘 ∈ 𝐼 ↦ (((1st ‘𝑧)‘𝑘)(+g‘(𝑅‘𝑘))((2nd ‘𝑧)‘𝑘)))) ∈ (((TopOpen‘𝑌) ×t
(TopOpen‘𝑌)) Cn
(∏t‘(TopOpen ∘ 𝑅)))) |
90 | 36, 89 | eqeltrd 2833 |
. . 3
⊢ (𝜑 →
(+𝑓‘𝑌) ∈ (((TopOpen‘𝑌) ×t (TopOpen‘𝑌)) Cn
(∏t‘(TopOpen ∘ 𝑅)))) |
91 | 62 | oveq2d 7180 |
. . 3
⊢ (𝜑 → (((TopOpen‘𝑌) ×t
(TopOpen‘𝑌)) Cn
(TopOpen‘𝑌)) =
(((TopOpen‘𝑌)
×t (TopOpen‘𝑌)) Cn (∏t‘(TopOpen
∘ 𝑅)))) |
92 | 90, 91 | eleqtrrd 2836 |
. 2
⊢ (𝜑 →
(+𝑓‘𝑌) ∈ (((TopOpen‘𝑌) ×t (TopOpen‘𝑌)) Cn (TopOpen‘𝑌))) |
93 | 25, 38 | istmd 22818 |
. 2
⊢ (𝑌 ∈ TopMnd ↔ (𝑌 ∈ Mnd ∧ 𝑌 ∈ TopSp ∧
(+𝑓‘𝑌) ∈ (((TopOpen‘𝑌) ×t (TopOpen‘𝑌)) Cn (TopOpen‘𝑌)))) |
94 | 9, 14, 92, 93 | syl3anbrc 1344 |
1
⊢ (𝜑 → 𝑌 ∈ TopMnd) |