Proof of Theorem ressress
Step | Hyp | Ref
| Expression |
1 | | simplr 788 |
. . . . . . . . 9
⊢ (((¬
(Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ ¬
(Base‘𝑊) ⊆
𝐴) ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → ¬ (Base‘𝑊) ⊆ 𝐴) |
2 | | simpr1 1060 |
. . . . . . . . 9
⊢ (((¬
(Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ ¬
(Base‘𝑊) ⊆
𝐴) ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → 𝑊 ∈ V) |
3 | | simpr2 1061 |
. . . . . . . . 9
⊢ (((¬
(Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ ¬
(Base‘𝑊) ⊆
𝐴) ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → 𝐴 ∈ 𝑋) |
4 | | eqid 2610 |
. . . . . . . . . 10
⊢ (𝑊 ↾s 𝐴) = (𝑊 ↾s 𝐴) |
5 | | eqid 2610 |
. . . . . . . . . 10
⊢
(Base‘𝑊) =
(Base‘𝑊) |
6 | 4, 5 | ressval2 15756 |
. . . . . . . . 9
⊢ ((¬
(Base‘𝑊) ⊆
𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ 𝑋) → (𝑊 ↾s 𝐴) = (𝑊 sSet 〈(Base‘ndx), (𝐴 ∩ (Base‘𝑊))〉)) |
7 | 1, 2, 3, 6 | syl3anc 1318 |
. . . . . . . 8
⊢ (((¬
(Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ ¬
(Base‘𝑊) ⊆
𝐴) ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝑊 ↾s 𝐴) = (𝑊 sSet 〈(Base‘ndx), (𝐴 ∩ (Base‘𝑊))〉)) |
8 | | inass 3785 |
. . . . . . . . . . 11
⊢ ((𝐴 ∩ 𝐵) ∩ (Base‘𝑊)) = (𝐴 ∩ (𝐵 ∩ (Base‘𝑊))) |
9 | | in12 3786 |
. . . . . . . . . . 11
⊢ (𝐴 ∩ (𝐵 ∩ (Base‘𝑊))) = (𝐵 ∩ (𝐴 ∩ (Base‘𝑊))) |
10 | 8, 9 | eqtri 2632 |
. . . . . . . . . 10
⊢ ((𝐴 ∩ 𝐵) ∩ (Base‘𝑊)) = (𝐵 ∩ (𝐴 ∩ (Base‘𝑊))) |
11 | 4, 5 | ressbas 15757 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ 𝑋 → (𝐴 ∩ (Base‘𝑊)) = (Base‘(𝑊 ↾s 𝐴))) |
12 | 3, 11 | syl 17 |
. . . . . . . . . . 11
⊢ (((¬
(Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ ¬
(Base‘𝑊) ⊆
𝐴) ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝐴 ∩ (Base‘𝑊)) = (Base‘(𝑊 ↾s 𝐴))) |
13 | 12 | ineq2d 3776 |
. . . . . . . . . 10
⊢ (((¬
(Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ ¬
(Base‘𝑊) ⊆
𝐴) ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝐵 ∩ (𝐴 ∩ (Base‘𝑊))) = (𝐵 ∩ (Base‘(𝑊 ↾s 𝐴)))) |
14 | 10, 13 | syl5req 2657 |
. . . . . . . . 9
⊢ (((¬
(Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ ¬
(Base‘𝑊) ⊆
𝐴) ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝐵 ∩ (Base‘(𝑊 ↾s 𝐴))) = ((𝐴 ∩ 𝐵) ∩ (Base‘𝑊))) |
15 | 14 | opeq2d 4347 |
. . . . . . . 8
⊢ (((¬
(Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ ¬
(Base‘𝑊) ⊆
𝐴) ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → 〈(Base‘ndx), (𝐵 ∩ (Base‘(𝑊 ↾s 𝐴)))〉 =
〈(Base‘ndx), ((𝐴
∩ 𝐵) ∩
(Base‘𝑊))〉) |
16 | 7, 15 | oveq12d 6567 |
. . . . . . 7
⊢ (((¬
(Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ ¬
(Base‘𝑊) ⊆
𝐴) ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → ((𝑊 ↾s 𝐴) sSet 〈(Base‘ndx), (𝐵 ∩ (Base‘(𝑊 ↾s 𝐴)))〉) = ((𝑊 sSet 〈(Base‘ndx), (𝐴 ∩ (Base‘𝑊))〉) sSet
〈(Base‘ndx), ((𝐴
∩ 𝐵) ∩
(Base‘𝑊))〉)) |
17 | | fvex 6113 |
. . . . . . . . 9
⊢
(Base‘𝑊)
∈ V |
18 | 17 | inex2 4728 |
. . . . . . . 8
⊢ ((𝐴 ∩ 𝐵) ∩ (Base‘𝑊)) ∈ V |
19 | | setsabs 15730 |
. . . . . . . 8
⊢ ((𝑊 ∈ V ∧ ((𝐴 ∩ 𝐵) ∩ (Base‘𝑊)) ∈ V) → ((𝑊 sSet 〈(Base‘ndx), (𝐴 ∩ (Base‘𝑊))〉) sSet
〈(Base‘ndx), ((𝐴
∩ 𝐵) ∩
(Base‘𝑊))〉) =
(𝑊 sSet
〈(Base‘ndx), ((𝐴
∩ 𝐵) ∩
(Base‘𝑊))〉)) |
20 | 2, 18, 19 | sylancl 693 |
. . . . . . 7
⊢ (((¬
(Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ ¬
(Base‘𝑊) ⊆
𝐴) ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → ((𝑊 sSet 〈(Base‘ndx), (𝐴 ∩ (Base‘𝑊))〉) sSet
〈(Base‘ndx), ((𝐴
∩ 𝐵) ∩
(Base‘𝑊))〉) =
(𝑊 sSet
〈(Base‘ndx), ((𝐴
∩ 𝐵) ∩
(Base‘𝑊))〉)) |
21 | 16, 20 | eqtrd 2644 |
. . . . . 6
⊢ (((¬
(Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ ¬
(Base‘𝑊) ⊆
𝐴) ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → ((𝑊 ↾s 𝐴) sSet 〈(Base‘ndx), (𝐵 ∩ (Base‘(𝑊 ↾s 𝐴)))〉) = (𝑊 sSet 〈(Base‘ndx), ((𝐴 ∩ 𝐵) ∩ (Base‘𝑊))〉)) |
22 | | simpll 786 |
. . . . . . 7
⊢ (((¬
(Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ ¬
(Base‘𝑊) ⊆
𝐴) ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → ¬ (Base‘(𝑊 ↾s 𝐴)) ⊆ 𝐵) |
23 | | ovex 6577 |
. . . . . . . 8
⊢ (𝑊 ↾s 𝐴) ∈ V |
24 | 23 | a1i 11 |
. . . . . . 7
⊢ (((¬
(Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ ¬
(Base‘𝑊) ⊆
𝐴) ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝑊 ↾s 𝐴) ∈ V) |
25 | | simpr3 1062 |
. . . . . . 7
⊢ (((¬
(Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ ¬
(Base‘𝑊) ⊆
𝐴) ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → 𝐵 ∈ 𝑌) |
26 | | eqid 2610 |
. . . . . . . 8
⊢ ((𝑊 ↾s 𝐴) ↾s 𝐵) = ((𝑊 ↾s 𝐴) ↾s 𝐵) |
27 | | eqid 2610 |
. . . . . . . 8
⊢
(Base‘(𝑊
↾s 𝐴)) =
(Base‘(𝑊
↾s 𝐴)) |
28 | 26, 27 | ressval2 15756 |
. . . . . . 7
⊢ ((¬
(Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ (𝑊 ↾s 𝐴) ∈ V ∧ 𝐵 ∈ 𝑌) → ((𝑊 ↾s 𝐴) ↾s 𝐵) = ((𝑊 ↾s 𝐴) sSet 〈(Base‘ndx), (𝐵 ∩ (Base‘(𝑊 ↾s 𝐴)))〉)) |
29 | 22, 24, 25, 28 | syl3anc 1318 |
. . . . . 6
⊢ (((¬
(Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ ¬
(Base‘𝑊) ⊆
𝐴) ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → ((𝑊 ↾s 𝐴) ↾s 𝐵) = ((𝑊 ↾s 𝐴) sSet 〈(Base‘ndx), (𝐵 ∩ (Base‘(𝑊 ↾s 𝐴)))〉)) |
30 | | inss1 3795 |
. . . . . . . . 9
⊢ (𝐴 ∩ 𝐵) ⊆ 𝐴 |
31 | | sstr 3576 |
. . . . . . . . 9
⊢
(((Base‘𝑊)
⊆ (𝐴 ∩ 𝐵) ∧ (𝐴 ∩ 𝐵) ⊆ 𝐴) → (Base‘𝑊) ⊆ 𝐴) |
32 | 30, 31 | mpan2 703 |
. . . . . . . 8
⊢
((Base‘𝑊)
⊆ (𝐴 ∩ 𝐵) → (Base‘𝑊) ⊆ 𝐴) |
33 | 1, 32 | nsyl 134 |
. . . . . . 7
⊢ (((¬
(Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ ¬
(Base‘𝑊) ⊆
𝐴) ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → ¬ (Base‘𝑊) ⊆ (𝐴 ∩ 𝐵)) |
34 | | inex1g 4729 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝑋 → (𝐴 ∩ 𝐵) ∈ V) |
35 | 3, 34 | syl 17 |
. . . . . . 7
⊢ (((¬
(Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ ¬
(Base‘𝑊) ⊆
𝐴) ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝐴 ∩ 𝐵) ∈ V) |
36 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑊 ↾s (𝐴 ∩ 𝐵)) = (𝑊 ↾s (𝐴 ∩ 𝐵)) |
37 | 36, 5 | ressval2 15756 |
. . . . . . 7
⊢ ((¬
(Base‘𝑊) ⊆
(𝐴 ∩ 𝐵) ∧ 𝑊 ∈ V ∧ (𝐴 ∩ 𝐵) ∈ V) → (𝑊 ↾s (𝐴 ∩ 𝐵)) = (𝑊 sSet 〈(Base‘ndx), ((𝐴 ∩ 𝐵) ∩ (Base‘𝑊))〉)) |
38 | 33, 2, 35, 37 | syl3anc 1318 |
. . . . . 6
⊢ (((¬
(Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ ¬
(Base‘𝑊) ⊆
𝐴) ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝑊 ↾s (𝐴 ∩ 𝐵)) = (𝑊 sSet 〈(Base‘ndx), ((𝐴 ∩ 𝐵) ∩ (Base‘𝑊))〉)) |
39 | 21, 29, 38 | 3eqtr4d 2654 |
. . . . 5
⊢ (((¬
(Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ ¬
(Base‘𝑊) ⊆
𝐴) ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → ((𝑊 ↾s 𝐴) ↾s 𝐵) = (𝑊 ↾s (𝐴 ∩ 𝐵))) |
40 | 39 | exp31 628 |
. . . 4
⊢ (¬
(Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 → (¬
(Base‘𝑊) ⊆
𝐴 → ((𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → ((𝑊 ↾s 𝐴) ↾s 𝐵) = (𝑊 ↾s (𝐴 ∩ 𝐵))))) |
41 | 26, 27 | ressid2 15755 |
. . . . . . . 8
⊢
(((Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ (𝑊 ↾s 𝐴) ∈ V ∧ 𝐵 ∈ 𝑌) → ((𝑊 ↾s 𝐴) ↾s 𝐵) = (𝑊 ↾s 𝐴)) |
42 | 23, 41 | mp3an2 1404 |
. . . . . . 7
⊢
(((Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ 𝐵 ∈ 𝑌) → ((𝑊 ↾s 𝐴) ↾s 𝐵) = (𝑊 ↾s 𝐴)) |
43 | 42 | 3ad2antr3 1221 |
. . . . . 6
⊢
(((Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → ((𝑊 ↾s 𝐴) ↾s 𝐵) = (𝑊 ↾s 𝐴)) |
44 | | in32 3787 |
. . . . . . . . 9
⊢ ((𝐴 ∩ 𝐵) ∩ (Base‘𝑊)) = ((𝐴 ∩ (Base‘𝑊)) ∩ 𝐵) |
45 | | simpr2 1061 |
. . . . . . . . . . . 12
⊢
(((Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → 𝐴 ∈ 𝑋) |
46 | 45, 11 | syl 17 |
. . . . . . . . . . 11
⊢
(((Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝐴 ∩ (Base‘𝑊)) = (Base‘(𝑊 ↾s 𝐴))) |
47 | | simpl 472 |
. . . . . . . . . . 11
⊢
(((Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (Base‘(𝑊 ↾s 𝐴)) ⊆ 𝐵) |
48 | 46, 47 | eqsstrd 3602 |
. . . . . . . . . 10
⊢
(((Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝐴 ∩ (Base‘𝑊)) ⊆ 𝐵) |
49 | | df-ss 3554 |
. . . . . . . . . 10
⊢ ((𝐴 ∩ (Base‘𝑊)) ⊆ 𝐵 ↔ ((𝐴 ∩ (Base‘𝑊)) ∩ 𝐵) = (𝐴 ∩ (Base‘𝑊))) |
50 | 48, 49 | sylib 207 |
. . . . . . . . 9
⊢
(((Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → ((𝐴 ∩ (Base‘𝑊)) ∩ 𝐵) = (𝐴 ∩ (Base‘𝑊))) |
51 | 44, 50 | syl5req 2657 |
. . . . . . . 8
⊢
(((Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝐴 ∩ (Base‘𝑊)) = ((𝐴 ∩ 𝐵) ∩ (Base‘𝑊))) |
52 | 51 | oveq2d 6565 |
. . . . . . 7
⊢
(((Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝑊 ↾s (𝐴 ∩ (Base‘𝑊))) = (𝑊 ↾s ((𝐴 ∩ 𝐵) ∩ (Base‘𝑊)))) |
53 | 5 | ressinbas 15763 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝑋 → (𝑊 ↾s 𝐴) = (𝑊 ↾s (𝐴 ∩ (Base‘𝑊)))) |
54 | 45, 53 | syl 17 |
. . . . . . 7
⊢
(((Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝑊 ↾s 𝐴) = (𝑊 ↾s (𝐴 ∩ (Base‘𝑊)))) |
55 | 5 | ressinbas 15763 |
. . . . . . . 8
⊢ ((𝐴 ∩ 𝐵) ∈ V → (𝑊 ↾s (𝐴 ∩ 𝐵)) = (𝑊 ↾s ((𝐴 ∩ 𝐵) ∩ (Base‘𝑊)))) |
56 | 45, 34, 55 | 3syl 18 |
. . . . . . 7
⊢
(((Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝑊 ↾s (𝐴 ∩ 𝐵)) = (𝑊 ↾s ((𝐴 ∩ 𝐵) ∩ (Base‘𝑊)))) |
57 | 52, 54, 56 | 3eqtr4d 2654 |
. . . . . 6
⊢
(((Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝑊 ↾s 𝐴) = (𝑊 ↾s (𝐴 ∩ 𝐵))) |
58 | 43, 57 | eqtrd 2644 |
. . . . 5
⊢
(((Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → ((𝑊 ↾s 𝐴) ↾s 𝐵) = (𝑊 ↾s (𝐴 ∩ 𝐵))) |
59 | 58 | ex 449 |
. . . 4
⊢
((Base‘(𝑊
↾s 𝐴))
⊆ 𝐵 → ((𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → ((𝑊 ↾s 𝐴) ↾s 𝐵) = (𝑊 ↾s (𝐴 ∩ 𝐵)))) |
60 | 4, 5 | ressid2 15755 |
. . . . . . . 8
⊢
(((Base‘𝑊)
⊆ 𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ 𝑋) → (𝑊 ↾s 𝐴) = 𝑊) |
61 | 60 | 3adant3r3 1268 |
. . . . . . 7
⊢
(((Base‘𝑊)
⊆ 𝐴 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝑊 ↾s 𝐴) = 𝑊) |
62 | 61 | oveq1d 6564 |
. . . . . 6
⊢
(((Base‘𝑊)
⊆ 𝐴 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → ((𝑊 ↾s 𝐴) ↾s 𝐵) = (𝑊 ↾s 𝐵)) |
63 | | inss2 3796 |
. . . . . . . . . . 11
⊢ (𝐵 ∩ (Base‘𝑊)) ⊆ (Base‘𝑊) |
64 | | simpl 472 |
. . . . . . . . . . 11
⊢
(((Base‘𝑊)
⊆ 𝐴 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (Base‘𝑊) ⊆ 𝐴) |
65 | 63, 64 | syl5ss 3579 |
. . . . . . . . . 10
⊢
(((Base‘𝑊)
⊆ 𝐴 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝐵 ∩ (Base‘𝑊)) ⊆ 𝐴) |
66 | | sseqin2 3779 |
. . . . . . . . . 10
⊢ ((𝐵 ∩ (Base‘𝑊)) ⊆ 𝐴 ↔ (𝐴 ∩ (𝐵 ∩ (Base‘𝑊))) = (𝐵 ∩ (Base‘𝑊))) |
67 | 65, 66 | sylib 207 |
. . . . . . . . 9
⊢
(((Base‘𝑊)
⊆ 𝐴 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝐴 ∩ (𝐵 ∩ (Base‘𝑊))) = (𝐵 ∩ (Base‘𝑊))) |
68 | 8, 67 | syl5req 2657 |
. . . . . . . 8
⊢
(((Base‘𝑊)
⊆ 𝐴 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝐵 ∩ (Base‘𝑊)) = ((𝐴 ∩ 𝐵) ∩ (Base‘𝑊))) |
69 | 68 | oveq2d 6565 |
. . . . . . 7
⊢
(((Base‘𝑊)
⊆ 𝐴 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝑊 ↾s (𝐵 ∩ (Base‘𝑊))) = (𝑊 ↾s ((𝐴 ∩ 𝐵) ∩ (Base‘𝑊)))) |
70 | | simpr3 1062 |
. . . . . . . 8
⊢
(((Base‘𝑊)
⊆ 𝐴 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → 𝐵 ∈ 𝑌) |
71 | 5 | ressinbas 15763 |
. . . . . . . 8
⊢ (𝐵 ∈ 𝑌 → (𝑊 ↾s 𝐵) = (𝑊 ↾s (𝐵 ∩ (Base‘𝑊)))) |
72 | 70, 71 | syl 17 |
. . . . . . 7
⊢
(((Base‘𝑊)
⊆ 𝐴 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝑊 ↾s 𝐵) = (𝑊 ↾s (𝐵 ∩ (Base‘𝑊)))) |
73 | | simpr2 1061 |
. . . . . . . 8
⊢
(((Base‘𝑊)
⊆ 𝐴 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → 𝐴 ∈ 𝑋) |
74 | 73, 34, 55 | 3syl 18 |
. . . . . . 7
⊢
(((Base‘𝑊)
⊆ 𝐴 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝑊 ↾s (𝐴 ∩ 𝐵)) = (𝑊 ↾s ((𝐴 ∩ 𝐵) ∩ (Base‘𝑊)))) |
75 | 69, 72, 74 | 3eqtr4d 2654 |
. . . . . 6
⊢
(((Base‘𝑊)
⊆ 𝐴 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝑊 ↾s 𝐵) = (𝑊 ↾s (𝐴 ∩ 𝐵))) |
76 | 62, 75 | eqtrd 2644 |
. . . . 5
⊢
(((Base‘𝑊)
⊆ 𝐴 ∧ (𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → ((𝑊 ↾s 𝐴) ↾s 𝐵) = (𝑊 ↾s (𝐴 ∩ 𝐵))) |
77 | 76 | ex 449 |
. . . 4
⊢
((Base‘𝑊)
⊆ 𝐴 → ((𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → ((𝑊 ↾s 𝐴) ↾s 𝐵) = (𝑊 ↾s (𝐴 ∩ 𝐵)))) |
78 | 40, 59, 77 | pm2.61ii 176 |
. . 3
⊢ ((𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → ((𝑊 ↾s 𝐴) ↾s 𝐵) = (𝑊 ↾s (𝐴 ∩ 𝐵))) |
79 | 78 | 3expib 1260 |
. 2
⊢ (𝑊 ∈ V → ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → ((𝑊 ↾s 𝐴) ↾s 𝐵) = (𝑊 ↾s (𝐴 ∩ 𝐵)))) |
80 | | ress0 15761 |
. . . 4
⊢ (∅
↾s 𝐵) =
∅ |
81 | | reldmress 15753 |
. . . . . 6
⊢ Rel dom
↾s |
82 | 81 | ovprc1 6582 |
. . . . 5
⊢ (¬
𝑊 ∈ V → (𝑊 ↾s 𝐴) = ∅) |
83 | 82 | oveq1d 6564 |
. . . 4
⊢ (¬
𝑊 ∈ V → ((𝑊 ↾s 𝐴) ↾s 𝐵) = (∅ ↾s
𝐵)) |
84 | 81 | ovprc1 6582 |
. . . 4
⊢ (¬
𝑊 ∈ V → (𝑊 ↾s (𝐴 ∩ 𝐵)) = ∅) |
85 | 80, 83, 84 | 3eqtr4a 2670 |
. . 3
⊢ (¬
𝑊 ∈ V → ((𝑊 ↾s 𝐴) ↾s 𝐵) = (𝑊 ↾s (𝐴 ∩ 𝐵))) |
86 | 85 | a1d 25 |
. 2
⊢ (¬
𝑊 ∈ V → ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → ((𝑊 ↾s 𝐴) ↾s 𝐵) = (𝑊 ↾s (𝐴 ∩ 𝐵)))) |
87 | 79, 86 | pm2.61i 175 |
1
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → ((𝑊 ↾s 𝐴) ↾s 𝐵) = (𝑊 ↾s (𝐴 ∩ 𝐵))) |