Metamath Proof Explorer


Theorem dff1o5

Description: Alternate definition of one-to-one onto function. (Contributed by NM, 10-Dec-2003) (Proof shortened by Andrew Salmon, 22-Oct-2011)

Ref Expression
Assertion dff1o5 ( 𝐹 : 𝐴1-1-onto𝐵 ↔ ( 𝐹 : 𝐴1-1𝐵 ∧ ran 𝐹 = 𝐵 ) )

Proof

Step Hyp Ref Expression
1 df-f1o ( 𝐹 : 𝐴1-1-onto𝐵 ↔ ( 𝐹 : 𝐴1-1𝐵𝐹 : 𝐴onto𝐵 ) )
2 dffo2 ( 𝐹 : 𝐴onto𝐵 ↔ ( 𝐹 : 𝐴𝐵 ∧ ran 𝐹 = 𝐵 ) )
3 f1f ( 𝐹 : 𝐴1-1𝐵𝐹 : 𝐴𝐵 )
4 3 biantrurd ( 𝐹 : 𝐴1-1𝐵 → ( ran 𝐹 = 𝐵 ↔ ( 𝐹 : 𝐴𝐵 ∧ ran 𝐹 = 𝐵 ) ) )
5 2 4 bitr4id ( 𝐹 : 𝐴1-1𝐵 → ( 𝐹 : 𝐴onto𝐵 ↔ ran 𝐹 = 𝐵 ) )
6 5 pm5.32i ( ( 𝐹 : 𝐴1-1𝐵𝐹 : 𝐴onto𝐵 ) ↔ ( 𝐹 : 𝐴1-1𝐵 ∧ ran 𝐹 = 𝐵 ) )
7 1 6 bitri ( 𝐹 : 𝐴1-1-onto𝐵 ↔ ( 𝐹 : 𝐴1-1𝐵 ∧ ran 𝐹 = 𝐵 ) )