Step | Hyp | Ref
| Expression |
1 | | anass 681 |
. . . . . . 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 3597 |
. . . . . . . 8
⊢ (𝐴 ⊆ 𝐵 → ((1st ‘𝑤) ∈ 𝐴 → (1st ‘𝑤) ∈ 𝐵)) |
4 | 3 | pm4.71d 666 |
. . . . . . 7
⊢ (𝐴 ⊆ 𝐵 → ((1st ‘𝑤) ∈ 𝐴 ↔ ((1st ‘𝑤) ∈ 𝐴 ∧ (1st ‘𝑤) ∈ 𝐵))) |
5 | 4 | anbi1d 741 |
. . . . . 6
⊢ (𝐴 ⊆ 𝐵 → (((1st ‘𝑤) ∈ 𝐴 ∧ (𝑤 ∈ (V × V) ∧ (2nd
‘𝑤) ∈ 𝐶)) ↔ (((1st
‘𝑤) ∈ 𝐴 ∧ (1st
‘𝑤) ∈ 𝐵) ∧ (𝑤 ∈ (V × V) ∧ (2nd
‘𝑤) ∈ 𝐶)))) |
6 | | an12 838 |
. . . . . . . 8
⊢ ((𝑤 ∈ (V × V) ∧
((1st ‘𝑤)
∈ 𝐵 ∧
(2nd ‘𝑤)
∈ 𝐶)) ↔
((1st ‘𝑤)
∈ 𝐵 ∧ (𝑤 ∈ (V × V) ∧
(2nd ‘𝑤)
∈ 𝐶))) |
7 | 6 | anbi2i 730 |
. . . . . . 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 300 |
. . . . 5
⊢ (𝐴 ⊆ 𝐵 → (((1st ‘𝑤) ∈ 𝐴 ∧ (𝑤 ∈ (V × V) ∧ (2nd
‘𝑤) ∈ 𝐶)) ↔ ((1st
‘𝑤) ∈ 𝐴 ∧ (𝑤 ∈ (V × V) ∧ ((1st
‘𝑤) ∈ 𝐵 ∧ (2nd
‘𝑤) ∈ 𝐶))))) |
10 | | elxp7 7201 |
. . . . . 6
⊢ (𝑤 ∈ (𝐵 × 𝐶) ↔ (𝑤 ∈ (V × V) ∧ ((1st
‘𝑤) ∈ 𝐵 ∧ (2nd
‘𝑤) ∈ 𝐶))) |
11 | 10 | anbi2i 730 |
. . . . 5
⊢
(((1st ‘𝑤) ∈ 𝐴 ∧ 𝑤 ∈ (𝐵 × 𝐶)) ↔ ((1st ‘𝑤) ∈ 𝐴 ∧ (𝑤 ∈ (V × V) ∧ ((1st
‘𝑤) ∈ 𝐵 ∧ (2nd
‘𝑤) ∈ 𝐶)))) |
12 | 9, 11 | syl6rbbr 279 |
. . . 4
⊢ (𝐴 ⊆ 𝐵 → (((1st ‘𝑤) ∈ 𝐴 ∧ 𝑤 ∈ (𝐵 × 𝐶)) ↔ ((1st ‘𝑤) ∈ 𝐴 ∧ (𝑤 ∈ (V × V) ∧ (2nd
‘𝑤) ∈ 𝐶)))) |
13 | | an12 838 |
. . . 4
⊢
(((1st ‘𝑤) ∈ 𝐴 ∧ (𝑤 ∈ (V × V) ∧ (2nd
‘𝑤) ∈ 𝐶)) ↔ (𝑤 ∈ (V × V) ∧ ((1st
‘𝑤) ∈ 𝐴 ∧ (2nd
‘𝑤) ∈ 𝐶))) |
14 | 12, 13 | syl6bb 276 |
. . 3
⊢ (𝐴 ⊆ 𝐵 → (((1st ‘𝑤) ∈ 𝐴 ∧ 𝑤 ∈ (𝐵 × 𝐶)) ↔ (𝑤 ∈ (V × V) ∧ ((1st
‘𝑤) ∈ 𝐴 ∧ (2nd
‘𝑤) ∈ 𝐶)))) |
15 | | cnvresima 5623 |
. . . . 5
⊢ (◡(1st ↾ (𝐵 × 𝐶)) “ 𝐴) = ((◡1st “ 𝐴) ∩ (𝐵 × 𝐶)) |
16 | 15 | eleq2i 2693 |
. . . 4
⊢ (𝑤 ∈ (◡(1st ↾ (𝐵 × 𝐶)) “ 𝐴) ↔ 𝑤 ∈ ((◡1st “ 𝐴) ∩ (𝐵 × 𝐶))) |
17 | | elin 3796 |
. . . 4
⊢ (𝑤 ∈ ((◡1st “ 𝐴) ∩ (𝐵 × 𝐶)) ↔ (𝑤 ∈ (◡1st “ 𝐴) ∧ 𝑤 ∈ (𝐵 × 𝐶))) |
18 | | vex 3203 |
. . . . . 6
⊢ 𝑤 ∈ V |
19 | | fo1st 7188 |
. . . . . . 7
⊢
1st :V–onto→V |
20 | | fofn 6117 |
. . . . . . 7
⊢
(1st :V–onto→V → 1st Fn V) |
21 | | elpreima 6337 |
. . . . . . 7
⊢
(1st Fn V → (𝑤 ∈ (◡1st “ 𝐴) ↔ (𝑤 ∈ V ∧ (1st ‘𝑤) ∈ 𝐴))) |
22 | 19, 20, 21 | mp2b 10 |
. . . . . 6
⊢ (𝑤 ∈ (◡1st “ 𝐴) ↔ (𝑤 ∈ V ∧ (1st ‘𝑤) ∈ 𝐴)) |
23 | 18, 22 | mpbiran 953 |
. . . . 5
⊢ (𝑤 ∈ (◡1st “ 𝐴) ↔ (1st ‘𝑤) ∈ 𝐴) |
24 | 23 | anbi1i 731 |
. . . 4
⊢ ((𝑤 ∈ (◡1st “ 𝐴) ∧ 𝑤 ∈ (𝐵 × 𝐶)) ↔ ((1st ‘𝑤) ∈ 𝐴 ∧ 𝑤 ∈ (𝐵 × 𝐶))) |
25 | 16, 17, 24 | 3bitri 286 |
. . 3
⊢ (𝑤 ∈ (◡(1st ↾ (𝐵 × 𝐶)) “ 𝐴) ↔ ((1st ‘𝑤) ∈ 𝐴 ∧ 𝑤 ∈ (𝐵 × 𝐶))) |
26 | | elxp7 7201 |
. . 3
⊢ (𝑤 ∈ (𝐴 × 𝐶) ↔ (𝑤 ∈ (V × V) ∧ ((1st
‘𝑤) ∈ 𝐴 ∧ (2nd
‘𝑤) ∈ 𝐶))) |
27 | 14, 25, 26 | 3bitr4g 303 |
. 2
⊢ (𝐴 ⊆ 𝐵 → (𝑤 ∈ (◡(1st ↾ (𝐵 × 𝐶)) “ 𝐴) ↔ 𝑤 ∈ (𝐴 × 𝐶))) |
28 | 27 | eqrdv 2620 |
1
⊢ (𝐴 ⊆ 𝐵 → (◡(1st ↾ (𝐵 × 𝐶)) “ 𝐴) = (𝐴 × 𝐶)) |