Metamath Proof Explorer


Theorem f1imaen3g

Description: If a set function is one-to-one, then a subset of its domain is equinumerous to the image of that subset. (This version of f1imaeng does not need ax-rep nor ax-pow .) (Contributed by BTernaryTau, 13-Jan-2025)

Ref Expression
Assertion f1imaen3g ( ( 𝐹 : 𝐴1-1𝐵𝐶𝐴𝐹𝑉 ) → 𝐶 ≈ ( 𝐹𝐶 ) )

Proof

Step Hyp Ref Expression
1 resexg ( 𝐹𝑉 → ( 𝐹𝐶 ) ∈ V )
2 1 3ad2ant3 ( ( 𝐹 : 𝐴1-1𝐵𝐶𝐴𝐹𝑉 ) → ( 𝐹𝐶 ) ∈ V )
3 f1ores ( ( 𝐹 : 𝐴1-1𝐵𝐶𝐴 ) → ( 𝐹𝐶 ) : 𝐶1-1-onto→ ( 𝐹𝐶 ) )
4 3 3adant3 ( ( 𝐹 : 𝐴1-1𝐵𝐶𝐴𝐹𝑉 ) → ( 𝐹𝐶 ) : 𝐶1-1-onto→ ( 𝐹𝐶 ) )
5 f1oen3g ( ( ( 𝐹𝐶 ) ∈ V ∧ ( 𝐹𝐶 ) : 𝐶1-1-onto→ ( 𝐹𝐶 ) ) → 𝐶 ≈ ( 𝐹𝐶 ) )
6 2 4 5 syl2anc ( ( 𝐹 : 𝐴1-1𝐵𝐶𝐴𝐹𝑉 ) → 𝐶 ≈ ( 𝐹𝐶 ) )