Theorem nvocnvb

Description: Equivalence to saying the converse of an involution is the function itself. (Contributed by RP, 13-Oct-2024)

	Ref	Expression
Assertion	nvocnvb	⊢ ( ( 𝐹 Fn 𝐴 ∧ ◡ 𝐹 = 𝐹 ) ↔ ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ ( 𝐹 ‘ 𝑥 ) ) = 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		nvof1o	⊢ ( ( 𝐹 Fn 𝐴 ∧ ◡ 𝐹 = 𝐹 ) → 𝐹 : 𝐴 –1-1-onto→ 𝐴 )
2		fveq1	⊢ ( ◡ 𝐹 = 𝐹 → ( ◡ 𝐹 ‘ ( 𝐹 ‘ 𝑥 ) ) = ( 𝐹 ‘ ( 𝐹 ‘ 𝑥 ) ) )
3	2	ad2antlr	⊢ ( ( ( 𝐹 Fn 𝐴 ∧ ◡ 𝐹 = 𝐹 ) ∧ 𝑥 ∈ 𝐴 ) → ( ◡ 𝐹 ‘ ( 𝐹 ‘ 𝑥 ) ) = ( 𝐹 ‘ ( 𝐹 ‘ 𝑥 ) ) )
4		f1ocnvfv1	⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( ◡ 𝐹 ‘ ( 𝐹 ‘ 𝑥 ) ) = 𝑥 )
5	1 4	sylan	⊢ ( ( ( 𝐹 Fn 𝐴 ∧ ◡ 𝐹 = 𝐹 ) ∧ 𝑥 ∈ 𝐴 ) → ( ◡ 𝐹 ‘ ( 𝐹 ‘ 𝑥 ) ) = 𝑥 )
6	3 5	eqtr3d	⊢ ( ( ( 𝐹 Fn 𝐴 ∧ ◡ 𝐹 = 𝐹 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ ( 𝐹 ‘ 𝑥 ) ) = 𝑥 )
7	6	ralrimiva	⊢ ( ( 𝐹 Fn 𝐴 ∧ ◡ 𝐹 = 𝐹 ) → ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ ( 𝐹 ‘ 𝑥 ) ) = 𝑥 )
8	1 7	jca	⊢ ( ( 𝐹 Fn 𝐴 ∧ ◡ 𝐹 = 𝐹 ) → ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ ( 𝐹 ‘ 𝑥 ) ) = 𝑥 ) )
9		f1of	⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 → 𝐹 : 𝐴 ⟶ 𝐴 )
10		ffn	⊢ ( 𝐹 : 𝐴 ⟶ 𝐴 → 𝐹 Fn 𝐴 )
11	10	adantr	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ ( 𝐹 ‘ 𝑥 ) ) = 𝑥 ) → 𝐹 Fn 𝐴 )
12		nvocnv	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ ( 𝐹 ‘ 𝑥 ) ) = 𝑥 ) → ◡ 𝐹 = 𝐹 )
13	11 12	jca	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ ( 𝐹 ‘ 𝑥 ) ) = 𝑥 ) → ( 𝐹 Fn 𝐴 ∧ ◡ 𝐹 = 𝐹 ) )
14	9 13	sylan	⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ ( 𝐹 ‘ 𝑥 ) ) = 𝑥 ) → ( 𝐹 Fn 𝐴 ∧ ◡ 𝐹 = 𝐹 ) )
15	8 14	impbii	⊢ ( ( 𝐹 Fn 𝐴 ∧ ◡ 𝐹 = 𝐹 ) ↔ ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ ( 𝐹 ‘ 𝑥 ) ) = 𝑥 ) )