Metamath Proof Explorer


Theorem f1dom2gOLD

Description: Obsolete version of f1dom2g as of 25-Sep-2024. (Contributed by Mario Carneiro, 24-Jun-2015) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 f1f ( 𝐹 : 𝐴1-1𝐵𝐹 : 𝐴𝐵 )
2 fex2 ( ( 𝐹 : 𝐴𝐵𝐴𝑉𝐵𝑊 ) → 𝐹 ∈ V )
3 1 2 syl3an1 ( ( 𝐹 : 𝐴1-1𝐵𝐴𝑉𝐵𝑊 ) → 𝐹 ∈ V )
4 3 3coml ( ( 𝐴𝑉𝐵𝑊𝐹 : 𝐴1-1𝐵 ) → 𝐹 ∈ V )
5 simp3 ( ( 𝐴𝑉𝐵𝑊𝐹 : 𝐴1-1𝐵 ) → 𝐹 : 𝐴1-1𝐵 )
6 f1eq1 ( 𝑓 = 𝐹 → ( 𝑓 : 𝐴1-1𝐵𝐹 : 𝐴1-1𝐵 ) )
7 4 5 6 spcedv ( ( 𝐴𝑉𝐵𝑊𝐹 : 𝐴1-1𝐵 ) → ∃ 𝑓 𝑓 : 𝐴1-1𝐵 )
8 brdomg ( 𝐵𝑊 → ( 𝐴𝐵 ↔ ∃ 𝑓 𝑓 : 𝐴1-1𝐵 ) )
9 8 3ad2ant2 ( ( 𝐴𝑉𝐵𝑊𝐹 : 𝐴1-1𝐵 ) → ( 𝐴𝐵 ↔ ∃ 𝑓 𝑓 : 𝐴1-1𝐵 ) )
10 7 9 mpbird ( ( 𝐴𝑉𝐵𝑊𝐹 : 𝐴1-1𝐵 ) → 𝐴𝐵 )