Step | Hyp | Ref
| Expression |
1 | | elxp7 7866 |
. . . . . 6
⊢ (𝑤 ∈ (𝐵 × 𝐶) ↔ (𝑤 ∈ (V × V) ∧ ((1st
‘𝑤) ∈ 𝐵 ∧ (2nd
‘𝑤) ∈ 𝐶))) |
2 | 1 | anbi2i 623 |
. . . . 5
⊢
(((1st ‘𝑤) ∈ 𝐴 ∧ 𝑤 ∈ (𝐵 × 𝐶)) ↔ ((1st ‘𝑤) ∈ 𝐴 ∧ (𝑤 ∈ (V × V) ∧ ((1st
‘𝑤) ∈ 𝐵 ∧ (2nd
‘𝑤) ∈ 𝐶)))) |
3 | | anass 469 |
. . . . . . 7
⊢
((((1st ‘𝑤) ∈ 𝐴 ∧ (1st ‘𝑤) ∈ 𝐵) ∧ (𝑤 ∈ (V × V) ∧ (2nd
‘𝑤) ∈ 𝐶)) ↔ ((1st
‘𝑤) ∈ 𝐴 ∧ ((1st
‘𝑤) ∈ 𝐵 ∧ (𝑤 ∈ (V × V) ∧ (2nd
‘𝑤) ∈ 𝐶)))) |
4 | 3 | a1i 11 |
. . . . . 6
⊢ (𝐴 ⊆ 𝐵 → ((((1st ‘𝑤) ∈ 𝐴 ∧ (1st ‘𝑤) ∈ 𝐵) ∧ (𝑤 ∈ (V × V) ∧ (2nd
‘𝑤) ∈ 𝐶)) ↔ ((1st
‘𝑤) ∈ 𝐴 ∧ ((1st
‘𝑤) ∈ 𝐵 ∧ (𝑤 ∈ (V × V) ∧ (2nd
‘𝑤) ∈ 𝐶))))) |
5 | | ssel 3915 |
. . . . . . . 8
⊢ (𝐴 ⊆ 𝐵 → ((1st ‘𝑤) ∈ 𝐴 → (1st ‘𝑤) ∈ 𝐵)) |
6 | 5 | pm4.71d 562 |
. . . . . . 7
⊢ (𝐴 ⊆ 𝐵 → ((1st ‘𝑤) ∈ 𝐴 ↔ ((1st ‘𝑤) ∈ 𝐴 ∧ (1st ‘𝑤) ∈ 𝐵))) |
7 | 6 | anbi1d 630 |
. . . . . 6
⊢ (𝐴 ⊆ 𝐵 → (((1st ‘𝑤) ∈ 𝐴 ∧ (𝑤 ∈ (V × V) ∧ (2nd
‘𝑤) ∈ 𝐶)) ↔ (((1st
‘𝑤) ∈ 𝐴 ∧ (1st
‘𝑤) ∈ 𝐵) ∧ (𝑤 ∈ (V × V) ∧ (2nd
‘𝑤) ∈ 𝐶)))) |
8 | | an12 642 |
. . . . . . . 8
⊢ ((𝑤 ∈ (V × V) ∧
((1st ‘𝑤)
∈ 𝐵 ∧
(2nd ‘𝑤)
∈ 𝐶)) ↔
((1st ‘𝑤)
∈ 𝐵 ∧ (𝑤 ∈ (V × V) ∧
(2nd ‘𝑤)
∈ 𝐶))) |
9 | 8 | anbi2i 623 |
. . . . . . 7
⊢
(((1st ‘𝑤) ∈ 𝐴 ∧ (𝑤 ∈ (V × V) ∧ ((1st
‘𝑤) ∈ 𝐵 ∧ (2nd
‘𝑤) ∈ 𝐶))) ↔ ((1st
‘𝑤) ∈ 𝐴 ∧ ((1st
‘𝑤) ∈ 𝐵 ∧ (𝑤 ∈ (V × V) ∧ (2nd
‘𝑤) ∈ 𝐶)))) |
10 | 9 | a1i 11 |
. . . . . 6
⊢ (𝐴 ⊆ 𝐵 → (((1st ‘𝑤) ∈ 𝐴 ∧ (𝑤 ∈ (V × V) ∧ ((1st
‘𝑤) ∈ 𝐵 ∧ (2nd
‘𝑤) ∈ 𝐶))) ↔ ((1st
‘𝑤) ∈ 𝐴 ∧ ((1st
‘𝑤) ∈ 𝐵 ∧ (𝑤 ∈ (V × V) ∧ (2nd
‘𝑤) ∈ 𝐶))))) |
11 | 4, 7, 10 | 3bitr4d 311 |
. . . . 5
⊢ (𝐴 ⊆ 𝐵 → (((1st ‘𝑤) ∈ 𝐴 ∧ (𝑤 ∈ (V × V) ∧ (2nd
‘𝑤) ∈ 𝐶)) ↔ ((1st
‘𝑤) ∈ 𝐴 ∧ (𝑤 ∈ (V × V) ∧ ((1st
‘𝑤) ∈ 𝐵 ∧ (2nd
‘𝑤) ∈ 𝐶))))) |
12 | 2, 11 | bitr4id 290 |
. . . 4
⊢ (𝐴 ⊆ 𝐵 → (((1st ‘𝑤) ∈ 𝐴 ∧ 𝑤 ∈ (𝐵 × 𝐶)) ↔ ((1st ‘𝑤) ∈ 𝐴 ∧ (𝑤 ∈ (V × V) ∧ (2nd
‘𝑤) ∈ 𝐶)))) |
13 | | an12 642 |
. . . 4
⊢
(((1st ‘𝑤) ∈ 𝐴 ∧ (𝑤 ∈ (V × V) ∧ (2nd
‘𝑤) ∈ 𝐶)) ↔ (𝑤 ∈ (V × V) ∧ ((1st
‘𝑤) ∈ 𝐴 ∧ (2nd
‘𝑤) ∈ 𝐶))) |
14 | 12, 13 | bitrdi 287 |
. . 3
⊢ (𝐴 ⊆ 𝐵 → (((1st ‘𝑤) ∈ 𝐴 ∧ 𝑤 ∈ (𝐵 × 𝐶)) ↔ (𝑤 ∈ (V × V) ∧ ((1st
‘𝑤) ∈ 𝐴 ∧ (2nd
‘𝑤) ∈ 𝐶)))) |
15 | | cnvresima 6135 |
. . . . 5
⊢ (◡(1st ↾ (𝐵 × 𝐶)) “ 𝐴) = ((◡1st “ 𝐴) ∩ (𝐵 × 𝐶)) |
16 | 15 | eleq2i 2830 |
. . . 4
⊢ (𝑤 ∈ (◡(1st ↾ (𝐵 × 𝐶)) “ 𝐴) ↔ 𝑤 ∈ ((◡1st “ 𝐴) ∩ (𝐵 × 𝐶))) |
17 | | elin 3904 |
. . . 4
⊢ (𝑤 ∈ ((◡1st “ 𝐴) ∩ (𝐵 × 𝐶)) ↔ (𝑤 ∈ (◡1st “ 𝐴) ∧ 𝑤 ∈ (𝐵 × 𝐶))) |
18 | | vex 3435 |
. . . . . 6
⊢ 𝑤 ∈ V |
19 | | fo1st 7851 |
. . . . . . 7
⊢
1st :V–onto→V |
20 | | fofn 6692 |
. . . . . . 7
⊢
(1st :V–onto→V → 1st Fn V) |
21 | | elpreima 6937 |
. . . . . . 7
⊢
(1st Fn V → (𝑤 ∈ (◡1st “ 𝐴) ↔ (𝑤 ∈ V ∧ (1st ‘𝑤) ∈ 𝐴))) |
22 | 19, 20, 21 | mp2b 10 |
. . . . . 6
⊢ (𝑤 ∈ (◡1st “ 𝐴) ↔ (𝑤 ∈ V ∧ (1st ‘𝑤) ∈ 𝐴)) |
23 | 18, 22 | mpbiran 706 |
. . . . 5
⊢ (𝑤 ∈ (◡1st “ 𝐴) ↔ (1st ‘𝑤) ∈ 𝐴) |
24 | 23 | anbi1i 624 |
. . . 4
⊢ ((𝑤 ∈ (◡1st “ 𝐴) ∧ 𝑤 ∈ (𝐵 × 𝐶)) ↔ ((1st ‘𝑤) ∈ 𝐴 ∧ 𝑤 ∈ (𝐵 × 𝐶))) |
25 | 16, 17, 24 | 3bitri 297 |
. . 3
⊢ (𝑤 ∈ (◡(1st ↾ (𝐵 × 𝐶)) “ 𝐴) ↔ ((1st ‘𝑤) ∈ 𝐴 ∧ 𝑤 ∈ (𝐵 × 𝐶))) |
26 | | elxp7 7866 |
. . 3
⊢ (𝑤 ∈ (𝐴 × 𝐶) ↔ (𝑤 ∈ (V × V) ∧ ((1st
‘𝑤) ∈ 𝐴 ∧ (2nd
‘𝑤) ∈ 𝐶))) |
27 | 14, 25, 26 | 3bitr4g 314 |
. 2
⊢ (𝐴 ⊆ 𝐵 → (𝑤 ∈ (◡(1st ↾ (𝐵 × 𝐶)) “ 𝐴) ↔ 𝑤 ∈ (𝐴 × 𝐶))) |
28 | 27 | eqrdv 2736 |
1
⊢ (𝐴 ⊆ 𝐵 → (◡(1st ↾ (𝐵 × 𝐶)) “ 𝐴) = (𝐴 × 𝐶)) |