Metamath Proof Explorer


Theorem f1dmex

Description: If the codomain of a one-to-one function exists, so does its domain. This theorem is equivalent to the Axiom of Replacement ax-rep . (Contributed by NM, 4-Sep-2004)

Ref Expression
Assertion f1dmex ( ( 𝐹 : 𝐴1-1𝐵𝐵𝐶 ) → 𝐴 ∈ V )

Proof

Step Hyp Ref Expression
1 f1f ( 𝐹 : 𝐴1-1𝐵𝐹 : 𝐴𝐵 )
2 1 frnd ( 𝐹 : 𝐴1-1𝐵 → ran 𝐹𝐵 )
3 ssexg ( ( ran 𝐹𝐵𝐵𝐶 ) → ran 𝐹 ∈ V )
4 2 3 sylan ( ( 𝐹 : 𝐴1-1𝐵𝐵𝐶 ) → ran 𝐹 ∈ V )
5 4 ex ( 𝐹 : 𝐴1-1𝐵 → ( 𝐵𝐶 → ran 𝐹 ∈ V ) )
6 f1cnv ( 𝐹 : 𝐴1-1𝐵 𝐹 : ran 𝐹1-1-onto𝐴 )
7 f1ofo ( 𝐹 : ran 𝐹1-1-onto𝐴 𝐹 : ran 𝐹onto𝐴 )
8 6 7 syl ( 𝐹 : 𝐴1-1𝐵 𝐹 : ran 𝐹onto𝐴 )
9 fornex ( ran 𝐹 ∈ V → ( 𝐹 : ran 𝐹onto𝐴𝐴 ∈ V ) )
10 5 8 9 syl6ci ( 𝐹 : 𝐴1-1𝐵 → ( 𝐵𝐶𝐴 ∈ V ) )
11 10 imp ( ( 𝐹 : 𝐴1-1𝐵𝐵𝐶 ) → 𝐴 ∈ V )