Step | Hyp | Ref
| Expression |
1 | | anass 461 |
. . . . . . 7
⊢
((((1st ‘𝑤) ∈ 𝐴 ∧ (1st ‘𝑤) ∈ 𝐵) ∧ (𝑤 ∈ (V × V) ∧ (2nd
‘𝑤) ∈ 𝐶)) ↔ ((1st
‘𝑤) ∈ 𝐴 ∧ ((1st
‘𝑤) ∈ 𝐵 ∧ (𝑤 ∈ (V × V) ∧ (2nd
‘𝑤) ∈ 𝐶)))) |
2 | 1 | a1i 11 |
. . . . . 6
⊢ (𝐴 ⊆ 𝐵 → ((((1st ‘𝑤) ∈ 𝐴 ∧ (1st ‘𝑤) ∈ 𝐵) ∧ (𝑤 ∈ (V × V) ∧ (2nd
‘𝑤) ∈ 𝐶)) ↔ ((1st
‘𝑤) ∈ 𝐴 ∧ ((1st
‘𝑤) ∈ 𝐵 ∧ (𝑤 ∈ (V × V) ∧ (2nd
‘𝑤) ∈ 𝐶))))) |
3 | | ssel 3848 |
. . . . . . . 8
⊢ (𝐴 ⊆ 𝐵 → ((1st ‘𝑤) ∈ 𝐴 → (1st ‘𝑤) ∈ 𝐵)) |
4 | 3 | pm4.71d 554 |
. . . . . . 7
⊢ (𝐴 ⊆ 𝐵 → ((1st ‘𝑤) ∈ 𝐴 ↔ ((1st ‘𝑤) ∈ 𝐴 ∧ (1st ‘𝑤) ∈ 𝐵))) |
5 | 4 | anbi1d 620 |
. . . . . 6
⊢ (𝐴 ⊆ 𝐵 → (((1st ‘𝑤) ∈ 𝐴 ∧ (𝑤 ∈ (V × V) ∧ (2nd
‘𝑤) ∈ 𝐶)) ↔ (((1st
‘𝑤) ∈ 𝐴 ∧ (1st
‘𝑤) ∈ 𝐵) ∧ (𝑤 ∈ (V × V) ∧ (2nd
‘𝑤) ∈ 𝐶)))) |
6 | | an12 632 |
. . . . . . . 8
⊢ ((𝑤 ∈ (V × V) ∧
((1st ‘𝑤)
∈ 𝐵 ∧
(2nd ‘𝑤)
∈ 𝐶)) ↔
((1st ‘𝑤)
∈ 𝐵 ∧ (𝑤 ∈ (V × V) ∧
(2nd ‘𝑤)
∈ 𝐶))) |
7 | 6 | anbi2i 613 |
. . . . . . 7
⊢
(((1st ‘𝑤) ∈ 𝐴 ∧ (𝑤 ∈ (V × V) ∧ ((1st
‘𝑤) ∈ 𝐵 ∧ (2nd
‘𝑤) ∈ 𝐶))) ↔ ((1st
‘𝑤) ∈ 𝐴 ∧ ((1st
‘𝑤) ∈ 𝐵 ∧ (𝑤 ∈ (V × V) ∧ (2nd
‘𝑤) ∈ 𝐶)))) |
8 | 7 | a1i 11 |
. . . . . 6
⊢ (𝐴 ⊆ 𝐵 → (((1st ‘𝑤) ∈ 𝐴 ∧ (𝑤 ∈ (V × V) ∧ ((1st
‘𝑤) ∈ 𝐵 ∧ (2nd
‘𝑤) ∈ 𝐶))) ↔ ((1st
‘𝑤) ∈ 𝐴 ∧ ((1st
‘𝑤) ∈ 𝐵 ∧ (𝑤 ∈ (V × V) ∧ (2nd
‘𝑤) ∈ 𝐶))))) |
9 | 2, 5, 8 | 3bitr4d 303 |
. . . . 5
⊢ (𝐴 ⊆ 𝐵 → (((1st ‘𝑤) ∈ 𝐴 ∧ (𝑤 ∈ (V × V) ∧ (2nd
‘𝑤) ∈ 𝐶)) ↔ ((1st
‘𝑤) ∈ 𝐴 ∧ (𝑤 ∈ (V × V) ∧ ((1st
‘𝑤) ∈ 𝐵 ∧ (2nd
‘𝑤) ∈ 𝐶))))) |
10 | | elxp7 7529 |
. . . . . 6
⊢ (𝑤 ∈ (𝐵 × 𝐶) ↔ (𝑤 ∈ (V × V) ∧ ((1st
‘𝑤) ∈ 𝐵 ∧ (2nd
‘𝑤) ∈ 𝐶))) |
11 | 10 | anbi2i 613 |
. . . . 5
⊢
(((1st ‘𝑤) ∈ 𝐴 ∧ 𝑤 ∈ (𝐵 × 𝐶)) ↔ ((1st ‘𝑤) ∈ 𝐴 ∧ (𝑤 ∈ (V × V) ∧ ((1st
‘𝑤) ∈ 𝐵 ∧ (2nd
‘𝑤) ∈ 𝐶)))) |
12 | 9, 11 | syl6rbbr 282 |
. . . 4
⊢ (𝐴 ⊆ 𝐵 → (((1st ‘𝑤) ∈ 𝐴 ∧ 𝑤 ∈ (𝐵 × 𝐶)) ↔ ((1st ‘𝑤) ∈ 𝐴 ∧ (𝑤 ∈ (V × V) ∧ (2nd
‘𝑤) ∈ 𝐶)))) |
13 | | an12 632 |
. . . 4
⊢
(((1st ‘𝑤) ∈ 𝐴 ∧ (𝑤 ∈ (V × V) ∧ (2nd
‘𝑤) ∈ 𝐶)) ↔ (𝑤 ∈ (V × V) ∧ ((1st
‘𝑤) ∈ 𝐴 ∧ (2nd
‘𝑤) ∈ 𝐶))) |
14 | 12, 13 | syl6bb 279 |
. . 3
⊢ (𝐴 ⊆ 𝐵 → (((1st ‘𝑤) ∈ 𝐴 ∧ 𝑤 ∈ (𝐵 × 𝐶)) ↔ (𝑤 ∈ (V × V) ∧ ((1st
‘𝑤) ∈ 𝐴 ∧ (2nd
‘𝑤) ∈ 𝐶)))) |
15 | | cnvresima 5920 |
. . . . 5
⊢ (◡(1st ↾ (𝐵 × 𝐶)) “ 𝐴) = ((◡1st “ 𝐴) ∩ (𝐵 × 𝐶)) |
16 | 15 | eleq2i 2851 |
. . . 4
⊢ (𝑤 ∈ (◡(1st ↾ (𝐵 × 𝐶)) “ 𝐴) ↔ 𝑤 ∈ ((◡1st “ 𝐴) ∩ (𝐵 × 𝐶))) |
17 | | elin 4053 |
. . . 4
⊢ (𝑤 ∈ ((◡1st “ 𝐴) ∩ (𝐵 × 𝐶)) ↔ (𝑤 ∈ (◡1st “ 𝐴) ∧ 𝑤 ∈ (𝐵 × 𝐶))) |
18 | | vex 3412 |
. . . . . 6
⊢ 𝑤 ∈ V |
19 | | fo1st 7514 |
. . . . . . 7
⊢
1st :V–onto→V |
20 | | fofn 6415 |
. . . . . . 7
⊢
(1st :V–onto→V → 1st Fn V) |
21 | | elpreima 6647 |
. . . . . . 7
⊢
(1st Fn V → (𝑤 ∈ (◡1st “ 𝐴) ↔ (𝑤 ∈ V ∧ (1st ‘𝑤) ∈ 𝐴))) |
22 | 19, 20, 21 | mp2b 10 |
. . . . . 6
⊢ (𝑤 ∈ (◡1st “ 𝐴) ↔ (𝑤 ∈ V ∧ (1st ‘𝑤) ∈ 𝐴)) |
23 | 18, 22 | mpbiran 696 |
. . . . 5
⊢ (𝑤 ∈ (◡1st “ 𝐴) ↔ (1st ‘𝑤) ∈ 𝐴) |
24 | 23 | anbi1i 614 |
. . . 4
⊢ ((𝑤 ∈ (◡1st “ 𝐴) ∧ 𝑤 ∈ (𝐵 × 𝐶)) ↔ ((1st ‘𝑤) ∈ 𝐴 ∧ 𝑤 ∈ (𝐵 × 𝐶))) |
25 | 16, 17, 24 | 3bitri 289 |
. . 3
⊢ (𝑤 ∈ (◡(1st ↾ (𝐵 × 𝐶)) “ 𝐴) ↔ ((1st ‘𝑤) ∈ 𝐴 ∧ 𝑤 ∈ (𝐵 × 𝐶))) |
26 | | elxp7 7529 |
. . 3
⊢ (𝑤 ∈ (𝐴 × 𝐶) ↔ (𝑤 ∈ (V × V) ∧ ((1st
‘𝑤) ∈ 𝐴 ∧ (2nd
‘𝑤) ∈ 𝐶))) |
27 | 14, 25, 26 | 3bitr4g 306 |
. 2
⊢ (𝐴 ⊆ 𝐵 → (𝑤 ∈ (◡(1st ↾ (𝐵 × 𝐶)) “ 𝐴) ↔ 𝑤 ∈ (𝐴 × 𝐶))) |
28 | 27 | eqrdv 2770 |
1
⊢ (𝐴 ⊆ 𝐵 → (◡(1st ↾ (𝐵 × 𝐶)) “ 𝐴) = (𝐴 × 𝐶)) |