Metamath Proof Explorer


Theorem f1dom4g

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 nor the Axiom of Union. (Contributed by BTernaryTau, 7-Dec-2024)

Ref Expression
Assertion f1dom4g ( ( ( 𝐹𝑉𝐴𝑊𝐵𝑋 ) ∧ 𝐹 : 𝐴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 3ad2antl1 ( ( ( 𝐹𝑉𝐴𝑊𝐵𝑋 ) ∧ 𝐹 : 𝐴1-1𝐵 ) → ∃ 𝑓 𝑓 : 𝐴1-1𝐵 )
5 brdom2g ( ( 𝐴𝑊𝐵𝑋 ) → ( 𝐴𝐵 ↔ ∃ 𝑓 𝑓 : 𝐴1-1𝐵 ) )
6 5 3adant1 ( ( 𝐹𝑉𝐴𝑊𝐵𝑋 ) → ( 𝐴𝐵 ↔ ∃ 𝑓 𝑓 : 𝐴1-1𝐵 ) )
7 6 adantr ( ( ( 𝐹𝑉𝐴𝑊𝐵𝑋 ) ∧ 𝐹 : 𝐴1-1𝐵 ) → ( 𝐴𝐵 ↔ ∃ 𝑓 𝑓 : 𝐴1-1𝐵 ) )
8 4 7 mpbird ( ( ( 𝐹𝑉𝐴𝑊𝐵𝑋 ) ∧ 𝐹 : 𝐴1-1𝐵 ) → 𝐴𝐵 )