Metamath Proof Explorer

Theorem f1ocnvfv2

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

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

Proof

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