This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 eqtrid ⊢ ( ◡ 𝐹 = 𝐹 → 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→ 𝐴 )