Proof of Theorem ressinbas
Step | Hyp | Ref
| Expression |
1 | | elex 3416 |
. 2
⊢ (𝐴 ∈ 𝑋 → 𝐴 ∈ V) |
2 | | eqid 2738 |
. . . . . . 7
⊢ (𝑊 ↾s 𝐴) = (𝑊 ↾s 𝐴) |
3 | | ressid.1 |
. . . . . . 7
⊢ 𝐵 = (Base‘𝑊) |
4 | 2, 3 | ressid2 16657 |
. . . . . 6
⊢ ((𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ V) → (𝑊 ↾s 𝐴) = 𝑊) |
5 | | ssid 3899 |
. . . . . . . 8
⊢ 𝐵 ⊆ 𝐵 |
6 | | incom 4091 |
. . . . . . . . 9
⊢ (𝐴 ∩ 𝐵) = (𝐵 ∩ 𝐴) |
7 | | df-ss 3860 |
. . . . . . . . . 10
⊢ (𝐵 ⊆ 𝐴 ↔ (𝐵 ∩ 𝐴) = 𝐵) |
8 | 7 | biimpi 219 |
. . . . . . . . 9
⊢ (𝐵 ⊆ 𝐴 → (𝐵 ∩ 𝐴) = 𝐵) |
9 | 6, 8 | syl5eq 2785 |
. . . . . . . 8
⊢ (𝐵 ⊆ 𝐴 → (𝐴 ∩ 𝐵) = 𝐵) |
10 | 5, 9 | sseqtrrid 3930 |
. . . . . . 7
⊢ (𝐵 ⊆ 𝐴 → 𝐵 ⊆ (𝐴 ∩ 𝐵)) |
11 | | elex 3416 |
. . . . . . 7
⊢ (𝑊 ∈ V → 𝑊 ∈ V) |
12 | | inex1g 5187 |
. . . . . . 7
⊢ (𝐴 ∈ V → (𝐴 ∩ 𝐵) ∈ V) |
13 | | eqid 2738 |
. . . . . . . 8
⊢ (𝑊 ↾s (𝐴 ∩ 𝐵)) = (𝑊 ↾s (𝐴 ∩ 𝐵)) |
14 | 13, 3 | ressid2 16657 |
. . . . . . 7
⊢ ((𝐵 ⊆ (𝐴 ∩ 𝐵) ∧ 𝑊 ∈ V ∧ (𝐴 ∩ 𝐵) ∈ V) → (𝑊 ↾s (𝐴 ∩ 𝐵)) = 𝑊) |
15 | 10, 11, 12, 14 | syl3an 1161 |
. . . . . 6
⊢ ((𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ V) → (𝑊 ↾s (𝐴 ∩ 𝐵)) = 𝑊) |
16 | 4, 15 | eqtr4d 2776 |
. . . . 5
⊢ ((𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ V) → (𝑊 ↾s 𝐴) = (𝑊 ↾s (𝐴 ∩ 𝐵))) |
17 | 16 | 3expb 1121 |
. . . 4
⊢ ((𝐵 ⊆ 𝐴 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ V)) → (𝑊 ↾s 𝐴) = (𝑊 ↾s (𝐴 ∩ 𝐵))) |
18 | | inass 4110 |
. . . . . . . . 9
⊢ ((𝐴 ∩ 𝐵) ∩ 𝐵) = (𝐴 ∩ (𝐵 ∩ 𝐵)) |
19 | | inidm 4109 |
. . . . . . . . . 10
⊢ (𝐵 ∩ 𝐵) = 𝐵 |
20 | 19 | ineq2i 4100 |
. . . . . . . . 9
⊢ (𝐴 ∩ (𝐵 ∩ 𝐵)) = (𝐴 ∩ 𝐵) |
21 | 18, 20 | eqtr2i 2762 |
. . . . . . . 8
⊢ (𝐴 ∩ 𝐵) = ((𝐴 ∩ 𝐵) ∩ 𝐵) |
22 | 21 | opeq2i 4765 |
. . . . . . 7
⊢
〈(Base‘ndx), (𝐴 ∩ 𝐵)〉 = 〈(Base‘ndx), ((𝐴 ∩ 𝐵) ∩ 𝐵)〉 |
23 | 22 | oveq2i 7183 |
. . . . . 6
⊢ (𝑊 sSet 〈(Base‘ndx),
(𝐴 ∩ 𝐵)〉) = (𝑊 sSet 〈(Base‘ndx), ((𝐴 ∩ 𝐵) ∩ 𝐵)〉) |
24 | 2, 3 | ressval2 16658 |
. . . . . 6
⊢ ((¬
𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ V) → (𝑊 ↾s 𝐴) = (𝑊 sSet 〈(Base‘ndx), (𝐴 ∩ 𝐵)〉)) |
25 | | inss1 4119 |
. . . . . . . . 9
⊢ (𝐴 ∩ 𝐵) ⊆ 𝐴 |
26 | | sstr 3885 |
. . . . . . . . 9
⊢ ((𝐵 ⊆ (𝐴 ∩ 𝐵) ∧ (𝐴 ∩ 𝐵) ⊆ 𝐴) → 𝐵 ⊆ 𝐴) |
27 | 25, 26 | mpan2 691 |
. . . . . . . 8
⊢ (𝐵 ⊆ (𝐴 ∩ 𝐵) → 𝐵 ⊆ 𝐴) |
28 | 27 | con3i 157 |
. . . . . . 7
⊢ (¬
𝐵 ⊆ 𝐴 → ¬ 𝐵 ⊆ (𝐴 ∩ 𝐵)) |
29 | 13, 3 | ressval2 16658 |
. . . . . . 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 2799 |
. . . . 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 16655 |
. . . . . 6
⊢ Rel dom
↾s |
35 | 34 | ovprc1 7211 |
. . . . 5
⊢ (¬
𝑊 ∈ V → (𝑊 ↾s 𝐴) = ∅) |
36 | 34 | ovprc1 7211 |
. . . . 5
⊢ (¬
𝑊 ∈ V → (𝑊 ↾s (𝐴 ∩ 𝐵)) = ∅) |
37 | 35, 36 | eqtr4d 2776 |
. . . 4
⊢ (¬
𝑊 ∈ V → (𝑊 ↾s 𝐴) = (𝑊 ↾s (𝐴 ∩ 𝐵))) |
38 | 37 | adantr 484 |
. . 3
⊢ ((¬
𝑊 ∈ V ∧ 𝐴 ∈ V) → (𝑊 ↾s 𝐴) = (𝑊 ↾s (𝐴 ∩ 𝐵))) |
39 | 33, 38 | pm2.61ian 812 |
. 2
⊢ (𝐴 ∈ V → (𝑊 ↾s 𝐴) = (𝑊 ↾s (𝐴 ∩ 𝐵))) |
40 | 1, 39 | syl 17 |
1
⊢ (𝐴 ∈ 𝑋 → (𝑊 ↾s 𝐴) = (𝑊 ↾s (𝐴 ∩ 𝐵))) |