Theorem f1ocan2fv

Description: Cancel a composition by the converse of a bijection by preapplying the bijection. (Contributed by Jeff Madsen, 2-Sep-2009)

	Ref	Expression
Assertion	f1ocan2fv	⊢ ( ( Fun 𝐹 ∧ 𝐺 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑋 ∈ 𝐴 ) → ( ( 𝐹 ∘ ◡ 𝐺 ) ‘ ( 𝐺 ‘ 𝑋 ) ) = ( 𝐹 ‘ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		f1orel	⊢ ( 𝐺 : 𝐴 –1-1-onto→ 𝐵 → Rel 𝐺 )
2		dfrel2	⊢ ( Rel 𝐺 ↔ ◡ ◡ 𝐺 = 𝐺 )
3	1 2	sylib	⊢ ( 𝐺 : 𝐴 –1-1-onto→ 𝐵 → ◡ ◡ 𝐺 = 𝐺 )
4	3	3ad2ant2	⊢ ( ( Fun 𝐹 ∧ 𝐺 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑋 ∈ 𝐴 ) → ◡ ◡ 𝐺 = 𝐺 )
5	4	fveq1d	⊢ ( ( Fun 𝐹 ∧ 𝐺 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑋 ∈ 𝐴 ) → ( ◡ ◡ 𝐺 ‘ 𝑋 ) = ( 𝐺 ‘ 𝑋 ) )
6	5	fveq2d	⊢ ( ( Fun 𝐹 ∧ 𝐺 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑋 ∈ 𝐴 ) → ( ( 𝐹 ∘ ◡ 𝐺 ) ‘ ( ◡ ◡ 𝐺 ‘ 𝑋 ) ) = ( ( 𝐹 ∘ ◡ 𝐺 ) ‘ ( 𝐺 ‘ 𝑋 ) ) )
7		f1ocnv	⊢ ( 𝐺 : 𝐴 –1-1-onto→ 𝐵 → ◡ 𝐺 : 𝐵 –1-1-onto→ 𝐴 )
8		f1ocan1fv	⊢ ( ( Fun 𝐹 ∧ ◡ 𝐺 : 𝐵 –1-1-onto→ 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( ( 𝐹 ∘ ◡ 𝐺 ) ‘ ( ◡ ◡ 𝐺 ‘ 𝑋 ) ) = ( 𝐹 ‘ 𝑋 ) )
9	7 8	syl3an2	⊢ ( ( Fun 𝐹 ∧ 𝐺 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑋 ∈ 𝐴 ) → ( ( 𝐹 ∘ ◡ 𝐺 ) ‘ ( ◡ ◡ 𝐺 ‘ 𝑋 ) ) = ( 𝐹 ‘ 𝑋 ) )
10	6 9	eqtr3d	⊢ ( ( Fun 𝐹 ∧ 𝐺 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑋 ∈ 𝐴 ) → ( ( 𝐹 ∘ ◡ 𝐺 ) ‘ ( 𝐺 ‘ 𝑋 ) ) = ( 𝐹 ‘ 𝑋 ) )