Proof of Theorem ressress
Step | Hyp | Ref
| Expression |
1 | | simplr 769 |
. . . . . . . . 9
⊢ (((¬
(Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ ¬
(Base‘𝑊) ⊆
𝐴) ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → ¬ (Base‘𝑊) ⊆ 𝐴) |
2 | | simpr1 1195 |
. . . . . . . . 9
⊢ (((¬
(Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ ¬
(Base‘𝑊) ⊆
𝐴) ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → 𝑊 ∈ V) |
3 | | simpr2 1196 |
. . . . . . . . 9
⊢ (((¬
(Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ ¬
(Base‘𝑊) ⊆
𝐴) ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → 𝐴 ∈ 𝑋) |
4 | | eqid 2739 |
. . . . . . . . . 10
⊢ (𝑊 ↾s 𝐴) = (𝑊 ↾s 𝐴) |
5 | | eqid 2739 |
. . . . . . . . . 10
⊢
(Base‘𝑊) =
(Base‘𝑊) |
6 | 4, 5 | ressval2 16669 |
. . . . . . . . 9
⊢ ((¬
(Base‘𝑊) ⊆
𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ 𝑋) → (𝑊 ↾s 𝐴) = (𝑊 sSet 〈(Base‘ndx), (𝐴 ∩ (Base‘𝑊))〉)) |
7 | 1, 2, 3, 6 | syl3anc 1372 |
. . . . . . . 8
⊢ (((¬
(Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ ¬
(Base‘𝑊) ⊆
𝐴) ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝑊 ↾s 𝐴) = (𝑊 sSet 〈(Base‘ndx), (𝐴 ∩ (Base‘𝑊))〉)) |
8 | | inass 4120 |
. . . . . . . . . . 11
⊢ ((𝐴 ∩ 𝐵) ∩ (Base‘𝑊)) = (𝐴 ∩ (𝐵 ∩ (Base‘𝑊))) |
9 | | in12 4121 |
. . . . . . . . . . 11
⊢ (𝐴 ∩ (𝐵 ∩ (Base‘𝑊))) = (𝐵 ∩ (𝐴 ∩ (Base‘𝑊))) |
10 | 8, 9 | eqtri 2762 |
. . . . . . . . . 10
⊢ ((𝐴 ∩ 𝐵) ∩ (Base‘𝑊)) = (𝐵 ∩ (𝐴 ∩ (Base‘𝑊))) |
11 | 4, 5 | ressbas 16670 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ 𝑋 → (𝐴 ∩ (Base‘𝑊)) = (Base‘(𝑊 ↾s 𝐴))) |
12 | 3, 11 | syl 17 |
. . . . . . . . . . 11
⊢ (((¬
(Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ ¬
(Base‘𝑊) ⊆
𝐴) ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝐴 ∩ (Base‘𝑊)) = (Base‘(𝑊 ↾s 𝐴))) |
13 | 12 | ineq2d 4113 |
. . . . . . . . . 10
⊢ (((¬
(Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ ¬
(Base‘𝑊) ⊆
𝐴) ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝐵 ∩ (𝐴 ∩ (Base‘𝑊))) = (𝐵 ∩ (Base‘(𝑊 ↾s 𝐴)))) |
14 | 10, 13 | eqtr2id 2787 |
. . . . . . . . 9
⊢ (((¬
(Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ ¬
(Base‘𝑊) ⊆
𝐴) ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝐵 ∩ (Base‘(𝑊 ↾s 𝐴))) = ((𝐴 ∩ 𝐵) ∩ (Base‘𝑊))) |
15 | 14 | opeq2d 4778 |
. . . . . . . 8
⊢ (((¬
(Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ ¬
(Base‘𝑊) ⊆
𝐴) ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → 〈(Base‘ndx), (𝐵 ∩ (Base‘(𝑊 ↾s 𝐴)))〉 =
〈(Base‘ndx), ((𝐴
∩ 𝐵) ∩
(Base‘𝑊))〉) |
16 | 7, 15 | oveq12d 7201 |
. . . . . . 7
⊢ (((¬
(Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ ¬
(Base‘𝑊) ⊆
𝐴) ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → ((𝑊 ↾s 𝐴) sSet 〈(Base‘ndx), (𝐵 ∩ (Base‘(𝑊 ↾s 𝐴)))〉) = ((𝑊 sSet 〈(Base‘ndx), (𝐴 ∩ (Base‘𝑊))〉) sSet
〈(Base‘ndx), ((𝐴
∩ 𝐵) ∩
(Base‘𝑊))〉)) |
17 | | fvex 6700 |
. . . . . . . . 9
⊢
(Base‘𝑊)
∈ V |
18 | 17 | inex2 5196 |
. . . . . . . 8
⊢ ((𝐴 ∩ 𝐵) ∩ (Base‘𝑊)) ∈ V |
19 | | setsabs 16642 |
. . . . . . . 8
⊢ ((𝑊 ∈ V ∧ ((𝐴 ∩ 𝐵) ∩ (Base‘𝑊)) ∈ V) → ((𝑊 sSet 〈(Base‘ndx), (𝐴 ∩ (Base‘𝑊))〉) sSet
〈(Base‘ndx), ((𝐴
∩ 𝐵) ∩
(Base‘𝑊))〉) =
(𝑊 sSet
〈(Base‘ndx), ((𝐴
∩ 𝐵) ∩
(Base‘𝑊))〉)) |
20 | 2, 18, 19 | sylancl 589 |
. . . . . . 7
⊢ (((¬
(Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ ¬
(Base‘𝑊) ⊆
𝐴) ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → ((𝑊 sSet 〈(Base‘ndx), (𝐴 ∩ (Base‘𝑊))〉) sSet
〈(Base‘ndx), ((𝐴
∩ 𝐵) ∩
(Base‘𝑊))〉) =
(𝑊 sSet
〈(Base‘ndx), ((𝐴
∩ 𝐵) ∩
(Base‘𝑊))〉)) |
21 | 16, 20 | eqtrd 2774 |
. . . . . 6
⊢ (((¬
(Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ ¬
(Base‘𝑊) ⊆
𝐴) ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → ((𝑊 ↾s 𝐴) sSet 〈(Base‘ndx), (𝐵 ∩ (Base‘(𝑊 ↾s 𝐴)))〉) = (𝑊 sSet 〈(Base‘ndx), ((𝐴 ∩ 𝐵) ∩ (Base‘𝑊))〉)) |
22 | | simpll 767 |
. . . . . . 7
⊢ (((¬
(Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ ¬
(Base‘𝑊) ⊆
𝐴) ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → ¬ (Base‘(𝑊 ↾s 𝐴)) ⊆ 𝐵) |
23 | | ovexd 7218 |
. . . . . . 7
⊢ (((¬
(Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ ¬
(Base‘𝑊) ⊆
𝐴) ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝑊 ↾s 𝐴) ∈ V) |
24 | | simpr3 1197 |
. . . . . . 7
⊢ (((¬
(Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ ¬
(Base‘𝑊) ⊆
𝐴) ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → 𝐵 ∈ 𝑌) |
25 | | eqid 2739 |
. . . . . . . 8
⊢ ((𝑊 ↾s 𝐴) ↾s 𝐵) = ((𝑊 ↾s 𝐴) ↾s 𝐵) |
26 | | eqid 2739 |
. . . . . . . 8
⊢
(Base‘(𝑊
↾s 𝐴)) =
(Base‘(𝑊
↾s 𝐴)) |
27 | 25, 26 | ressval2 16669 |
. . . . . . 7
⊢ ((¬
(Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ (𝑊 ↾s 𝐴) ∈ V ∧ 𝐵 ∈ 𝑌) → ((𝑊 ↾s 𝐴) ↾s 𝐵) = ((𝑊 ↾s 𝐴) sSet 〈(Base‘ndx), (𝐵 ∩ (Base‘(𝑊 ↾s 𝐴)))〉)) |
28 | 22, 23, 24, 27 | syl3anc 1372 |
. . . . . 6
⊢ (((¬
(Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ ¬
(Base‘𝑊) ⊆
𝐴) ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → ((𝑊 ↾s 𝐴) ↾s 𝐵) = ((𝑊 ↾s 𝐴) sSet 〈(Base‘ndx), (𝐵 ∩ (Base‘(𝑊 ↾s 𝐴)))〉)) |
29 | | inss1 4129 |
. . . . . . . . 9
⊢ (𝐴 ∩ 𝐵) ⊆ 𝐴 |
30 | | sstr 3895 |
. . . . . . . . 9
⊢
(((Base‘𝑊)
⊆ (𝐴 ∩ 𝐵) ∧ (𝐴 ∩ 𝐵) ⊆ 𝐴) → (Base‘𝑊) ⊆ 𝐴) |
31 | 29, 30 | mpan2 691 |
. . . . . . . 8
⊢
((Base‘𝑊)
⊆ (𝐴 ∩ 𝐵) → (Base‘𝑊) ⊆ 𝐴) |
32 | 1, 31 | nsyl 142 |
. . . . . . 7
⊢ (((¬
(Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ ¬
(Base‘𝑊) ⊆
𝐴) ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → ¬ (Base‘𝑊) ⊆ (𝐴 ∩ 𝐵)) |
33 | | inex1g 5197 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝑋 → (𝐴 ∩ 𝐵) ∈ V) |
34 | 3, 33 | syl 17 |
. . . . . . 7
⊢ (((¬
(Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ ¬
(Base‘𝑊) ⊆
𝐴) ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝐴 ∩ 𝐵) ∈ V) |
35 | | eqid 2739 |
. . . . . . . 8
⊢ (𝑊 ↾s (𝐴 ∩ 𝐵)) = (𝑊 ↾s (𝐴 ∩ 𝐵)) |
36 | 35, 5 | ressval2 16669 |
. . . . . . 7
⊢ ((¬
(Base‘𝑊) ⊆
(𝐴 ∩ 𝐵) ∧ 𝑊 ∈ V ∧ (𝐴 ∩ 𝐵) ∈ V) → (𝑊 ↾s (𝐴 ∩ 𝐵)) = (𝑊 sSet 〈(Base‘ndx), ((𝐴 ∩ 𝐵) ∩ (Base‘𝑊))〉)) |
37 | 32, 2, 34, 36 | syl3anc 1372 |
. . . . . 6
⊢ (((¬
(Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ ¬
(Base‘𝑊) ⊆
𝐴) ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝑊 ↾s (𝐴 ∩ 𝐵)) = (𝑊 sSet 〈(Base‘ndx), ((𝐴 ∩ 𝐵) ∩ (Base‘𝑊))〉)) |
38 | 21, 28, 37 | 3eqtr4d 2784 |
. . . . 5
⊢ (((¬
(Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ ¬
(Base‘𝑊) ⊆
𝐴) ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → ((𝑊 ↾s 𝐴) ↾s 𝐵) = (𝑊 ↾s (𝐴 ∩ 𝐵))) |
39 | 38 | exp31 423 |
. . . 4
⊢ (¬
(Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 → (¬
(Base‘𝑊) ⊆
𝐴 → ((𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → ((𝑊 ↾s 𝐴) ↾s 𝐵) = (𝑊 ↾s (𝐴 ∩ 𝐵))))) |
40 | | ovex 7216 |
. . . . . . . 8
⊢ (𝑊 ↾s 𝐴) ∈ V |
41 | 25, 26 | ressid2 16668 |
. . . . . . . 8
⊢
(((Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ (𝑊 ↾s 𝐴) ∈ V ∧ 𝐵 ∈ 𝑌) → ((𝑊 ↾s 𝐴) ↾s 𝐵) = (𝑊 ↾s 𝐴)) |
42 | 40, 41 | mp3an2 1450 |
. . . . . . 7
⊢
(((Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ 𝐵 ∈ 𝑌) → ((𝑊 ↾s 𝐴) ↾s 𝐵) = (𝑊 ↾s 𝐴)) |
43 | 42 | 3ad2antr3 1191 |
. . . . . 6
⊢
(((Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → ((𝑊 ↾s 𝐴) ↾s 𝐵) = (𝑊 ↾s 𝐴)) |
44 | | in32 4122 |
. . . . . . . . 9
⊢ ((𝐴 ∩ 𝐵) ∩ (Base‘𝑊)) = ((𝐴 ∩ (Base‘𝑊)) ∩ 𝐵) |
45 | | simpr2 1196 |
. . . . . . . . . . . 12
⊢
(((Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → 𝐴 ∈ 𝑋) |
46 | 45, 11 | syl 17 |
. . . . . . . . . . 11
⊢
(((Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝐴 ∩ (Base‘𝑊)) = (Base‘(𝑊 ↾s 𝐴))) |
47 | | simpl 486 |
. . . . . . . . . . 11
⊢
(((Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (Base‘(𝑊 ↾s 𝐴)) ⊆ 𝐵) |
48 | 46, 47 | eqsstrd 3925 |
. . . . . . . . . 10
⊢
(((Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝐴 ∩ (Base‘𝑊)) ⊆ 𝐵) |
49 | | df-ss 3870 |
. . . . . . . . . 10
⊢ ((𝐴 ∩ (Base‘𝑊)) ⊆ 𝐵 ↔ ((𝐴 ∩ (Base‘𝑊)) ∩ 𝐵) = (𝐴 ∩ (Base‘𝑊))) |
50 | 48, 49 | sylib 221 |
. . . . . . . . 9
⊢
(((Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → ((𝐴 ∩ (Base‘𝑊)) ∩ 𝐵) = (𝐴 ∩ (Base‘𝑊))) |
51 | 44, 50 | eqtr2id 2787 |
. . . . . . . 8
⊢
(((Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝐴 ∩ (Base‘𝑊)) = ((𝐴 ∩ 𝐵) ∩ (Base‘𝑊))) |
52 | 51 | oveq2d 7199 |
. . . . . . 7
⊢
(((Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝑊 ↾s (𝐴 ∩ (Base‘𝑊))) = (𝑊 ↾s ((𝐴 ∩ 𝐵) ∩ (Base‘𝑊)))) |
53 | 5 | ressinbas 16676 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝑋 → (𝑊 ↾s 𝐴) = (𝑊 ↾s (𝐴 ∩ (Base‘𝑊)))) |
54 | 45, 53 | syl 17 |
. . . . . . 7
⊢
(((Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝑊 ↾s 𝐴) = (𝑊 ↾s (𝐴 ∩ (Base‘𝑊)))) |
55 | 5 | ressinbas 16676 |
. . . . . . . 8
⊢ ((𝐴 ∩ 𝐵) ∈ V → (𝑊 ↾s (𝐴 ∩ 𝐵)) = (𝑊 ↾s ((𝐴 ∩ 𝐵) ∩ (Base‘𝑊)))) |
56 | 45, 33, 55 | 3syl 18 |
. . . . . . 7
⊢
(((Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝑊 ↾s (𝐴 ∩ 𝐵)) = (𝑊 ↾s ((𝐴 ∩ 𝐵) ∩ (Base‘𝑊)))) |
57 | 52, 54, 56 | 3eqtr4d 2784 |
. . . . . 6
⊢
(((Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝑊 ↾s 𝐴) = (𝑊 ↾s (𝐴 ∩ 𝐵))) |
58 | 43, 57 | eqtrd 2774 |
. . . . 5
⊢
(((Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → ((𝑊 ↾s 𝐴) ↾s 𝐵) = (𝑊 ↾s (𝐴 ∩ 𝐵))) |
59 | 58 | ex 416 |
. . . 4
⊢
((Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 → ((𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → ((𝑊 ↾s 𝐴) ↾s 𝐵) = (𝑊 ↾s (𝐴 ∩ 𝐵)))) |
60 | 4, 5 | ressid2 16668 |
. . . . . . . 8
⊢
(((Base‘𝑊)
⊆ 𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ 𝑋) → (𝑊 ↾s 𝐴) = 𝑊) |
61 | 60 | 3adant3r3 1185 |
. . . . . . 7
⊢
(((Base‘𝑊)
⊆ 𝐴 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝑊 ↾s 𝐴) = 𝑊) |
62 | 61 | oveq1d 7198 |
. . . . . 6
⊢
(((Base‘𝑊)
⊆ 𝐴 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → ((𝑊 ↾s 𝐴) ↾s 𝐵) = (𝑊 ↾s 𝐵)) |
63 | | inss2 4130 |
. . . . . . . . . . 11
⊢ (𝐵 ∩ (Base‘𝑊)) ⊆ (Base‘𝑊) |
64 | | simpl 486 |
. . . . . . . . . . 11
⊢
(((Base‘𝑊)
⊆ 𝐴 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (Base‘𝑊) ⊆ 𝐴) |
65 | 63, 64 | sstrid 3898 |
. . . . . . . . . 10
⊢
(((Base‘𝑊)
⊆ 𝐴 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝐵 ∩ (Base‘𝑊)) ⊆ 𝐴) |
66 | | sseqin2 4116 |
. . . . . . . . . 10
⊢ ((𝐵 ∩ (Base‘𝑊)) ⊆ 𝐴 ↔ (𝐴 ∩ (𝐵 ∩ (Base‘𝑊))) = (𝐵 ∩ (Base‘𝑊))) |
67 | 65, 66 | sylib 221 |
. . . . . . . . 9
⊢
(((Base‘𝑊)
⊆ 𝐴 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝐴 ∩ (𝐵 ∩ (Base‘𝑊))) = (𝐵 ∩ (Base‘𝑊))) |
68 | 8, 67 | eqtr2id 2787 |
. . . . . . . 8
⊢
(((Base‘𝑊)
⊆ 𝐴 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝐵 ∩ (Base‘𝑊)) = ((𝐴 ∩ 𝐵) ∩ (Base‘𝑊))) |
69 | 68 | oveq2d 7199 |
. . . . . . 7
⊢
(((Base‘𝑊)
⊆ 𝐴 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝑊 ↾s (𝐵 ∩ (Base‘𝑊))) = (𝑊 ↾s ((𝐴 ∩ 𝐵) ∩ (Base‘𝑊)))) |
70 | | simpr3 1197 |
. . . . . . . 8
⊢
(((Base‘𝑊)
⊆ 𝐴 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → 𝐵 ∈ 𝑌) |
71 | 5 | ressinbas 16676 |
. . . . . . . 8
⊢ (𝐵 ∈ 𝑌 → (𝑊 ↾s 𝐵) = (𝑊 ↾s (𝐵 ∩ (Base‘𝑊)))) |
72 | 70, 71 | syl 17 |
. . . . . . 7
⊢
(((Base‘𝑊)
⊆ 𝐴 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝑊 ↾s 𝐵) = (𝑊 ↾s (𝐵 ∩ (Base‘𝑊)))) |
73 | | simpr2 1196 |
. . . . . . . 8
⊢
(((Base‘𝑊)
⊆ 𝐴 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → 𝐴 ∈ 𝑋) |
74 | 73, 33, 55 | 3syl 18 |
. . . . . . 7
⊢
(((Base‘𝑊)
⊆ 𝐴 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝑊 ↾s (𝐴 ∩ 𝐵)) = (𝑊 ↾s ((𝐴 ∩ 𝐵) ∩ (Base‘𝑊)))) |
75 | 69, 72, 74 | 3eqtr4d 2784 |
. . . . . 6
⊢
(((Base‘𝑊)
⊆ 𝐴 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝑊 ↾s 𝐵) = (𝑊 ↾s (𝐴 ∩ 𝐵))) |
76 | 62, 75 | eqtrd 2774 |
. . . . 5
⊢
(((Base‘𝑊)
⊆ 𝐴 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → ((𝑊 ↾s 𝐴) ↾s 𝐵) = (𝑊 ↾s (𝐴 ∩ 𝐵))) |
77 | 76 | ex 416 |
. . . 4
⊢
((Base‘𝑊)
⊆ 𝐴 → ((𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → ((𝑊 ↾s 𝐴) ↾s 𝐵) = (𝑊 ↾s (𝐴 ∩ 𝐵)))) |
78 | 39, 59, 77 | pm2.61ii 186 |
. . 3
⊢ ((𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → ((𝑊 ↾s 𝐴) ↾s 𝐵) = (𝑊 ↾s (𝐴 ∩ 𝐵))) |
79 | 78 | 3expib 1123 |
. 2
⊢ (𝑊 ∈ V → ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → ((𝑊 ↾s 𝐴) ↾s 𝐵) = (𝑊 ↾s (𝐴 ∩ 𝐵)))) |
80 | | ress0 16674 |
. . . 4
⊢ (∅
↾s 𝐵) =
∅ |
81 | | reldmress 16666 |
. . . . . 6
⊢ Rel dom
↾s |
82 | 81 | ovprc1 7222 |
. . . . 5
⊢ (¬
𝑊 ∈ V → (𝑊 ↾s 𝐴) = ∅) |
83 | 82 | oveq1d 7198 |
. . . 4
⊢ (¬
𝑊 ∈ V → ((𝑊 ↾s 𝐴) ↾s 𝐵) = (∅ ↾s
𝐵)) |
84 | 81 | ovprc1 7222 |
. . . 4
⊢ (¬
𝑊 ∈ V → (𝑊 ↾s (𝐴 ∩ 𝐵)) = ∅) |
85 | 80, 83, 84 | 3eqtr4a 2800 |
. . 3
⊢ (¬
𝑊 ∈ V → ((𝑊 ↾s 𝐴) ↾s 𝐵) = (𝑊 ↾s (𝐴 ∩ 𝐵))) |
86 | 85 | a1d 25 |
. 2
⊢ (¬
𝑊 ∈ V → ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → ((𝑊 ↾s 𝐴) ↾s 𝐵) = (𝑊 ↾s (𝐴 ∩ 𝐵)))) |
87 | 79, 86 | pm2.61i 185 |
1
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → ((𝑊 ↾s 𝐴) ↾s 𝐵) = (𝑊 ↾s (𝐴 ∩ 𝐵))) |