Proof of Theorem ressinbas
| Step | Hyp | Ref
| Expression |
| 1 | | elex 3501 |
. 2
⊢ (𝐴 ∈ 𝑋 → 𝐴 ∈ V) |
| 2 | | eqid 2737 |
. . . . . . 7
⊢ (𝑊 ↾s 𝐴) = (𝑊 ↾s 𝐴) |
| 3 | | ressid.1 |
. . . . . . 7
⊢ 𝐵 = (Base‘𝑊) |
| 4 | 2, 3 | ressid2 17278 |
. . . . . 6
⊢ ((𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ V) → (𝑊 ↾s 𝐴) = 𝑊) |
| 5 | | ssid 4006 |
. . . . . . . 8
⊢ 𝐵 ⊆ 𝐵 |
| 6 | | incom 4209 |
. . . . . . . . 9
⊢ (𝐴 ∩ 𝐵) = (𝐵 ∩ 𝐴) |
| 7 | | dfss2 3969 |
. . . . . . . . . 10
⊢ (𝐵 ⊆ 𝐴 ↔ (𝐵 ∩ 𝐴) = 𝐵) |
| 8 | 7 | biimpi 216 |
. . . . . . . . 9
⊢ (𝐵 ⊆ 𝐴 → (𝐵 ∩ 𝐴) = 𝐵) |
| 9 | 6, 8 | eqtrid 2789 |
. . . . . . . 8
⊢ (𝐵 ⊆ 𝐴 → (𝐴 ∩ 𝐵) = 𝐵) |
| 10 | 5, 9 | sseqtrrid 4027 |
. . . . . . 7
⊢ (𝐵 ⊆ 𝐴 → 𝐵 ⊆ (𝐴 ∩ 𝐵)) |
| 11 | | elex 3501 |
. . . . . . 7
⊢ (𝑊 ∈ V → 𝑊 ∈ V) |
| 12 | | inex1g 5319 |
. . . . . . 7
⊢ (𝐴 ∈ V → (𝐴 ∩ 𝐵) ∈ V) |
| 13 | | eqid 2737 |
. . . . . . . 8
⊢ (𝑊 ↾s (𝐴 ∩ 𝐵)) = (𝑊 ↾s (𝐴 ∩ 𝐵)) |
| 14 | 13, 3 | ressid2 17278 |
. . . . . . 7
⊢ ((𝐵 ⊆ (𝐴 ∩ 𝐵) ∧ 𝑊 ∈ V ∧ (𝐴 ∩ 𝐵) ∈ V) → (𝑊 ↾s (𝐴 ∩ 𝐵)) = 𝑊) |
| 15 | 10, 11, 12, 14 | syl3an 1161 |
. . . . . 6
⊢ ((𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ V) → (𝑊 ↾s (𝐴 ∩ 𝐵)) = 𝑊) |
| 16 | 4, 15 | eqtr4d 2780 |
. . . . 5
⊢ ((𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ V) → (𝑊 ↾s 𝐴) = (𝑊 ↾s (𝐴 ∩ 𝐵))) |
| 17 | 16 | 3expb 1121 |
. . . 4
⊢ ((𝐵 ⊆ 𝐴 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ V)) → (𝑊 ↾s 𝐴) = (𝑊 ↾s (𝐴 ∩ 𝐵))) |
| 18 | | inass 4228 |
. . . . . . . . 9
⊢ ((𝐴 ∩ 𝐵) ∩ 𝐵) = (𝐴 ∩ (𝐵 ∩ 𝐵)) |
| 19 | | inidm 4227 |
. . . . . . . . . 10
⊢ (𝐵 ∩ 𝐵) = 𝐵 |
| 20 | 19 | ineq2i 4217 |
. . . . . . . . 9
⊢ (𝐴 ∩ (𝐵 ∩ 𝐵)) = (𝐴 ∩ 𝐵) |
| 21 | 18, 20 | eqtr2i 2766 |
. . . . . . . 8
⊢ (𝐴 ∩ 𝐵) = ((𝐴 ∩ 𝐵) ∩ 𝐵) |
| 22 | 21 | opeq2i 4877 |
. . . . . . 7
⊢
〈(Base‘ndx), (𝐴 ∩ 𝐵)〉 = 〈(Base‘ndx), ((𝐴 ∩ 𝐵) ∩ 𝐵)〉 |
| 23 | 22 | oveq2i 7442 |
. . . . . 6
⊢ (𝑊 sSet 〈(Base‘ndx),
(𝐴 ∩ 𝐵)〉) = (𝑊 sSet 〈(Base‘ndx), ((𝐴 ∩ 𝐵) ∩ 𝐵)〉) |
| 24 | 2, 3 | ressval2 17279 |
. . . . . 6
⊢ ((¬
𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ V) → (𝑊 ↾s 𝐴) = (𝑊 sSet 〈(Base‘ndx), (𝐴 ∩ 𝐵)〉)) |
| 25 | | inss1 4237 |
. . . . . . . . 9
⊢ (𝐴 ∩ 𝐵) ⊆ 𝐴 |
| 26 | | sstr 3992 |
. . . . . . . . 9
⊢ ((𝐵 ⊆ (𝐴 ∩ 𝐵) ∧ (𝐴 ∩ 𝐵) ⊆ 𝐴) → 𝐵 ⊆ 𝐴) |
| 27 | 25, 26 | mpan2 691 |
. . . . . . . 8
⊢ (𝐵 ⊆ (𝐴 ∩ 𝐵) → 𝐵 ⊆ 𝐴) |
| 28 | 27 | con3i 154 |
. . . . . . 7
⊢ (¬
𝐵 ⊆ 𝐴 → ¬ 𝐵 ⊆ (𝐴 ∩ 𝐵)) |
| 29 | 13, 3 | ressval2 17279 |
. . . . . . 7
⊢ ((¬
𝐵 ⊆ (𝐴 ∩ 𝐵) ∧ 𝑊 ∈ V ∧ (𝐴 ∩ 𝐵) ∈ V) → (𝑊 ↾s (𝐴 ∩ 𝐵)) = (𝑊 sSet 〈(Base‘ndx), ((𝐴 ∩ 𝐵) ∩ 𝐵)〉)) |
| 30 | 28, 11, 12, 29 | syl3an 1161 |
. . . . . 6
⊢ ((¬
𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ V) → (𝑊 ↾s (𝐴 ∩ 𝐵)) = (𝑊 sSet 〈(Base‘ndx), ((𝐴 ∩ 𝐵) ∩ 𝐵)〉)) |
| 31 | 23, 24, 30 | 3eqtr4a 2803 |
. . . . 5
⊢ ((¬
𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ V) → (𝑊 ↾s 𝐴) = (𝑊 ↾s (𝐴 ∩ 𝐵))) |
| 32 | 31 | 3expb 1121 |
. . . 4
⊢ ((¬
𝐵 ⊆ 𝐴 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ V)) → (𝑊 ↾s 𝐴) = (𝑊 ↾s (𝐴 ∩ 𝐵))) |
| 33 | 17, 32 | pm2.61ian 812 |
. . 3
⊢ ((𝑊 ∈ V ∧ 𝐴 ∈ V) → (𝑊 ↾s 𝐴) = (𝑊 ↾s (𝐴 ∩ 𝐵))) |
| 34 | | reldmress 17276 |
. . . . . 6
⊢ Rel dom
↾s |
| 35 | 34 | ovprc1 7470 |
. . . . 5
⊢ (¬
𝑊 ∈ V → (𝑊 ↾s 𝐴) = ∅) |
| 36 | 34 | ovprc1 7470 |
. . . . 5
⊢ (¬
𝑊 ∈ V → (𝑊 ↾s (𝐴 ∩ 𝐵)) = ∅) |
| 37 | 35, 36 | eqtr4d 2780 |
. . . 4
⊢ (¬
𝑊 ∈ V → (𝑊 ↾s 𝐴) = (𝑊 ↾s (𝐴 ∩ 𝐵))) |
| 38 | 37 | adantr 480 |
. . 3
⊢ ((¬
𝑊 ∈ V ∧ 𝐴 ∈ V) → (𝑊 ↾s 𝐴) = (𝑊 ↾s (𝐴 ∩ 𝐵))) |
| 39 | 33, 38 | pm2.61ian 812 |
. 2
⊢ (𝐴 ∈ V → (𝑊 ↾s 𝐴) = (𝑊 ↾s (𝐴 ∩ 𝐵))) |
| 40 | 1, 39 | syl 17 |
1
⊢ (𝐴 ∈ 𝑋 → (𝑊 ↾s 𝐴) = (𝑊 ↾s (𝐴 ∩ 𝐵))) |