Metamath Proof Explorer

Theorem nvocnv

Description: The converse of an involution is the function itself. (Contributed by Thierry Arnoux, 7-May-2019)

Ref Expression
Assertion nvocnv ( ( 𝐹 : 𝐴 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ ( 𝐹 ‘ 𝑥 ) ) = 𝑥 ) → ◡ 𝐹 = 𝐹 )

Proof

Step Hyp Ref Expression
1 simprr ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ ( 𝐹 ‘ 𝑥 ) ) = 𝑥 ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑦 = ( 𝐹 ‘ 𝑧 ) ) ) → 𝑦 = ( 𝐹 ‘ 𝑧 ) )
2 simpll ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ ( 𝐹 ‘ 𝑥 ) ) = 𝑥 ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑦 = ( 𝐹 ‘ 𝑧 ) ) ) → 𝐹 : 𝐴 ⟶ 𝐴 )
3 simprl ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ ( 𝐹 ‘ 𝑥 ) ) = 𝑥 ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑦 = ( 𝐹 ‘ 𝑧 ) ) ) → 𝑧 ∈ 𝐴 )
4 2 3 ffvelcdmd ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ ( 𝐹 ‘ 𝑥 ) ) = 𝑥 ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑦 = ( 𝐹 ‘ 𝑧 ) ) ) → ( 𝐹 ‘ 𝑧 ) ∈ 𝐴 )
5 1 4 eqeltrd ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ ( 𝐹 ‘ 𝑥 ) ) = 𝑥 ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑦 = ( 𝐹 ‘ 𝑧 ) ) ) → 𝑦 ∈ 𝐴 )
6 1 fveq2d ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ ( 𝐹 ‘ 𝑥 ) ) = 𝑥 ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑦 = ( 𝐹 ‘ 𝑧 ) ) ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝐹 ‘ 𝑧 ) ) )
7 2fveq3 ⊢ ( 𝑥 = 𝑧 → ( 𝐹 ‘ ( 𝐹 ‘ 𝑥 ) ) = ( 𝐹 ‘ ( 𝐹 ‘ 𝑧 ) ) )
8 id ⊢ ( 𝑥 = 𝑧 → 𝑥 = 𝑧 )
9 7 8 eqeq12d ⊢ ( 𝑥 = 𝑧 → ( ( 𝐹 ‘ ( 𝐹 ‘ 𝑥 ) ) = 𝑥 ↔ ( 𝐹 ‘ ( 𝐹 ‘ 𝑧 ) ) = 𝑧 ) )
10 simplr ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ ( 𝐹 ‘ 𝑥 ) ) = 𝑥 ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑦 = ( 𝐹 ‘ 𝑧 ) ) ) → ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ ( 𝐹 ‘ 𝑥 ) ) = 𝑥 )
11 9 10 3 rspcdva ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ ( 𝐹 ‘ 𝑥 ) ) = 𝑥 ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑦 = ( 𝐹 ‘ 𝑧 ) ) ) → ( 𝐹 ‘ ( 𝐹 ‘ 𝑧 ) ) = 𝑧 )
12 6 11 eqtr2d ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ ( 𝐹 ‘ 𝑥 ) ) = 𝑥 ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑦 = ( 𝐹 ‘ 𝑧 ) ) ) → 𝑧 = ( 𝐹 ‘ 𝑦 ) )
13 5 12 jca ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ ( 𝐹 ‘ 𝑥 ) ) = 𝑥 ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑦 = ( 𝐹 ‘ 𝑧 ) ) ) → ( 𝑦 ∈ 𝐴 ∧ 𝑧 = ( 𝐹 ‘ 𝑦 ) ) )
14 simprr ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ ( 𝐹 ‘ 𝑥 ) ) = 𝑥 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 = ( 𝐹 ‘ 𝑦 ) ) ) → 𝑧 = ( 𝐹 ‘ 𝑦 ) )
15 simpll ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ ( 𝐹 ‘ 𝑥 ) ) = 𝑥 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 = ( 𝐹 ‘ 𝑦 ) ) ) → 𝐹 : 𝐴 ⟶ 𝐴 )
16 simprl ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ ( 𝐹 ‘ 𝑥 ) ) = 𝑥 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 = ( 𝐹 ‘ 𝑦 ) ) ) → 𝑦 ∈ 𝐴 )
17 15 16 ffvelcdmd ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ ( 𝐹 ‘ 𝑥 ) ) = 𝑥 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 = ( 𝐹 ‘ 𝑦 ) ) ) → ( 𝐹 ‘ 𝑦 ) ∈ 𝐴 )
18 14 17 eqeltrd ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ ( 𝐹 ‘ 𝑥 ) ) = 𝑥 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 = ( 𝐹 ‘ 𝑦 ) ) ) → 𝑧 ∈ 𝐴 )
19 14 fveq2d ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ ( 𝐹 ‘ 𝑥 ) ) = 𝑥 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 = ( 𝐹 ‘ 𝑦 ) ) ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ ( 𝐹 ‘ 𝑦 ) ) )
20 2fveq3 ⊢ ( 𝑥 = 𝑦 → ( 𝐹 ‘ ( 𝐹 ‘ 𝑥 ) ) = ( 𝐹 ‘ ( 𝐹 ‘ 𝑦 ) ) )
21 id ⊢ ( 𝑥 = 𝑦 → 𝑥 = 𝑦 )
22 20 21 eqeq12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐹 ‘ ( 𝐹 ‘ 𝑥 ) ) = 𝑥 ↔ ( 𝐹 ‘ ( 𝐹 ‘ 𝑦 ) ) = 𝑦 ) )
23 simplr ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ ( 𝐹 ‘ 𝑥 ) ) = 𝑥 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 = ( 𝐹 ‘ 𝑦 ) ) ) → ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ ( 𝐹 ‘ 𝑥 ) ) = 𝑥 )
24 22 23 16 rspcdva ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ ( 𝐹 ‘ 𝑥 ) ) = 𝑥 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 = ( 𝐹 ‘ 𝑦 ) ) ) → ( 𝐹 ‘ ( 𝐹 ‘ 𝑦 ) ) = 𝑦 )
25 19 24 eqtr2d ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ ( 𝐹 ‘ 𝑥 ) ) = 𝑥 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 = ( 𝐹 ‘ 𝑦 ) ) ) → 𝑦 = ( 𝐹 ‘ 𝑧 ) )
26 18 25 jca ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ ( 𝐹 ‘ 𝑥 ) ) = 𝑥 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 = ( 𝐹 ‘ 𝑦 ) ) ) → ( 𝑧 ∈ 𝐴 ∧ 𝑦 = ( 𝐹 ‘ 𝑧 ) ) )
27 13 26 impbida ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ ( 𝐹 ‘ 𝑥 ) ) = 𝑥 ) → ( ( 𝑧 ∈ 𝐴 ∧ 𝑦 = ( 𝐹 ‘ 𝑧 ) ) ↔ ( 𝑦 ∈ 𝐴 ∧ 𝑧 = ( 𝐹 ‘ 𝑦 ) ) ) )
28 27 mptcnv ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ ( 𝐹 ‘ 𝑥 ) ) = 𝑥 ) → ◡ ( 𝑧 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑧 ) ) = ( 𝑦 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑦 ) ) )
29 ffn ⊢ ( 𝐹 : 𝐴 ⟶ 𝐴 → 𝐹 Fn 𝐴 )
30 dffn5 ⊢ ( 𝐹 Fn 𝐴 ↔ 𝐹 = ( 𝑧 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑧 ) ) )
31 30 birani ⊢ ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ ( 𝐹 ‘ 𝑥 ) ) = 𝑥 ) → 𝐹 = ( 𝑧 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑧 ) ) )
32 29 31 sylan ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ ( 𝐹 ‘ 𝑥 ) ) = 𝑥 ) → 𝐹 = ( 𝑧 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑧 ) ) )
33 32 cnveqd ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ ( 𝐹 ‘ 𝑥 ) ) = 𝑥 ) → ◡ 𝐹 = ◡ ( 𝑧 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑧 ) ) )
34 dffn5 ⊢ ( 𝐹 Fn 𝐴 ↔ 𝐹 = ( 𝑦 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑦 ) ) )
35 34 birani ⊢ ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ ( 𝐹 ‘ 𝑥 ) ) = 𝑥 ) → 𝐹 = ( 𝑦 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑦 ) ) )
36 29 35 sylan ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ ( 𝐹 ‘ 𝑥 ) ) = 𝑥 ) → 𝐹 = ( 𝑦 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑦 ) ) )
37 28 33 36 3eqtr4d ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ ( 𝐹 ‘ 𝑥 ) ) = 𝑥 ) → ◡ 𝐹 = 𝐹 )