Metamath Proof Explorer


Theorem f1dom3g

Description: The domain of a one-to-one set function is dominated by its codomain when the latter is a set. This variation of f1domg does not require the Axiom of Replacement nor the Axiom of Power Sets. (Contributed by BTernaryTau, 9-Sep-2024)

Ref Expression
Assertion f1dom3g ( ( 𝐹𝑉𝐵𝑊𝐹 : 𝐴1-1𝐵 ) → 𝐴𝐵 )

Proof

Step Hyp Ref Expression
1 f1eq1 ( 𝑓 = 𝐹 → ( 𝑓 : 𝐴1-1𝐵𝐹 : 𝐴1-1𝐵 ) )
2 1 spcegv ( 𝐹𝑉 → ( 𝐹 : 𝐴1-1𝐵 → ∃ 𝑓 𝑓 : 𝐴1-1𝐵 ) )
3 2 imp ( ( 𝐹𝑉𝐹 : 𝐴1-1𝐵 ) → ∃ 𝑓 𝑓 : 𝐴1-1𝐵 )
4 3 3adant2 ( ( 𝐹𝑉𝐵𝑊𝐹 : 𝐴1-1𝐵 ) → ∃ 𝑓 𝑓 : 𝐴1-1𝐵 )
5 brdomg ( 𝐵𝑊 → ( 𝐴𝐵 ↔ ∃ 𝑓 𝑓 : 𝐴1-1𝐵 ) )
6 5 3ad2ant2 ( ( 𝐹𝑉𝐵𝑊𝐹 : 𝐴1-1𝐵 ) → ( 𝐴𝐵 ↔ ∃ 𝑓 𝑓 : 𝐴1-1𝐵 ) )
7 4 6 mpbird ( ( 𝐹𝑉𝐵𝑊𝐹 : 𝐴1-1𝐵 ) → 𝐴𝐵 )