| Step | Hyp | Ref
| Expression |
| 1 | | funfn 6596 |
. . . . 5
⊢ (Fun
𝐹 ↔ 𝐹 Fn dom 𝐹) |
| 2 | | fncnvima2 7081 |
. . . . 5
⊢ (𝐹 Fn dom 𝐹 → (◡𝐹 “ (𝑌 × 𝑍)) = {𝑥 ∈ dom 𝐹 ∣ (𝐹‘𝑥) ∈ (𝑌 × 𝑍)}) |
| 3 | 1, 2 | sylbi 217 |
. . . 4
⊢ (Fun
𝐹 → (◡𝐹 “ (𝑌 × 𝑍)) = {𝑥 ∈ dom 𝐹 ∣ (𝐹‘𝑥) ∈ (𝑌 × 𝑍)}) |
| 4 | 3 | adantr 480 |
. . 3
⊢ ((Fun
𝐹 ∧ ran 𝐹 ⊆ (V × V)) →
(◡𝐹 “ (𝑌 × 𝑍)) = {𝑥 ∈ dom 𝐹 ∣ (𝐹‘𝑥) ∈ (𝑌 × 𝑍)}) |
| 5 | | elxp6 8048 |
. . . . . . 7
⊢ ((𝐹‘𝑥) ∈ (𝑌 × 𝑍) ↔ ((𝐹‘𝑥) = 〈(1st ‘(𝐹‘𝑥)), (2nd ‘(𝐹‘𝑥))〉 ∧ ((1st ‘(𝐹‘𝑥)) ∈ 𝑌 ∧ (2nd ‘(𝐹‘𝑥)) ∈ 𝑍))) |
| 6 | | fvco 7007 |
. . . . . . . . . 10
⊢ ((Fun
𝐹 ∧ 𝑥 ∈ dom 𝐹) → ((1st ∘ 𝐹)‘𝑥) = (1st ‘(𝐹‘𝑥))) |
| 7 | | fvco 7007 |
. . . . . . . . . 10
⊢ ((Fun
𝐹 ∧ 𝑥 ∈ dom 𝐹) → ((2nd ∘ 𝐹)‘𝑥) = (2nd ‘(𝐹‘𝑥))) |
| 8 | 6, 7 | opeq12d 4881 |
. . . . . . . . 9
⊢ ((Fun
𝐹 ∧ 𝑥 ∈ dom 𝐹) → 〈((1st ∘
𝐹)‘𝑥), ((2nd ∘ 𝐹)‘𝑥)〉 = 〈(1st ‘(𝐹‘𝑥)), (2nd ‘(𝐹‘𝑥))〉) |
| 9 | 8 | eqeq2d 2748 |
. . . . . . . 8
⊢ ((Fun
𝐹 ∧ 𝑥 ∈ dom 𝐹) → ((𝐹‘𝑥) = 〈((1st ∘ 𝐹)‘𝑥), ((2nd ∘ 𝐹)‘𝑥)〉 ↔ (𝐹‘𝑥) = 〈(1st ‘(𝐹‘𝑥)), (2nd ‘(𝐹‘𝑥))〉)) |
| 10 | 6 | eleq1d 2826 |
. . . . . . . . 9
⊢ ((Fun
𝐹 ∧ 𝑥 ∈ dom 𝐹) → (((1st ∘ 𝐹)‘𝑥) ∈ 𝑌 ↔ (1st ‘(𝐹‘𝑥)) ∈ 𝑌)) |
| 11 | 7 | eleq1d 2826 |
. . . . . . . . 9
⊢ ((Fun
𝐹 ∧ 𝑥 ∈ dom 𝐹) → (((2nd ∘ 𝐹)‘𝑥) ∈ 𝑍 ↔ (2nd ‘(𝐹‘𝑥)) ∈ 𝑍)) |
| 12 | 10, 11 | anbi12d 632 |
. . . . . . . 8
⊢ ((Fun
𝐹 ∧ 𝑥 ∈ dom 𝐹) → ((((1st ∘ 𝐹)‘𝑥) ∈ 𝑌 ∧ ((2nd ∘ 𝐹)‘𝑥) ∈ 𝑍) ↔ ((1st ‘(𝐹‘𝑥)) ∈ 𝑌 ∧ (2nd ‘(𝐹‘𝑥)) ∈ 𝑍))) |
| 13 | 9, 12 | anbi12d 632 |
. . . . . . 7
⊢ ((Fun
𝐹 ∧ 𝑥 ∈ dom 𝐹) → (((𝐹‘𝑥) = 〈((1st ∘ 𝐹)‘𝑥), ((2nd ∘ 𝐹)‘𝑥)〉 ∧ (((1st ∘ 𝐹)‘𝑥) ∈ 𝑌 ∧ ((2nd ∘ 𝐹)‘𝑥) ∈ 𝑍)) ↔ ((𝐹‘𝑥) = 〈(1st ‘(𝐹‘𝑥)), (2nd ‘(𝐹‘𝑥))〉 ∧ ((1st ‘(𝐹‘𝑥)) ∈ 𝑌 ∧ (2nd ‘(𝐹‘𝑥)) ∈ 𝑍)))) |
| 14 | 5, 13 | bitr4id 290 |
. . . . . 6
⊢ ((Fun
𝐹 ∧ 𝑥 ∈ dom 𝐹) → ((𝐹‘𝑥) ∈ (𝑌 × 𝑍) ↔ ((𝐹‘𝑥) = 〈((1st ∘ 𝐹)‘𝑥), ((2nd ∘ 𝐹)‘𝑥)〉 ∧ (((1st ∘ 𝐹)‘𝑥) ∈ 𝑌 ∧ ((2nd ∘ 𝐹)‘𝑥) ∈ 𝑍)))) |
| 15 | 14 | adantlr 715 |
. . . . 5
⊢ (((Fun
𝐹 ∧ ran 𝐹 ⊆ (V × V)) ∧
𝑥 ∈ dom 𝐹) → ((𝐹‘𝑥) ∈ (𝑌 × 𝑍) ↔ ((𝐹‘𝑥) = 〈((1st ∘ 𝐹)‘𝑥), ((2nd ∘ 𝐹)‘𝑥)〉 ∧ (((1st ∘ 𝐹)‘𝑥) ∈ 𝑌 ∧ ((2nd ∘ 𝐹)‘𝑥) ∈ 𝑍)))) |
| 16 | | opfv 32654 |
. . . . . 6
⊢ (((Fun
𝐹 ∧ ran 𝐹 ⊆ (V × V)) ∧
𝑥 ∈ dom 𝐹) → (𝐹‘𝑥) = 〈((1st ∘ 𝐹)‘𝑥), ((2nd ∘ 𝐹)‘𝑥)〉) |
| 17 | 16 | biantrurd 532 |
. . . . 5
⊢ (((Fun
𝐹 ∧ ran 𝐹 ⊆ (V × V)) ∧
𝑥 ∈ dom 𝐹) → ((((1st
∘ 𝐹)‘𝑥) ∈ 𝑌 ∧ ((2nd ∘ 𝐹)‘𝑥) ∈ 𝑍) ↔ ((𝐹‘𝑥) = 〈((1st ∘ 𝐹)‘𝑥), ((2nd ∘ 𝐹)‘𝑥)〉 ∧ (((1st ∘ 𝐹)‘𝑥) ∈ 𝑌 ∧ ((2nd ∘ 𝐹)‘𝑥) ∈ 𝑍)))) |
| 18 | | fo1st 8034 |
. . . . . . . . . . 11
⊢
1st :V–onto→V |
| 19 | | fofun 6821 |
. . . . . . . . . . 11
⊢
(1st :V–onto→V → Fun 1st ) |
| 20 | 18, 19 | ax-mp 5 |
. . . . . . . . . 10
⊢ Fun
1st |
| 21 | | funco 6606 |
. . . . . . . . . 10
⊢ ((Fun
1st ∧ Fun 𝐹)
→ Fun (1st ∘ 𝐹)) |
| 22 | 20, 21 | mpan 690 |
. . . . . . . . 9
⊢ (Fun
𝐹 → Fun
(1st ∘ 𝐹)) |
| 23 | 22 | adantr 480 |
. . . . . . . 8
⊢ ((Fun
𝐹 ∧ 𝑥 ∈ dom 𝐹) → Fun (1st ∘ 𝐹)) |
| 24 | | ssv 4008 |
. . . . . . . . . . . 12
⊢ (𝐹 “ dom 𝐹) ⊆ V |
| 25 | | fof 6820 |
. . . . . . . . . . . . 13
⊢
(1st :V–onto→V → 1st
:V⟶V) |
| 26 | | fdm 6745 |
. . . . . . . . . . . . 13
⊢
(1st :V⟶V → dom 1st =
V) |
| 27 | 18, 25, 26 | mp2b 10 |
. . . . . . . . . . . 12
⊢ dom
1st = V |
| 28 | 24, 27 | sseqtrri 4033 |
. . . . . . . . . . 11
⊢ (𝐹 “ dom 𝐹) ⊆ dom
1st |
| 29 | | ssid 4006 |
. . . . . . . . . . . 12
⊢ dom 𝐹 ⊆ dom 𝐹 |
| 30 | | funimass3 7074 |
. . . . . . . . . . . 12
⊢ ((Fun
𝐹 ∧ dom 𝐹 ⊆ dom 𝐹) → ((𝐹 “ dom 𝐹) ⊆ dom 1st ↔ dom
𝐹 ⊆ (◡𝐹 “ dom 1st
))) |
| 31 | 29, 30 | mpan2 691 |
. . . . . . . . . . 11
⊢ (Fun
𝐹 → ((𝐹 “ dom 𝐹) ⊆ dom 1st ↔ dom
𝐹 ⊆ (◡𝐹 “ dom 1st
))) |
| 32 | 28, 31 | mpbii 233 |
. . . . . . . . . 10
⊢ (Fun
𝐹 → dom 𝐹 ⊆ (◡𝐹 “ dom 1st
)) |
| 33 | 32 | sselda 3983 |
. . . . . . . . 9
⊢ ((Fun
𝐹 ∧ 𝑥 ∈ dom 𝐹) → 𝑥 ∈ (◡𝐹 “ dom 1st
)) |
| 34 | | dmco 6274 |
. . . . . . . . 9
⊢ dom
(1st ∘ 𝐹)
= (◡𝐹 “ dom 1st
) |
| 35 | 33, 34 | eleqtrrdi 2852 |
. . . . . . . 8
⊢ ((Fun
𝐹 ∧ 𝑥 ∈ dom 𝐹) → 𝑥 ∈ dom (1st ∘ 𝐹)) |
| 36 | | fvimacnv 7073 |
. . . . . . . 8
⊢ ((Fun
(1st ∘ 𝐹)
∧ 𝑥 ∈ dom
(1st ∘ 𝐹))
→ (((1st ∘ 𝐹)‘𝑥) ∈ 𝑌 ↔ 𝑥 ∈ (◡(1st ∘ 𝐹) “ 𝑌))) |
| 37 | 23, 35, 36 | syl2anc 584 |
. . . . . . 7
⊢ ((Fun
𝐹 ∧ 𝑥 ∈ dom 𝐹) → (((1st ∘ 𝐹)‘𝑥) ∈ 𝑌 ↔ 𝑥 ∈ (◡(1st ∘ 𝐹) “ 𝑌))) |
| 38 | | fo2nd 8035 |
. . . . . . . . . . 11
⊢
2nd :V–onto→V |
| 39 | | fofun 6821 |
. . . . . . . . . . 11
⊢
(2nd :V–onto→V → Fun 2nd ) |
| 40 | 38, 39 | ax-mp 5 |
. . . . . . . . . 10
⊢ Fun
2nd |
| 41 | | funco 6606 |
. . . . . . . . . 10
⊢ ((Fun
2nd ∧ Fun 𝐹)
→ Fun (2nd ∘ 𝐹)) |
| 42 | 40, 41 | mpan 690 |
. . . . . . . . 9
⊢ (Fun
𝐹 → Fun
(2nd ∘ 𝐹)) |
| 43 | 42 | adantr 480 |
. . . . . . . 8
⊢ ((Fun
𝐹 ∧ 𝑥 ∈ dom 𝐹) → Fun (2nd ∘ 𝐹)) |
| 44 | | fof 6820 |
. . . . . . . . . . . . 13
⊢
(2nd :V–onto→V → 2nd
:V⟶V) |
| 45 | | fdm 6745 |
. . . . . . . . . . . . 13
⊢
(2nd :V⟶V → dom 2nd =
V) |
| 46 | 38, 44, 45 | mp2b 10 |
. . . . . . . . . . . 12
⊢ dom
2nd = V |
| 47 | 24, 46 | sseqtrri 4033 |
. . . . . . . . . . 11
⊢ (𝐹 “ dom 𝐹) ⊆ dom
2nd |
| 48 | | funimass3 7074 |
. . . . . . . . . . . 12
⊢ ((Fun
𝐹 ∧ dom 𝐹 ⊆ dom 𝐹) → ((𝐹 “ dom 𝐹) ⊆ dom 2nd ↔ dom
𝐹 ⊆ (◡𝐹 “ dom 2nd
))) |
| 49 | 29, 48 | mpan2 691 |
. . . . . . . . . . 11
⊢ (Fun
𝐹 → ((𝐹 “ dom 𝐹) ⊆ dom 2nd ↔ dom
𝐹 ⊆ (◡𝐹 “ dom 2nd
))) |
| 50 | 47, 49 | mpbii 233 |
. . . . . . . . . 10
⊢ (Fun
𝐹 → dom 𝐹 ⊆ (◡𝐹 “ dom 2nd
)) |
| 51 | 50 | sselda 3983 |
. . . . . . . . 9
⊢ ((Fun
𝐹 ∧ 𝑥 ∈ dom 𝐹) → 𝑥 ∈ (◡𝐹 “ dom 2nd
)) |
| 52 | | dmco 6274 |
. . . . . . . . 9
⊢ dom
(2nd ∘ 𝐹)
= (◡𝐹 “ dom 2nd
) |
| 53 | 51, 52 | eleqtrrdi 2852 |
. . . . . . . 8
⊢ ((Fun
𝐹 ∧ 𝑥 ∈ dom 𝐹) → 𝑥 ∈ dom (2nd ∘ 𝐹)) |
| 54 | | fvimacnv 7073 |
. . . . . . . 8
⊢ ((Fun
(2nd ∘ 𝐹)
∧ 𝑥 ∈ dom
(2nd ∘ 𝐹))
→ (((2nd ∘ 𝐹)‘𝑥) ∈ 𝑍 ↔ 𝑥 ∈ (◡(2nd ∘ 𝐹) “ 𝑍))) |
| 55 | 43, 53, 54 | syl2anc 584 |
. . . . . . 7
⊢ ((Fun
𝐹 ∧ 𝑥 ∈ dom 𝐹) → (((2nd ∘ 𝐹)‘𝑥) ∈ 𝑍 ↔ 𝑥 ∈ (◡(2nd ∘ 𝐹) “ 𝑍))) |
| 56 | 37, 55 | anbi12d 632 |
. . . . . 6
⊢ ((Fun
𝐹 ∧ 𝑥 ∈ dom 𝐹) → ((((1st ∘ 𝐹)‘𝑥) ∈ 𝑌 ∧ ((2nd ∘ 𝐹)‘𝑥) ∈ 𝑍) ↔ (𝑥 ∈ (◡(1st ∘ 𝐹) “ 𝑌) ∧ 𝑥 ∈ (◡(2nd ∘ 𝐹) “ 𝑍)))) |
| 57 | 56 | adantlr 715 |
. . . . 5
⊢ (((Fun
𝐹 ∧ ran 𝐹 ⊆ (V × V)) ∧
𝑥 ∈ dom 𝐹) → ((((1st
∘ 𝐹)‘𝑥) ∈ 𝑌 ∧ ((2nd ∘ 𝐹)‘𝑥) ∈ 𝑍) ↔ (𝑥 ∈ (◡(1st ∘ 𝐹) “ 𝑌) ∧ 𝑥 ∈ (◡(2nd ∘ 𝐹) “ 𝑍)))) |
| 58 | 15, 17, 57 | 3bitr2d 307 |
. . . 4
⊢ (((Fun
𝐹 ∧ ran 𝐹 ⊆ (V × V)) ∧
𝑥 ∈ dom 𝐹) → ((𝐹‘𝑥) ∈ (𝑌 × 𝑍) ↔ (𝑥 ∈ (◡(1st ∘ 𝐹) “ 𝑌) ∧ 𝑥 ∈ (◡(2nd ∘ 𝐹) “ 𝑍)))) |
| 59 | 58 | rabbidva 3443 |
. . 3
⊢ ((Fun
𝐹 ∧ ran 𝐹 ⊆ (V × V)) →
{𝑥 ∈ dom 𝐹 ∣ (𝐹‘𝑥) ∈ (𝑌 × 𝑍)} = {𝑥 ∈ dom 𝐹 ∣ (𝑥 ∈ (◡(1st ∘ 𝐹) “ 𝑌) ∧ 𝑥 ∈ (◡(2nd ∘ 𝐹) “ 𝑍))}) |
| 60 | 4, 59 | eqtrd 2777 |
. 2
⊢ ((Fun
𝐹 ∧ ran 𝐹 ⊆ (V × V)) →
(◡𝐹 “ (𝑌 × 𝑍)) = {𝑥 ∈ dom 𝐹 ∣ (𝑥 ∈ (◡(1st ∘ 𝐹) “ 𝑌) ∧ 𝑥 ∈ (◡(2nd ∘ 𝐹) “ 𝑍))}) |
| 61 | | dfin5 3959 |
. . . 4
⊢ (dom
𝐹 ∩ (◡(1st ∘ 𝐹) “ 𝑌)) = {𝑥 ∈ dom 𝐹 ∣ 𝑥 ∈ (◡(1st ∘ 𝐹) “ 𝑌)} |
| 62 | | dfin5 3959 |
. . . 4
⊢ (dom
𝐹 ∩ (◡(2nd ∘ 𝐹) “ 𝑍)) = {𝑥 ∈ dom 𝐹 ∣ 𝑥 ∈ (◡(2nd ∘ 𝐹) “ 𝑍)} |
| 63 | 61, 62 | ineq12i 4218 |
. . 3
⊢ ((dom
𝐹 ∩ (◡(1st ∘ 𝐹) “ 𝑌)) ∩ (dom 𝐹 ∩ (◡(2nd ∘ 𝐹) “ 𝑍))) = ({𝑥 ∈ dom 𝐹 ∣ 𝑥 ∈ (◡(1st ∘ 𝐹) “ 𝑌)} ∩ {𝑥 ∈ dom 𝐹 ∣ 𝑥 ∈ (◡(2nd ∘ 𝐹) “ 𝑍)}) |
| 64 | | cnvimass 6100 |
. . . . . 6
⊢ (◡(1st ∘ 𝐹) “ 𝑌) ⊆ dom (1st ∘ 𝐹) |
| 65 | | dmcoss 5985 |
. . . . . 6
⊢ dom
(1st ∘ 𝐹)
⊆ dom 𝐹 |
| 66 | 64, 65 | sstri 3993 |
. . . . 5
⊢ (◡(1st ∘ 𝐹) “ 𝑌) ⊆ dom 𝐹 |
| 67 | | sseqin2 4223 |
. . . . 5
⊢ ((◡(1st ∘ 𝐹) “ 𝑌) ⊆ dom 𝐹 ↔ (dom 𝐹 ∩ (◡(1st ∘ 𝐹) “ 𝑌)) = (◡(1st ∘ 𝐹) “ 𝑌)) |
| 68 | 66, 67 | mpbi 230 |
. . . 4
⊢ (dom
𝐹 ∩ (◡(1st ∘ 𝐹) “ 𝑌)) = (◡(1st ∘ 𝐹) “ 𝑌) |
| 69 | | cnvimass 6100 |
. . . . . 6
⊢ (◡(2nd ∘ 𝐹) “ 𝑍) ⊆ dom (2nd ∘ 𝐹) |
| 70 | | dmcoss 5985 |
. . . . . 6
⊢ dom
(2nd ∘ 𝐹)
⊆ dom 𝐹 |
| 71 | 69, 70 | sstri 3993 |
. . . . 5
⊢ (◡(2nd ∘ 𝐹) “ 𝑍) ⊆ dom 𝐹 |
| 72 | | sseqin2 4223 |
. . . . 5
⊢ ((◡(2nd ∘ 𝐹) “ 𝑍) ⊆ dom 𝐹 ↔ (dom 𝐹 ∩ (◡(2nd ∘ 𝐹) “ 𝑍)) = (◡(2nd ∘ 𝐹) “ 𝑍)) |
| 73 | 71, 72 | mpbi 230 |
. . . 4
⊢ (dom
𝐹 ∩ (◡(2nd ∘ 𝐹) “ 𝑍)) = (◡(2nd ∘ 𝐹) “ 𝑍) |
| 74 | 68, 73 | ineq12i 4218 |
. . 3
⊢ ((dom
𝐹 ∩ (◡(1st ∘ 𝐹) “ 𝑌)) ∩ (dom 𝐹 ∩ (◡(2nd ∘ 𝐹) “ 𝑍))) = ((◡(1st ∘ 𝐹) “ 𝑌) ∩ (◡(2nd ∘ 𝐹) “ 𝑍)) |
| 75 | | inrab 4316 |
. . 3
⊢ ({𝑥 ∈ dom 𝐹 ∣ 𝑥 ∈ (◡(1st ∘ 𝐹) “ 𝑌)} ∩ {𝑥 ∈ dom 𝐹 ∣ 𝑥 ∈ (◡(2nd ∘ 𝐹) “ 𝑍)}) = {𝑥 ∈ dom 𝐹 ∣ (𝑥 ∈ (◡(1st ∘ 𝐹) “ 𝑌) ∧ 𝑥 ∈ (◡(2nd ∘ 𝐹) “ 𝑍))} |
| 76 | 63, 74, 75 | 3eqtr3ri 2774 |
. 2
⊢ {𝑥 ∈ dom 𝐹 ∣ (𝑥 ∈ (◡(1st ∘ 𝐹) “ 𝑌) ∧ 𝑥 ∈ (◡(2nd ∘ 𝐹) “ 𝑍))} = ((◡(1st ∘ 𝐹) “ 𝑌) ∩ (◡(2nd ∘ 𝐹) “ 𝑍)) |
| 77 | 60, 76 | eqtrdi 2793 |
1
⊢ ((Fun
𝐹 ∧ ran 𝐹 ⊆ (V × V)) →
(◡𝐹 “ (𝑌 × 𝑍)) = ((◡(1st ∘ 𝐹) “ 𝑌) ∩ (◡(2nd ∘ 𝐹) “ 𝑍))) |