| Step | Hyp | Ref
| Expression |
| 1 | | fcores.g |
. . . . 5
⊢ (𝜑 → 𝐺:𝐶⟶𝐷) |
| 2 | | fcores.f |
. . . . . 6
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
| 3 | 2 | ffund 6740 |
. . . . 5
⊢ (𝜑 → Fun 𝐹) |
| 4 | | fcof 6759 |
. . . . 5
⊢ ((𝐺:𝐶⟶𝐷 ∧ Fun 𝐹) → (𝐺 ∘ 𝐹):(◡𝐹 “ 𝐶)⟶𝐷) |
| 5 | 1, 3, 4 | syl2anc 584 |
. . . 4
⊢ (𝜑 → (𝐺 ∘ 𝐹):(◡𝐹 “ 𝐶)⟶𝐷) |
| 6 | 5 | ffnd 6737 |
. . 3
⊢ (𝜑 → (𝐺 ∘ 𝐹) Fn (◡𝐹 “ 𝐶)) |
| 7 | | fcores.p |
. . . 4
⊢ 𝑃 = (◡𝐹 “ 𝐶) |
| 8 | 7 | fneq2i 6666 |
. . 3
⊢ ((𝐺 ∘ 𝐹) Fn 𝑃 ↔ (𝐺 ∘ 𝐹) Fn (◡𝐹 “ 𝐶)) |
| 9 | 6, 8 | sylibr 234 |
. 2
⊢ (𝜑 → (𝐺 ∘ 𝐹) Fn 𝑃) |
| 10 | | fcores.e |
. . 3
⊢ 𝐸 = (ran 𝐹 ∩ 𝐶) |
| 11 | | fcores.x |
. . 3
⊢ 𝑋 = (𝐹 ↾ 𝑃) |
| 12 | | fcores.y |
. . 3
⊢ 𝑌 = (𝐺 ↾ 𝐸) |
| 13 | 2, 10, 7, 11, 1, 12 | fcoreslem4 47078 |
. 2
⊢ (𝜑 → (𝑌 ∘ 𝑋) Fn 𝑃) |
| 14 | 11 | fveq1i 6907 |
. . . . . 6
⊢ (𝑋‘𝑥) = ((𝐹 ↾ 𝑃)‘𝑥) |
| 15 | | simpr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑃) → 𝑥 ∈ 𝑃) |
| 16 | 15 | fvresd 6926 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑃) → ((𝐹 ↾ 𝑃)‘𝑥) = (𝐹‘𝑥)) |
| 17 | 14, 16 | eqtrid 2789 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑃) → (𝑋‘𝑥) = (𝐹‘𝑥)) |
| 18 | 17 | fveq2d 6910 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑃) → (𝑌‘(𝑋‘𝑥)) = (𝑌‘(𝐹‘𝑥))) |
| 19 | 12 | fveq1i 6907 |
. . . . 5
⊢ (𝑌‘(𝐹‘𝑥)) = ((𝐺 ↾ 𝐸)‘(𝐹‘𝑥)) |
| 20 | | cnvimass 6100 |
. . . . . . . . . . 11
⊢ (◡𝐹 “ 𝐶) ⊆ dom 𝐹 |
| 21 | 7, 20 | eqsstri 4030 |
. . . . . . . . . 10
⊢ 𝑃 ⊆ dom 𝐹 |
| 22 | 21 | sseli 3979 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝑃 → 𝑥 ∈ dom 𝐹) |
| 23 | | fvelrn 7096 |
. . . . . . . . 9
⊢ ((Fun
𝐹 ∧ 𝑥 ∈ dom 𝐹) → (𝐹‘𝑥) ∈ ran 𝐹) |
| 24 | 3, 22, 23 | syl2an 596 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑃) → (𝐹‘𝑥) ∈ ran 𝐹) |
| 25 | 7 | eleq2i 2833 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝑃 ↔ 𝑥 ∈ (◡𝐹 “ 𝐶)) |
| 26 | 25 | biimpi 216 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝑃 → 𝑥 ∈ (◡𝐹 “ 𝐶)) |
| 27 | | fvimacnvi 7072 |
. . . . . . . . 9
⊢ ((Fun
𝐹 ∧ 𝑥 ∈ (◡𝐹 “ 𝐶)) → (𝐹‘𝑥) ∈ 𝐶) |
| 28 | 3, 26, 27 | syl2an 596 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑃) → (𝐹‘𝑥) ∈ 𝐶) |
| 29 | 24, 28 | elind 4200 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑃) → (𝐹‘𝑥) ∈ (ran 𝐹 ∩ 𝐶)) |
| 30 | 29, 10 | eleqtrrdi 2852 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑃) → (𝐹‘𝑥) ∈ 𝐸) |
| 31 | 30 | fvresd 6926 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑃) → ((𝐺 ↾ 𝐸)‘(𝐹‘𝑥)) = (𝐺‘(𝐹‘𝑥))) |
| 32 | 19, 31 | eqtrid 2789 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑃) → (𝑌‘(𝐹‘𝑥)) = (𝐺‘(𝐹‘𝑥))) |
| 33 | 18, 32 | eqtrd 2777 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑃) → (𝑌‘(𝑋‘𝑥)) = (𝐺‘(𝐹‘𝑥))) |
| 34 | 2, 10, 7, 11 | fcoreslem3 47077 |
. . . . . 6
⊢ (𝜑 → 𝑋:𝑃–onto→𝐸) |
| 35 | | fof 6820 |
. . . . . 6
⊢ (𝑋:𝑃–onto→𝐸 → 𝑋:𝑃⟶𝐸) |
| 36 | 34, 35 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑋:𝑃⟶𝐸) |
| 37 | 36 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑃) → 𝑋:𝑃⟶𝐸) |
| 38 | 37, 15 | fvco3d 7009 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑃) → ((𝑌 ∘ 𝑋)‘𝑥) = (𝑌‘(𝑋‘𝑥))) |
| 39 | 2 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑃) → 𝐹:𝐴⟶𝐵) |
| 40 | 21 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 𝑃 ⊆ dom 𝐹) |
| 41 | 40 | sselda 3983 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑃) → 𝑥 ∈ dom 𝐹) |
| 42 | 2 | fdmd 6746 |
. . . . . . . 8
⊢ (𝜑 → dom 𝐹 = 𝐴) |
| 43 | 42 | eqcomd 2743 |
. . . . . . 7
⊢ (𝜑 → 𝐴 = dom 𝐹) |
| 44 | 43 | eleq2d 2827 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ dom 𝐹)) |
| 45 | 44 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑃) → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ dom 𝐹)) |
| 46 | 41, 45 | mpbird 257 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑃) → 𝑥 ∈ 𝐴) |
| 47 | 39, 46 | fvco3d 7009 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑃) → ((𝐺 ∘ 𝐹)‘𝑥) = (𝐺‘(𝐹‘𝑥))) |
| 48 | 33, 38, 47 | 3eqtr4rd 2788 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑃) → ((𝐺 ∘ 𝐹)‘𝑥) = ((𝑌 ∘ 𝑋)‘𝑥)) |
| 49 | 9, 13, 48 | eqfnfvd 7054 |
1
⊢ (𝜑 → (𝐺 ∘ 𝐹) = (𝑌 ∘ 𝑋)) |