Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . 3
⊢
(Base‘(𝑆
⊕m 𝑅)) =
(Base‘(𝑆
⊕m 𝑅)) |
2 | 1 | dsmmval2 21158 |
. 2
⊢ (𝑆 ⊕m 𝑅) = ((𝑆Xs𝑅) ↾s (Base‘(𝑆 ⊕m 𝑅))) |
3 | | eqid 2733 |
. . . . . . . . . . 11
⊢ (𝑆Xs𝑅) = (𝑆Xs𝑅) |
4 | | eqid 2733 |
. . . . . . . . . . 11
⊢
(Base‘(𝑆Xs𝑅)) = (Base‘(𝑆Xs𝑅)) |
5 | | noel 4291 |
. . . . . . . . . . . . . 14
⊢ ¬
𝑓 ∈
∅ |
6 | | reldmprds 17335 |
. . . . . . . . . . . . . . . . . 18
⊢ Rel dom
Xs |
7 | 6 | ovprc1 7397 |
. . . . . . . . . . . . . . . . 17
⊢ (¬
𝑆 ∈ V → (𝑆Xs𝑅) = ∅) |
8 | 7 | fveq2d 6847 |
. . . . . . . . . . . . . . . 16
⊢ (¬
𝑆 ∈ V →
(Base‘(𝑆Xs𝑅)) = (Base‘∅)) |
9 | | base0 17093 |
. . . . . . . . . . . . . . . 16
⊢ ∅ =
(Base‘∅) |
10 | 8, 9 | eqtr4di 2791 |
. . . . . . . . . . . . . . 15
⊢ (¬
𝑆 ∈ V →
(Base‘(𝑆Xs𝑅)) = ∅) |
11 | 10 | eleq2d 2820 |
. . . . . . . . . . . . . 14
⊢ (¬
𝑆 ∈ V → (𝑓 ∈ (Base‘(𝑆Xs𝑅)) ↔ 𝑓 ∈ ∅)) |
12 | 5, 11 | mtbiri 327 |
. . . . . . . . . . . . 13
⊢ (¬
𝑆 ∈ V → ¬
𝑓 ∈ (Base‘(𝑆Xs𝑅))) |
13 | 12 | con4i 114 |
. . . . . . . . . . . 12
⊢ (𝑓 ∈ (Base‘(𝑆Xs𝑅)) → 𝑆 ∈ V) |
14 | 13 | adantl 483 |
. . . . . . . . . . 11
⊢ (((𝑅 Fn 𝐼 ∧ 𝐼 ∈ Fin) ∧ 𝑓 ∈ (Base‘(𝑆Xs𝑅))) → 𝑆 ∈ V) |
15 | | simplr 768 |
. . . . . . . . . . 11
⊢ (((𝑅 Fn 𝐼 ∧ 𝐼 ∈ Fin) ∧ 𝑓 ∈ (Base‘(𝑆Xs𝑅))) → 𝐼 ∈ Fin) |
16 | | simpll 766 |
. . . . . . . . . . 11
⊢ (((𝑅 Fn 𝐼 ∧ 𝐼 ∈ Fin) ∧ 𝑓 ∈ (Base‘(𝑆Xs𝑅))) → 𝑅 Fn 𝐼) |
17 | | simpr 486 |
. . . . . . . . . . 11
⊢ (((𝑅 Fn 𝐼 ∧ 𝐼 ∈ Fin) ∧ 𝑓 ∈ (Base‘(𝑆Xs𝑅))) → 𝑓 ∈ (Base‘(𝑆Xs𝑅))) |
18 | 3, 4, 14, 15, 16, 17 | prdsbasfn 17358 |
. . . . . . . . . 10
⊢ (((𝑅 Fn 𝐼 ∧ 𝐼 ∈ Fin) ∧ 𝑓 ∈ (Base‘(𝑆Xs𝑅))) → 𝑓 Fn 𝐼) |
19 | 18 | fndmd 6608 |
. . . . . . . . 9
⊢ (((𝑅 Fn 𝐼 ∧ 𝐼 ∈ Fin) ∧ 𝑓 ∈ (Base‘(𝑆Xs𝑅))) → dom 𝑓 = 𝐼) |
20 | 19, 15 | eqeltrd 2834 |
. . . . . . . 8
⊢ (((𝑅 Fn 𝐼 ∧ 𝐼 ∈ Fin) ∧ 𝑓 ∈ (Base‘(𝑆Xs𝑅))) → dom 𝑓 ∈ Fin) |
21 | | difss 4092 |
. . . . . . . . 9
⊢ (𝑓 ∖ (0g ∘
𝑅)) ⊆ 𝑓 |
22 | | dmss 5859 |
. . . . . . . . 9
⊢ ((𝑓 ∖ (0g ∘
𝑅)) ⊆ 𝑓 → dom (𝑓 ∖ (0g ∘ 𝑅)) ⊆ dom 𝑓) |
23 | 21, 22 | ax-mp 5 |
. . . . . . . 8
⊢ dom
(𝑓 ∖ (0g
∘ 𝑅)) ⊆ dom
𝑓 |
24 | | ssfi 9120 |
. . . . . . . 8
⊢ ((dom
𝑓 ∈ Fin ∧ dom
(𝑓 ∖ (0g
∘ 𝑅)) ⊆ dom
𝑓) → dom (𝑓 ∖ (0g ∘
𝑅)) ∈
Fin) |
25 | 20, 23, 24 | sylancl 587 |
. . . . . . 7
⊢ (((𝑅 Fn 𝐼 ∧ 𝐼 ∈ Fin) ∧ 𝑓 ∈ (Base‘(𝑆Xs𝑅))) → dom (𝑓 ∖ (0g ∘ 𝑅)) ∈ Fin) |
26 | 25 | ralrimiva 3140 |
. . . . . 6
⊢ ((𝑅 Fn 𝐼 ∧ 𝐼 ∈ Fin) → ∀𝑓 ∈ (Base‘(𝑆Xs𝑅))dom (𝑓 ∖ (0g ∘ 𝑅)) ∈ Fin) |
27 | | rabid2 3435 |
. . . . . 6
⊢
((Base‘(𝑆Xs𝑅)) = {𝑓 ∈ (Base‘(𝑆Xs𝑅)) ∣ dom (𝑓 ∖ (0g ∘ 𝑅)) ∈ Fin} ↔
∀𝑓 ∈
(Base‘(𝑆Xs𝑅))dom (𝑓 ∖ (0g ∘ 𝑅)) ∈ Fin) |
28 | 26, 27 | sylibr 233 |
. . . . 5
⊢ ((𝑅 Fn 𝐼 ∧ 𝐼 ∈ Fin) → (Base‘(𝑆Xs𝑅)) = {𝑓 ∈ (Base‘(𝑆Xs𝑅)) ∣ dom (𝑓 ∖ (0g ∘ 𝑅)) ∈ Fin}) |
29 | | eqid 2733 |
. . . . . 6
⊢ {𝑓 ∈ (Base‘(𝑆Xs𝑅)) ∣ dom (𝑓 ∖ (0g ∘ 𝑅)) ∈ Fin} = {𝑓 ∈ (Base‘(𝑆Xs𝑅)) ∣ dom (𝑓 ∖ (0g ∘ 𝑅)) ∈ Fin} |
30 | 3, 29 | dsmmbas2 21159 |
. . . . 5
⊢ ((𝑅 Fn 𝐼 ∧ 𝐼 ∈ Fin) → {𝑓 ∈ (Base‘(𝑆Xs𝑅)) ∣ dom (𝑓 ∖ (0g ∘ 𝑅)) ∈ Fin} =
(Base‘(𝑆
⊕m 𝑅))) |
31 | 28, 30 | eqtr2d 2774 |
. . . 4
⊢ ((𝑅 Fn 𝐼 ∧ 𝐼 ∈ Fin) → (Base‘(𝑆 ⊕m 𝑅)) = (Base‘(𝑆Xs𝑅))) |
32 | 31 | oveq2d 7374 |
. . 3
⊢ ((𝑅 Fn 𝐼 ∧ 𝐼 ∈ Fin) → ((𝑆Xs𝑅) ↾s (Base‘(𝑆 ⊕m 𝑅))) = ((𝑆Xs𝑅) ↾s (Base‘(𝑆Xs𝑅)))) |
33 | | ovex 7391 |
. . . 4
⊢ (𝑆Xs𝑅) ∈ V |
34 | 4 | ressid 17130 |
. . . 4
⊢ ((𝑆Xs𝑅) ∈ V → ((𝑆Xs𝑅) ↾s (Base‘(𝑆Xs𝑅))) = (𝑆Xs𝑅)) |
35 | 33, 34 | ax-mp 5 |
. . 3
⊢ ((𝑆Xs𝑅) ↾s (Base‘(𝑆Xs𝑅))) = (𝑆Xs𝑅) |
36 | 32, 35 | eqtrdi 2789 |
. 2
⊢ ((𝑅 Fn 𝐼 ∧ 𝐼 ∈ Fin) → ((𝑆Xs𝑅) ↾s (Base‘(𝑆 ⊕m 𝑅))) = (𝑆Xs𝑅)) |
37 | 2, 36 | eqtrid 2785 |
1
⊢ ((𝑅 Fn 𝐼 ∧ 𝐼 ∈ Fin) → (𝑆 ⊕m 𝑅) = (𝑆Xs𝑅)) |