| Step | Hyp | Ref
| Expression |
| 1 | | ressbas.r |
. 2
⊢ 𝑅 = (𝑊 ↾s 𝐴) |
| 2 | | elex 3501 |
. . 3
⊢ (𝑊 ∈ 𝑋 → 𝑊 ∈ V) |
| 3 | | elex 3501 |
. . 3
⊢ (𝐴 ∈ 𝑌 → 𝐴 ∈ V) |
| 4 | | simpl 482 |
. . . . 5
⊢ ((𝑊 ∈ V ∧ 𝐴 ∈ V) → 𝑊 ∈ V) |
| 5 | | ovex 7464 |
. . . . 5
⊢ (𝑊 sSet 〈(Base‘ndx),
(𝐴 ∩ 𝐵)〉) ∈ V |
| 6 | | ifcl 4571 |
. . . . 5
⊢ ((𝑊 ∈ V ∧ (𝑊 sSet 〈(Base‘ndx),
(𝐴 ∩ 𝐵)〉) ∈ V) → if(𝐵 ⊆ 𝐴, 𝑊, (𝑊 sSet 〈(Base‘ndx), (𝐴 ∩ 𝐵)〉)) ∈ V) |
| 7 | 4, 5, 6 | sylancl 586 |
. . . 4
⊢ ((𝑊 ∈ V ∧ 𝐴 ∈ V) → if(𝐵 ⊆ 𝐴, 𝑊, (𝑊 sSet 〈(Base‘ndx), (𝐴 ∩ 𝐵)〉)) ∈ V) |
| 8 | | simpl 482 |
. . . . . . . . 9
⊢ ((𝑤 = 𝑊 ∧ 𝑎 = 𝐴) → 𝑤 = 𝑊) |
| 9 | 8 | fveq2d 6910 |
. . . . . . . 8
⊢ ((𝑤 = 𝑊 ∧ 𝑎 = 𝐴) → (Base‘𝑤) = (Base‘𝑊)) |
| 10 | | ressbas.b |
. . . . . . . 8
⊢ 𝐵 = (Base‘𝑊) |
| 11 | 9, 10 | eqtr4di 2795 |
. . . . . . 7
⊢ ((𝑤 = 𝑊 ∧ 𝑎 = 𝐴) → (Base‘𝑤) = 𝐵) |
| 12 | | simpr 484 |
. . . . . . 7
⊢ ((𝑤 = 𝑊 ∧ 𝑎 = 𝐴) → 𝑎 = 𝐴) |
| 13 | 11, 12 | sseq12d 4017 |
. . . . . 6
⊢ ((𝑤 = 𝑊 ∧ 𝑎 = 𝐴) → ((Base‘𝑤) ⊆ 𝑎 ↔ 𝐵 ⊆ 𝐴)) |
| 14 | 12, 11 | ineq12d 4221 |
. . . . . . . 8
⊢ ((𝑤 = 𝑊 ∧ 𝑎 = 𝐴) → (𝑎 ∩ (Base‘𝑤)) = (𝐴 ∩ 𝐵)) |
| 15 | 14 | opeq2d 4880 |
. . . . . . 7
⊢ ((𝑤 = 𝑊 ∧ 𝑎 = 𝐴) → 〈(Base‘ndx), (𝑎 ∩ (Base‘𝑤))〉 =
〈(Base‘ndx), (𝐴
∩ 𝐵)〉) |
| 16 | 8, 15 | oveq12d 7449 |
. . . . . 6
⊢ ((𝑤 = 𝑊 ∧ 𝑎 = 𝐴) → (𝑤 sSet 〈(Base‘ndx), (𝑎 ∩ (Base‘𝑤))〉) = (𝑊 sSet 〈(Base‘ndx), (𝐴 ∩ 𝐵)〉)) |
| 17 | 13, 8, 16 | ifbieq12d 4554 |
. . . . 5
⊢ ((𝑤 = 𝑊 ∧ 𝑎 = 𝐴) → if((Base‘𝑤) ⊆ 𝑎, 𝑤, (𝑤 sSet 〈(Base‘ndx), (𝑎 ∩ (Base‘𝑤))〉)) = if(𝐵 ⊆ 𝐴, 𝑊, (𝑊 sSet 〈(Base‘ndx), (𝐴 ∩ 𝐵)〉))) |
| 18 | | df-ress 17275 |
. . . . 5
⊢
↾s = (𝑤
∈ V, 𝑎 ∈ V
↦ if((Base‘𝑤)
⊆ 𝑎, 𝑤, (𝑤 sSet 〈(Base‘ndx), (𝑎 ∩ (Base‘𝑤))〉))) |
| 19 | 17, 18 | ovmpoga 7587 |
. . . 4
⊢ ((𝑊 ∈ V ∧ 𝐴 ∈ V ∧ if(𝐵 ⊆ 𝐴, 𝑊, (𝑊 sSet 〈(Base‘ndx), (𝐴 ∩ 𝐵)〉)) ∈ V) → (𝑊 ↾s 𝐴) = if(𝐵 ⊆ 𝐴, 𝑊, (𝑊 sSet 〈(Base‘ndx), (𝐴 ∩ 𝐵)〉))) |
| 20 | 7, 19 | mpd3an3 1464 |
. . 3
⊢ ((𝑊 ∈ V ∧ 𝐴 ∈ V) → (𝑊 ↾s 𝐴) = if(𝐵 ⊆ 𝐴, 𝑊, (𝑊 sSet 〈(Base‘ndx), (𝐴 ∩ 𝐵)〉))) |
| 21 | 2, 3, 20 | syl2an 596 |
. 2
⊢ ((𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → (𝑊 ↾s 𝐴) = if(𝐵 ⊆ 𝐴, 𝑊, (𝑊 sSet 〈(Base‘ndx), (𝐴 ∩ 𝐵)〉))) |
| 22 | 1, 21 | eqtrid 2789 |
1
⊢ ((𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → 𝑅 = if(𝐵 ⊆ 𝐴, 𝑊, (𝑊 sSet 〈(Base‘ndx), (𝐴 ∩ 𝐵)〉))) |