Metamath Proof Explorer

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 ⁡ F ∧ G : A ⟶ 1-1 onto B ∧ X ∈ B → F ∘ G ⁡ G -1 ⁡ X = F ⁡ X

Proof

Step Hyp Ref Expression
1 f1of ⊢ G : A ⟶ 1-1 onto B → G : A ⟶ B
2 1 3ad2ant2 ⊢ Fun ⁡ F ∧ G : A ⟶ 1-1 onto B ∧ X ∈ B → G : A ⟶ B
3 f1ocnv ⊢ G : A ⟶ 1-1 onto B → G -1 : B ⟶ 1-1 onto A
4 f1of ⊢ G -1 : B ⟶ 1-1 onto A → G -1 : B ⟶ A
5 3 4 syl ⊢ G : A ⟶ 1-1 onto B → G -1 : B ⟶ A
6 5 3ad2ant2 ⊢ Fun ⁡ F ∧ G : A ⟶ 1-1 onto B ∧ X ∈ B → G -1 : B ⟶ A
7 simp3 ⊢ Fun ⁡ F ∧ G : A ⟶ 1-1 onto B ∧ X ∈ B → X ∈ B
8 6 7 ffvelrnd ⊢ Fun ⁡ F ∧ G : A ⟶ 1-1 onto B ∧ X ∈ B → G -1 ⁡ X ∈ A
9 fvco3 ⊢ G : A ⟶ B ∧ G -1 ⁡ X ∈ A → F ∘ G ⁡ G -1 ⁡ X = F ⁡ G ⁡ G -1 ⁡ X
10 2 8 9 syl2anc ⊢ Fun ⁡ F ∧ G : A ⟶ 1-1 onto B ∧ X ∈ B → F ∘ G ⁡ G -1 ⁡ X = F ⁡ G ⁡ G -1 ⁡ X
11 f1ocnvfv2 ⊢ G : A ⟶ 1-1 onto B ∧ X ∈ B → G ⁡ G -1 ⁡ X = X
12 11 3adant1 ⊢ Fun ⁡ F ∧ G : A ⟶ 1-1 onto B ∧ X ∈ B → G ⁡ G -1 ⁡ X = X
13 12 fveq2d ⊢ Fun ⁡ F ∧ G : A ⟶ 1-1 onto B ∧ X ∈ B → F ⁡ G ⁡ G -1 ⁡ X = F ⁡ X
14 10 13 eqtrd ⊢ Fun ⁡ F ∧ G : A ⟶ 1-1 onto B ∧ X ∈ B → F ∘ G ⁡ G -1 ⁡ X = F ⁡ X