Theorem f1ocan1fv

Description: Cancel a composition by a bijection by preapplying the converse. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 27-Dec-2014)

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

Proof

Step	Hyp	Ref	Expression
1		f1of	⊢ ( 𝐺 : 𝐴 –1-1-onto→ 𝐵 → 𝐺 : 𝐴 ⟶ 𝐵 )
2	1	3ad2ant2	⊢ ( ( Fun 𝐹 ∧ 𝐺 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → 𝐺 : 𝐴 ⟶ 𝐵 )
3		f1ocnv	⊢ ( 𝐺 : 𝐴 –1-1-onto→ 𝐵 → ◡ 𝐺 : 𝐵 –1-1-onto→ 𝐴 )
4		f1of	⊢ ( ◡ 𝐺 : 𝐵 –1-1-onto→ 𝐴 → ◡ 𝐺 : 𝐵 ⟶ 𝐴 )
5	3 4	syl	⊢ ( 𝐺 : 𝐴 –1-1-onto→ 𝐵 → ◡ 𝐺 : 𝐵 ⟶ 𝐴 )
6	5	3ad2ant2	⊢ ( ( Fun 𝐹 ∧ 𝐺 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ◡ 𝐺 : 𝐵 ⟶ 𝐴 )
7		simp3	⊢ ( ( Fun 𝐹 ∧ 𝐺 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
8	6 7	ffvelcdmd	⊢ ( ( Fun 𝐹 ∧ 𝐺 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( ◡ 𝐺 ‘ 𝑋 ) ∈ 𝐴 )
9		fvco3	⊢ ( ( 𝐺 : 𝐴 ⟶ 𝐵 ∧ ( ◡ 𝐺 ‘ 𝑋 ) ∈ 𝐴 ) → ( ( 𝐹 ∘ 𝐺 ) ‘ ( ◡ 𝐺 ‘ 𝑋 ) ) = ( 𝐹 ‘ ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝑋 ) ) ) )
10	2 8 9	syl2anc	⊢ ( ( Fun 𝐹 ∧ 𝐺 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝐹 ∘ 𝐺 ) ‘ ( ◡ 𝐺 ‘ 𝑋 ) ) = ( 𝐹 ‘ ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝑋 ) ) ) )
11		f1ocnvfv2	⊢ ( ( 𝐺 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝑋 ) ) = 𝑋 )
12	11	3adant1	⊢ ( ( Fun 𝐹 ∧ 𝐺 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝑋 ) ) = 𝑋 )
13	12	fveq2d	⊢ ( ( Fun 𝐹 ∧ 𝐺 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝑋 ) ) ) = ( 𝐹 ‘ 𝑋 ) )
14	10 13	eqtrd	⊢ ( ( Fun 𝐹 ∧ 𝐺 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝐹 ∘ 𝐺 ) ‘ ( ◡ 𝐺 ‘ 𝑋 ) ) = ( 𝐹 ‘ 𝑋 ) )