Theorem nvof1o

Description: An involution is a bijection. (Contributed by Thierry Arnoux, 7-Dec-2016)

	Ref	Expression
Assertion	nvof1o	⊢ ( ( 𝐹 Fn 𝐴 ∧ ◡ 𝐹 = 𝐹 ) → 𝐹 : 𝐴 –1-1-onto→ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		fnfun	⊢ ( 𝐹 Fn 𝐴 → Fun 𝐹 )
2		fdmrn	⊢ ( Fun 𝐹 ↔ 𝐹 : dom 𝐹 ⟶ ran 𝐹 )
3	1 2	sylib	⊢ ( 𝐹 Fn 𝐴 → 𝐹 : dom 𝐹 ⟶ ran 𝐹 )
4	3	adantr	⊢ ( ( 𝐹 Fn 𝐴 ∧ ◡ 𝐹 = 𝐹 ) → 𝐹 : dom 𝐹 ⟶ ran 𝐹 )
5		fndm	⊢ ( 𝐹 Fn 𝐴 → dom 𝐹 = 𝐴 )
6	5	adantr	⊢ ( ( 𝐹 Fn 𝐴 ∧ ◡ 𝐹 = 𝐹 ) → dom 𝐹 = 𝐴 )
7		df-rn	⊢ ran 𝐹 = dom ◡ 𝐹
8		dmeq	⊢ ( ◡ 𝐹 = 𝐹 → dom ◡ 𝐹 = dom 𝐹 )
9	7 8	syl5eq	⊢ ( ◡ 𝐹 = 𝐹 → ran 𝐹 = dom 𝐹 )
10	9 5	sylan9eqr	⊢ ( ( 𝐹 Fn 𝐴 ∧ ◡ 𝐹 = 𝐹 ) → ran 𝐹 = 𝐴 )
11	6 10	feq23d	⊢ ( ( 𝐹 Fn 𝐴 ∧ ◡ 𝐹 = 𝐹 ) → ( 𝐹 : dom 𝐹 ⟶ ran 𝐹 ↔ 𝐹 : 𝐴 ⟶ 𝐴 ) )
12	4 11	mpbid	⊢ ( ( 𝐹 Fn 𝐴 ∧ ◡ 𝐹 = 𝐹 ) → 𝐹 : 𝐴 ⟶ 𝐴 )
13	1	adantr	⊢ ( ( 𝐹 Fn 𝐴 ∧ ◡ 𝐹 = 𝐹 ) → Fun 𝐹 )
14		funeq	⊢ ( ◡ 𝐹 = 𝐹 → ( Fun ◡ 𝐹 ↔ Fun 𝐹 ) )
15	14	adantl	⊢ ( ( 𝐹 Fn 𝐴 ∧ ◡ 𝐹 = 𝐹 ) → ( Fun ◡ 𝐹 ↔ Fun 𝐹 ) )
16	13 15	mpbird	⊢ ( ( 𝐹 Fn 𝐴 ∧ ◡ 𝐹 = 𝐹 ) → Fun ◡ 𝐹 )
17		df-f1	⊢ ( 𝐹 : 𝐴 –1-1→ 𝐴 ↔ ( 𝐹 : 𝐴 ⟶ 𝐴 ∧ Fun ◡ 𝐹 ) )
18	12 16 17	sylanbrc	⊢ ( ( 𝐹 Fn 𝐴 ∧ ◡ 𝐹 = 𝐹 ) → 𝐹 : 𝐴 –1-1→ 𝐴 )
19		simpl	⊢ ( ( 𝐹 Fn 𝐴 ∧ ◡ 𝐹 = 𝐹 ) → 𝐹 Fn 𝐴 )
20		df-fo	⊢ ( 𝐹 : 𝐴 –onto→ 𝐴 ↔ ( 𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐴 ) )
21	19 10 20	sylanbrc	⊢ ( ( 𝐹 Fn 𝐴 ∧ ◡ 𝐹 = 𝐹 ) → 𝐹 : 𝐴 –onto→ 𝐴 )
22		df-f1o	⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ↔ ( 𝐹 : 𝐴 –1-1→ 𝐴 ∧ 𝐹 : 𝐴 –onto→ 𝐴 ) )
23	18 21 22	sylanbrc	⊢ ( ( 𝐹 Fn 𝐴 ∧ ◡ 𝐹 = 𝐹 ) → 𝐹 : 𝐴 –1-1-onto→ 𝐴 )