Proof of Theorem f1cof1blem
| Step | Hyp | Ref
| Expression |
| 1 | | fcores.p |
. . . . 5
⊢ 𝑃 = (◡𝐹 “ 𝐶) |
| 2 | | f1cof1blem.s |
. . . . . . 7
⊢ (𝜑 → ran 𝐹 = 𝐶) |
| 3 | 2 | eqcomd 2743 |
. . . . . 6
⊢ (𝜑 → 𝐶 = ran 𝐹) |
| 4 | 3 | imaeq2d 6078 |
. . . . 5
⊢ (𝜑 → (◡𝐹 “ 𝐶) = (◡𝐹 “ ran 𝐹)) |
| 5 | 1, 4 | eqtrid 2789 |
. . . 4
⊢ (𝜑 → 𝑃 = (◡𝐹 “ ran 𝐹)) |
| 6 | | cnvimarndm 6101 |
. . . . 5
⊢ (◡𝐹 “ ran 𝐹) = dom 𝐹 |
| 7 | | fcores.f |
. . . . . 6
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
| 8 | 7 | fdmd 6746 |
. . . . 5
⊢ (𝜑 → dom 𝐹 = 𝐴) |
| 9 | 6, 8 | eqtrid 2789 |
. . . 4
⊢ (𝜑 → (◡𝐹 “ ran 𝐹) = 𝐴) |
| 10 | 5, 9 | eqtrd 2777 |
. . 3
⊢ (𝜑 → 𝑃 = 𝐴) |
| 11 | | fcores.e |
. . . 4
⊢ 𝐸 = (ran 𝐹 ∩ 𝐶) |
| 12 | | simpr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ ran 𝐹 = 𝐶) → ran 𝐹 = 𝐶) |
| 13 | 12 | ineq1d 4219 |
. . . . . 6
⊢ ((𝜑 ∧ ran 𝐹 = 𝐶) → (ran 𝐹 ∩ 𝐶) = (𝐶 ∩ 𝐶)) |
| 14 | | inidm 4227 |
. . . . . 6
⊢ (𝐶 ∩ 𝐶) = 𝐶 |
| 15 | 13, 14 | eqtrdi 2793 |
. . . . 5
⊢ ((𝜑 ∧ ran 𝐹 = 𝐶) → (ran 𝐹 ∩ 𝐶) = 𝐶) |
| 16 | 2, 15 | mpdan 687 |
. . . 4
⊢ (𝜑 → (ran 𝐹 ∩ 𝐶) = 𝐶) |
| 17 | 11, 16 | eqtrid 2789 |
. . 3
⊢ (𝜑 → 𝐸 = 𝐶) |
| 18 | 10, 17 | jca 511 |
. 2
⊢ (𝜑 → (𝑃 = 𝐴 ∧ 𝐸 = 𝐶)) |
| 19 | | fcores.x |
. . . 4
⊢ 𝑋 = (𝐹 ↾ 𝑃) |
| 20 | 5, 6 | eqtrdi 2793 |
. . . . 5
⊢ (𝜑 → 𝑃 = dom 𝐹) |
| 21 | 20 | reseq2d 5997 |
. . . 4
⊢ (𝜑 → (𝐹 ↾ 𝑃) = (𝐹 ↾ dom 𝐹)) |
| 22 | 19, 21 | eqtrid 2789 |
. . 3
⊢ (𝜑 → 𝑋 = (𝐹 ↾ dom 𝐹)) |
| 23 | 7 | freld 6742 |
. . . 4
⊢ (𝜑 → Rel 𝐹) |
| 24 | | resdm 6044 |
. . . 4
⊢ (Rel
𝐹 → (𝐹 ↾ dom 𝐹) = 𝐹) |
| 25 | 23, 24 | syl 17 |
. . 3
⊢ (𝜑 → (𝐹 ↾ dom 𝐹) = 𝐹) |
| 26 | 22, 25 | eqtrd 2777 |
. 2
⊢ (𝜑 → 𝑋 = 𝐹) |
| 27 | | fcores.y |
. . . 4
⊢ 𝑌 = (𝐺 ↾ 𝐸) |
| 28 | | fcores.g |
. . . . . . 7
⊢ (𝜑 → 𝐺:𝐶⟶𝐷) |
| 29 | 28 | fdmd 6746 |
. . . . . 6
⊢ (𝜑 → dom 𝐺 = 𝐶) |
| 30 | 17, 29 | eqtr4d 2780 |
. . . . 5
⊢ (𝜑 → 𝐸 = dom 𝐺) |
| 31 | 30 | reseq2d 5997 |
. . . 4
⊢ (𝜑 → (𝐺 ↾ 𝐸) = (𝐺 ↾ dom 𝐺)) |
| 32 | 27, 31 | eqtrid 2789 |
. . 3
⊢ (𝜑 → 𝑌 = (𝐺 ↾ dom 𝐺)) |
| 33 | 28 | freld 6742 |
. . . 4
⊢ (𝜑 → Rel 𝐺) |
| 34 | | resdm 6044 |
. . . 4
⊢ (Rel
𝐺 → (𝐺 ↾ dom 𝐺) = 𝐺) |
| 35 | 33, 34 | syl 17 |
. . 3
⊢ (𝜑 → (𝐺 ↾ dom 𝐺) = 𝐺) |
| 36 | 32, 35 | eqtrd 2777 |
. 2
⊢ (𝜑 → 𝑌 = 𝐺) |
| 37 | 18, 26, 36 | jca32 515 |
1
⊢ (𝜑 → ((𝑃 = 𝐴 ∧ 𝐸 = 𝐶) ∧ (𝑋 = 𝐹 ∧ 𝑌 = 𝐺))) |