Theorem f1o3d

Description: Describe an implicit one-to-one onto function. (Contributed by Thierry Arnoux, 23-Apr-2017)

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

Proof

Step	Hyp	Ref	Expression
1		f1o3d.1	⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) )
2		f1o3d.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝐵 )
3		f1o3d.3	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → 𝐷 ∈ 𝐴 )
4		f1o3d.4	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 = 𝐷 ↔ 𝑦 = 𝐶 ) )
5	2	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 )
6		eqid	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐶 )
7	6	fnmpt	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) Fn 𝐴 )
8	5 7	syl	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) Fn 𝐴 )
9	1	fneq1d	⊢ ( 𝜑 → ( 𝐹 Fn 𝐴 ↔ ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) Fn 𝐴 ) )
10	8 9	mpbird	⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
11	3	ralrimiva	⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝐵 𝐷 ∈ 𝐴 )
12		eqid	⊢ ( 𝑦 ∈ 𝐵 ↦ 𝐷 ) = ( 𝑦 ∈ 𝐵 ↦ 𝐷 )
13	12	fnmpt	⊢ ( ∀ 𝑦 ∈ 𝐵 𝐷 ∈ 𝐴 → ( 𝑦 ∈ 𝐵 ↦ 𝐷 ) Fn 𝐵 )
14	11 13	syl	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐵 ↦ 𝐷 ) Fn 𝐵 )
15		eleq1a	⊢ ( 𝐶 ∈ 𝐵 → ( 𝑦 = 𝐶 → 𝑦 ∈ 𝐵 ) )
16	2 15	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 = 𝐶 → 𝑦 ∈ 𝐵 ) )
17	16	impr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶 ) ) → 𝑦 ∈ 𝐵 )
18	4	biimpar	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑦 = 𝐶 ) → 𝑥 = 𝐷 )
19	18	exp42	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐵 → ( 𝑦 = 𝐶 → 𝑥 = 𝐷 ) ) ) )
20	19	com34	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → ( 𝑦 = 𝐶 → ( 𝑦 ∈ 𝐵 → 𝑥 = 𝐷 ) ) ) )
21	20	imp32	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶 ) ) → ( 𝑦 ∈ 𝐵 → 𝑥 = 𝐷 ) )
22	17 21	jcai	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶 ) ) → ( 𝑦 ∈ 𝐵 ∧ 𝑥 = 𝐷 ) )
23		eleq1a	⊢ ( 𝐷 ∈ 𝐴 → ( 𝑥 = 𝐷 → 𝑥 ∈ 𝐴 ) )
24	3 23	syl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 = 𝐷 → 𝑥 ∈ 𝐴 ) )
25	24	impr	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 = 𝐷 ) ) → 𝑥 ∈ 𝐴 )
26	4	biimpa	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑥 = 𝐷 ) → 𝑦 = 𝐶 )
27	26	exp42	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐵 → ( 𝑥 = 𝐷 → 𝑦 = 𝐶 ) ) ) )
28	27	com23	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐵 → ( 𝑥 ∈ 𝐴 → ( 𝑥 = 𝐷 → 𝑦 = 𝐶 ) ) ) )
29	28	com34	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐵 → ( 𝑥 = 𝐷 → ( 𝑥 ∈ 𝐴 → 𝑦 = 𝐶 ) ) ) )
30	29	imp32	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 = 𝐷 ) ) → ( 𝑥 ∈ 𝐴 → 𝑦 = 𝐶 ) )
31	25 30	jcai	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 = 𝐷 ) ) → ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶 ) )
32	22 31	impbida	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶 ) ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑥 = 𝐷 ) ) )
33	32	opabbidv	⊢ ( 𝜑 → { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶 ) } = { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( 𝑦 ∈ 𝐵 ∧ 𝑥 = 𝐷 ) } )
34		df-mpt	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶 ) }
35	1 34	eqtrdi	⊢ ( 𝜑 → 𝐹 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶 ) } )
36	35	cnveqd	⊢ ( 𝜑 → ◡ 𝐹 = ◡ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶 ) } )
37		cnvopab	⊢ ◡ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶 ) } = { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶 ) }
38	36 37	eqtrdi	⊢ ( 𝜑 → ◡ 𝐹 = { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶 ) } )
39		df-mpt	⊢ ( 𝑦 ∈ 𝐵 ↦ 𝐷 ) = { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( 𝑦 ∈ 𝐵 ∧ 𝑥 = 𝐷 ) }
40	39	a1i	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐵 ↦ 𝐷 ) = { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( 𝑦 ∈ 𝐵 ∧ 𝑥 = 𝐷 ) } )
41	33 38 40	3eqtr4d	⊢ ( 𝜑 → ◡ 𝐹 = ( 𝑦 ∈ 𝐵 ↦ 𝐷 ) )
42	41	fneq1d	⊢ ( 𝜑 → ( ◡ 𝐹 Fn 𝐵 ↔ ( 𝑦 ∈ 𝐵 ↦ 𝐷 ) Fn 𝐵 ) )
43	14 42	mpbird	⊢ ( 𝜑 → ◡ 𝐹 Fn 𝐵 )
44		dff1o4	⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ↔ ( 𝐹 Fn 𝐴 ∧ ◡ 𝐹 Fn 𝐵 ) )
45	10 43 44	sylanbrc	⊢ ( 𝜑 → 𝐹 : 𝐴 –1-1-onto→ 𝐵 )
46	45 41	jca	⊢ ( 𝜑 → ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ ◡ 𝐹 = ( 𝑦 ∈ 𝐵 ↦ 𝐷 ) ) )