Metamath Proof Explorer


Theorem fodomg

Description: An onto function implies dominance of domain over range. Lemma 10.20 of Kunen p. 30. This theorem uses the axiom of choice ac7g . The axiom of choice is not needed for finite sets, see fodomfi . See also fodomnum . (Contributed by NM, 23-Jul-2004) (Proof shortened by BJ, 20-May-2024)

Ref Expression
Assertion fodomg ( 𝐴𝑉 → ( 𝐹 : 𝐴onto𝐵𝐵𝐴 ) )

Proof

Step Hyp Ref Expression
1 numth3 ( 𝐴𝑉𝐴 ∈ dom card )
2 fodomnum ( 𝐴 ∈ dom card → ( 𝐹 : 𝐴onto𝐵𝐵𝐴 ) )
3 1 2 syl ( 𝐴𝑉 → ( 𝐹 : 𝐴onto𝐵𝐵𝐴 ) )