Step | Hyp | Ref
| Expression |
1 | | prdstmdd.y |
. . 3
⊢ 𝑌 = (𝑆Xs𝑅) |
2 | | prdstmdd.i |
. . 3
⊢ (𝜑 → 𝐼 ∈ 𝑊) |
3 | | prdstmdd.s |
. . 3
⊢ (𝜑 → 𝑆 ∈ 𝑉) |
4 | | prdstmdd.r |
. . . 4
⊢ (𝜑 → 𝑅:𝐼⟶TopMnd) |
5 | | tmdmnd 21879 |
. . . . 5
⊢ (𝑥 ∈ TopMnd → 𝑥 ∈ Mnd) |
6 | 5 | ssriv 3607 |
. . . 4
⊢ TopMnd
⊆ Mnd |
7 | | fss 6056 |
. . . 4
⊢ ((𝑅:𝐼⟶TopMnd ∧ TopMnd ⊆ Mnd)
→ 𝑅:𝐼⟶Mnd) |
8 | 4, 6, 7 | sylancl 694 |
. . 3
⊢ (𝜑 → 𝑅:𝐼⟶Mnd) |
9 | 1, 2, 3, 8 | prdsmndd 17323 |
. 2
⊢ (𝜑 → 𝑌 ∈ Mnd) |
10 | | tmdtps 21880 |
. . . . 5
⊢ (𝑥 ∈ TopMnd → 𝑥 ∈ TopSp) |
11 | 10 | ssriv 3607 |
. . . 4
⊢ TopMnd
⊆ TopSp |
12 | | fss 6056 |
. . . 4
⊢ ((𝑅:𝐼⟶TopMnd ∧ TopMnd ⊆ TopSp)
→ 𝑅:𝐼⟶TopSp) |
13 | 4, 11, 12 | sylancl 694 |
. . 3
⊢ (𝜑 → 𝑅:𝐼⟶TopSp) |
14 | 1, 3, 2, 13 | prdstps 21432 |
. 2
⊢ (𝜑 → 𝑌 ∈ TopSp) |
15 | | eqid 2622 |
. . . . . . 7
⊢
(Base‘𝑌) =
(Base‘𝑌) |
16 | 3 | 3ad2ant1 1082 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ (Base‘𝑌) ∧ 𝑔 ∈ (Base‘𝑌)) → 𝑆 ∈ 𝑉) |
17 | 2 | 3ad2ant1 1082 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ (Base‘𝑌) ∧ 𝑔 ∈ (Base‘𝑌)) → 𝐼 ∈ 𝑊) |
18 | | ffn 6045 |
. . . . . . . . 9
⊢ (𝑅:𝐼⟶TopMnd → 𝑅 Fn 𝐼) |
19 | 4, 18 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑅 Fn 𝐼) |
20 | 19 | 3ad2ant1 1082 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ (Base‘𝑌) ∧ 𝑔 ∈ (Base‘𝑌)) → 𝑅 Fn 𝐼) |
21 | | simp2 1062 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ (Base‘𝑌) ∧ 𝑔 ∈ (Base‘𝑌)) → 𝑓 ∈ (Base‘𝑌)) |
22 | | simp3 1063 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ (Base‘𝑌) ∧ 𝑔 ∈ (Base‘𝑌)) → 𝑔 ∈ (Base‘𝑌)) |
23 | | eqid 2622 |
. . . . . . 7
⊢
(+g‘𝑌) = (+g‘𝑌) |
24 | 1, 15, 16, 17, 20, 21, 22, 23 | prdsplusgval 16133 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓 ∈ (Base‘𝑌) ∧ 𝑔 ∈ (Base‘𝑌)) → (𝑓(+g‘𝑌)𝑔) = (𝑘 ∈ 𝐼 ↦ ((𝑓‘𝑘)(+g‘(𝑅‘𝑘))(𝑔‘𝑘)))) |
25 | 24 | mpt2eq3dva 6719 |
. . . . 5
⊢ (𝜑 → (𝑓 ∈ (Base‘𝑌), 𝑔 ∈ (Base‘𝑌) ↦ (𝑓(+g‘𝑌)𝑔)) = (𝑓 ∈ (Base‘𝑌), 𝑔 ∈ (Base‘𝑌) ↦ (𝑘 ∈ 𝐼 ↦ ((𝑓‘𝑘)(+g‘(𝑅‘𝑘))(𝑔‘𝑘))))) |
26 | | eqid 2622 |
. . . . . 6
⊢
(+𝑓‘𝑌) = (+𝑓‘𝑌) |
27 | 15, 23, 26 | plusffval 17247 |
. . . . 5
⊢
(+𝑓‘𝑌) = (𝑓 ∈ (Base‘𝑌), 𝑔 ∈ (Base‘𝑌) ↦ (𝑓(+g‘𝑌)𝑔)) |
28 | | vex 3203 |
. . . . . . . . . 10
⊢ 𝑓 ∈ V |
29 | | vex 3203 |
. . . . . . . . . 10
⊢ 𝑔 ∈ V |
30 | 28, 29 | op1std 7178 |
. . . . . . . . 9
⊢ (𝑧 = 〈𝑓, 𝑔〉 → (1st ‘𝑧) = 𝑓) |
31 | 30 | fveq1d 6193 |
. . . . . . . 8
⊢ (𝑧 = 〈𝑓, 𝑔〉 → ((1st ‘𝑧)‘𝑘) = (𝑓‘𝑘)) |
32 | 28, 29 | op2ndd 7179 |
. . . . . . . . 9
⊢ (𝑧 = 〈𝑓, 𝑔〉 → (2nd ‘𝑧) = 𝑔) |
33 | 32 | fveq1d 6193 |
. . . . . . . 8
⊢ (𝑧 = 〈𝑓, 𝑔〉 → ((2nd ‘𝑧)‘𝑘) = (𝑔‘𝑘)) |
34 | 31, 33 | oveq12d 6668 |
. . . . . . 7
⊢ (𝑧 = 〈𝑓, 𝑔〉 → (((1st ‘𝑧)‘𝑘)(+g‘(𝑅‘𝑘))((2nd ‘𝑧)‘𝑘)) = ((𝑓‘𝑘)(+g‘(𝑅‘𝑘))(𝑔‘𝑘))) |
35 | 34 | mpteq2dv 4745 |
. . . . . 6
⊢ (𝑧 = 〈𝑓, 𝑔〉 → (𝑘 ∈ 𝐼 ↦ (((1st ‘𝑧)‘𝑘)(+g‘(𝑅‘𝑘))((2nd ‘𝑧)‘𝑘))) = (𝑘 ∈ 𝐼 ↦ ((𝑓‘𝑘)(+g‘(𝑅‘𝑘))(𝑔‘𝑘)))) |
36 | 35 | mpt2mpt 6752 |
. . . . 5
⊢ (𝑧 ∈ ((Base‘𝑌) × (Base‘𝑌)) ↦ (𝑘 ∈ 𝐼 ↦ (((1st ‘𝑧)‘𝑘)(+g‘(𝑅‘𝑘))((2nd ‘𝑧)‘𝑘)))) = (𝑓 ∈ (Base‘𝑌), 𝑔 ∈ (Base‘𝑌) ↦ (𝑘 ∈ 𝐼 ↦ ((𝑓‘𝑘)(+g‘(𝑅‘𝑘))(𝑔‘𝑘)))) |
37 | 25, 27, 36 | 3eqtr4g 2681 |
. . . 4
⊢ (𝜑 →
(+𝑓‘𝑌) = (𝑧 ∈ ((Base‘𝑌) × (Base‘𝑌)) ↦ (𝑘 ∈ 𝐼 ↦ (((1st ‘𝑧)‘𝑘)(+g‘(𝑅‘𝑘))((2nd ‘𝑧)‘𝑘))))) |
38 | | eqid 2622 |
. . . . 5
⊢
(∏t‘(TopOpen ∘ 𝑅)) = (∏t‘(TopOpen
∘ 𝑅)) |
39 | | eqid 2622 |
. . . . . . . 8
⊢
(TopOpen‘𝑌) =
(TopOpen‘𝑌) |
40 | 15, 39 | istps 20738 |
. . . . . . 7
⊢ (𝑌 ∈ TopSp ↔
(TopOpen‘𝑌) ∈
(TopOn‘(Base‘𝑌))) |
41 | 14, 40 | sylib 208 |
. . . . . 6
⊢ (𝜑 → (TopOpen‘𝑌) ∈
(TopOn‘(Base‘𝑌))) |
42 | | txtopon 21394 |
. . . . . 6
⊢
(((TopOpen‘𝑌)
∈ (TopOn‘(Base‘𝑌)) ∧ (TopOpen‘𝑌) ∈ (TopOn‘(Base‘𝑌))) → ((TopOpen‘𝑌) ×t
(TopOpen‘𝑌)) ∈
(TopOn‘((Base‘𝑌) × (Base‘𝑌)))) |
43 | 41, 41, 42 | syl2anc 693 |
. . . . 5
⊢ (𝜑 → ((TopOpen‘𝑌) ×t
(TopOpen‘𝑌)) ∈
(TopOn‘((Base‘𝑌) × (Base‘𝑌)))) |
44 | | topnfn 16086 |
. . . . . . . 8
⊢ TopOpen
Fn V |
45 | | ssv 3625 |
. . . . . . . 8
⊢ TopSp
⊆ V |
46 | | fnssres 6004 |
. . . . . . . 8
⊢ ((TopOpen
Fn V ∧ TopSp ⊆ V) → (TopOpen ↾ TopSp) Fn
TopSp) |
47 | 44, 45, 46 | mp2an 708 |
. . . . . . 7
⊢ (TopOpen
↾ TopSp) Fn TopSp |
48 | | fvres 6207 |
. . . . . . . . 9
⊢ (𝑥 ∈ TopSp → ((TopOpen
↾ TopSp)‘𝑥) =
(TopOpen‘𝑥)) |
49 | | eqid 2622 |
. . . . . . . . . 10
⊢
(TopOpen‘𝑥) =
(TopOpen‘𝑥) |
50 | 49 | tpstop 20741 |
. . . . . . . . 9
⊢ (𝑥 ∈ TopSp →
(TopOpen‘𝑥) ∈
Top) |
51 | 48, 50 | eqeltrd 2701 |
. . . . . . . 8
⊢ (𝑥 ∈ TopSp → ((TopOpen
↾ TopSp)‘𝑥)
∈ Top) |
52 | 51 | rgen 2922 |
. . . . . . 7
⊢
∀𝑥 ∈
TopSp ((TopOpen ↾ TopSp)‘𝑥) ∈ Top |
53 | | ffnfv 6388 |
. . . . . . 7
⊢ ((TopOpen
↾ TopSp):TopSp⟶Top ↔ ((TopOpen ↾ TopSp) Fn TopSp ∧
∀𝑥 ∈ TopSp
((TopOpen ↾ TopSp)‘𝑥) ∈ Top)) |
54 | 47, 52, 53 | mpbir2an 955 |
. . . . . 6
⊢ (TopOpen
↾ TopSp):TopSp⟶Top |
55 | | fco2 6059 |
. . . . . 6
⊢
(((TopOpen ↾ TopSp):TopSp⟶Top ∧ 𝑅:𝐼⟶TopSp) → (TopOpen ∘ 𝑅):𝐼⟶Top) |
56 | 54, 13, 55 | sylancr 695 |
. . . . 5
⊢ (𝜑 → (TopOpen ∘ 𝑅):𝐼⟶Top) |
57 | 34 | mpt2mpt 6752 |
. . . . . 6
⊢ (𝑧 ∈ ((Base‘𝑌) × (Base‘𝑌)) ↦ (((1st
‘𝑧)‘𝑘)(+g‘(𝑅‘𝑘))((2nd ‘𝑧)‘𝑘))) = (𝑓 ∈ (Base‘𝑌), 𝑔 ∈ (Base‘𝑌) ↦ ((𝑓‘𝑘)(+g‘(𝑅‘𝑘))(𝑔‘𝑘))) |
58 | | eqid 2622 |
. . . . . . . 8
⊢
(TopOpen‘(𝑅‘𝑘)) = (TopOpen‘(𝑅‘𝑘)) |
59 | | eqid 2622 |
. . . . . . . 8
⊢
(+g‘(𝑅‘𝑘)) = (+g‘(𝑅‘𝑘)) |
60 | 4 | ffvelrnda 6359 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝑅‘𝑘) ∈ TopMnd) |
61 | 41 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (TopOpen‘𝑌) ∈ (TopOn‘(Base‘𝑌))) |
62 | 61, 61 | cnmpt1st 21471 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝑓 ∈ (Base‘𝑌), 𝑔 ∈ (Base‘𝑌) ↦ 𝑓) ∈ (((TopOpen‘𝑌) ×t (TopOpen‘𝑌)) Cn (TopOpen‘𝑌))) |
63 | 1, 3, 2, 19, 39 | prdstopn 21431 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (TopOpen‘𝑌) =
(∏t‘(TopOpen ∘ 𝑅))) |
64 | 63 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (TopOpen‘𝑌) = (∏t‘(TopOpen
∘ 𝑅))) |
65 | 64, 61 | eqeltrrd 2702 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (∏t‘(TopOpen
∘ 𝑅)) ∈
(TopOn‘(Base‘𝑌))) |
66 | | toponuni 20719 |
. . . . . . . . . . . . 13
⊢
((∏t‘(TopOpen ∘ 𝑅)) ∈ (TopOn‘(Base‘𝑌)) → (Base‘𝑌) = ∪
(∏t‘(TopOpen ∘ 𝑅))) |
67 | 65, 66 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (Base‘𝑌) = ∪
(∏t‘(TopOpen ∘ 𝑅))) |
68 | 67 | mpteq1d 4738 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝑥 ∈ (Base‘𝑌) ↦ (𝑥‘𝑘)) = (𝑥 ∈ ∪
(∏t‘(TopOpen ∘ 𝑅)) ↦ (𝑥‘𝑘))) |
69 | 2 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → 𝐼 ∈ 𝑊) |
70 | 56 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (TopOpen ∘ 𝑅):𝐼⟶Top) |
71 | | simpr 477 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → 𝑘 ∈ 𝐼) |
72 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢ ∪ (∏t‘(TopOpen ∘ 𝑅)) = ∪ (∏t‘(TopOpen ∘ 𝑅)) |
73 | 72, 38 | ptpjcn 21414 |
. . . . . . . . . . . 12
⊢ ((𝐼 ∈ 𝑊 ∧ (TopOpen ∘ 𝑅):𝐼⟶Top ∧ 𝑘 ∈ 𝐼) → (𝑥 ∈ ∪
(∏t‘(TopOpen ∘ 𝑅)) ↦ (𝑥‘𝑘)) ∈ ((∏t‘(TopOpen
∘ 𝑅)) Cn ((TopOpen
∘ 𝑅)‘𝑘))) |
74 | 69, 70, 71, 73 | syl3anc 1326 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝑥 ∈ ∪
(∏t‘(TopOpen ∘ 𝑅)) ↦ (𝑥‘𝑘)) ∈ ((∏t‘(TopOpen
∘ 𝑅)) Cn ((TopOpen
∘ 𝑅)‘𝑘))) |
75 | 68, 74 | eqeltrd 2701 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝑥 ∈ (Base‘𝑌) ↦ (𝑥‘𝑘)) ∈ ((∏t‘(TopOpen
∘ 𝑅)) Cn ((TopOpen
∘ 𝑅)‘𝑘))) |
76 | 64 | eqcomd 2628 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (∏t‘(TopOpen
∘ 𝑅)) =
(TopOpen‘𝑌)) |
77 | | fvco3 6275 |
. . . . . . . . . . . 12
⊢ ((𝑅:𝐼⟶TopMnd ∧ 𝑘 ∈ 𝐼) → ((TopOpen ∘ 𝑅)‘𝑘) = (TopOpen‘(𝑅‘𝑘))) |
78 | 4, 77 | sylan 488 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → ((TopOpen ∘ 𝑅)‘𝑘) = (TopOpen‘(𝑅‘𝑘))) |
79 | 76, 78 | oveq12d 6668 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → ((∏t‘(TopOpen
∘ 𝑅)) Cn ((TopOpen
∘ 𝑅)‘𝑘)) = ((TopOpen‘𝑌) Cn (TopOpen‘(𝑅‘𝑘)))) |
80 | 75, 79 | eleqtrd 2703 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝑥 ∈ (Base‘𝑌) ↦ (𝑥‘𝑘)) ∈ ((TopOpen‘𝑌) Cn (TopOpen‘(𝑅‘𝑘)))) |
81 | | fveq1 6190 |
. . . . . . . . 9
⊢ (𝑥 = 𝑓 → (𝑥‘𝑘) = (𝑓‘𝑘)) |
82 | 61, 61, 62, 61, 80, 81 | cnmpt21 21474 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝑓 ∈ (Base‘𝑌), 𝑔 ∈ (Base‘𝑌) ↦ (𝑓‘𝑘)) ∈ (((TopOpen‘𝑌) ×t (TopOpen‘𝑌)) Cn (TopOpen‘(𝑅‘𝑘)))) |
83 | 61, 61 | cnmpt2nd 21472 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝑓 ∈ (Base‘𝑌), 𝑔 ∈ (Base‘𝑌) ↦ 𝑔) ∈ (((TopOpen‘𝑌) ×t (TopOpen‘𝑌)) Cn (TopOpen‘𝑌))) |
84 | | fveq1 6190 |
. . . . . . . . 9
⊢ (𝑥 = 𝑔 → (𝑥‘𝑘) = (𝑔‘𝑘)) |
85 | 61, 61, 83, 61, 80, 84 | cnmpt21 21474 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝑓 ∈ (Base‘𝑌), 𝑔 ∈ (Base‘𝑌) ↦ (𝑔‘𝑘)) ∈ (((TopOpen‘𝑌) ×t (TopOpen‘𝑌)) Cn (TopOpen‘(𝑅‘𝑘)))) |
86 | 58, 59, 60, 61, 61, 82, 85 | cnmpt2plusg 21892 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝑓 ∈ (Base‘𝑌), 𝑔 ∈ (Base‘𝑌) ↦ ((𝑓‘𝑘)(+g‘(𝑅‘𝑘))(𝑔‘𝑘))) ∈ (((TopOpen‘𝑌) ×t (TopOpen‘𝑌)) Cn (TopOpen‘(𝑅‘𝑘)))) |
87 | 78 | oveq2d 6666 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (((TopOpen‘𝑌) ×t (TopOpen‘𝑌)) Cn ((TopOpen ∘ 𝑅)‘𝑘)) = (((TopOpen‘𝑌) ×t (TopOpen‘𝑌)) Cn (TopOpen‘(𝑅‘𝑘)))) |
88 | 86, 87 | eleqtrrd 2704 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝑓 ∈ (Base‘𝑌), 𝑔 ∈ (Base‘𝑌) ↦ ((𝑓‘𝑘)(+g‘(𝑅‘𝑘))(𝑔‘𝑘))) ∈ (((TopOpen‘𝑌) ×t (TopOpen‘𝑌)) Cn ((TopOpen ∘ 𝑅)‘𝑘))) |
89 | 57, 88 | syl5eqel 2705 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝑧 ∈ ((Base‘𝑌) × (Base‘𝑌)) ↦ (((1st ‘𝑧)‘𝑘)(+g‘(𝑅‘𝑘))((2nd ‘𝑧)‘𝑘))) ∈ (((TopOpen‘𝑌) ×t (TopOpen‘𝑌)) Cn ((TopOpen ∘ 𝑅)‘𝑘))) |
90 | 38, 43, 2, 56, 89 | ptcn 21430 |
. . . 4
⊢ (𝜑 → (𝑧 ∈ ((Base‘𝑌) × (Base‘𝑌)) ↦ (𝑘 ∈ 𝐼 ↦ (((1st ‘𝑧)‘𝑘)(+g‘(𝑅‘𝑘))((2nd ‘𝑧)‘𝑘)))) ∈ (((TopOpen‘𝑌) ×t
(TopOpen‘𝑌)) Cn
(∏t‘(TopOpen ∘ 𝑅)))) |
91 | 37, 90 | eqeltrd 2701 |
. . 3
⊢ (𝜑 →
(+𝑓‘𝑌) ∈ (((TopOpen‘𝑌) ×t (TopOpen‘𝑌)) Cn
(∏t‘(TopOpen ∘ 𝑅)))) |
92 | 63 | oveq2d 6666 |
. . 3
⊢ (𝜑 → (((TopOpen‘𝑌) ×t
(TopOpen‘𝑌)) Cn
(TopOpen‘𝑌)) =
(((TopOpen‘𝑌)
×t (TopOpen‘𝑌)) Cn (∏t‘(TopOpen
∘ 𝑅)))) |
93 | 91, 92 | eleqtrrd 2704 |
. 2
⊢ (𝜑 →
(+𝑓‘𝑌) ∈ (((TopOpen‘𝑌) ×t (TopOpen‘𝑌)) Cn (TopOpen‘𝑌))) |
94 | 26, 39 | istmd 21878 |
. 2
⊢ (𝑌 ∈ TopMnd ↔ (𝑌 ∈ Mnd ∧ 𝑌 ∈ TopSp ∧
(+𝑓‘𝑌) ∈ (((TopOpen‘𝑌) ×t (TopOpen‘𝑌)) Cn (TopOpen‘𝑌)))) |
95 | 9, 14, 93, 94 | syl3anbrc 1246 |
1
⊢ (𝜑 → 𝑌 ∈ TopMnd) |