Step | Hyp | Ref
| Expression |
1 | | ressbas.r |
. 2
⊢ 𝑅 = (𝑊 ↾s 𝐴) |
2 | | simp2 983 |
. . . . 5
⊢ ((𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → 𝑊 ∈ 𝑋) |
3 | 2 | elexd 2725 |
. . . 4
⊢ ((𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → 𝑊 ∈ V) |
4 | | simp3 984 |
. . . . 5
⊢ ((𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → 𝐴 ∈ 𝑌) |
5 | 4 | elexd 2725 |
. . . 4
⊢ ((𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → 𝐴 ∈ V) |
6 | | simp1 982 |
. . . . . 6
⊢ ((𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → 𝐵 ⊆ 𝐴) |
7 | 6 | iftrued 3513 |
. . . . 5
⊢ ((𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → if(𝐵 ⊆ 𝐴, 𝑊, (𝑊 sSet 〈(Base‘ndx), (𝐴 ∩ 𝐵)〉)) = 𝑊) |
8 | 7, 3 | eqeltrd 2234 |
. . . 4
⊢ ((𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → if(𝐵 ⊆ 𝐴, 𝑊, (𝑊 sSet 〈(Base‘ndx), (𝐴 ∩ 𝐵)〉)) ∈ V) |
9 | | simpl 108 |
. . . . . . . . 9
⊢ ((𝑤 = 𝑊 ∧ 𝑎 = 𝐴) → 𝑤 = 𝑊) |
10 | 9 | fveq2d 5475 |
. . . . . . . 8
⊢ ((𝑤 = 𝑊 ∧ 𝑎 = 𝐴) → (Base‘𝑤) = (Base‘𝑊)) |
11 | | ressbas.b |
. . . . . . . 8
⊢ 𝐵 = (Base‘𝑊) |
12 | 10, 11 | eqtr4di 2208 |
. . . . . . 7
⊢ ((𝑤 = 𝑊 ∧ 𝑎 = 𝐴) → (Base‘𝑤) = 𝐵) |
13 | | simpr 109 |
. . . . . . 7
⊢ ((𝑤 = 𝑊 ∧ 𝑎 = 𝐴) → 𝑎 = 𝐴) |
14 | 12, 13 | sseq12d 3159 |
. . . . . 6
⊢ ((𝑤 = 𝑊 ∧ 𝑎 = 𝐴) → ((Base‘𝑤) ⊆ 𝑎 ↔ 𝐵 ⊆ 𝐴)) |
15 | 13, 12 | ineq12d 3310 |
. . . . . . . 8
⊢ ((𝑤 = 𝑊 ∧ 𝑎 = 𝐴) → (𝑎 ∩ (Base‘𝑤)) = (𝐴 ∩ 𝐵)) |
16 | 15 | opeq2d 3750 |
. . . . . . 7
⊢ ((𝑤 = 𝑊 ∧ 𝑎 = 𝐴) → 〈(Base‘ndx), (𝑎 ∩ (Base‘𝑤))〉 =
〈(Base‘ndx), (𝐴
∩ 𝐵)〉) |
17 | 9, 16 | oveq12d 5845 |
. . . . . 6
⊢ ((𝑤 = 𝑊 ∧ 𝑎 = 𝐴) → (𝑤 sSet 〈(Base‘ndx), (𝑎 ∩ (Base‘𝑤))〉) = (𝑊 sSet 〈(Base‘ndx), (𝐴 ∩ 𝐵)〉)) |
18 | 14, 9, 17 | ifbieq12d 3532 |
. . . . 5
⊢ ((𝑤 = 𝑊 ∧ 𝑎 = 𝐴) → if((Base‘𝑤) ⊆ 𝑎, 𝑤, (𝑤 sSet 〈(Base‘ndx), (𝑎 ∩ (Base‘𝑤))〉)) = if(𝐵 ⊆ 𝐴, 𝑊, (𝑊 sSet 〈(Base‘ndx), (𝐴 ∩ 𝐵)〉))) |
19 | | df-ress 12294 |
. . . . 5
⊢
↾s = (𝑤
∈ V, 𝑎 ∈ V
↦ if((Base‘𝑤)
⊆ 𝑎, 𝑤, (𝑤 sSet 〈(Base‘ndx), (𝑎 ∩ (Base‘𝑤))〉))) |
20 | 18, 19 | ovmpoga 5953 |
. . . 4
⊢ ((𝑊 ∈ V ∧ 𝐴 ∈ V ∧ if(𝐵 ⊆ 𝐴, 𝑊, (𝑊 sSet 〈(Base‘ndx), (𝐴 ∩ 𝐵)〉)) ∈ V) → (𝑊 ↾s 𝐴) = if(𝐵 ⊆ 𝐴, 𝑊, (𝑊 sSet 〈(Base‘ndx), (𝐴 ∩ 𝐵)〉))) |
21 | 3, 5, 8, 20 | syl3anc 1220 |
. . 3
⊢ ((𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → (𝑊 ↾s 𝐴) = if(𝐵 ⊆ 𝐴, 𝑊, (𝑊 sSet 〈(Base‘ndx), (𝐴 ∩ 𝐵)〉))) |
22 | 21, 7 | eqtrd 2190 |
. 2
⊢ ((𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → (𝑊 ↾s 𝐴) = 𝑊) |
23 | 1, 22 | syl5eq 2202 |
1
⊢ ((𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → 𝑅 = 𝑊) |