Theorem f1ocnvfv1

Description: The converse value of the value of a one-to-one onto function. (Contributed by NM, 20-May-2004)

	Ref	Expression
Assertion	f1ocnvfv1	⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐶 ∈ 𝐴 ) → ( ◡ 𝐹 ‘ ( 𝐹 ‘ 𝐶 ) ) = 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		f1ococnv1	⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → ( ◡ 𝐹 ∘ 𝐹 ) = ( I ↾ 𝐴 ) )
2	1	fveq1d	⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → ( ( ◡ 𝐹 ∘ 𝐹 ) ‘ 𝐶 ) = ( ( I ↾ 𝐴 ) ‘ 𝐶 ) )
3	2	adantr	⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐶 ∈ 𝐴 ) → ( ( ◡ 𝐹 ∘ 𝐹 ) ‘ 𝐶 ) = ( ( I ↾ 𝐴 ) ‘ 𝐶 ) )
4		f1of	⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → 𝐹 : 𝐴 ⟶ 𝐵 )
5		fvco3	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐶 ∈ 𝐴 ) → ( ( ◡ 𝐹 ∘ 𝐹 ) ‘ 𝐶 ) = ( ◡ 𝐹 ‘ ( 𝐹 ‘ 𝐶 ) ) )
6	4 5	sylan	⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐶 ∈ 𝐴 ) → ( ( ◡ 𝐹 ∘ 𝐹 ) ‘ 𝐶 ) = ( ◡ 𝐹 ‘ ( 𝐹 ‘ 𝐶 ) ) )
7		fvresi	⊢ ( 𝐶 ∈ 𝐴 → ( ( I ↾ 𝐴 ) ‘ 𝐶 ) = 𝐶 )
8	7	adantl	⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐶 ∈ 𝐴 ) → ( ( I ↾ 𝐴 ) ‘ 𝐶 ) = 𝐶 )
9	3 6 8	3eqtr3d	⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐶 ∈ 𝐴 ) → ( ◡ 𝐹 ‘ ( 𝐹 ‘ 𝐶 ) ) = 𝐶 )