Step | Hyp | Ref
| Expression |
1 | | prdstgpd.y |
. . 3
⊢ 𝑌 = (𝑆Xs𝑅) |
2 | | prdstgpd.i |
. . 3
⊢ (𝜑 → 𝐼 ∈ 𝑊) |
3 | | prdstgpd.s |
. . 3
⊢ (𝜑 → 𝑆 ∈ 𝑉) |
4 | | prdstgpd.r |
. . . 4
⊢ (𝜑 → 𝑅:𝐼⟶TopGrp) |
5 | | tgpgrp 21882 |
. . . . 5
⊢ (𝑥 ∈ TopGrp → 𝑥 ∈ Grp) |
6 | 5 | ssriv 3607 |
. . . 4
⊢ TopGrp
⊆ Grp |
7 | | fss 6056 |
. . . 4
⊢ ((𝑅:𝐼⟶TopGrp ∧ TopGrp ⊆ Grp)
→ 𝑅:𝐼⟶Grp) |
8 | 4, 6, 7 | sylancl 694 |
. . 3
⊢ (𝜑 → 𝑅:𝐼⟶Grp) |
9 | 1, 2, 3, 8 | prdsgrpd 17525 |
. 2
⊢ (𝜑 → 𝑌 ∈ Grp) |
10 | | tgptmd 21883 |
. . . . 5
⊢ (𝑥 ∈ TopGrp → 𝑥 ∈ TopMnd) |
11 | 10 | ssriv 3607 |
. . . 4
⊢ TopGrp
⊆ TopMnd |
12 | | fss 6056 |
. . . 4
⊢ ((𝑅:𝐼⟶TopGrp ∧ TopGrp ⊆ TopMnd)
→ 𝑅:𝐼⟶TopMnd) |
13 | 4, 11, 12 | sylancl 694 |
. . 3
⊢ (𝜑 → 𝑅:𝐼⟶TopMnd) |
14 | 1, 2, 3, 13 | prdstmdd 21927 |
. 2
⊢ (𝜑 → 𝑌 ∈ TopMnd) |
15 | | eqid 2622 |
. . . . . . . 8
⊢
(Base‘𝑌) =
(Base‘𝑌) |
16 | | eqid 2622 |
. . . . . . . 8
⊢
(invg‘𝑌) = (invg‘𝑌) |
17 | 15, 16 | grpinvf 17466 |
. . . . . . 7
⊢ (𝑌 ∈ Grp →
(invg‘𝑌):(Base‘𝑌)⟶(Base‘𝑌)) |
18 | 9, 17 | syl 17 |
. . . . . 6
⊢ (𝜑 →
(invg‘𝑌):(Base‘𝑌)⟶(Base‘𝑌)) |
19 | 18 | feqmptd 6249 |
. . . . 5
⊢ (𝜑 →
(invg‘𝑌) =
(𝑥 ∈ (Base‘𝑌) ↦
((invg‘𝑌)‘𝑥))) |
20 | 2 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑌)) → 𝐼 ∈ 𝑊) |
21 | 3 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑌)) → 𝑆 ∈ 𝑉) |
22 | 8 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑌)) → 𝑅:𝐼⟶Grp) |
23 | | simpr 477 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑌)) → 𝑥 ∈ (Base‘𝑌)) |
24 | 1, 20, 21, 22, 15, 16, 23 | prdsinvgd 17526 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑌)) → ((invg‘𝑌)‘𝑥) = (𝑦 ∈ 𝐼 ↦ ((invg‘(𝑅‘𝑦))‘(𝑥‘𝑦)))) |
25 | 24 | mpteq2dva 4744 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (Base‘𝑌) ↦ ((invg‘𝑌)‘𝑥)) = (𝑥 ∈ (Base‘𝑌) ↦ (𝑦 ∈ 𝐼 ↦ ((invg‘(𝑅‘𝑦))‘(𝑥‘𝑦))))) |
26 | 19, 25 | eqtrd 2656 |
. . . 4
⊢ (𝜑 →
(invg‘𝑌) =
(𝑥 ∈ (Base‘𝑌) ↦ (𝑦 ∈ 𝐼 ↦ ((invg‘(𝑅‘𝑦))‘(𝑥‘𝑦))))) |
27 | | eqid 2622 |
. . . . 5
⊢
(∏t‘(TopOpen ∘ 𝑅)) = (∏t‘(TopOpen
∘ 𝑅)) |
28 | | eqid 2622 |
. . . . . . 7
⊢
(TopOpen‘𝑌) =
(TopOpen‘𝑌) |
29 | 28, 15 | tmdtopon 21885 |
. . . . . 6
⊢ (𝑌 ∈ TopMnd →
(TopOpen‘𝑌) ∈
(TopOn‘(Base‘𝑌))) |
30 | 14, 29 | syl 17 |
. . . . 5
⊢ (𝜑 → (TopOpen‘𝑌) ∈
(TopOn‘(Base‘𝑌))) |
31 | | topnfn 16086 |
. . . . . . 7
⊢ TopOpen
Fn V |
32 | | ffn 6045 |
. . . . . . . . 9
⊢ (𝑅:𝐼⟶TopGrp → 𝑅 Fn 𝐼) |
33 | 4, 32 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑅 Fn 𝐼) |
34 | | dffn2 6047 |
. . . . . . . 8
⊢ (𝑅 Fn 𝐼 ↔ 𝑅:𝐼⟶V) |
35 | 33, 34 | sylib 208 |
. . . . . . 7
⊢ (𝜑 → 𝑅:𝐼⟶V) |
36 | | fnfco 6069 |
. . . . . . 7
⊢ ((TopOpen
Fn V ∧ 𝑅:𝐼⟶V) → (TopOpen
∘ 𝑅) Fn 𝐼) |
37 | 31, 35, 36 | sylancr 695 |
. . . . . 6
⊢ (𝜑 → (TopOpen ∘ 𝑅) Fn 𝐼) |
38 | | fvco3 6275 |
. . . . . . . . 9
⊢ ((𝑅:𝐼⟶TopGrp ∧ 𝑦 ∈ 𝐼) → ((TopOpen ∘ 𝑅)‘𝑦) = (TopOpen‘(𝑅‘𝑦))) |
39 | 4, 38 | sylan 488 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → ((TopOpen ∘ 𝑅)‘𝑦) = (TopOpen‘(𝑅‘𝑦))) |
40 | 4 | ffvelrnda 6359 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (𝑅‘𝑦) ∈ TopGrp) |
41 | | eqid 2622 |
. . . . . . . . . 10
⊢
(TopOpen‘(𝑅‘𝑦)) = (TopOpen‘(𝑅‘𝑦)) |
42 | | eqid 2622 |
. . . . . . . . . 10
⊢
(Base‘(𝑅‘𝑦)) = (Base‘(𝑅‘𝑦)) |
43 | 41, 42 | tgptopon 21886 |
. . . . . . . . 9
⊢ ((𝑅‘𝑦) ∈ TopGrp → (TopOpen‘(𝑅‘𝑦)) ∈ (TopOn‘(Base‘(𝑅‘𝑦)))) |
44 | | topontop 20718 |
. . . . . . . . 9
⊢
((TopOpen‘(𝑅‘𝑦)) ∈ (TopOn‘(Base‘(𝑅‘𝑦))) → (TopOpen‘(𝑅‘𝑦)) ∈ Top) |
45 | 40, 43, 44 | 3syl 18 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (TopOpen‘(𝑅‘𝑦)) ∈ Top) |
46 | 39, 45 | eqeltrd 2701 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → ((TopOpen ∘ 𝑅)‘𝑦) ∈ Top) |
47 | 46 | ralrimiva 2966 |
. . . . . 6
⊢ (𝜑 → ∀𝑦 ∈ 𝐼 ((TopOpen ∘ 𝑅)‘𝑦) ∈ Top) |
48 | | ffnfv 6388 |
. . . . . 6
⊢ ((TopOpen
∘ 𝑅):𝐼⟶Top ↔ ((TopOpen
∘ 𝑅) Fn 𝐼 ∧ ∀𝑦 ∈ 𝐼 ((TopOpen ∘ 𝑅)‘𝑦) ∈ Top)) |
49 | 37, 47, 48 | sylanbrc 698 |
. . . . 5
⊢ (𝜑 → (TopOpen ∘ 𝑅):𝐼⟶Top) |
50 | 30 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (TopOpen‘𝑌) ∈ (TopOn‘(Base‘𝑌))) |
51 | 1, 3, 2, 33, 28 | prdstopn 21431 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (TopOpen‘𝑌) =
(∏t‘(TopOpen ∘ 𝑅))) |
52 | 51 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (TopOpen‘𝑌) = (∏t‘(TopOpen
∘ 𝑅))) |
53 | 52 | eqcomd 2628 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (∏t‘(TopOpen
∘ 𝑅)) =
(TopOpen‘𝑌)) |
54 | 53, 50 | eqeltrd 2701 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (∏t‘(TopOpen
∘ 𝑅)) ∈
(TopOn‘(Base‘𝑌))) |
55 | | toponuni 20719 |
. . . . . . . . . 10
⊢
((∏t‘(TopOpen ∘ 𝑅)) ∈ (TopOn‘(Base‘𝑌)) → (Base‘𝑌) = ∪
(∏t‘(TopOpen ∘ 𝑅))) |
56 | | mpteq1 4737 |
. . . . . . . . . 10
⊢
((Base‘𝑌) =
∪ (∏t‘(TopOpen ∘ 𝑅)) → (𝑥 ∈ (Base‘𝑌) ↦ (𝑥‘𝑦)) = (𝑥 ∈ ∪
(∏t‘(TopOpen ∘ 𝑅)) ↦ (𝑥‘𝑦))) |
57 | 54, 55, 56 | 3syl 18 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (𝑥 ∈ (Base‘𝑌) ↦ (𝑥‘𝑦)) = (𝑥 ∈ ∪
(∏t‘(TopOpen ∘ 𝑅)) ↦ (𝑥‘𝑦))) |
58 | 2 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → 𝐼 ∈ 𝑊) |
59 | 49 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (TopOpen ∘ 𝑅):𝐼⟶Top) |
60 | | simpr 477 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → 𝑦 ∈ 𝐼) |
61 | | eqid 2622 |
. . . . . . . . . . 11
⊢ ∪ (∏t‘(TopOpen ∘ 𝑅)) = ∪ (∏t‘(TopOpen ∘ 𝑅)) |
62 | 61, 27 | ptpjcn 21414 |
. . . . . . . . . 10
⊢ ((𝐼 ∈ 𝑊 ∧ (TopOpen ∘ 𝑅):𝐼⟶Top ∧ 𝑦 ∈ 𝐼) → (𝑥 ∈ ∪
(∏t‘(TopOpen ∘ 𝑅)) ↦ (𝑥‘𝑦)) ∈ ((∏t‘(TopOpen
∘ 𝑅)) Cn ((TopOpen
∘ 𝑅)‘𝑦))) |
63 | 58, 59, 60, 62 | syl3anc 1326 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (𝑥 ∈ ∪
(∏t‘(TopOpen ∘ 𝑅)) ↦ (𝑥‘𝑦)) ∈ ((∏t‘(TopOpen
∘ 𝑅)) Cn ((TopOpen
∘ 𝑅)‘𝑦))) |
64 | 57, 63 | eqeltrd 2701 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (𝑥 ∈ (Base‘𝑌) ↦ (𝑥‘𝑦)) ∈ ((∏t‘(TopOpen
∘ 𝑅)) Cn ((TopOpen
∘ 𝑅)‘𝑦))) |
65 | 53, 39 | oveq12d 6668 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → ((∏t‘(TopOpen
∘ 𝑅)) Cn ((TopOpen
∘ 𝑅)‘𝑦)) = ((TopOpen‘𝑌) Cn (TopOpen‘(𝑅‘𝑦)))) |
66 | 64, 65 | eleqtrd 2703 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (𝑥 ∈ (Base‘𝑌) ↦ (𝑥‘𝑦)) ∈ ((TopOpen‘𝑌) Cn (TopOpen‘(𝑅‘𝑦)))) |
67 | | eqid 2622 |
. . . . . . . . 9
⊢
(invg‘(𝑅‘𝑦)) = (invg‘(𝑅‘𝑦)) |
68 | 41, 67 | tgpinv 21889 |
. . . . . . . 8
⊢ ((𝑅‘𝑦) ∈ TopGrp →
(invg‘(𝑅‘𝑦)) ∈ ((TopOpen‘(𝑅‘𝑦)) Cn (TopOpen‘(𝑅‘𝑦)))) |
69 | 40, 68 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (invg‘(𝑅‘𝑦)) ∈ ((TopOpen‘(𝑅‘𝑦)) Cn (TopOpen‘(𝑅‘𝑦)))) |
70 | 50, 66, 69 | cnmpt11f 21467 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (𝑥 ∈ (Base‘𝑌) ↦ ((invg‘(𝑅‘𝑦))‘(𝑥‘𝑦))) ∈ ((TopOpen‘𝑌) Cn (TopOpen‘(𝑅‘𝑦)))) |
71 | 39 | oveq2d 6666 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → ((TopOpen‘𝑌) Cn ((TopOpen ∘ 𝑅)‘𝑦)) = ((TopOpen‘𝑌) Cn (TopOpen‘(𝑅‘𝑦)))) |
72 | 70, 71 | eleqtrrd 2704 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (𝑥 ∈ (Base‘𝑌) ↦ ((invg‘(𝑅‘𝑦))‘(𝑥‘𝑦))) ∈ ((TopOpen‘𝑌) Cn ((TopOpen ∘ 𝑅)‘𝑦))) |
73 | 27, 30, 2, 49, 72 | ptcn 21430 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (Base‘𝑌) ↦ (𝑦 ∈ 𝐼 ↦ ((invg‘(𝑅‘𝑦))‘(𝑥‘𝑦)))) ∈ ((TopOpen‘𝑌) Cn (∏t‘(TopOpen
∘ 𝑅)))) |
74 | 26, 73 | eqeltrd 2701 |
. . 3
⊢ (𝜑 →
(invg‘𝑌)
∈ ((TopOpen‘𝑌)
Cn (∏t‘(TopOpen ∘ 𝑅)))) |
75 | 51 | oveq2d 6666 |
. . 3
⊢ (𝜑 → ((TopOpen‘𝑌) Cn (TopOpen‘𝑌)) = ((TopOpen‘𝑌) Cn
(∏t‘(TopOpen ∘ 𝑅)))) |
76 | 74, 75 | eleqtrrd 2704 |
. 2
⊢ (𝜑 →
(invg‘𝑌)
∈ ((TopOpen‘𝑌)
Cn (TopOpen‘𝑌))) |
77 | 28, 16 | istgp 21881 |
. 2
⊢ (𝑌 ∈ TopGrp ↔ (𝑌 ∈ Grp ∧ 𝑌 ∈ TopMnd ∧
(invg‘𝑌)
∈ ((TopOpen‘𝑌)
Cn (TopOpen‘𝑌)))) |
78 | 9, 14, 76, 77 | syl3anbrc 1246 |
1
⊢ (𝜑 → 𝑌 ∈ TopGrp) |