Proof of Theorem xppreima2
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | xppreima2.3 | . . . 4
⊢ 𝐻 = (𝑥 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉) | 
| 2 | 1 | funmpt2 6604 | . . 3
⊢ Fun 𝐻 | 
| 3 |  | xppreima2.1 | . . . . . . . 8
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) | 
| 4 | 3 | ffvelcdmda 7103 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝐵) | 
| 5 |  | xppreima2.2 | . . . . . . . 8
⊢ (𝜑 → 𝐺:𝐴⟶𝐶) | 
| 6 | 5 | ffvelcdmda 7103 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) ∈ 𝐶) | 
| 7 |  | opelxp 5720 | . . . . . . 7
⊢
(〈(𝐹‘𝑥), (𝐺‘𝑥)〉 ∈ (𝐵 × 𝐶) ↔ ((𝐹‘𝑥) ∈ 𝐵 ∧ (𝐺‘𝑥) ∈ 𝐶)) | 
| 8 | 4, 6, 7 | sylanbrc 583 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 〈(𝐹‘𝑥), (𝐺‘𝑥)〉 ∈ (𝐵 × 𝐶)) | 
| 9 | 8, 1 | fmptd 7133 | . . . . 5
⊢ (𝜑 → 𝐻:𝐴⟶(𝐵 × 𝐶)) | 
| 10 | 9 | frnd 6743 | . . . 4
⊢ (𝜑 → ran 𝐻 ⊆ (𝐵 × 𝐶)) | 
| 11 |  | xpss 5700 | . . . 4
⊢ (𝐵 × 𝐶) ⊆ (V × V) | 
| 12 | 10, 11 | sstrdi 3995 | . . 3
⊢ (𝜑 → ran 𝐻 ⊆ (V × V)) | 
| 13 |  | xppreima 32656 | . . 3
⊢ ((Fun
𝐻 ∧ ran 𝐻 ⊆ (V × V)) →
(◡𝐻 “ (𝑌 × 𝑍)) = ((◡(1st ∘ 𝐻) “ 𝑌) ∩ (◡(2nd ∘ 𝐻) “ 𝑍))) | 
| 14 | 2, 12, 13 | sylancr 587 | . 2
⊢ (𝜑 → (◡𝐻 “ (𝑌 × 𝑍)) = ((◡(1st ∘ 𝐻) “ 𝑌) ∩ (◡(2nd ∘ 𝐻) “ 𝑍))) | 
| 15 |  | fo1st 8035 | . . . . . . . . 9
⊢
1st :V–onto→V | 
| 16 |  | fofn 6821 | . . . . . . . . 9
⊢
(1st :V–onto→V → 1st Fn V) | 
| 17 | 15, 16 | ax-mp 5 | . . . . . . . 8
⊢
1st Fn V | 
| 18 |  | opex 5468 | . . . . . . . . 9
⊢
〈(𝐹‘𝑥), (𝐺‘𝑥)〉 ∈ V | 
| 19 | 18, 1 | fnmpti 6710 | . . . . . . . 8
⊢ 𝐻 Fn 𝐴 | 
| 20 |  | ssv 4007 | . . . . . . . 8
⊢ ran 𝐻 ⊆ V | 
| 21 |  | fnco 6685 | . . . . . . . 8
⊢
((1st Fn V ∧ 𝐻 Fn 𝐴 ∧ ran 𝐻 ⊆ V) → (1st ∘
𝐻) Fn 𝐴) | 
| 22 | 17, 19, 20, 21 | mp3an 1462 | . . . . . . 7
⊢
(1st ∘ 𝐻) Fn 𝐴 | 
| 23 | 22 | a1i 11 | . . . . . 6
⊢ (𝜑 → (1st ∘
𝐻) Fn 𝐴) | 
| 24 | 3 | ffnd 6736 | . . . . . 6
⊢ (𝜑 → 𝐹 Fn 𝐴) | 
| 25 | 2 | a1i 11 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → Fun 𝐻) | 
| 26 | 12 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ran 𝐻 ⊆ (V × V)) | 
| 27 |  | simpr 484 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴) | 
| 28 | 18, 1 | dmmpti 6711 | . . . . . . . . . . 11
⊢ dom 𝐻 = 𝐴 | 
| 29 | 27, 28 | eleqtrrdi 2851 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ dom 𝐻) | 
| 30 |  | opfv 32655 | . . . . . . . . . 10
⊢ (((Fun
𝐻 ∧ ran 𝐻 ⊆ (V × V)) ∧
𝑥 ∈ dom 𝐻) → (𝐻‘𝑥) = 〈((1st ∘ 𝐻)‘𝑥), ((2nd ∘ 𝐻)‘𝑥)〉) | 
| 31 | 25, 26, 29, 30 | syl21anc 837 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐻‘𝑥) = 〈((1st ∘ 𝐻)‘𝑥), ((2nd ∘ 𝐻)‘𝑥)〉) | 
| 32 | 1 | fvmpt2 7026 | . . . . . . . . . 10
⊢ ((𝑥 ∈ 𝐴 ∧ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉 ∈ (𝐵 × 𝐶)) → (𝐻‘𝑥) = 〈(𝐹‘𝑥), (𝐺‘𝑥)〉) | 
| 33 | 27, 8, 32 | syl2anc 584 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐻‘𝑥) = 〈(𝐹‘𝑥), (𝐺‘𝑥)〉) | 
| 34 | 31, 33 | eqtr3d 2778 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 〈((1st ∘
𝐻)‘𝑥), ((2nd ∘ 𝐻)‘𝑥)〉 = 〈(𝐹‘𝑥), (𝐺‘𝑥)〉) | 
| 35 |  | fvex 6918 | . . . . . . . . 9
⊢
((1st ∘ 𝐻)‘𝑥) ∈ V | 
| 36 |  | fvex 6918 | . . . . . . . . 9
⊢
((2nd ∘ 𝐻)‘𝑥) ∈ V | 
| 37 | 35, 36 | opth 5480 | . . . . . . . 8
⊢
(〈((1st ∘ 𝐻)‘𝑥), ((2nd ∘ 𝐻)‘𝑥)〉 = 〈(𝐹‘𝑥), (𝐺‘𝑥)〉 ↔ (((1st ∘
𝐻)‘𝑥) = (𝐹‘𝑥) ∧ ((2nd ∘ 𝐻)‘𝑥) = (𝐺‘𝑥))) | 
| 38 | 34, 37 | sylib 218 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((1st ∘ 𝐻)‘𝑥) = (𝐹‘𝑥) ∧ ((2nd ∘ 𝐻)‘𝑥) = (𝐺‘𝑥))) | 
| 39 | 38 | simpld 494 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((1st ∘ 𝐻)‘𝑥) = (𝐹‘𝑥)) | 
| 40 | 23, 24, 39 | eqfnfvd 7053 | . . . . 5
⊢ (𝜑 → (1st ∘
𝐻) = 𝐹) | 
| 41 | 40 | cnveqd 5885 | . . . 4
⊢ (𝜑 → ◡(1st ∘ 𝐻) = ◡𝐹) | 
| 42 | 41 | imaeq1d 6076 | . . 3
⊢ (𝜑 → (◡(1st ∘ 𝐻) “ 𝑌) = (◡𝐹 “ 𝑌)) | 
| 43 |  | fo2nd 8036 | . . . . . . . . 9
⊢
2nd :V–onto→V | 
| 44 |  | fofn 6821 | . . . . . . . . 9
⊢
(2nd :V–onto→V → 2nd Fn V) | 
| 45 | 43, 44 | ax-mp 5 | . . . . . . . 8
⊢
2nd Fn V | 
| 46 |  | fnco 6685 | . . . . . . . 8
⊢
((2nd Fn V ∧ 𝐻 Fn 𝐴 ∧ ran 𝐻 ⊆ V) → (2nd ∘
𝐻) Fn 𝐴) | 
| 47 | 45, 19, 20, 46 | mp3an 1462 | . . . . . . 7
⊢
(2nd ∘ 𝐻) Fn 𝐴 | 
| 48 | 47 | a1i 11 | . . . . . 6
⊢ (𝜑 → (2nd ∘
𝐻) Fn 𝐴) | 
| 49 | 5 | ffnd 6736 | . . . . . 6
⊢ (𝜑 → 𝐺 Fn 𝐴) | 
| 50 | 38 | simprd 495 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((2nd ∘ 𝐻)‘𝑥) = (𝐺‘𝑥)) | 
| 51 | 48, 49, 50 | eqfnfvd 7053 | . . . . 5
⊢ (𝜑 → (2nd ∘
𝐻) = 𝐺) | 
| 52 | 51 | cnveqd 5885 | . . . 4
⊢ (𝜑 → ◡(2nd ∘ 𝐻) = ◡𝐺) | 
| 53 | 52 | imaeq1d 6076 | . . 3
⊢ (𝜑 → (◡(2nd ∘ 𝐻) “ 𝑍) = (◡𝐺 “ 𝑍)) | 
| 54 | 42, 53 | ineq12d 4220 | . 2
⊢ (𝜑 → ((◡(1st ∘ 𝐻) “ 𝑌) ∩ (◡(2nd ∘ 𝐻) “ 𝑍)) = ((◡𝐹 “ 𝑌) ∩ (◡𝐺 “ 𝑍))) | 
| 55 | 14, 54 | eqtrd 2776 | 1
⊢ (𝜑 → (◡𝐻 “ (𝑌 × 𝑍)) = ((◡𝐹 “ 𝑌) ∩ (◡𝐺 “ 𝑍))) |