| Step | Hyp | Ref
| Expression |
| 1 | | elxp7 8049 |
. . . . . 6
⊢ (𝑤 ∈ (𝐵 × 𝐶) ↔ (𝑤 ∈ (V × V) ∧ ((1st
‘𝑤) ∈ 𝐵 ∧ (2nd
‘𝑤) ∈ 𝐶))) |
| 2 | 1 | anbi2i 623 |
. . . . 5
⊢
(((1st ‘𝑤) ∈ 𝐴 ∧ 𝑤 ∈ (𝐵 × 𝐶)) ↔ ((1st ‘𝑤) ∈ 𝐴 ∧ (𝑤 ∈ (V × V) ∧ ((1st
‘𝑤) ∈ 𝐵 ∧ (2nd
‘𝑤) ∈ 𝐶)))) |
| 3 | | anass 468 |
. . . . . . 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 3977 |
. . . . . . . 8
⊢ (𝐴 ⊆ 𝐵 → ((1st ‘𝑤) ∈ 𝐴 → (1st ‘𝑤) ∈ 𝐵)) |
| 6 | 5 | pm4.71d 561 |
. . . . . . 7
⊢ (𝐴 ⊆ 𝐵 → ((1st ‘𝑤) ∈ 𝐴 ↔ ((1st ‘𝑤) ∈ 𝐴 ∧ (1st ‘𝑤) ∈ 𝐵))) |
| 7 | 6 | anbi1d 631 |
. . . . . 6
⊢ (𝐴 ⊆ 𝐵 → (((1st ‘𝑤) ∈ 𝐴 ∧ (𝑤 ∈ (V × V) ∧ (2nd
‘𝑤) ∈ 𝐶)) ↔ (((1st
‘𝑤) ∈ 𝐴 ∧ (1st
‘𝑤) ∈ 𝐵) ∧ (𝑤 ∈ (V × V) ∧ (2nd
‘𝑤) ∈ 𝐶)))) |
| 8 | | an12 645 |
. . . . . . . 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 645 |
. . . 4
⊢
(((1st ‘𝑤) ∈ 𝐴 ∧ (𝑤 ∈ (V × V) ∧ (2nd
‘𝑤) ∈ 𝐶)) ↔ (𝑤 ∈ (V × V) ∧ ((1st
‘𝑤) ∈ 𝐴 ∧ (2nd
‘𝑤) ∈ 𝐶))) |
| 14 | 12, 13 | bitrdi 287 |
. . 3
⊢ (𝐴 ⊆ 𝐵 → (((1st ‘𝑤) ∈ 𝐴 ∧ 𝑤 ∈ (𝐵 × 𝐶)) ↔ (𝑤 ∈ (V × V) ∧ ((1st
‘𝑤) ∈ 𝐴 ∧ (2nd
‘𝑤) ∈ 𝐶)))) |
| 15 | | cnvresima 6250 |
. . . . 5
⊢ (◡(1st ↾ (𝐵 × 𝐶)) “ 𝐴) = ((◡1st “ 𝐴) ∩ (𝐵 × 𝐶)) |
| 16 | 15 | eleq2i 2833 |
. . . 4
⊢ (𝑤 ∈ (◡(1st ↾ (𝐵 × 𝐶)) “ 𝐴) ↔ 𝑤 ∈ ((◡1st “ 𝐴) ∩ (𝐵 × 𝐶))) |
| 17 | | elin 3967 |
. . . 4
⊢ (𝑤 ∈ ((◡1st “ 𝐴) ∩ (𝐵 × 𝐶)) ↔ (𝑤 ∈ (◡1st “ 𝐴) ∧ 𝑤 ∈ (𝐵 × 𝐶))) |
| 18 | | vex 3484 |
. . . . . 6
⊢ 𝑤 ∈ V |
| 19 | | fo1st 8034 |
. . . . . . 7
⊢
1st :V–onto→V |
| 20 | | fofn 6822 |
. . . . . . 7
⊢
(1st :V–onto→V → 1st Fn V) |
| 21 | | elpreima 7078 |
. . . . . . 7
⊢
(1st Fn V → (𝑤 ∈ (◡1st “ 𝐴) ↔ (𝑤 ∈ V ∧ (1st ‘𝑤) ∈ 𝐴))) |
| 22 | 19, 20, 21 | mp2b 10 |
. . . . . 6
⊢ (𝑤 ∈ (◡1st “ 𝐴) ↔ (𝑤 ∈ V ∧ (1st ‘𝑤) ∈ 𝐴)) |
| 23 | 18, 22 | mpbiran 709 |
. . . . 5
⊢ (𝑤 ∈ (◡1st “ 𝐴) ↔ (1st ‘𝑤) ∈ 𝐴) |
| 24 | 23 | anbi1i 624 |
. . . 4
⊢ ((𝑤 ∈ (◡1st “ 𝐴) ∧ 𝑤 ∈ (𝐵 × 𝐶)) ↔ ((1st ‘𝑤) ∈ 𝐴 ∧ 𝑤 ∈ (𝐵 × 𝐶))) |
| 25 | 16, 17, 24 | 3bitri 297 |
. . 3
⊢ (𝑤 ∈ (◡(1st ↾ (𝐵 × 𝐶)) “ 𝐴) ↔ ((1st ‘𝑤) ∈ 𝐴 ∧ 𝑤 ∈ (𝐵 × 𝐶))) |
| 26 | | elxp7 8049 |
. . 3
⊢ (𝑤 ∈ (𝐴 × 𝐶) ↔ (𝑤 ∈ (V × V) ∧ ((1st
‘𝑤) ∈ 𝐴 ∧ (2nd
‘𝑤) ∈ 𝐶))) |
| 27 | 14, 25, 26 | 3bitr4g 314 |
. 2
⊢ (𝐴 ⊆ 𝐵 → (𝑤 ∈ (◡(1st ↾ (𝐵 × 𝐶)) “ 𝐴) ↔ 𝑤 ∈ (𝐴 × 𝐶))) |
| 28 | 27 | eqrdv 2735 |
1
⊢ (𝐴 ⊆ 𝐵 → (◡(1st ↾ (𝐵 × 𝐶)) “ 𝐴) = (𝐴 × 𝐶)) |