Proof of Theorem ressress
Step | Hyp | Ref
| Expression |
1 | | simplr 766 |
. . . . . . . . 9
⊢ (((¬
(Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ ¬
(Base‘𝑊) ⊆
𝐴) ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → ¬ (Base‘𝑊) ⊆ 𝐴) |
2 | | simpr1 1193 |
. . . . . . . . 9
⊢ (((¬
(Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ ¬
(Base‘𝑊) ⊆
𝐴) ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → 𝑊 ∈ V) |
3 | | simpr2 1194 |
. . . . . . . . 9
⊢ (((¬
(Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ ¬
(Base‘𝑊) ⊆
𝐴) ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → 𝐴 ∈ 𝑋) |
4 | | eqid 2738 |
. . . . . . . . . 10
⊢ (𝑊 ↾s 𝐴) = (𝑊 ↾s 𝐴) |
5 | | eqid 2738 |
. . . . . . . . . 10
⊢
(Base‘𝑊) =
(Base‘𝑊) |
6 | 4, 5 | ressval2 16946 |
. . . . . . . . 9
⊢ ((¬
(Base‘𝑊) ⊆
𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ 𝑋) → (𝑊 ↾s 𝐴) = (𝑊 sSet 〈(Base‘ndx), (𝐴 ∩ (Base‘𝑊))〉)) |
7 | 1, 2, 3, 6 | syl3anc 1370 |
. . . . . . . 8
⊢ (((¬
(Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ ¬
(Base‘𝑊) ⊆
𝐴) ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝑊 ↾s 𝐴) = (𝑊 sSet 〈(Base‘ndx), (𝐴 ∩ (Base‘𝑊))〉)) |
8 | | inass 4153 |
. . . . . . . . . . 11
⊢ ((𝐴 ∩ 𝐵) ∩ (Base‘𝑊)) = (𝐴 ∩ (𝐵 ∩ (Base‘𝑊))) |
9 | | in12 4154 |
. . . . . . . . . . 11
⊢ (𝐴 ∩ (𝐵 ∩ (Base‘𝑊))) = (𝐵 ∩ (𝐴 ∩ (Base‘𝑊))) |
10 | 8, 9 | eqtri 2766 |
. . . . . . . . . 10
⊢ ((𝐴 ∩ 𝐵) ∩ (Base‘𝑊)) = (𝐵 ∩ (𝐴 ∩ (Base‘𝑊))) |
11 | 4, 5 | ressbas 16947 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ 𝑋 → (𝐴 ∩ (Base‘𝑊)) = (Base‘(𝑊 ↾s 𝐴))) |
12 | 3, 11 | syl 17 |
. . . . . . . . . . 11
⊢ (((¬
(Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ ¬
(Base‘𝑊) ⊆
𝐴) ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝐴 ∩ (Base‘𝑊)) = (Base‘(𝑊 ↾s 𝐴))) |
13 | 12 | ineq2d 4146 |
. . . . . . . . . 10
⊢ (((¬
(Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ ¬
(Base‘𝑊) ⊆
𝐴) ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝐵 ∩ (𝐴 ∩ (Base‘𝑊))) = (𝐵 ∩ (Base‘(𝑊 ↾s 𝐴)))) |
14 | 10, 13 | eqtr2id 2791 |
. . . . . . . . 9
⊢ (((¬
(Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ ¬
(Base‘𝑊) ⊆
𝐴) ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝐵 ∩ (Base‘(𝑊 ↾s 𝐴))) = ((𝐴 ∩ 𝐵) ∩ (Base‘𝑊))) |
15 | 14 | opeq2d 4811 |
. . . . . . . 8
⊢ (((¬
(Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ ¬
(Base‘𝑊) ⊆
𝐴) ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → 〈(Base‘ndx), (𝐵 ∩ (Base‘(𝑊 ↾s 𝐴)))〉 =
〈(Base‘ndx), ((𝐴
∩ 𝐵) ∩
(Base‘𝑊))〉) |
16 | 7, 15 | oveq12d 7293 |
. . . . . . 7
⊢ (((¬
(Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ ¬
(Base‘𝑊) ⊆
𝐴) ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → ((𝑊 ↾s 𝐴) sSet 〈(Base‘ndx), (𝐵 ∩ (Base‘(𝑊 ↾s 𝐴)))〉) = ((𝑊 sSet 〈(Base‘ndx), (𝐴 ∩ (Base‘𝑊))〉) sSet
〈(Base‘ndx), ((𝐴
∩ 𝐵) ∩
(Base‘𝑊))〉)) |
17 | | fvex 6787 |
. . . . . . . . 9
⊢
(Base‘𝑊)
∈ V |
18 | 17 | inex2 5242 |
. . . . . . . 8
⊢ ((𝐴 ∩ 𝐵) ∩ (Base‘𝑊)) ∈ V |
19 | | setsabs 16880 |
. . . . . . . 8
⊢ ((𝑊 ∈ V ∧ ((𝐴 ∩ 𝐵) ∩ (Base‘𝑊)) ∈ V) → ((𝑊 sSet 〈(Base‘ndx), (𝐴 ∩ (Base‘𝑊))〉) sSet
〈(Base‘ndx), ((𝐴
∩ 𝐵) ∩
(Base‘𝑊))〉) =
(𝑊 sSet
〈(Base‘ndx), ((𝐴
∩ 𝐵) ∩
(Base‘𝑊))〉)) |
20 | 2, 18, 19 | sylancl 586 |
. . . . . . 7
⊢ (((¬
(Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ ¬
(Base‘𝑊) ⊆
𝐴) ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → ((𝑊 sSet 〈(Base‘ndx), (𝐴 ∩ (Base‘𝑊))〉) sSet
〈(Base‘ndx), ((𝐴
∩ 𝐵) ∩
(Base‘𝑊))〉) =
(𝑊 sSet
〈(Base‘ndx), ((𝐴
∩ 𝐵) ∩
(Base‘𝑊))〉)) |
21 | 16, 20 | eqtrd 2778 |
. . . . . 6
⊢ (((¬
(Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ ¬
(Base‘𝑊) ⊆
𝐴) ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → ((𝑊 ↾s 𝐴) sSet 〈(Base‘ndx), (𝐵 ∩ (Base‘(𝑊 ↾s 𝐴)))〉) = (𝑊 sSet 〈(Base‘ndx), ((𝐴 ∩ 𝐵) ∩ (Base‘𝑊))〉)) |
22 | | simpll 764 |
. . . . . . 7
⊢ (((¬
(Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ ¬
(Base‘𝑊) ⊆
𝐴) ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → ¬ (Base‘(𝑊 ↾s 𝐴)) ⊆ 𝐵) |
23 | | ovexd 7310 |
. . . . . . 7
⊢ (((¬
(Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ ¬
(Base‘𝑊) ⊆
𝐴) ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝑊 ↾s 𝐴) ∈ V) |
24 | | simpr3 1195 |
. . . . . . 7
⊢ (((¬
(Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ ¬
(Base‘𝑊) ⊆
𝐴) ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → 𝐵 ∈ 𝑌) |
25 | | eqid 2738 |
. . . . . . . 8
⊢ ((𝑊 ↾s 𝐴) ↾s 𝐵) = ((𝑊 ↾s 𝐴) ↾s 𝐵) |
26 | | eqid 2738 |
. . . . . . . 8
⊢
(Base‘(𝑊
↾s 𝐴)) =
(Base‘(𝑊
↾s 𝐴)) |
27 | 25, 26 | ressval2 16946 |
. . . . . . 7
⊢ ((¬
(Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ (𝑊 ↾s 𝐴) ∈ V ∧ 𝐵 ∈ 𝑌) → ((𝑊 ↾s 𝐴) ↾s 𝐵) = ((𝑊 ↾s 𝐴) sSet 〈(Base‘ndx), (𝐵 ∩ (Base‘(𝑊 ↾s 𝐴)))〉)) |
28 | 22, 23, 24, 27 | syl3anc 1370 |
. . . . . 6
⊢ (((¬
(Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ ¬
(Base‘𝑊) ⊆
𝐴) ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → ((𝑊 ↾s 𝐴) ↾s 𝐵) = ((𝑊 ↾s 𝐴) sSet 〈(Base‘ndx), (𝐵 ∩ (Base‘(𝑊 ↾s 𝐴)))〉)) |
29 | | inss1 4162 |
. . . . . . . . 9
⊢ (𝐴 ∩ 𝐵) ⊆ 𝐴 |
30 | | sstr 3929 |
. . . . . . . . 9
⊢
(((Base‘𝑊)
⊆ (𝐴 ∩ 𝐵) ∧ (𝐴 ∩ 𝐵) ⊆ 𝐴) → (Base‘𝑊) ⊆ 𝐴) |
31 | 29, 30 | mpan2 688 |
. . . . . . . 8
⊢
((Base‘𝑊)
⊆ (𝐴 ∩ 𝐵) → (Base‘𝑊) ⊆ 𝐴) |
32 | 1, 31 | nsyl 140 |
. . . . . . 7
⊢ (((¬
(Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ ¬
(Base‘𝑊) ⊆
𝐴) ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → ¬ (Base‘𝑊) ⊆ (𝐴 ∩ 𝐵)) |
33 | | inex1g 5243 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝑋 → (𝐴 ∩ 𝐵) ∈ V) |
34 | 3, 33 | syl 17 |
. . . . . . 7
⊢ (((¬
(Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ ¬
(Base‘𝑊) ⊆
𝐴) ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝐴 ∩ 𝐵) ∈ V) |
35 | | eqid 2738 |
. . . . . . . 8
⊢ (𝑊 ↾s (𝐴 ∩ 𝐵)) = (𝑊 ↾s (𝐴 ∩ 𝐵)) |
36 | 35, 5 | ressval2 16946 |
. . . . . . 7
⊢ ((¬
(Base‘𝑊) ⊆
(𝐴 ∩ 𝐵) ∧ 𝑊 ∈ V ∧ (𝐴 ∩ 𝐵) ∈ V) → (𝑊 ↾s (𝐴 ∩ 𝐵)) = (𝑊 sSet 〈(Base‘ndx), ((𝐴 ∩ 𝐵) ∩ (Base‘𝑊))〉)) |
37 | 32, 2, 34, 36 | syl3anc 1370 |
. . . . . 6
⊢ (((¬
(Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ ¬
(Base‘𝑊) ⊆
𝐴) ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝑊 ↾s (𝐴 ∩ 𝐵)) = (𝑊 sSet 〈(Base‘ndx), ((𝐴 ∩ 𝐵) ∩ (Base‘𝑊))〉)) |
38 | 21, 28, 37 | 3eqtr4d 2788 |
. . . . 5
⊢ (((¬
(Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ ¬
(Base‘𝑊) ⊆
𝐴) ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → ((𝑊 ↾s 𝐴) ↾s 𝐵) = (𝑊 ↾s (𝐴 ∩ 𝐵))) |
39 | 38 | exp31 420 |
. . . 4
⊢ (¬
(Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 → (¬
(Base‘𝑊) ⊆
𝐴 → ((𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → ((𝑊 ↾s 𝐴) ↾s 𝐵) = (𝑊 ↾s (𝐴 ∩ 𝐵))))) |
40 | | ovex 7308 |
. . . . . . . 8
⊢ (𝑊 ↾s 𝐴) ∈ V |
41 | 25, 26 | ressid2 16945 |
. . . . . . . 8
⊢
(((Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ (𝑊 ↾s 𝐴) ∈ V ∧ 𝐵 ∈ 𝑌) → ((𝑊 ↾s 𝐴) ↾s 𝐵) = (𝑊 ↾s 𝐴)) |
42 | 40, 41 | mp3an2 1448 |
. . . . . . 7
⊢
(((Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ 𝐵 ∈ 𝑌) → ((𝑊 ↾s 𝐴) ↾s 𝐵) = (𝑊 ↾s 𝐴)) |
43 | 42 | 3ad2antr3 1189 |
. . . . . 6
⊢
(((Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → ((𝑊 ↾s 𝐴) ↾s 𝐵) = (𝑊 ↾s 𝐴)) |
44 | | in32 4155 |
. . . . . . . . 9
⊢ ((𝐴 ∩ 𝐵) ∩ (Base‘𝑊)) = ((𝐴 ∩ (Base‘𝑊)) ∩ 𝐵) |
45 | | simpr2 1194 |
. . . . . . . . . . . 12
⊢
(((Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → 𝐴 ∈ 𝑋) |
46 | 45, 11 | syl 17 |
. . . . . . . . . . 11
⊢
(((Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝐴 ∩ (Base‘𝑊)) = (Base‘(𝑊 ↾s 𝐴))) |
47 | | simpl 483 |
. . . . . . . . . . 11
⊢
(((Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (Base‘(𝑊 ↾s 𝐴)) ⊆ 𝐵) |
48 | 46, 47 | eqsstrd 3959 |
. . . . . . . . . 10
⊢
(((Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝐴 ∩ (Base‘𝑊)) ⊆ 𝐵) |
49 | | df-ss 3904 |
. . . . . . . . . 10
⊢ ((𝐴 ∩ (Base‘𝑊)) ⊆ 𝐵 ↔ ((𝐴 ∩ (Base‘𝑊)) ∩ 𝐵) = (𝐴 ∩ (Base‘𝑊))) |
50 | 48, 49 | sylib 217 |
. . . . . . . . 9
⊢
(((Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → ((𝐴 ∩ (Base‘𝑊)) ∩ 𝐵) = (𝐴 ∩ (Base‘𝑊))) |
51 | 44, 50 | eqtr2id 2791 |
. . . . . . . 8
⊢
(((Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝐴 ∩ (Base‘𝑊)) = ((𝐴 ∩ 𝐵) ∩ (Base‘𝑊))) |
52 | 51 | oveq2d 7291 |
. . . . . . 7
⊢
(((Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝑊 ↾s (𝐴 ∩ (Base‘𝑊))) = (𝑊 ↾s ((𝐴 ∩ 𝐵) ∩ (Base‘𝑊)))) |
53 | 5 | ressinbas 16955 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝑋 → (𝑊 ↾s 𝐴) = (𝑊 ↾s (𝐴 ∩ (Base‘𝑊)))) |
54 | 45, 53 | syl 17 |
. . . . . . 7
⊢
(((Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝑊 ↾s 𝐴) = (𝑊 ↾s (𝐴 ∩ (Base‘𝑊)))) |
55 | 5 | ressinbas 16955 |
. . . . . . . 8
⊢ ((𝐴 ∩ 𝐵) ∈ V → (𝑊 ↾s (𝐴 ∩ 𝐵)) = (𝑊 ↾s ((𝐴 ∩ 𝐵) ∩ (Base‘𝑊)))) |
56 | 45, 33, 55 | 3syl 18 |
. . . . . . 7
⊢
(((Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝑊 ↾s (𝐴 ∩ 𝐵)) = (𝑊 ↾s ((𝐴 ∩ 𝐵) ∩ (Base‘𝑊)))) |
57 | 52, 54, 56 | 3eqtr4d 2788 |
. . . . . 6
⊢
(((Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝑊 ↾s 𝐴) = (𝑊 ↾s (𝐴 ∩ 𝐵))) |
58 | 43, 57 | eqtrd 2778 |
. . . . 5
⊢
(((Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → ((𝑊 ↾s 𝐴) ↾s 𝐵) = (𝑊 ↾s (𝐴 ∩ 𝐵))) |
59 | 58 | ex 413 |
. . . 4
⊢
((Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 → ((𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → ((𝑊 ↾s 𝐴) ↾s 𝐵) = (𝑊 ↾s (𝐴 ∩ 𝐵)))) |
60 | 4, 5 | ressid2 16945 |
. . . . . . . 8
⊢
(((Base‘𝑊)
⊆ 𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ 𝑋) → (𝑊 ↾s 𝐴) = 𝑊) |
61 | 60 | 3adant3r3 1183 |
. . . . . . 7
⊢
(((Base‘𝑊)
⊆ 𝐴 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝑊 ↾s 𝐴) = 𝑊) |
62 | 61 | oveq1d 7290 |
. . . . . 6
⊢
(((Base‘𝑊)
⊆ 𝐴 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → ((𝑊 ↾s 𝐴) ↾s 𝐵) = (𝑊 ↾s 𝐵)) |
63 | | inss2 4163 |
. . . . . . . . . . 11
⊢ (𝐵 ∩ (Base‘𝑊)) ⊆ (Base‘𝑊) |
64 | | simpl 483 |
. . . . . . . . . . 11
⊢
(((Base‘𝑊)
⊆ 𝐴 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (Base‘𝑊) ⊆ 𝐴) |
65 | 63, 64 | sstrid 3932 |
. . . . . . . . . 10
⊢
(((Base‘𝑊)
⊆ 𝐴 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝐵 ∩ (Base‘𝑊)) ⊆ 𝐴) |
66 | | sseqin2 4149 |
. . . . . . . . . 10
⊢ ((𝐵 ∩ (Base‘𝑊)) ⊆ 𝐴 ↔ (𝐴 ∩ (𝐵 ∩ (Base‘𝑊))) = (𝐵 ∩ (Base‘𝑊))) |
67 | 65, 66 | sylib 217 |
. . . . . . . . 9
⊢
(((Base‘𝑊)
⊆ 𝐴 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝐴 ∩ (𝐵 ∩ (Base‘𝑊))) = (𝐵 ∩ (Base‘𝑊))) |
68 | 8, 67 | eqtr2id 2791 |
. . . . . . . 8
⊢
(((Base‘𝑊)
⊆ 𝐴 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝐵 ∩ (Base‘𝑊)) = ((𝐴 ∩ 𝐵) ∩ (Base‘𝑊))) |
69 | 68 | oveq2d 7291 |
. . . . . . 7
⊢
(((Base‘𝑊)
⊆ 𝐴 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝑊 ↾s (𝐵 ∩ (Base‘𝑊))) = (𝑊 ↾s ((𝐴 ∩ 𝐵) ∩ (Base‘𝑊)))) |
70 | | simpr3 1195 |
. . . . . . . 8
⊢
(((Base‘𝑊)
⊆ 𝐴 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → 𝐵 ∈ 𝑌) |
71 | 5 | ressinbas 16955 |
. . . . . . . 8
⊢ (𝐵 ∈ 𝑌 → (𝑊 ↾s 𝐵) = (𝑊 ↾s (𝐵 ∩ (Base‘𝑊)))) |
72 | 70, 71 | syl 17 |
. . . . . . 7
⊢
(((Base‘𝑊)
⊆ 𝐴 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝑊 ↾s 𝐵) = (𝑊 ↾s (𝐵 ∩ (Base‘𝑊)))) |
73 | | simpr2 1194 |
. . . . . . . 8
⊢
(((Base‘𝑊)
⊆ 𝐴 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → 𝐴 ∈ 𝑋) |
74 | 73, 33, 55 | 3syl 18 |
. . . . . . 7
⊢
(((Base‘𝑊)
⊆ 𝐴 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝑊 ↾s (𝐴 ∩ 𝐵)) = (𝑊 ↾s ((𝐴 ∩ 𝐵) ∩ (Base‘𝑊)))) |
75 | 69, 72, 74 | 3eqtr4d 2788 |
. . . . . 6
⊢
(((Base‘𝑊)
⊆ 𝐴 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝑊 ↾s 𝐵) = (𝑊 ↾s (𝐴 ∩ 𝐵))) |
76 | 62, 75 | eqtrd 2778 |
. . . . 5
⊢
(((Base‘𝑊)
⊆ 𝐴 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → ((𝑊 ↾s 𝐴) ↾s 𝐵) = (𝑊 ↾s (𝐴 ∩ 𝐵))) |
77 | 76 | ex 413 |
. . . 4
⊢
((Base‘𝑊)
⊆ 𝐴 → ((𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → ((𝑊 ↾s 𝐴) ↾s 𝐵) = (𝑊 ↾s (𝐴 ∩ 𝐵)))) |
78 | 39, 59, 77 | pm2.61ii 183 |
. . 3
⊢ ((𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → ((𝑊 ↾s 𝐴) ↾s 𝐵) = (𝑊 ↾s (𝐴 ∩ 𝐵))) |
79 | 78 | 3expib 1121 |
. 2
⊢ (𝑊 ∈ V → ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → ((𝑊 ↾s 𝐴) ↾s 𝐵) = (𝑊 ↾s (𝐴 ∩ 𝐵)))) |
80 | | ress0 16953 |
. . . 4
⊢ (∅
↾s 𝐵) =
∅ |
81 | | reldmress 16943 |
. . . . . 6
⊢ Rel dom
↾s |
82 | 81 | ovprc1 7314 |
. . . . 5
⊢ (¬
𝑊 ∈ V → (𝑊 ↾s 𝐴) = ∅) |
83 | 82 | oveq1d 7290 |
. . . 4
⊢ (¬
𝑊 ∈ V → ((𝑊 ↾s 𝐴) ↾s 𝐵) = (∅ ↾s
𝐵)) |
84 | 81 | ovprc1 7314 |
. . . 4
⊢ (¬
𝑊 ∈ V → (𝑊 ↾s (𝐴 ∩ 𝐵)) = ∅) |
85 | 80, 83, 84 | 3eqtr4a 2804 |
. . 3
⊢ (¬
𝑊 ∈ V → ((𝑊 ↾s 𝐴) ↾s 𝐵) = (𝑊 ↾s (𝐴 ∩ 𝐵))) |
86 | 85 | a1d 25 |
. 2
⊢ (¬
𝑊 ∈ V → ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → ((𝑊 ↾s 𝐴) ↾s 𝐵) = (𝑊 ↾s (𝐴 ∩ 𝐵)))) |
87 | 79, 86 | pm2.61i 182 |
1
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → ((𝑊 ↾s 𝐴) ↾s 𝐵) = (𝑊 ↾s (𝐴 ∩ 𝐵))) |