Metamath Proof Explorer

Theorem f1cofveqaeq

Description: If the values of a composition of one-to-one functions for two arguments are equal, the arguments themselves must be equal. (Contributed by AV, 3-Feb-2021)

Ref Expression
Assertion f1cofveqaeq ⊢ F : B ⟶ 1-1 C ∧ G : A ⟶ 1-1 B ∧ X ∈ A ∧ Y ∈ A → F ⁡ G ⁡ X = F ⁡ G ⁡ Y → X = Y

Proof

Step Hyp Ref Expression
1 simpl ⊢ F : B ⟶ 1-1 C ∧ G : A ⟶ 1-1 B → F : B ⟶ 1-1 C
2 f1f ⊢ G : A ⟶ 1-1 B → G : A ⟶ B
3 ffvelrn ⊢ G : A ⟶ B ∧ X ∈ A → G ⁡ X ∈ B
4 3 ex ⊢ G : A ⟶ B → X ∈ A → G ⁡ X ∈ B
5 ffvelrn ⊢ G : A ⟶ B ∧ Y ∈ A → G ⁡ Y ∈ B
6 5 ex ⊢ G : A ⟶ B → Y ∈ A → G ⁡ Y ∈ B
7 4 6 anim12d ⊢ G : A ⟶ B → X ∈ A ∧ Y ∈ A → G ⁡ X ∈ B ∧ G ⁡ Y ∈ B
8 2 7 syl ⊢ G : A ⟶ 1-1 B → X ∈ A ∧ Y ∈ A → G ⁡ X ∈ B ∧ G ⁡ Y ∈ B
9 8 adantl ⊢ F : B ⟶ 1-1 C ∧ G : A ⟶ 1-1 B → X ∈ A ∧ Y ∈ A → G ⁡ X ∈ B ∧ G ⁡ Y ∈ B
10 9 imp ⊢ F : B ⟶ 1-1 C ∧ G : A ⟶ 1-1 B ∧ X ∈ A ∧ Y ∈ A → G ⁡ X ∈ B ∧ G ⁡ Y ∈ B
11 f1veqaeq ⊢ F : B ⟶ 1-1 C ∧ G ⁡ X ∈ B ∧ G ⁡ Y ∈ B → F ⁡ G ⁡ X = F ⁡ G ⁡ Y → G ⁡ X = G ⁡ Y
12 1 10 11 syl2an2r ⊢ F : B ⟶ 1-1 C ∧ G : A ⟶ 1-1 B ∧ X ∈ A ∧ Y ∈ A → F ⁡ G ⁡ X = F ⁡ G ⁡ Y → G ⁡ X = G ⁡ Y
13 f1veqaeq ⊢ G : A ⟶ 1-1 B ∧ X ∈ A ∧ Y ∈ A → G ⁡ X = G ⁡ Y → X = Y
14 13 adantll ⊢ F : B ⟶ 1-1 C ∧ G : A ⟶ 1-1 B ∧ X ∈ A ∧ Y ∈ A → G ⁡ X = G ⁡ Y → X = Y
15 12 14 syld ⊢ F : B ⟶ 1-1 C ∧ G : A ⟶ 1-1 B ∧ X ∈ A ∧ Y ∈ A → F ⁡ G ⁡ X = F ⁡ G ⁡ Y → X = Y