This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fcoreslem3

Description: Lemma 3 for fcores . (Contributed by AV, 13-Sep-2024)

Ref Expression
Hypotheses fcores.f ⊢ φ → F : A ⟶ B
fcores.e ⊢ E = ran ⁡ F ∩ C
fcores.p ⊢ P = F -1 C
fcores.x ⊢ X = F ↾ P
Assertion fcoreslem3 ⊢ φ → X : P ⟶ onto E

Proof

Step Hyp Ref Expression
1 fcores.f ⊢ φ → F : A ⟶ B
2 fcores.e ⊢ E = ran ⁡ F ∩ C
3 fcores.p ⊢ P = F -1 C
4 fcores.x ⊢ X = F ↾ P
5 1 ffnd ⊢ φ → F Fn A
6 2 a1i ⊢ φ → E = ran ⁡ F ∩ C
7 3 a1i ⊢ φ → P = F -1 C
8 5 6 7 rescnvimafod ⊢ φ → F ↾ P : P ⟶ onto E
9 foeq1 ⊢ X = F ↾ P → X : P ⟶ onto E ↔ F ↾ P : P ⟶ onto E
10 4 9 mp1i ⊢ φ → X : P ⟶ onto E ↔ F ↾ P : P ⟶ onto E
11 8 10 mpbird ⊢ φ → X : P ⟶ onto E