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 2737 |
. . . . . . . . . 10
⊢ (𝑊 ↾s 𝐴) = (𝑊 ↾s 𝐴) |
| 5 | | eqid 2737 |
. . . . . . . . . 10
⊢
(Base‘𝑊) =
(Base‘𝑊) |
| 6 | 4, 5 | ressval2 17279 |
. . . . . . . . 9
⊢ ((¬
(Base‘𝑊) ⊆
𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ 𝑋) → (𝑊 ↾s 𝐴) = (𝑊 sSet 〈(Base‘ndx), (𝐴 ∩ (Base‘𝑊))〉)) |
| 7 | 1, 2, 3, 6 | syl3anc 1373 |
. . . . . . . 8
⊢ (((¬
(Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ ¬
(Base‘𝑊) ⊆
𝐴) ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝑊 ↾s 𝐴) = (𝑊 sSet 〈(Base‘ndx), (𝐴 ∩ (Base‘𝑊))〉)) |
| 8 | | inass 4228 |
. . . . . . . . . . 11
⊢ ((𝐴 ∩ 𝐵) ∩ (Base‘𝑊)) = (𝐴 ∩ (𝐵 ∩ (Base‘𝑊))) |
| 9 | | in12 4229 |
. . . . . . . . . . 11
⊢ (𝐴 ∩ (𝐵 ∩ (Base‘𝑊))) = (𝐵 ∩ (𝐴 ∩ (Base‘𝑊))) |
| 10 | 8, 9 | eqtri 2765 |
. . . . . . . . . 10
⊢ ((𝐴 ∩ 𝐵) ∩ (Base‘𝑊)) = (𝐵 ∩ (𝐴 ∩ (Base‘𝑊))) |
| 11 | 4, 5 | ressbas 17280 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ 𝑋 → (𝐴 ∩ (Base‘𝑊)) = (Base‘(𝑊 ↾s 𝐴))) |
| 12 | 3, 11 | syl 17 |
. . . . . . . . . . 11
⊢ (((¬
(Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ ¬
(Base‘𝑊) ⊆
𝐴) ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝐴 ∩ (Base‘𝑊)) = (Base‘(𝑊 ↾s 𝐴))) |
| 13 | 12 | ineq2d 4220 |
. . . . . . . . . 10
⊢ (((¬
(Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ ¬
(Base‘𝑊) ⊆
𝐴) ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝐵 ∩ (𝐴 ∩ (Base‘𝑊))) = (𝐵 ∩ (Base‘(𝑊 ↾s 𝐴)))) |
| 14 | 10, 13 | eqtr2id 2790 |
. . . . . . . . 9
⊢ (((¬
(Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ ¬
(Base‘𝑊) ⊆
𝐴) ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝐵 ∩ (Base‘(𝑊 ↾s 𝐴))) = ((𝐴 ∩ 𝐵) ∩ (Base‘𝑊))) |
| 15 | 14 | opeq2d 4880 |
. . . . . . . 8
⊢ (((¬
(Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ ¬
(Base‘𝑊) ⊆
𝐴) ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → 〈(Base‘ndx), (𝐵 ∩ (Base‘(𝑊 ↾s 𝐴)))〉 =
〈(Base‘ndx), ((𝐴
∩ 𝐵) ∩
(Base‘𝑊))〉) |
| 16 | 7, 15 | oveq12d 7449 |
. . . . . . 7
⊢ (((¬
(Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ ¬
(Base‘𝑊) ⊆
𝐴) ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → ((𝑊 ↾s 𝐴) sSet 〈(Base‘ndx), (𝐵 ∩ (Base‘(𝑊 ↾s 𝐴)))〉) = ((𝑊 sSet 〈(Base‘ndx), (𝐴 ∩ (Base‘𝑊))〉) sSet
〈(Base‘ndx), ((𝐴
∩ 𝐵) ∩
(Base‘𝑊))〉)) |
| 17 | | fvex 6919 |
. . . . . . . . 9
⊢
(Base‘𝑊)
∈ V |
| 18 | 17 | inex2 5318 |
. . . . . . . 8
⊢ ((𝐴 ∩ 𝐵) ∩ (Base‘𝑊)) ∈ V |
| 19 | | setsabs 17216 |
. . . . . . . 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 2777 |
. . . . . 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 7466 |
. . . . . . 7
⊢ (((¬
(Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ ¬
(Base‘𝑊) ⊆
𝐴) ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝑊 ↾s 𝐴) ∈ V) |
| 24 | | simpr3 1197 |
. . . . . . 7
⊢ (((¬
(Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ ¬
(Base‘𝑊) ⊆
𝐴) ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → 𝐵 ∈ 𝑌) |
| 25 | | eqid 2737 |
. . . . . . . 8
⊢ ((𝑊 ↾s 𝐴) ↾s 𝐵) = ((𝑊 ↾s 𝐴) ↾s 𝐵) |
| 26 | | eqid 2737 |
. . . . . . . 8
⊢
(Base‘(𝑊
↾s 𝐴)) =
(Base‘(𝑊
↾s 𝐴)) |
| 27 | 25, 26 | ressval2 17279 |
. . . . . . 7
⊢ ((¬
(Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ (𝑊 ↾s 𝐴) ∈ V ∧ 𝐵 ∈ 𝑌) → ((𝑊 ↾s 𝐴) ↾s 𝐵) = ((𝑊 ↾s 𝐴) sSet 〈(Base‘ndx), (𝐵 ∩ (Base‘(𝑊 ↾s 𝐴)))〉)) |
| 28 | 22, 23, 24, 27 | syl3anc 1373 |
. . . . . 6
⊢ (((¬
(Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ ¬
(Base‘𝑊) ⊆
𝐴) ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → ((𝑊 ↾s 𝐴) ↾s 𝐵) = ((𝑊 ↾s 𝐴) sSet 〈(Base‘ndx), (𝐵 ∩ (Base‘(𝑊 ↾s 𝐴)))〉)) |
| 29 | | inss1 4237 |
. . . . . . . . 9
⊢ (𝐴 ∩ 𝐵) ⊆ 𝐴 |
| 30 | | sstr 3992 |
. . . . . . . . 9
⊢
(((Base‘𝑊)
⊆ (𝐴 ∩ 𝐵) ∧ (𝐴 ∩ 𝐵) ⊆ 𝐴) → (Base‘𝑊) ⊆ 𝐴) |
| 31 | 29, 30 | mpan2 691 |
. . . . . . . 8
⊢
((Base‘𝑊)
⊆ (𝐴 ∩ 𝐵) → (Base‘𝑊) ⊆ 𝐴) |
| 32 | 1, 31 | nsyl 140 |
. . . . . . 7
⊢ (((¬
(Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ ¬
(Base‘𝑊) ⊆
𝐴) ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → ¬ (Base‘𝑊) ⊆ (𝐴 ∩ 𝐵)) |
| 33 | | inex1g 5319 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝑋 → (𝐴 ∩ 𝐵) ∈ V) |
| 34 | 3, 33 | syl 17 |
. . . . . . 7
⊢ (((¬
(Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ ¬
(Base‘𝑊) ⊆
𝐴) ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝐴 ∩ 𝐵) ∈ V) |
| 35 | | eqid 2737 |
. . . . . . . 8
⊢ (𝑊 ↾s (𝐴 ∩ 𝐵)) = (𝑊 ↾s (𝐴 ∩ 𝐵)) |
| 36 | 35, 5 | ressval2 17279 |
. . . . . . 7
⊢ ((¬
(Base‘𝑊) ⊆
(𝐴 ∩ 𝐵) ∧ 𝑊 ∈ V ∧ (𝐴 ∩ 𝐵) ∈ V) → (𝑊 ↾s (𝐴 ∩ 𝐵)) = (𝑊 sSet 〈(Base‘ndx), ((𝐴 ∩ 𝐵) ∩ (Base‘𝑊))〉)) |
| 37 | 32, 2, 34, 36 | syl3anc 1373 |
. . . . . 6
⊢ (((¬
(Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ ¬
(Base‘𝑊) ⊆
𝐴) ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝑊 ↾s (𝐴 ∩ 𝐵)) = (𝑊 sSet 〈(Base‘ndx), ((𝐴 ∩ 𝐵) ∩ (Base‘𝑊))〉)) |
| 38 | 21, 28, 37 | 3eqtr4d 2787 |
. . . . 5
⊢ (((¬
(Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ ¬
(Base‘𝑊) ⊆
𝐴) ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → ((𝑊 ↾s 𝐴) ↾s 𝐵) = (𝑊 ↾s (𝐴 ∩ 𝐵))) |
| 39 | 38 | exp31 419 |
. . . 4
⊢ (¬
(Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 → (¬
(Base‘𝑊) ⊆
𝐴 → ((𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → ((𝑊 ↾s 𝐴) ↾s 𝐵) = (𝑊 ↾s (𝐴 ∩ 𝐵))))) |
| 40 | | ovex 7464 |
. . . . . . . 8
⊢ (𝑊 ↾s 𝐴) ∈ V |
| 41 | 25, 26 | ressid2 17278 |
. . . . . . . 8
⊢
(((Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ (𝑊 ↾s 𝐴) ∈ V ∧ 𝐵 ∈ 𝑌) → ((𝑊 ↾s 𝐴) ↾s 𝐵) = (𝑊 ↾s 𝐴)) |
| 42 | 40, 41 | mp3an2 1451 |
. . . . . . 7
⊢
(((Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ 𝐵 ∈ 𝑌) → ((𝑊 ↾s 𝐴) ↾s 𝐵) = (𝑊 ↾s 𝐴)) |
| 43 | 42 | 3ad2antr3 1191 |
. . . . . 6
⊢
(((Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → ((𝑊 ↾s 𝐴) ↾s 𝐵) = (𝑊 ↾s 𝐴)) |
| 44 | | in32 4230 |
. . . . . . . . 9
⊢ ((𝐴 ∩ 𝐵) ∩ (Base‘𝑊)) = ((𝐴 ∩ (Base‘𝑊)) ∩ 𝐵) |
| 45 | | simpr2 1196 |
. . . . . . . . . . . 12
⊢
(((Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → 𝐴 ∈ 𝑋) |
| 46 | 45, 11 | syl 17 |
. . . . . . . . . . 11
⊢
(((Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝐴 ∩ (Base‘𝑊)) = (Base‘(𝑊 ↾s 𝐴))) |
| 47 | | simpl 482 |
. . . . . . . . . . 11
⊢
(((Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (Base‘(𝑊 ↾s 𝐴)) ⊆ 𝐵) |
| 48 | 46, 47 | eqsstrd 4018 |
. . . . . . . . . 10
⊢
(((Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝐴 ∩ (Base‘𝑊)) ⊆ 𝐵) |
| 49 | | dfss2 3969 |
. . . . . . . . . 10
⊢ ((𝐴 ∩ (Base‘𝑊)) ⊆ 𝐵 ↔ ((𝐴 ∩ (Base‘𝑊)) ∩ 𝐵) = (𝐴 ∩ (Base‘𝑊))) |
| 50 | 48, 49 | sylib 218 |
. . . . . . . . 9
⊢
(((Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → ((𝐴 ∩ (Base‘𝑊)) ∩ 𝐵) = (𝐴 ∩ (Base‘𝑊))) |
| 51 | 44, 50 | eqtr2id 2790 |
. . . . . . . 8
⊢
(((Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝐴 ∩ (Base‘𝑊)) = ((𝐴 ∩ 𝐵) ∩ (Base‘𝑊))) |
| 52 | 51 | oveq2d 7447 |
. . . . . . 7
⊢
(((Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝑊 ↾s (𝐴 ∩ (Base‘𝑊))) = (𝑊 ↾s ((𝐴 ∩ 𝐵) ∩ (Base‘𝑊)))) |
| 53 | 5 | ressinbas 17291 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝑋 → (𝑊 ↾s 𝐴) = (𝑊 ↾s (𝐴 ∩ (Base‘𝑊)))) |
| 54 | 45, 53 | syl 17 |
. . . . . . 7
⊢
(((Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝑊 ↾s 𝐴) = (𝑊 ↾s (𝐴 ∩ (Base‘𝑊)))) |
| 55 | 5 | ressinbas 17291 |
. . . . . . . 8
⊢ ((𝐴 ∩ 𝐵) ∈ V → (𝑊 ↾s (𝐴 ∩ 𝐵)) = (𝑊 ↾s ((𝐴 ∩ 𝐵) ∩ (Base‘𝑊)))) |
| 56 | 45, 33, 55 | 3syl 18 |
. . . . . . 7
⊢
(((Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝑊 ↾s (𝐴 ∩ 𝐵)) = (𝑊 ↾s ((𝐴 ∩ 𝐵) ∩ (Base‘𝑊)))) |
| 57 | 52, 54, 56 | 3eqtr4d 2787 |
. . . . . 6
⊢
(((Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝑊 ↾s 𝐴) = (𝑊 ↾s (𝐴 ∩ 𝐵))) |
| 58 | 43, 57 | eqtrd 2777 |
. . . . 5
⊢
(((Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → ((𝑊 ↾s 𝐴) ↾s 𝐵) = (𝑊 ↾s (𝐴 ∩ 𝐵))) |
| 59 | 58 | ex 412 |
. . . 4
⊢
((Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 → ((𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → ((𝑊 ↾s 𝐴) ↾s 𝐵) = (𝑊 ↾s (𝐴 ∩ 𝐵)))) |
| 60 | 4, 5 | ressid2 17278 |
. . . . . . . 8
⊢
(((Base‘𝑊)
⊆ 𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ 𝑋) → (𝑊 ↾s 𝐴) = 𝑊) |
| 61 | 60 | 3adant3r3 1185 |
. . . . . . 7
⊢
(((Base‘𝑊)
⊆ 𝐴 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝑊 ↾s 𝐴) = 𝑊) |
| 62 | 61 | oveq1d 7446 |
. . . . . 6
⊢
(((Base‘𝑊)
⊆ 𝐴 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → ((𝑊 ↾s 𝐴) ↾s 𝐵) = (𝑊 ↾s 𝐵)) |
| 63 | | inss2 4238 |
. . . . . . . . . . 11
⊢ (𝐵 ∩ (Base‘𝑊)) ⊆ (Base‘𝑊) |
| 64 | | simpl 482 |
. . . . . . . . . . 11
⊢
(((Base‘𝑊)
⊆ 𝐴 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (Base‘𝑊) ⊆ 𝐴) |
| 65 | 63, 64 | sstrid 3995 |
. . . . . . . . . 10
⊢
(((Base‘𝑊)
⊆ 𝐴 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝐵 ∩ (Base‘𝑊)) ⊆ 𝐴) |
| 66 | | sseqin2 4223 |
. . . . . . . . . 10
⊢ ((𝐵 ∩ (Base‘𝑊)) ⊆ 𝐴 ↔ (𝐴 ∩ (𝐵 ∩ (Base‘𝑊))) = (𝐵 ∩ (Base‘𝑊))) |
| 67 | 65, 66 | sylib 218 |
. . . . . . . . 9
⊢
(((Base‘𝑊)
⊆ 𝐴 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝐴 ∩ (𝐵 ∩ (Base‘𝑊))) = (𝐵 ∩ (Base‘𝑊))) |
| 68 | 8, 67 | eqtr2id 2790 |
. . . . . . . 8
⊢
(((Base‘𝑊)
⊆ 𝐴 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝐵 ∩ (Base‘𝑊)) = ((𝐴 ∩ 𝐵) ∩ (Base‘𝑊))) |
| 69 | 68 | oveq2d 7447 |
. . . . . . 7
⊢
(((Base‘𝑊)
⊆ 𝐴 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝑊 ↾s (𝐵 ∩ (Base‘𝑊))) = (𝑊 ↾s ((𝐴 ∩ 𝐵) ∩ (Base‘𝑊)))) |
| 70 | | simpr3 1197 |
. . . . . . . 8
⊢
(((Base‘𝑊)
⊆ 𝐴 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → 𝐵 ∈ 𝑌) |
| 71 | 5 | ressinbas 17291 |
. . . . . . . 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 2787 |
. . . . . 6
⊢
(((Base‘𝑊)
⊆ 𝐴 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝑊 ↾s 𝐵) = (𝑊 ↾s (𝐴 ∩ 𝐵))) |
| 76 | 62, 75 | eqtrd 2777 |
. . . . 5
⊢
(((Base‘𝑊)
⊆ 𝐴 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → ((𝑊 ↾s 𝐴) ↾s 𝐵) = (𝑊 ↾s (𝐴 ∩ 𝐵))) |
| 77 | 76 | ex 412 |
. . . 4
⊢
((Base‘𝑊)
⊆ 𝐴 → ((𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → ((𝑊 ↾s 𝐴) ↾s 𝐵) = (𝑊 ↾s (𝐴 ∩ 𝐵)))) |
| 78 | 39, 59, 77 | pm2.61ii 183 |
. . 3
⊢ ((𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → ((𝑊 ↾s 𝐴) ↾s 𝐵) = (𝑊 ↾s (𝐴 ∩ 𝐵))) |
| 79 | 78 | 3expib 1123 |
. 2
⊢ (𝑊 ∈ V → ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → ((𝑊 ↾s 𝐴) ↾s 𝐵) = (𝑊 ↾s (𝐴 ∩ 𝐵)))) |
| 80 | | ress0 17289 |
. . . 4
⊢ (∅
↾s 𝐵) =
∅ |
| 81 | | reldmress 17276 |
. . . . . 6
⊢ Rel dom
↾s |
| 82 | 81 | ovprc1 7470 |
. . . . 5
⊢ (¬
𝑊 ∈ V → (𝑊 ↾s 𝐴) = ∅) |
| 83 | 82 | oveq1d 7446 |
. . . 4
⊢ (¬
𝑊 ∈ V → ((𝑊 ↾s 𝐴) ↾s 𝐵) = (∅ ↾s
𝐵)) |
| 84 | 81 | ovprc1 7470 |
. . . 4
⊢ (¬
𝑊 ∈ V → (𝑊 ↾s (𝐴 ∩ 𝐵)) = ∅) |
| 85 | 80, 83, 84 | 3eqtr4a 2803 |
. . 3
⊢ (¬
𝑊 ∈ V → ((𝑊 ↾s 𝐴) ↾s 𝐵) = (𝑊 ↾s (𝐴 ∩ 𝐵))) |
| 86 | 85 | a1d 25 |
. 2
⊢ (¬
𝑊 ∈ V → ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → ((𝑊 ↾s 𝐴) ↾s 𝐵) = (𝑊 ↾s (𝐴 ∩ 𝐵)))) |
| 87 | 79, 86 | pm2.61i 182 |
1
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → ((𝑊 ↾s 𝐴) ↾s 𝐵) = (𝑊 ↾s (𝐴 ∩ 𝐵))) |