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		f1f	⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → 𝐹 : 𝐴 ⟶ 𝐵 )
3	2	biantrurd	⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → ( ran 𝐹 = 𝐵 ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ran 𝐹 = 𝐵 ) ) )
4		dffo2	⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ran 𝐹 = 𝐵 ) )
5	3 4	syl6rbbr	⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → ( 𝐹 : 𝐴 –onto→ 𝐵 ↔ ran 𝐹 = 𝐵 ) )
6	5	pm5.32i	⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) ↔ ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ ran 𝐹 = 𝐵 ) )
7	1 6	bitri	⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ↔ ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ ran 𝐹 = 𝐵 ) )