Step | Hyp | Ref
| Expression |
1 | | xpss 5149 |
. . . . . 6
⊢ (𝐸 × 𝐹) ⊆ (V × V) |
2 | | rabss2 3648 |
. . . . . 6
⊢ ((𝐸 × 𝐹) ⊆ (V × V) → {𝑟 ∈ (𝐸 × 𝐹) ∣ ((1st ‘𝑟) ∈ 𝐴 ∧ (2nd ‘𝑟) ∈ 𝐵)} ⊆ {𝑟 ∈ (V × V) ∣
((1st ‘𝑟)
∈ 𝐴 ∧
(2nd ‘𝑟)
∈ 𝐵)}) |
3 | 1, 2 | mp1i 13 |
. . . . 5
⊢ ((𝐴 ⊆ 𝐸 ∧ 𝐵 ⊆ 𝐹) → {𝑟 ∈ (𝐸 × 𝐹) ∣ ((1st ‘𝑟) ∈ 𝐴 ∧ (2nd ‘𝑟) ∈ 𝐵)} ⊆ {𝑟 ∈ (V × V) ∣
((1st ‘𝑟)
∈ 𝐴 ∧
(2nd ‘𝑟)
∈ 𝐵)}) |
4 | | simprl 790 |
. . . . . . 7
⊢ (((𝐴 ⊆ 𝐸 ∧ 𝐵 ⊆ 𝐹) ∧ (𝑟 ∈ (V × V) ∧ ((1st
‘𝑟) ∈ 𝐴 ∧ (2nd
‘𝑟) ∈ 𝐵))) → 𝑟 ∈ (V × V)) |
5 | | simpll 786 |
. . . . . . . . 9
⊢ (((𝐴 ⊆ 𝐸 ∧ 𝐵 ⊆ 𝐹) ∧ (𝑟 ∈ (V × V) ∧ ((1st
‘𝑟) ∈ 𝐴 ∧ (2nd
‘𝑟) ∈ 𝐵))) → 𝐴 ⊆ 𝐸) |
6 | | simprrl 800 |
. . . . . . . . 9
⊢ (((𝐴 ⊆ 𝐸 ∧ 𝐵 ⊆ 𝐹) ∧ (𝑟 ∈ (V × V) ∧ ((1st
‘𝑟) ∈ 𝐴 ∧ (2nd
‘𝑟) ∈ 𝐵))) → (1st
‘𝑟) ∈ 𝐴) |
7 | 5, 6 | sseldd 3569 |
. . . . . . . 8
⊢ (((𝐴 ⊆ 𝐸 ∧ 𝐵 ⊆ 𝐹) ∧ (𝑟 ∈ (V × V) ∧ ((1st
‘𝑟) ∈ 𝐴 ∧ (2nd
‘𝑟) ∈ 𝐵))) → (1st
‘𝑟) ∈ 𝐸) |
8 | | simplr 788 |
. . . . . . . . 9
⊢ (((𝐴 ⊆ 𝐸 ∧ 𝐵 ⊆ 𝐹) ∧ (𝑟 ∈ (V × V) ∧ ((1st
‘𝑟) ∈ 𝐴 ∧ (2nd
‘𝑟) ∈ 𝐵))) → 𝐵 ⊆ 𝐹) |
9 | | simprrr 801 |
. . . . . . . . 9
⊢ (((𝐴 ⊆ 𝐸 ∧ 𝐵 ⊆ 𝐹) ∧ (𝑟 ∈ (V × V) ∧ ((1st
‘𝑟) ∈ 𝐴 ∧ (2nd
‘𝑟) ∈ 𝐵))) → (2nd
‘𝑟) ∈ 𝐵) |
10 | 8, 9 | sseldd 3569 |
. . . . . . . 8
⊢ (((𝐴 ⊆ 𝐸 ∧ 𝐵 ⊆ 𝐹) ∧ (𝑟 ∈ (V × V) ∧ ((1st
‘𝑟) ∈ 𝐴 ∧ (2nd
‘𝑟) ∈ 𝐵))) → (2nd
‘𝑟) ∈ 𝐹) |
11 | 7, 10 | jca 553 |
. . . . . . 7
⊢ (((𝐴 ⊆ 𝐸 ∧ 𝐵 ⊆ 𝐹) ∧ (𝑟 ∈ (V × V) ∧ ((1st
‘𝑟) ∈ 𝐴 ∧ (2nd
‘𝑟) ∈ 𝐵))) → ((1st
‘𝑟) ∈ 𝐸 ∧ (2nd
‘𝑟) ∈ 𝐹)) |
12 | | elxp7 7092 |
. . . . . . 7
⊢ (𝑟 ∈ (𝐸 × 𝐹) ↔ (𝑟 ∈ (V × V) ∧ ((1st
‘𝑟) ∈ 𝐸 ∧ (2nd
‘𝑟) ∈ 𝐹))) |
13 | 4, 11, 12 | sylanbrc 695 |
. . . . . 6
⊢ (((𝐴 ⊆ 𝐸 ∧ 𝐵 ⊆ 𝐹) ∧ (𝑟 ∈ (V × V) ∧ ((1st
‘𝑟) ∈ 𝐴 ∧ (2nd
‘𝑟) ∈ 𝐵))) → 𝑟 ∈ (𝐸 × 𝐹)) |
14 | 13 | rabss3d 28736 |
. . . . 5
⊢ ((𝐴 ⊆ 𝐸 ∧ 𝐵 ⊆ 𝐹) → {𝑟 ∈ (V × V) ∣
((1st ‘𝑟)
∈ 𝐴 ∧
(2nd ‘𝑟)
∈ 𝐵)} ⊆ {𝑟 ∈ (𝐸 × 𝐹) ∣ ((1st ‘𝑟) ∈ 𝐴 ∧ (2nd ‘𝑟) ∈ 𝐵)}) |
15 | 3, 14 | eqssd 3585 |
. . . 4
⊢ ((𝐴 ⊆ 𝐸 ∧ 𝐵 ⊆ 𝐹) → {𝑟 ∈ (𝐸 × 𝐹) ∣ ((1st ‘𝑟) ∈ 𝐴 ∧ (2nd ‘𝑟) ∈ 𝐵)} = {𝑟 ∈ (V × V) ∣
((1st ‘𝑟)
∈ 𝐴 ∧
(2nd ‘𝑟)
∈ 𝐵)}) |
16 | | xp2 7094 |
. . . 4
⊢ (𝐴 × 𝐵) = {𝑟 ∈ (V × V) ∣
((1st ‘𝑟)
∈ 𝐴 ∧
(2nd ‘𝑟)
∈ 𝐵)} |
17 | 15, 16 | syl6reqr 2663 |
. . 3
⊢ ((𝐴 ⊆ 𝐸 ∧ 𝐵 ⊆ 𝐹) → (𝐴 × 𝐵) = {𝑟 ∈ (𝐸 × 𝐹) ∣ ((1st ‘𝑟) ∈ 𝐴 ∧ (2nd ‘𝑟) ∈ 𝐵)}) |
18 | | inrab 3858 |
. . 3
⊢ ({𝑟 ∈ (𝐸 × 𝐹) ∣ (1st ‘𝑟) ∈ 𝐴} ∩ {𝑟 ∈ (𝐸 × 𝐹) ∣ (2nd ‘𝑟) ∈ 𝐵}) = {𝑟 ∈ (𝐸 × 𝐹) ∣ ((1st ‘𝑟) ∈ 𝐴 ∧ (2nd ‘𝑟) ∈ 𝐵)} |
19 | 17, 18 | syl6eqr 2662 |
. 2
⊢ ((𝐴 ⊆ 𝐸 ∧ 𝐵 ⊆ 𝐹) → (𝐴 × 𝐵) = ({𝑟 ∈ (𝐸 × 𝐹) ∣ (1st ‘𝑟) ∈ 𝐴} ∩ {𝑟 ∈ (𝐸 × 𝐹) ∣ (2nd ‘𝑟) ∈ 𝐵})) |
20 | | f1stres 7081 |
. . . . 5
⊢
(1st ↾ (𝐸 × 𝐹)):(𝐸 × 𝐹)⟶𝐸 |
21 | | ffn 5958 |
. . . . 5
⊢
((1st ↾ (𝐸 × 𝐹)):(𝐸 × 𝐹)⟶𝐸 → (1st ↾ (𝐸 × 𝐹)) Fn (𝐸 × 𝐹)) |
22 | | fncnvima2 6247 |
. . . . 5
⊢
((1st ↾ (𝐸 × 𝐹)) Fn (𝐸 × 𝐹) → (◡(1st ↾ (𝐸 × 𝐹)) “ 𝐴) = {𝑟 ∈ (𝐸 × 𝐹) ∣ ((1st ↾ (𝐸 × 𝐹))‘𝑟) ∈ 𝐴}) |
23 | 20, 21, 22 | mp2b 10 |
. . . 4
⊢ (◡(1st ↾ (𝐸 × 𝐹)) “ 𝐴) = {𝑟 ∈ (𝐸 × 𝐹) ∣ ((1st ↾ (𝐸 × 𝐹))‘𝑟) ∈ 𝐴} |
24 | | fvres 6117 |
. . . . . 6
⊢ (𝑟 ∈ (𝐸 × 𝐹) → ((1st ↾ (𝐸 × 𝐹))‘𝑟) = (1st ‘𝑟)) |
25 | 24 | eleq1d 2672 |
. . . . 5
⊢ (𝑟 ∈ (𝐸 × 𝐹) → (((1st ↾ (𝐸 × 𝐹))‘𝑟) ∈ 𝐴 ↔ (1st ‘𝑟) ∈ 𝐴)) |
26 | 25 | rabbiia 3161 |
. . . 4
⊢ {𝑟 ∈ (𝐸 × 𝐹) ∣ ((1st ↾ (𝐸 × 𝐹))‘𝑟) ∈ 𝐴} = {𝑟 ∈ (𝐸 × 𝐹) ∣ (1st ‘𝑟) ∈ 𝐴} |
27 | 23, 26 | eqtri 2632 |
. . 3
⊢ (◡(1st ↾ (𝐸 × 𝐹)) “ 𝐴) = {𝑟 ∈ (𝐸 × 𝐹) ∣ (1st ‘𝑟) ∈ 𝐴} |
28 | | f2ndres 7082 |
. . . . 5
⊢
(2nd ↾ (𝐸 × 𝐹)):(𝐸 × 𝐹)⟶𝐹 |
29 | | ffn 5958 |
. . . . 5
⊢
((2nd ↾ (𝐸 × 𝐹)):(𝐸 × 𝐹)⟶𝐹 → (2nd ↾ (𝐸 × 𝐹)) Fn (𝐸 × 𝐹)) |
30 | | fncnvima2 6247 |
. . . . 5
⊢
((2nd ↾ (𝐸 × 𝐹)) Fn (𝐸 × 𝐹) → (◡(2nd ↾ (𝐸 × 𝐹)) “ 𝐵) = {𝑟 ∈ (𝐸 × 𝐹) ∣ ((2nd ↾ (𝐸 × 𝐹))‘𝑟) ∈ 𝐵}) |
31 | 28, 29, 30 | mp2b 10 |
. . . 4
⊢ (◡(2nd ↾ (𝐸 × 𝐹)) “ 𝐵) = {𝑟 ∈ (𝐸 × 𝐹) ∣ ((2nd ↾ (𝐸 × 𝐹))‘𝑟) ∈ 𝐵} |
32 | | fvres 6117 |
. . . . . 6
⊢ (𝑟 ∈ (𝐸 × 𝐹) → ((2nd ↾ (𝐸 × 𝐹))‘𝑟) = (2nd ‘𝑟)) |
33 | 32 | eleq1d 2672 |
. . . . 5
⊢ (𝑟 ∈ (𝐸 × 𝐹) → (((2nd ↾ (𝐸 × 𝐹))‘𝑟) ∈ 𝐵 ↔ (2nd ‘𝑟) ∈ 𝐵)) |
34 | 33 | rabbiia 3161 |
. . . 4
⊢ {𝑟 ∈ (𝐸 × 𝐹) ∣ ((2nd ↾ (𝐸 × 𝐹))‘𝑟) ∈ 𝐵} = {𝑟 ∈ (𝐸 × 𝐹) ∣ (2nd ‘𝑟) ∈ 𝐵} |
35 | 31, 34 | eqtri 2632 |
. . 3
⊢ (◡(2nd ↾ (𝐸 × 𝐹)) “ 𝐵) = {𝑟 ∈ (𝐸 × 𝐹) ∣ (2nd ‘𝑟) ∈ 𝐵} |
36 | 27, 35 | ineq12i 3774 |
. 2
⊢ ((◡(1st ↾ (𝐸 × 𝐹)) “ 𝐴) ∩ (◡(2nd ↾ (𝐸 × 𝐹)) “ 𝐵)) = ({𝑟 ∈ (𝐸 × 𝐹) ∣ (1st ‘𝑟) ∈ 𝐴} ∩ {𝑟 ∈ (𝐸 × 𝐹) ∣ (2nd ‘𝑟) ∈ 𝐵}) |
37 | 19, 36 | syl6eqr 2662 |
1
⊢ ((𝐴 ⊆ 𝐸 ∧ 𝐵 ⊆ 𝐹) → (𝐴 × 𝐵) = ((◡(1st ↾ (𝐸 × 𝐹)) “ 𝐴) ∩ (◡(2nd ↾ (𝐸 × 𝐹)) “ 𝐵))) |