Metamath Proof Explorer

Theorem nvof1o

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

Ref Expression
Assertion nvof1o ⊢ F Fn A ∧ F -1 = F → F : A ⟶ 1-1 onto A

Proof

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