| Step | Hyp | Ref
| Expression |
| 1 | | xp2 8051 |
. . . 4
⊢ (𝐴 × 𝐵) = {𝑟 ∈ (V × V) ∣
((1st ‘𝑟)
∈ 𝐴 ∧
(2nd ‘𝑟)
∈ 𝐵)} |
| 2 | | xpss 5701 |
. . . . . 6
⊢ (𝐸 × 𝐹) ⊆ (V × V) |
| 3 | | rabss2 4078 |
. . . . . 6
⊢ ((𝐸 × 𝐹) ⊆ (V × V) → {𝑟 ∈ (𝐸 × 𝐹) ∣ ((1st ‘𝑟) ∈ 𝐴 ∧ (2nd ‘𝑟) ∈ 𝐵)} ⊆ {𝑟 ∈ (V × V) ∣
((1st ‘𝑟)
∈ 𝐴 ∧
(2nd ‘𝑟)
∈ 𝐵)}) |
| 4 | 2, 3 | mp1i 13 |
. . . . 5
⊢ ((𝐴 ⊆ 𝐸 ∧ 𝐵 ⊆ 𝐹) → {𝑟 ∈ (𝐸 × 𝐹) ∣ ((1st ‘𝑟) ∈ 𝐴 ∧ (2nd ‘𝑟) ∈ 𝐵)} ⊆ {𝑟 ∈ (V × V) ∣
((1st ‘𝑟)
∈ 𝐴 ∧
(2nd ‘𝑟)
∈ 𝐵)}) |
| 5 | | simprl 771 |
. . . . . . 7
⊢ (((𝐴 ⊆ 𝐸 ∧ 𝐵 ⊆ 𝐹) ∧ (𝑟 ∈ (V × V) ∧ ((1st
‘𝑟) ∈ 𝐴 ∧ (2nd
‘𝑟) ∈ 𝐵))) → 𝑟 ∈ (V × V)) |
| 6 | | simpll 767 |
. . . . . . . . 9
⊢ (((𝐴 ⊆ 𝐸 ∧ 𝐵 ⊆ 𝐹) ∧ (𝑟 ∈ (V × V) ∧ ((1st
‘𝑟) ∈ 𝐴 ∧ (2nd
‘𝑟) ∈ 𝐵))) → 𝐴 ⊆ 𝐸) |
| 7 | | simprrl 781 |
. . . . . . . . 9
⊢ (((𝐴 ⊆ 𝐸 ∧ 𝐵 ⊆ 𝐹) ∧ (𝑟 ∈ (V × V) ∧ ((1st
‘𝑟) ∈ 𝐴 ∧ (2nd
‘𝑟) ∈ 𝐵))) → (1st
‘𝑟) ∈ 𝐴) |
| 8 | 6, 7 | sseldd 3984 |
. . . . . . . 8
⊢ (((𝐴 ⊆ 𝐸 ∧ 𝐵 ⊆ 𝐹) ∧ (𝑟 ∈ (V × V) ∧ ((1st
‘𝑟) ∈ 𝐴 ∧ (2nd
‘𝑟) ∈ 𝐵))) → (1st
‘𝑟) ∈ 𝐸) |
| 9 | | simplr 769 |
. . . . . . . . 9
⊢ (((𝐴 ⊆ 𝐸 ∧ 𝐵 ⊆ 𝐹) ∧ (𝑟 ∈ (V × V) ∧ ((1st
‘𝑟) ∈ 𝐴 ∧ (2nd
‘𝑟) ∈ 𝐵))) → 𝐵 ⊆ 𝐹) |
| 10 | | simprrr 782 |
. . . . . . . . 9
⊢ (((𝐴 ⊆ 𝐸 ∧ 𝐵 ⊆ 𝐹) ∧ (𝑟 ∈ (V × V) ∧ ((1st
‘𝑟) ∈ 𝐴 ∧ (2nd
‘𝑟) ∈ 𝐵))) → (2nd
‘𝑟) ∈ 𝐵) |
| 11 | 9, 10 | sseldd 3984 |
. . . . . . . 8
⊢ (((𝐴 ⊆ 𝐸 ∧ 𝐵 ⊆ 𝐹) ∧ (𝑟 ∈ (V × V) ∧ ((1st
‘𝑟) ∈ 𝐴 ∧ (2nd
‘𝑟) ∈ 𝐵))) → (2nd
‘𝑟) ∈ 𝐹) |
| 12 | 8, 11 | jca 511 |
. . . . . . 7
⊢ (((𝐴 ⊆ 𝐸 ∧ 𝐵 ⊆ 𝐹) ∧ (𝑟 ∈ (V × V) ∧ ((1st
‘𝑟) ∈ 𝐴 ∧ (2nd
‘𝑟) ∈ 𝐵))) → ((1st
‘𝑟) ∈ 𝐸 ∧ (2nd
‘𝑟) ∈ 𝐹)) |
| 13 | | elxp7 8049 |
. . . . . . 7
⊢ (𝑟 ∈ (𝐸 × 𝐹) ↔ (𝑟 ∈ (V × V) ∧ ((1st
‘𝑟) ∈ 𝐸 ∧ (2nd
‘𝑟) ∈ 𝐹))) |
| 14 | 5, 12, 13 | sylanbrc 583 |
. . . . . 6
⊢ (((𝐴 ⊆ 𝐸 ∧ 𝐵 ⊆ 𝐹) ∧ (𝑟 ∈ (V × V) ∧ ((1st
‘𝑟) ∈ 𝐴 ∧ (2nd
‘𝑟) ∈ 𝐵))) → 𝑟 ∈ (𝐸 × 𝐹)) |
| 15 | 14 | rabss3d 4081 |
. . . . 5
⊢ ((𝐴 ⊆ 𝐸 ∧ 𝐵 ⊆ 𝐹) → {𝑟 ∈ (V × V) ∣
((1st ‘𝑟)
∈ 𝐴 ∧
(2nd ‘𝑟)
∈ 𝐵)} ⊆ {𝑟 ∈ (𝐸 × 𝐹) ∣ ((1st ‘𝑟) ∈ 𝐴 ∧ (2nd ‘𝑟) ∈ 𝐵)}) |
| 16 | 4, 15 | eqssd 4001 |
. . . 4
⊢ ((𝐴 ⊆ 𝐸 ∧ 𝐵 ⊆ 𝐹) → {𝑟 ∈ (𝐸 × 𝐹) ∣ ((1st ‘𝑟) ∈ 𝐴 ∧ (2nd ‘𝑟) ∈ 𝐵)} = {𝑟 ∈ (V × V) ∣
((1st ‘𝑟)
∈ 𝐴 ∧
(2nd ‘𝑟)
∈ 𝐵)}) |
| 17 | 1, 16 | eqtr4id 2796 |
. . 3
⊢ ((𝐴 ⊆ 𝐸 ∧ 𝐵 ⊆ 𝐹) → (𝐴 × 𝐵) = {𝑟 ∈ (𝐸 × 𝐹) ∣ ((1st ‘𝑟) ∈ 𝐴 ∧ (2nd ‘𝑟) ∈ 𝐵)}) |
| 18 | | inrab 4316 |
. . 3
⊢ ({𝑟 ∈ (𝐸 × 𝐹) ∣ (1st ‘𝑟) ∈ 𝐴} ∩ {𝑟 ∈ (𝐸 × 𝐹) ∣ (2nd ‘𝑟) ∈ 𝐵}) = {𝑟 ∈ (𝐸 × 𝐹) ∣ ((1st ‘𝑟) ∈ 𝐴 ∧ (2nd ‘𝑟) ∈ 𝐵)} |
| 19 | 17, 18 | eqtr4di 2795 |
. 2
⊢ ((𝐴 ⊆ 𝐸 ∧ 𝐵 ⊆ 𝐹) → (𝐴 × 𝐵) = ({𝑟 ∈ (𝐸 × 𝐹) ∣ (1st ‘𝑟) ∈ 𝐴} ∩ {𝑟 ∈ (𝐸 × 𝐹) ∣ (2nd ‘𝑟) ∈ 𝐵})) |
| 20 | | f1stres 8038 |
. . . . 5
⊢
(1st ↾ (𝐸 × 𝐹)):(𝐸 × 𝐹)⟶𝐸 |
| 21 | | ffn 6736 |
. . . . 5
⊢
((1st ↾ (𝐸 × 𝐹)):(𝐸 × 𝐹)⟶𝐸 → (1st ↾ (𝐸 × 𝐹)) Fn (𝐸 × 𝐹)) |
| 22 | | fncnvima2 7081 |
. . . . 5
⊢
((1st ↾ (𝐸 × 𝐹)) Fn (𝐸 × 𝐹) → (◡(1st ↾ (𝐸 × 𝐹)) “ 𝐴) = {𝑟 ∈ (𝐸 × 𝐹) ∣ ((1st ↾ (𝐸 × 𝐹))‘𝑟) ∈ 𝐴}) |
| 23 | 20, 21, 22 | mp2b 10 |
. . . 4
⊢ (◡(1st ↾ (𝐸 × 𝐹)) “ 𝐴) = {𝑟 ∈ (𝐸 × 𝐹) ∣ ((1st ↾ (𝐸 × 𝐹))‘𝑟) ∈ 𝐴} |
| 24 | | fvres 6925 |
. . . . . 6
⊢ (𝑟 ∈ (𝐸 × 𝐹) → ((1st ↾ (𝐸 × 𝐹))‘𝑟) = (1st ‘𝑟)) |
| 25 | 24 | eleq1d 2826 |
. . . . 5
⊢ (𝑟 ∈ (𝐸 × 𝐹) → (((1st ↾ (𝐸 × 𝐹))‘𝑟) ∈ 𝐴 ↔ (1st ‘𝑟) ∈ 𝐴)) |
| 26 | 25 | rabbiia 3440 |
. . . 4
⊢ {𝑟 ∈ (𝐸 × 𝐹) ∣ ((1st ↾ (𝐸 × 𝐹))‘𝑟) ∈ 𝐴} = {𝑟 ∈ (𝐸 × 𝐹) ∣ (1st ‘𝑟) ∈ 𝐴} |
| 27 | 23, 26 | eqtri 2765 |
. . 3
⊢ (◡(1st ↾ (𝐸 × 𝐹)) “ 𝐴) = {𝑟 ∈ (𝐸 × 𝐹) ∣ (1st ‘𝑟) ∈ 𝐴} |
| 28 | | f2ndres 8039 |
. . . . 5
⊢
(2nd ↾ (𝐸 × 𝐹)):(𝐸 × 𝐹)⟶𝐹 |
| 29 | | ffn 6736 |
. . . . 5
⊢
((2nd ↾ (𝐸 × 𝐹)):(𝐸 × 𝐹)⟶𝐹 → (2nd ↾ (𝐸 × 𝐹)) Fn (𝐸 × 𝐹)) |
| 30 | | fncnvima2 7081 |
. . . . 5
⊢
((2nd ↾ (𝐸 × 𝐹)) Fn (𝐸 × 𝐹) → (◡(2nd ↾ (𝐸 × 𝐹)) “ 𝐵) = {𝑟 ∈ (𝐸 × 𝐹) ∣ ((2nd ↾ (𝐸 × 𝐹))‘𝑟) ∈ 𝐵}) |
| 31 | 28, 29, 30 | mp2b 10 |
. . . 4
⊢ (◡(2nd ↾ (𝐸 × 𝐹)) “ 𝐵) = {𝑟 ∈ (𝐸 × 𝐹) ∣ ((2nd ↾ (𝐸 × 𝐹))‘𝑟) ∈ 𝐵} |
| 32 | | fvres 6925 |
. . . . . 6
⊢ (𝑟 ∈ (𝐸 × 𝐹) → ((2nd ↾ (𝐸 × 𝐹))‘𝑟) = (2nd ‘𝑟)) |
| 33 | 32 | eleq1d 2826 |
. . . . 5
⊢ (𝑟 ∈ (𝐸 × 𝐹) → (((2nd ↾ (𝐸 × 𝐹))‘𝑟) ∈ 𝐵 ↔ (2nd ‘𝑟) ∈ 𝐵)) |
| 34 | 33 | rabbiia 3440 |
. . . 4
⊢ {𝑟 ∈ (𝐸 × 𝐹) ∣ ((2nd ↾ (𝐸 × 𝐹))‘𝑟) ∈ 𝐵} = {𝑟 ∈ (𝐸 × 𝐹) ∣ (2nd ‘𝑟) ∈ 𝐵} |
| 35 | 31, 34 | eqtri 2765 |
. . 3
⊢ (◡(2nd ↾ (𝐸 × 𝐹)) “ 𝐵) = {𝑟 ∈ (𝐸 × 𝐹) ∣ (2nd ‘𝑟) ∈ 𝐵} |
| 36 | 27, 35 | ineq12i 4218 |
. 2
⊢ ((◡(1st ↾ (𝐸 × 𝐹)) “ 𝐴) ∩ (◡(2nd ↾ (𝐸 × 𝐹)) “ 𝐵)) = ({𝑟 ∈ (𝐸 × 𝐹) ∣ (1st ‘𝑟) ∈ 𝐴} ∩ {𝑟 ∈ (𝐸 × 𝐹) ∣ (2nd ‘𝑟) ∈ 𝐵}) |
| 37 | 19, 36 | eqtr4di 2795 |
1
⊢ ((𝐴 ⊆ 𝐸 ∧ 𝐵 ⊆ 𝐹) → (𝐴 × 𝐵) = ((◡(1st ↾ (𝐸 × 𝐹)) “ 𝐴) ∩ (◡(2nd ↾ (𝐸 × 𝐹)) “ 𝐵))) |