| Step | Hyp | Ref
| Expression |
| 1 | | psrbas.s |
. . . . 5
⊢ 𝑆 = (𝐼 mPwSer 𝑅) |
| 2 | | psrbas.k |
. . . . 5
⊢ 𝐾 = (Base‘𝑅) |
| 3 | | eqid 2737 |
. . . . 5
⊢
(+g‘𝑅) = (+g‘𝑅) |
| 4 | | eqid 2737 |
. . . . 5
⊢
(.r‘𝑅) = (.r‘𝑅) |
| 5 | | eqid 2737 |
. . . . 5
⊢
(TopOpen‘𝑅) =
(TopOpen‘𝑅) |
| 6 | | psrbas.d |
. . . . 5
⊢ 𝐷 = {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈
Fin} |
| 7 | | eqidd 2738 |
. . . . 5
⊢ ((𝜑 ∧ 𝑅 ∈ V) → (𝐾 ↑m 𝐷) = (𝐾 ↑m 𝐷)) |
| 8 | | eqid 2737 |
. . . . 5
⊢ (
∘f (+g‘𝑅) ↾ ((𝐾 ↑m 𝐷) × (𝐾 ↑m 𝐷))) = ( ∘f
(+g‘𝑅)
↾ ((𝐾
↑m 𝐷)
× (𝐾
↑m 𝐷))) |
| 9 | | eqid 2737 |
. . . . 5
⊢ (𝑔 ∈ (𝐾 ↑m 𝐷), ℎ ∈ (𝐾 ↑m 𝐷) ↦ (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑔‘𝑥)(.r‘𝑅)(ℎ‘(𝑘 ∘f − 𝑥))))))) = (𝑔 ∈ (𝐾 ↑m 𝐷), ℎ ∈ (𝐾 ↑m 𝐷) ↦ (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑔‘𝑥)(.r‘𝑅)(ℎ‘(𝑘 ∘f − 𝑥))))))) |
| 10 | | eqid 2737 |
. . . . 5
⊢ (𝑥 ∈ 𝐾, 𝑔 ∈ (𝐾 ↑m 𝐷) ↦ ((𝐷 × {𝑥}) ∘f
(.r‘𝑅)𝑔)) = (𝑥 ∈ 𝐾, 𝑔 ∈ (𝐾 ↑m 𝐷) ↦ ((𝐷 × {𝑥}) ∘f
(.r‘𝑅)𝑔)) |
| 11 | | eqidd 2738 |
. . . . 5
⊢ ((𝜑 ∧ 𝑅 ∈ V) →
(∏t‘(𝐷 × {(TopOpen‘𝑅)})) = (∏t‘(𝐷 × {(TopOpen‘𝑅)}))) |
| 12 | | psrbas.i |
. . . . . 6
⊢ (𝜑 → 𝐼 ∈ 𝑉) |
| 13 | 12 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑅 ∈ V) → 𝐼 ∈ 𝑉) |
| 14 | | simpr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑅 ∈ V) → 𝑅 ∈ V) |
| 15 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 13, 14 | psrval 21935 |
. . . 4
⊢ ((𝜑 ∧ 𝑅 ∈ V) → 𝑆 = ({〈(Base‘ndx), (𝐾 ↑m 𝐷)〉,
〈(+g‘ndx), ( ∘f
(+g‘𝑅)
↾ ((𝐾
↑m 𝐷)
× (𝐾
↑m 𝐷)))〉, 〈(.r‘ndx),
(𝑔 ∈ (𝐾 ↑m 𝐷), ℎ ∈ (𝐾 ↑m 𝐷) ↦ (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑔‘𝑥)(.r‘𝑅)(ℎ‘(𝑘 ∘f − 𝑥)))))))〉} ∪
{〈(Scalar‘ndx), 𝑅〉, 〈(
·𝑠 ‘ndx), (𝑥 ∈ 𝐾, 𝑔 ∈ (𝐾 ↑m 𝐷) ↦ ((𝐷 × {𝑥}) ∘f
(.r‘𝑅)𝑔))〉, 〈(TopSet‘ndx),
(∏t‘(𝐷 × {(TopOpen‘𝑅)}))〉})) |
| 16 | 15 | fveq2d 6910 |
. . 3
⊢ ((𝜑 ∧ 𝑅 ∈ V) → (Base‘𝑆) =
(Base‘({〈(Base‘ndx), (𝐾 ↑m 𝐷)〉, 〈(+g‘ndx), (
∘f (+g‘𝑅) ↾ ((𝐾 ↑m 𝐷) × (𝐾 ↑m 𝐷)))〉, 〈(.r‘ndx),
(𝑔 ∈ (𝐾 ↑m 𝐷), ℎ ∈ (𝐾 ↑m 𝐷) ↦ (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑔‘𝑥)(.r‘𝑅)(ℎ‘(𝑘 ∘f − 𝑥)))))))〉} ∪
{〈(Scalar‘ndx), 𝑅〉, 〈(
·𝑠 ‘ndx), (𝑥 ∈ 𝐾, 𝑔 ∈ (𝐾 ↑m 𝐷) ↦ ((𝐷 × {𝑥}) ∘f
(.r‘𝑅)𝑔))〉, 〈(TopSet‘ndx),
(∏t‘(𝐷 × {(TopOpen‘𝑅)}))〉}))) |
| 17 | | psrbas.b |
. . 3
⊢ 𝐵 = (Base‘𝑆) |
| 18 | | ovex 7464 |
. . . 4
⊢ (𝐾 ↑m 𝐷) ∈ V |
| 19 | | psrvalstr 21936 |
. . . . 5
⊢
({〈(Base‘ndx), (𝐾 ↑m 𝐷)〉, 〈(+g‘ndx), (
∘f (+g‘𝑅) ↾ ((𝐾 ↑m 𝐷) × (𝐾 ↑m 𝐷)))〉, 〈(.r‘ndx),
(𝑔 ∈ (𝐾 ↑m 𝐷), ℎ ∈ (𝐾 ↑m 𝐷) ↦ (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑔‘𝑥)(.r‘𝑅)(ℎ‘(𝑘 ∘f − 𝑥)))))))〉} ∪
{〈(Scalar‘ndx), 𝑅〉, 〈(
·𝑠 ‘ndx), (𝑥 ∈ 𝐾, 𝑔 ∈ (𝐾 ↑m 𝐷) ↦ ((𝐷 × {𝑥}) ∘f
(.r‘𝑅)𝑔))〉, 〈(TopSet‘ndx),
(∏t‘(𝐷 × {(TopOpen‘𝑅)}))〉}) Struct 〈1,
9〉 |
| 20 | | baseid 17250 |
. . . . 5
⊢ Base =
Slot (Base‘ndx) |
| 21 | | snsstp1 4816 |
. . . . . 6
⊢
{〈(Base‘ndx), (𝐾 ↑m 𝐷)〉} ⊆ {〈(Base‘ndx),
(𝐾 ↑m 𝐷)〉,
〈(+g‘ndx), ( ∘f
(+g‘𝑅)
↾ ((𝐾
↑m 𝐷)
× (𝐾
↑m 𝐷)))〉, 〈(.r‘ndx),
(𝑔 ∈ (𝐾 ↑m 𝐷), ℎ ∈ (𝐾 ↑m 𝐷) ↦ (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑔‘𝑥)(.r‘𝑅)(ℎ‘(𝑘 ∘f − 𝑥)))))))〉} |
| 22 | | ssun1 4178 |
. . . . . 6
⊢
{〈(Base‘ndx), (𝐾 ↑m 𝐷)〉, 〈(+g‘ndx), (
∘f (+g‘𝑅) ↾ ((𝐾 ↑m 𝐷) × (𝐾 ↑m 𝐷)))〉, 〈(.r‘ndx),
(𝑔 ∈ (𝐾 ↑m 𝐷), ℎ ∈ (𝐾 ↑m 𝐷) ↦ (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑔‘𝑥)(.r‘𝑅)(ℎ‘(𝑘 ∘f − 𝑥)))))))〉} ⊆
({〈(Base‘ndx), (𝐾 ↑m 𝐷)〉, 〈(+g‘ndx), (
∘f (+g‘𝑅) ↾ ((𝐾 ↑m 𝐷) × (𝐾 ↑m 𝐷)))〉, 〈(.r‘ndx),
(𝑔 ∈ (𝐾 ↑m 𝐷), ℎ ∈ (𝐾 ↑m 𝐷) ↦ (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑔‘𝑥)(.r‘𝑅)(ℎ‘(𝑘 ∘f − 𝑥)))))))〉} ∪
{〈(Scalar‘ndx), 𝑅〉, 〈(
·𝑠 ‘ndx), (𝑥 ∈ 𝐾, 𝑔 ∈ (𝐾 ↑m 𝐷) ↦ ((𝐷 × {𝑥}) ∘f
(.r‘𝑅)𝑔))〉, 〈(TopSet‘ndx),
(∏t‘(𝐷 × {(TopOpen‘𝑅)}))〉}) |
| 23 | 21, 22 | sstri 3993 |
. . . . 5
⊢
{〈(Base‘ndx), (𝐾 ↑m 𝐷)〉} ⊆ ({〈(Base‘ndx),
(𝐾 ↑m 𝐷)〉,
〈(+g‘ndx), ( ∘f
(+g‘𝑅)
↾ ((𝐾
↑m 𝐷)
× (𝐾
↑m 𝐷)))〉, 〈(.r‘ndx),
(𝑔 ∈ (𝐾 ↑m 𝐷), ℎ ∈ (𝐾 ↑m 𝐷) ↦ (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑔‘𝑥)(.r‘𝑅)(ℎ‘(𝑘 ∘f − 𝑥)))))))〉} ∪
{〈(Scalar‘ndx), 𝑅〉, 〈(
·𝑠 ‘ndx), (𝑥 ∈ 𝐾, 𝑔 ∈ (𝐾 ↑m 𝐷) ↦ ((𝐷 × {𝑥}) ∘f
(.r‘𝑅)𝑔))〉, 〈(TopSet‘ndx),
(∏t‘(𝐷 × {(TopOpen‘𝑅)}))〉}) |
| 24 | 19, 20, 23 | strfv 17240 |
. . . 4
⊢ ((𝐾 ↑m 𝐷) ∈ V → (𝐾 ↑m 𝐷) =
(Base‘({〈(Base‘ndx), (𝐾 ↑m 𝐷)〉, 〈(+g‘ndx), (
∘f (+g‘𝑅) ↾ ((𝐾 ↑m 𝐷) × (𝐾 ↑m 𝐷)))〉, 〈(.r‘ndx),
(𝑔 ∈ (𝐾 ↑m 𝐷), ℎ ∈ (𝐾 ↑m 𝐷) ↦ (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑔‘𝑥)(.r‘𝑅)(ℎ‘(𝑘 ∘f − 𝑥)))))))〉} ∪
{〈(Scalar‘ndx), 𝑅〉, 〈(
·𝑠 ‘ndx), (𝑥 ∈ 𝐾, 𝑔 ∈ (𝐾 ↑m 𝐷) ↦ ((𝐷 × {𝑥}) ∘f
(.r‘𝑅)𝑔))〉, 〈(TopSet‘ndx),
(∏t‘(𝐷 × {(TopOpen‘𝑅)}))〉}))) |
| 25 | 18, 24 | ax-mp 5 |
. . 3
⊢ (𝐾 ↑m 𝐷) =
(Base‘({〈(Base‘ndx), (𝐾 ↑m 𝐷)〉, 〈(+g‘ndx), (
∘f (+g‘𝑅) ↾ ((𝐾 ↑m 𝐷) × (𝐾 ↑m 𝐷)))〉, 〈(.r‘ndx),
(𝑔 ∈ (𝐾 ↑m 𝐷), ℎ ∈ (𝐾 ↑m 𝐷) ↦ (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑔‘𝑥)(.r‘𝑅)(ℎ‘(𝑘 ∘f − 𝑥)))))))〉} ∪
{〈(Scalar‘ndx), 𝑅〉, 〈(
·𝑠 ‘ndx), (𝑥 ∈ 𝐾, 𝑔 ∈ (𝐾 ↑m 𝐷) ↦ ((𝐷 × {𝑥}) ∘f
(.r‘𝑅)𝑔))〉, 〈(TopSet‘ndx),
(∏t‘(𝐷 × {(TopOpen‘𝑅)}))〉})) |
| 26 | 16, 17, 25 | 3eqtr4g 2802 |
. 2
⊢ ((𝜑 ∧ 𝑅 ∈ V) → 𝐵 = (𝐾 ↑m 𝐷)) |
| 27 | | reldmpsr 21934 |
. . . . . . . 8
⊢ Rel dom
mPwSer |
| 28 | 27 | ovprc2 7471 |
. . . . . . 7
⊢ (¬
𝑅 ∈ V → (𝐼 mPwSer 𝑅) = ∅) |
| 29 | 28 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝑅 ∈ V) → (𝐼 mPwSer 𝑅) = ∅) |
| 30 | 1, 29 | eqtrid 2789 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝑅 ∈ V) → 𝑆 = ∅) |
| 31 | 30 | fveq2d 6910 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝑅 ∈ V) → (Base‘𝑆) =
(Base‘∅)) |
| 32 | | base0 17252 |
. . . 4
⊢ ∅ =
(Base‘∅) |
| 33 | 31, 17, 32 | 3eqtr4g 2802 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝑅 ∈ V) → 𝐵 = ∅) |
| 34 | | fvprc 6898 |
. . . . . 6
⊢ (¬
𝑅 ∈ V →
(Base‘𝑅) =
∅) |
| 35 | 34 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝑅 ∈ V) → (Base‘𝑅) = ∅) |
| 36 | 2, 35 | eqtrid 2789 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝑅 ∈ V) → 𝐾 = ∅) |
| 37 | 6 | fczpsrbag 21941 |
. . . . . . 7
⊢ (𝐼 ∈ 𝑉 → (𝑥 ∈ 𝐼 ↦ 0) ∈ 𝐷) |
| 38 | 12, 37 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ 0) ∈ 𝐷) |
| 39 | 38 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝑅 ∈ V) → (𝑥 ∈ 𝐼 ↦ 0) ∈ 𝐷) |
| 40 | 39 | ne0d 4342 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝑅 ∈ V) → 𝐷 ≠ ∅) |
| 41 | 2 | fvexi 6920 |
. . . . 5
⊢ 𝐾 ∈ V |
| 42 | | ovex 7464 |
. . . . . 6
⊢
(ℕ0 ↑m 𝐼) ∈ V |
| 43 | 6, 42 | rabex2 5341 |
. . . . 5
⊢ 𝐷 ∈ V |
| 44 | 41, 43 | map0 8927 |
. . . 4
⊢ ((𝐾 ↑m 𝐷) = ∅ ↔ (𝐾 = ∅ ∧ 𝐷 ≠ ∅)) |
| 45 | 36, 40, 44 | sylanbrc 583 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝑅 ∈ V) → (𝐾 ↑m 𝐷) = ∅) |
| 46 | 33, 45 | eqtr4d 2780 |
. 2
⊢ ((𝜑 ∧ ¬ 𝑅 ∈ V) → 𝐵 = (𝐾 ↑m 𝐷)) |
| 47 | 26, 46 | pm2.61dan 813 |
1
⊢ (𝜑 → 𝐵 = (𝐾 ↑m 𝐷)) |