Metamath Proof Explorer

Theorem fundcmpsurinjlem2

Description: Lemma 2 for fundcmpsurinj . (Contributed by AV, 4-Mar-2024)

Ref Expression
Hypotheses fundcmpsurinj.p ⊢ P = z | ∃ x ∈ A z = F -1 F ⁡ x
fundcmpsurinj.g ⊢ G = x ∈ A ⟼ F -1 F ⁡ x
Assertion fundcmpsurinjlem2 ⊢ F Fn A ∧ A ∈ V → G : A ⟶ onto P

Proof

Step Hyp Ref Expression
1 fundcmpsurinj.p ⊢ P = z | ∃ x ∈ A z = F -1 F ⁡ x
2 fundcmpsurinj.g ⊢ G = x ∈ A ⟼ F -1 F ⁡ x
3 fnex ⊢ F Fn A ∧ A ∈ V → F ∈ V
4 cnvexg ⊢ F ∈ V → F -1 ∈ V
5 imaexg ⊢ F -1 ∈ V → F -1 F ⁡ x ∈ V
6 3 4 5 3syl ⊢ F Fn A ∧ A ∈ V → F -1 F ⁡ x ∈ V
7 6 ralrimivw ⊢ F Fn A ∧ A ∈ V → ∀ x ∈ A F -1 F ⁡ x ∈ V
8 2 fnmpt ⊢ ∀ x ∈ A F -1 F ⁡ x ∈ V → G Fn A
9 7 8 syl ⊢ F Fn A ∧ A ∈ V → G Fn A
10 1 2 fundcmpsurinjlem1 ⊢ ran ⁡ G = P
11 df-fo ⊢ G : A ⟶ onto P ↔ G Fn A ∧ ran ⁡ G = P
12 9 10 11 sylanblrc ⊢ F Fn A ∧ A ∈ V → G : A ⟶ onto P