Theorem f1ocnv2d

Description: Describe an implicit one-to-one onto function. (Contributed by Mario Carneiro, 30-Apr-2015)

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

Proof

Step	Hyp	Ref	Expression
1		f1od.1	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐶 )
2		f1o2d.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝐵 )
3		f1o2d.3	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → 𝐷 ∈ 𝐴 )
4		f1o2d.4	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 = 𝐷 ↔ 𝑦 = 𝐶 ) )
5		eleq1a	⊢ ( 𝐶 ∈ 𝐵 → ( 𝑦 = 𝐶 → 𝑦 ∈ 𝐵 ) )
6	2 5	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 = 𝐶 → 𝑦 ∈ 𝐵 ) )
7	6	impr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶 ) ) → 𝑦 ∈ 𝐵 )
8	4	biimpar	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑦 = 𝐶 ) → 𝑥 = 𝐷 )
9	8	exp42	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐵 → ( 𝑦 = 𝐶 → 𝑥 = 𝐷 ) ) ) )
10	9	com34	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → ( 𝑦 = 𝐶 → ( 𝑦 ∈ 𝐵 → 𝑥 = 𝐷 ) ) ) )
11	10	imp32	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶 ) ) → ( 𝑦 ∈ 𝐵 → 𝑥 = 𝐷 ) )
12	7 11	jcai	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶 ) ) → ( 𝑦 ∈ 𝐵 ∧ 𝑥 = 𝐷 ) )
13		eleq1a	⊢ ( 𝐷 ∈ 𝐴 → ( 𝑥 = 𝐷 → 𝑥 ∈ 𝐴 ) )
14	3 13	syl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 = 𝐷 → 𝑥 ∈ 𝐴 ) )
15	14	impr	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 = 𝐷 ) ) → 𝑥 ∈ 𝐴 )
16	4	biimpa	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑥 = 𝐷 ) → 𝑦 = 𝐶 )
17	16	exp42	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐵 → ( 𝑥 = 𝐷 → 𝑦 = 𝐶 ) ) ) )
18	17	com23	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐵 → ( 𝑥 ∈ 𝐴 → ( 𝑥 = 𝐷 → 𝑦 = 𝐶 ) ) ) )
19	18	com34	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐵 → ( 𝑥 = 𝐷 → ( 𝑥 ∈ 𝐴 → 𝑦 = 𝐶 ) ) ) )
20	19	imp32	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 = 𝐷 ) ) → ( 𝑥 ∈ 𝐴 → 𝑦 = 𝐶 ) )
21	15 20	jcai	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 = 𝐷 ) ) → ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶 ) )
22	12 21	impbida	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶 ) ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑥 = 𝐷 ) ) )
23	1 2 3 22	f1ocnvd	⊢ ( 𝜑 → ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ ◡ 𝐹 = ( 𝑦 ∈ 𝐵 ↦ 𝐷 ) ) )