Theorem f1o2d

Description: Describe an implicit one-to-one onto function. (Contributed by Mario Carneiro, 12-May-2014)

	Ref	Expression
Hypotheses	f1od.1	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐶 )
	f1o2d.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝐵 )
	f1o2d.3	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → 𝐷 ∈ 𝐴 )
	f1o2d.4	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 = 𝐷 ↔ 𝑦 = 𝐶 ) )
Assertion	f1o2d	⊢ ( 𝜑 → 𝐹 : 𝐴 –1-1-onto→ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		f1od.1	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐶 )
2		f1o2d.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝐵 )
3		f1o2d.3	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → 𝐷 ∈ 𝐴 )
4		f1o2d.4	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 = 𝐷 ↔ 𝑦 = 𝐶 ) )
5	1 2 3 4	f1ocnv2d	⊢ ( 𝜑 → ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ ◡ 𝐹 = ( 𝑦 ∈ 𝐵 ↦ 𝐷 ) ) )
6	5	simpld	⊢ ( 𝜑 → 𝐹 : 𝐴 –1-1-onto→ 𝐵 )