Step | Hyp | Ref
| Expression |
1 | | elxp7 7721 |
. . . . . 6
⊢ (𝑤 ∈ (𝐵 × 𝐶) ↔ (𝑤 ∈ (V × V) ∧ ((1st
‘𝑤) ∈ 𝐵 ∧ (2nd
‘𝑤) ∈ 𝐶))) |
2 | 1 | anbi1i 627 |
. . . . 5
⊢ ((𝑤 ∈ (𝐵 × 𝐶) ∧ (2nd ‘𝑤) ∈ 𝐴) ↔ ((𝑤 ∈ (V × V) ∧ ((1st
‘𝑤) ∈ 𝐵 ∧ (2nd
‘𝑤) ∈ 𝐶)) ∧ (2nd
‘𝑤) ∈ 𝐴)) |
3 | | ssel 3881 |
. . . . . . . 8
⊢ (𝐴 ⊆ 𝐶 → ((2nd ‘𝑤) ∈ 𝐴 → (2nd ‘𝑤) ∈ 𝐶)) |
4 | 3 | pm4.71rd 567 |
. . . . . . 7
⊢ (𝐴 ⊆ 𝐶 → ((2nd ‘𝑤) ∈ 𝐴 ↔ ((2nd ‘𝑤) ∈ 𝐶 ∧ (2nd ‘𝑤) ∈ 𝐴))) |
5 | 4 | anbi2d 632 |
. . . . . 6
⊢ (𝐴 ⊆ 𝐶 → (((𝑤 ∈ (V × V) ∧ (1st
‘𝑤) ∈ 𝐵) ∧ (2nd
‘𝑤) ∈ 𝐴) ↔ ((𝑤 ∈ (V × V) ∧ (1st
‘𝑤) ∈ 𝐵) ∧ ((2nd
‘𝑤) ∈ 𝐶 ∧ (2nd
‘𝑤) ∈ 𝐴)))) |
6 | | anass 473 |
. . . . . . . 8
⊢ ((((𝑤 ∈ (V × V) ∧
(1st ‘𝑤)
∈ 𝐵) ∧
(2nd ‘𝑤)
∈ 𝐶) ∧
(2nd ‘𝑤)
∈ 𝐴) ↔ ((𝑤 ∈ (V × V) ∧
(1st ‘𝑤)
∈ 𝐵) ∧
((2nd ‘𝑤)
∈ 𝐶 ∧
(2nd ‘𝑤)
∈ 𝐴))) |
7 | 6 | bicomi 227 |
. . . . . . 7
⊢ (((𝑤 ∈ (V × V) ∧
(1st ‘𝑤)
∈ 𝐵) ∧
((2nd ‘𝑤)
∈ 𝐶 ∧
(2nd ‘𝑤)
∈ 𝐴)) ↔ (((𝑤 ∈ (V × V) ∧
(1st ‘𝑤)
∈ 𝐵) ∧
(2nd ‘𝑤)
∈ 𝐶) ∧
(2nd ‘𝑤)
∈ 𝐴)) |
8 | 7 | a1i 11 |
. . . . . 6
⊢ (𝐴 ⊆ 𝐶 → (((𝑤 ∈ (V × V) ∧ (1st
‘𝑤) ∈ 𝐵) ∧ ((2nd
‘𝑤) ∈ 𝐶 ∧ (2nd
‘𝑤) ∈ 𝐴)) ↔ (((𝑤 ∈ (V × V) ∧ (1st
‘𝑤) ∈ 𝐵) ∧ (2nd
‘𝑤) ∈ 𝐶) ∧ (2nd
‘𝑤) ∈ 𝐴))) |
9 | | anass 473 |
. . . . . . . 8
⊢ (((𝑤 ∈ (V × V) ∧
(1st ‘𝑤)
∈ 𝐵) ∧
(2nd ‘𝑤)
∈ 𝐶) ↔ (𝑤 ∈ (V × V) ∧
((1st ‘𝑤)
∈ 𝐵 ∧
(2nd ‘𝑤)
∈ 𝐶))) |
10 | 9 | anbi1i 627 |
. . . . . . 7
⊢ ((((𝑤 ∈ (V × V) ∧
(1st ‘𝑤)
∈ 𝐵) ∧
(2nd ‘𝑤)
∈ 𝐶) ∧
(2nd ‘𝑤)
∈ 𝐴) ↔ ((𝑤 ∈ (V × V) ∧
((1st ‘𝑤)
∈ 𝐵 ∧
(2nd ‘𝑤)
∈ 𝐶)) ∧
(2nd ‘𝑤)
∈ 𝐴)) |
11 | 10 | a1i 11 |
. . . . . 6
⊢ (𝐴 ⊆ 𝐶 → ((((𝑤 ∈ (V × V) ∧ (1st
‘𝑤) ∈ 𝐵) ∧ (2nd
‘𝑤) ∈ 𝐶) ∧ (2nd
‘𝑤) ∈ 𝐴) ↔ ((𝑤 ∈ (V × V) ∧ ((1st
‘𝑤) ∈ 𝐵 ∧ (2nd
‘𝑤) ∈ 𝐶)) ∧ (2nd
‘𝑤) ∈ 𝐴))) |
12 | 5, 8, 11 | 3bitrd 309 |
. . . . 5
⊢ (𝐴 ⊆ 𝐶 → (((𝑤 ∈ (V × V) ∧ (1st
‘𝑤) ∈ 𝐵) ∧ (2nd
‘𝑤) ∈ 𝐴) ↔ ((𝑤 ∈ (V × V) ∧ ((1st
‘𝑤) ∈ 𝐵 ∧ (2nd
‘𝑤) ∈ 𝐶)) ∧ (2nd
‘𝑤) ∈ 𝐴))) |
13 | 2, 12 | bitr4id 294 |
. . . 4
⊢ (𝐴 ⊆ 𝐶 → ((𝑤 ∈ (𝐵 × 𝐶) ∧ (2nd ‘𝑤) ∈ 𝐴) ↔ ((𝑤 ∈ (V × V) ∧ (1st
‘𝑤) ∈ 𝐵) ∧ (2nd
‘𝑤) ∈ 𝐴))) |
14 | | ancom 465 |
. . . 4
⊢ ((𝑤 ∈ (𝐵 × 𝐶) ∧ (2nd ‘𝑤) ∈ 𝐴) ↔ ((2nd ‘𝑤) ∈ 𝐴 ∧ 𝑤 ∈ (𝐵 × 𝐶))) |
15 | | anass 473 |
. . . 4
⊢ (((𝑤 ∈ (V × V) ∧
(1st ‘𝑤)
∈ 𝐵) ∧
(2nd ‘𝑤)
∈ 𝐴) ↔ (𝑤 ∈ (V × V) ∧
((1st ‘𝑤)
∈ 𝐵 ∧
(2nd ‘𝑤)
∈ 𝐴))) |
16 | 13, 14, 15 | 3bitr3g 317 |
. . 3
⊢ (𝐴 ⊆ 𝐶 → (((2nd ‘𝑤) ∈ 𝐴 ∧ 𝑤 ∈ (𝐵 × 𝐶)) ↔ (𝑤 ∈ (V × V) ∧ ((1st
‘𝑤) ∈ 𝐵 ∧ (2nd
‘𝑤) ∈ 𝐴)))) |
17 | | cnvresima 6052 |
. . . . 5
⊢ (◡(2nd ↾ (𝐵 × 𝐶)) “ 𝐴) = ((◡2nd “ 𝐴) ∩ (𝐵 × 𝐶)) |
18 | 17 | eleq2i 2842 |
. . . 4
⊢ (𝑤 ∈ (◡(2nd ↾ (𝐵 × 𝐶)) “ 𝐴) ↔ 𝑤 ∈ ((◡2nd “ 𝐴) ∩ (𝐵 × 𝐶))) |
19 | | elin 3870 |
. . . 4
⊢ (𝑤 ∈ ((◡2nd “ 𝐴) ∩ (𝐵 × 𝐶)) ↔ (𝑤 ∈ (◡2nd “ 𝐴) ∧ 𝑤 ∈ (𝐵 × 𝐶))) |
20 | | vex 3411 |
. . . . . 6
⊢ 𝑤 ∈ V |
21 | | fo2nd 7707 |
. . . . . . 7
⊢
2nd :V–onto→V |
22 | | fofn 6571 |
. . . . . . 7
⊢
(2nd :V–onto→V → 2nd Fn V) |
23 | | elpreima 6812 |
. . . . . . 7
⊢
(2nd Fn V → (𝑤 ∈ (◡2nd “ 𝐴) ↔ (𝑤 ∈ V ∧ (2nd ‘𝑤) ∈ 𝐴))) |
24 | 21, 22, 23 | mp2b 10 |
. . . . . 6
⊢ (𝑤 ∈ (◡2nd “ 𝐴) ↔ (𝑤 ∈ V ∧ (2nd ‘𝑤) ∈ 𝐴)) |
25 | 20, 24 | mpbiran 709 |
. . . . 5
⊢ (𝑤 ∈ (◡2nd “ 𝐴) ↔ (2nd ‘𝑤) ∈ 𝐴) |
26 | 25 | anbi1i 627 |
. . . 4
⊢ ((𝑤 ∈ (◡2nd “ 𝐴) ∧ 𝑤 ∈ (𝐵 × 𝐶)) ↔ ((2nd ‘𝑤) ∈ 𝐴 ∧ 𝑤 ∈ (𝐵 × 𝐶))) |
27 | 18, 19, 26 | 3bitri 301 |
. . 3
⊢ (𝑤 ∈ (◡(2nd ↾ (𝐵 × 𝐶)) “ 𝐴) ↔ ((2nd ‘𝑤) ∈ 𝐴 ∧ 𝑤 ∈ (𝐵 × 𝐶))) |
28 | | elxp7 7721 |
. . 3
⊢ (𝑤 ∈ (𝐵 × 𝐴) ↔ (𝑤 ∈ (V × V) ∧ ((1st
‘𝑤) ∈ 𝐵 ∧ (2nd
‘𝑤) ∈ 𝐴))) |
29 | 16, 27, 28 | 3bitr4g 318 |
. 2
⊢ (𝐴 ⊆ 𝐶 → (𝑤 ∈ (◡(2nd ↾ (𝐵 × 𝐶)) “ 𝐴) ↔ 𝑤 ∈ (𝐵 × 𝐴))) |
30 | 29 | eqrdv 2757 |
1
⊢ (𝐴 ⊆ 𝐶 → (◡(2nd ↾ (𝐵 × 𝐶)) “ 𝐴) = (𝐵 × 𝐴)) |