Proof of Theorem xppreima2
Step | Hyp | Ref
| Expression |
1 | | xppreima2.3 |
. . . 4
⊢ 𝐻 = (𝑥 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉) |
2 | 1 | funmpt2 5841 |
. . 3
⊢ Fun 𝐻 |
3 | | xppreima2.1 |
. . . . . . . 8
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
4 | 3 | ffvelrnda 6267 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝐵) |
5 | | xppreima2.2 |
. . . . . . . 8
⊢ (𝜑 → 𝐺:𝐴⟶𝐶) |
6 | 5 | ffvelrnda 6267 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) ∈ 𝐶) |
7 | | opelxp 5070 |
. . . . . . 7
⊢
(〈(𝐹‘𝑥), (𝐺‘𝑥)〉 ∈ (𝐵 × 𝐶) ↔ ((𝐹‘𝑥) ∈ 𝐵 ∧ (𝐺‘𝑥) ∈ 𝐶)) |
8 | 4, 6, 7 | sylanbrc 695 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 〈(𝐹‘𝑥), (𝐺‘𝑥)〉 ∈ (𝐵 × 𝐶)) |
9 | 8, 1 | fmptd 6292 |
. . . . 5
⊢ (𝜑 → 𝐻:𝐴⟶(𝐵 × 𝐶)) |
10 | | frn 5966 |
. . . . 5
⊢ (𝐻:𝐴⟶(𝐵 × 𝐶) → ran 𝐻 ⊆ (𝐵 × 𝐶)) |
11 | 9, 10 | syl 17 |
. . . 4
⊢ (𝜑 → ran 𝐻 ⊆ (𝐵 × 𝐶)) |
12 | | xpss 5149 |
. . . 4
⊢ (𝐵 × 𝐶) ⊆ (V × V) |
13 | 11, 12 | syl6ss 3580 |
. . 3
⊢ (𝜑 → ran 𝐻 ⊆ (V × V)) |
14 | | xppreima 28829 |
. . 3
⊢ ((Fun
𝐻 ∧ ran 𝐻 ⊆ (V × V)) →
(◡𝐻 “ (𝑌 × 𝑍)) = ((◡(1st ∘ 𝐻) “ 𝑌) ∩ (◡(2nd ∘ 𝐻) “ 𝑍))) |
15 | 2, 13, 14 | sylancr 694 |
. 2
⊢ (𝜑 → (◡𝐻 “ (𝑌 × 𝑍)) = ((◡(1st ∘ 𝐻) “ 𝑌) ∩ (◡(2nd ∘ 𝐻) “ 𝑍))) |
16 | | fo1st 7079 |
. . . . . . . . 9
⊢
1st :V–onto→V |
17 | | fofn 6030 |
. . . . . . . . 9
⊢
(1st :V–onto→V → 1st Fn V) |
18 | 16, 17 | ax-mp 5 |
. . . . . . . 8
⊢
1st Fn V |
19 | | opex 4859 |
. . . . . . . . 9
⊢
〈(𝐹‘𝑥), (𝐺‘𝑥)〉 ∈ V |
20 | 19, 1 | fnmpti 5935 |
. . . . . . . 8
⊢ 𝐻 Fn 𝐴 |
21 | | ssv 3588 |
. . . . . . . 8
⊢ ran 𝐻 ⊆ V |
22 | | fnco 5913 |
. . . . . . . 8
⊢
((1st Fn V ∧ 𝐻 Fn 𝐴 ∧ ran 𝐻 ⊆ V) → (1st ∘
𝐻) Fn 𝐴) |
23 | 18, 20, 21, 22 | mp3an 1416 |
. . . . . . 7
⊢
(1st ∘ 𝐻) Fn 𝐴 |
24 | 23 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (1st ∘
𝐻) Fn 𝐴) |
25 | | ffn 5958 |
. . . . . . 7
⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴) |
26 | 3, 25 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐹 Fn 𝐴) |
27 | 2 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → Fun 𝐻) |
28 | 13 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ran 𝐻 ⊆ (V × V)) |
29 | | simpr 476 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴) |
30 | 19, 1 | dmmpti 5936 |
. . . . . . . . . . 11
⊢ dom 𝐻 = 𝐴 |
31 | 29, 30 | syl6eleqr 2699 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ dom 𝐻) |
32 | | opfv 28828 |
. . . . . . . . . 10
⊢ (((Fun
𝐻 ∧ ran 𝐻 ⊆ (V × V)) ∧
𝑥 ∈ dom 𝐻) → (𝐻‘𝑥) = 〈((1st ∘ 𝐻)‘𝑥), ((2nd ∘ 𝐻)‘𝑥)〉) |
33 | 27, 28, 31, 32 | syl21anc 1317 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐻‘𝑥) = 〈((1st ∘ 𝐻)‘𝑥), ((2nd ∘ 𝐻)‘𝑥)〉) |
34 | 1 | fvmpt2 6200 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝐴 ∧ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉 ∈ (𝐵 × 𝐶)) → (𝐻‘𝑥) = 〈(𝐹‘𝑥), (𝐺‘𝑥)〉) |
35 | 29, 8, 34 | syl2anc 691 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐻‘𝑥) = 〈(𝐹‘𝑥), (𝐺‘𝑥)〉) |
36 | 33, 35 | eqtr3d 2646 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 〈((1st ∘
𝐻)‘𝑥), ((2nd ∘ 𝐻)‘𝑥)〉 = 〈(𝐹‘𝑥), (𝐺‘𝑥)〉) |
37 | | fvex 6113 |
. . . . . . . . 9
⊢
((1st ∘ 𝐻)‘𝑥) ∈ V |
38 | | fvex 6113 |
. . . . . . . . 9
⊢
((2nd ∘ 𝐻)‘𝑥) ∈ V |
39 | 37, 38 | opth 4871 |
. . . . . . . 8
⊢
(〈((1st ∘ 𝐻)‘𝑥), ((2nd ∘ 𝐻)‘𝑥)〉 = 〈(𝐹‘𝑥), (𝐺‘𝑥)〉 ↔ (((1st ∘
𝐻)‘𝑥) = (𝐹‘𝑥) ∧ ((2nd ∘ 𝐻)‘𝑥) = (𝐺‘𝑥))) |
40 | 36, 39 | sylib 207 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((1st ∘ 𝐻)‘𝑥) = (𝐹‘𝑥) ∧ ((2nd ∘ 𝐻)‘𝑥) = (𝐺‘𝑥))) |
41 | 40 | simpld 474 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((1st ∘ 𝐻)‘𝑥) = (𝐹‘𝑥)) |
42 | 24, 26, 41 | eqfnfvd 6222 |
. . . . 5
⊢ (𝜑 → (1st ∘
𝐻) = 𝐹) |
43 | 42 | cnveqd 5220 |
. . . 4
⊢ (𝜑 → ◡(1st ∘ 𝐻) = ◡𝐹) |
44 | 43 | imaeq1d 5384 |
. . 3
⊢ (𝜑 → (◡(1st ∘ 𝐻) “ 𝑌) = (◡𝐹 “ 𝑌)) |
45 | | fo2nd 7080 |
. . . . . . . . 9
⊢
2nd :V–onto→V |
46 | | fofn 6030 |
. . . . . . . . 9
⊢
(2nd :V–onto→V → 2nd Fn V) |
47 | 45, 46 | ax-mp 5 |
. . . . . . . 8
⊢
2nd Fn V |
48 | | fnco 5913 |
. . . . . . . 8
⊢
((2nd Fn V ∧ 𝐻 Fn 𝐴 ∧ ran 𝐻 ⊆ V) → (2nd ∘
𝐻) Fn 𝐴) |
49 | 47, 20, 21, 48 | mp3an 1416 |
. . . . . . 7
⊢
(2nd ∘ 𝐻) Fn 𝐴 |
50 | 49 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (2nd ∘
𝐻) Fn 𝐴) |
51 | | ffn 5958 |
. . . . . . 7
⊢ (𝐺:𝐴⟶𝐶 → 𝐺 Fn 𝐴) |
52 | 5, 51 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐺 Fn 𝐴) |
53 | 40 | simprd 478 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((2nd ∘ 𝐻)‘𝑥) = (𝐺‘𝑥)) |
54 | 50, 52, 53 | eqfnfvd 6222 |
. . . . 5
⊢ (𝜑 → (2nd ∘
𝐻) = 𝐺) |
55 | 54 | cnveqd 5220 |
. . . 4
⊢ (𝜑 → ◡(2nd ∘ 𝐻) = ◡𝐺) |
56 | 55 | imaeq1d 5384 |
. . 3
⊢ (𝜑 → (◡(2nd ∘ 𝐻) “ 𝑍) = (◡𝐺 “ 𝑍)) |
57 | 44, 56 | ineq12d 3777 |
. 2
⊢ (𝜑 → ((◡(1st ∘ 𝐻) “ 𝑌) ∩ (◡(2nd ∘ 𝐻) “ 𝑍)) = ((◡𝐹 “ 𝑌) ∩ (◡𝐺 “ 𝑍))) |
58 | 15, 57 | eqtrd 2644 |
1
⊢ (𝜑 → (◡𝐻 “ (𝑌 × 𝑍)) = ((◡𝐹 “ 𝑌) ∩ (◡𝐺 “ 𝑍))) |