Step | Hyp | Ref
| Expression |
1 | | ressbas.r |
. 2
⊢ 𝑅 = (𝑊 ↾s 𝐴) |
2 | | elex 3426 |
. . 3
⊢ (𝑊 ∈ 𝑋 → 𝑊 ∈ V) |
3 | | elex 3426 |
. . 3
⊢ (𝐴 ∈ 𝑌 → 𝐴 ∈ V) |
4 | | simpl 486 |
. . . . 5
⊢ ((𝑊 ∈ V ∧ 𝐴 ∈ V) → 𝑊 ∈ V) |
5 | | ovex 7246 |
. . . . 5
⊢ (𝑊 sSet 〈(Base‘ndx),
(𝐴 ∩ 𝐵)〉) ∈ V |
6 | | ifcl 4484 |
. . . . 5
⊢ ((𝑊 ∈ V ∧ (𝑊 sSet 〈(Base‘ndx),
(𝐴 ∩ 𝐵)〉) ∈ V) → if(𝐵 ⊆ 𝐴, 𝑊, (𝑊 sSet 〈(Base‘ndx), (𝐴 ∩ 𝐵)〉)) ∈ V) |
7 | 4, 5, 6 | sylancl 589 |
. . . 4
⊢ ((𝑊 ∈ V ∧ 𝐴 ∈ V) → if(𝐵 ⊆ 𝐴, 𝑊, (𝑊 sSet 〈(Base‘ndx), (𝐴 ∩ 𝐵)〉)) ∈ V) |
8 | | simpl 486 |
. . . . . . . . 9
⊢ ((𝑤 = 𝑊 ∧ 𝑎 = 𝐴) → 𝑤 = 𝑊) |
9 | 8 | fveq2d 6721 |
. . . . . . . 8
⊢ ((𝑤 = 𝑊 ∧ 𝑎 = 𝐴) → (Base‘𝑤) = (Base‘𝑊)) |
10 | | ressbas.b |
. . . . . . . 8
⊢ 𝐵 = (Base‘𝑊) |
11 | 9, 10 | eqtr4di 2796 |
. . . . . . 7
⊢ ((𝑤 = 𝑊 ∧ 𝑎 = 𝐴) → (Base‘𝑤) = 𝐵) |
12 | | simpr 488 |
. . . . . . 7
⊢ ((𝑤 = 𝑊 ∧ 𝑎 = 𝐴) → 𝑎 = 𝐴) |
13 | 11, 12 | sseq12d 3934 |
. . . . . 6
⊢ ((𝑤 = 𝑊 ∧ 𝑎 = 𝐴) → ((Base‘𝑤) ⊆ 𝑎 ↔ 𝐵 ⊆ 𝐴)) |
14 | 12, 11 | ineq12d 4128 |
. . . . . . . 8
⊢ ((𝑤 = 𝑊 ∧ 𝑎 = 𝐴) → (𝑎 ∩ (Base‘𝑤)) = (𝐴 ∩ 𝐵)) |
15 | 14 | opeq2d 4791 |
. . . . . . 7
⊢ ((𝑤 = 𝑊 ∧ 𝑎 = 𝐴) → 〈(Base‘ndx), (𝑎 ∩ (Base‘𝑤))〉 =
〈(Base‘ndx), (𝐴
∩ 𝐵)〉) |
16 | 8, 15 | oveq12d 7231 |
. . . . . 6
⊢ ((𝑤 = 𝑊 ∧ 𝑎 = 𝐴) → (𝑤 sSet 〈(Base‘ndx), (𝑎 ∩ (Base‘𝑤))〉) = (𝑊 sSet 〈(Base‘ndx), (𝐴 ∩ 𝐵)〉)) |
17 | 13, 8, 16 | ifbieq12d 4467 |
. . . . 5
⊢ ((𝑤 = 𝑊 ∧ 𝑎 = 𝐴) → if((Base‘𝑤) ⊆ 𝑎, 𝑤, (𝑤 sSet 〈(Base‘ndx), (𝑎 ∩ (Base‘𝑤))〉)) = if(𝐵 ⊆ 𝐴, 𝑊, (𝑊 sSet 〈(Base‘ndx), (𝐴 ∩ 𝐵)〉))) |
18 | | df-ress 16785 |
. . . . 5
⊢
↾s = (𝑤
∈ V, 𝑎 ∈ V
↦ if((Base‘𝑤)
⊆ 𝑎, 𝑤, (𝑤 sSet 〈(Base‘ndx), (𝑎 ∩ (Base‘𝑤))〉))) |
19 | 17, 18 | ovmpoga 7363 |
. . . 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 599 |
. 2
⊢ ((𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → (𝑊 ↾s 𝐴) = if(𝐵 ⊆ 𝐴, 𝑊, (𝑊 sSet 〈(Base‘ndx), (𝐴 ∩ 𝐵)〉))) |
22 | 1, 21 | syl5eq 2790 |
1
⊢ ((𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → 𝑅 = if(𝐵 ⊆ 𝐴, 𝑊, (𝑊 sSet 〈(Base‘ndx), (𝐴 ∩ 𝐵)〉))) |