Theorem f1cofveqaeqALT

Description: Alternate proof of f1cofveqaeq , 1 essential step shorter, but having more bytes (305 versus 282). (Contributed by AV, 3-Feb-2021) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Assertion	f1cofveqaeqALT	⊢ ( ( ( 𝐹 : 𝐵 –1-1→ 𝐶 ∧ 𝐺 : 𝐴 –1-1→ 𝐵 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ) → ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑌 ) ) → 𝑋 = 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		f1f	⊢ ( 𝐺 : 𝐴 –1-1→ 𝐵 → 𝐺 : 𝐴 ⟶ 𝐵 )
2		fvco3	⊢ ( ( 𝐺 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ 𝐴 ) → ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑋 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) )
3	2	adantrr	⊢ ( ( 𝐺 : 𝐴 ⟶ 𝐵 ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ) → ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑋 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) )
4		fvco3	⊢ ( ( 𝐺 : 𝐴 ⟶ 𝐵 ∧ 𝑌 ∈ 𝐴 ) → ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑌 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑌 ) ) )
5	4	adantrl	⊢ ( ( 𝐺 : 𝐴 ⟶ 𝐵 ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ) → ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑌 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑌 ) ) )
6	3 5	eqeq12d	⊢ ( ( 𝐺 : 𝐴 ⟶ 𝐵 ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ) → ( ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑋 ) = ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑌 ) ↔ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑌 ) ) ) )
7	6	ex	⊢ ( 𝐺 : 𝐴 ⟶ 𝐵 → ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑋 ) = ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑌 ) ↔ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑌 ) ) ) ) )
8	1 7	syl	⊢ ( 𝐺 : 𝐴 –1-1→ 𝐵 → ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑋 ) = ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑌 ) ↔ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑌 ) ) ) ) )
9	8	adantl	⊢ ( ( 𝐹 : 𝐵 –1-1→ 𝐶 ∧ 𝐺 : 𝐴 –1-1→ 𝐵 ) → ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑋 ) = ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑌 ) ↔ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑌 ) ) ) ) )
10	9	imp	⊢ ( ( ( 𝐹 : 𝐵 –1-1→ 𝐶 ∧ 𝐺 : 𝐴 –1-1→ 𝐵 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ) → ( ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑋 ) = ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑌 ) ↔ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑌 ) ) ) )
11		f1co	⊢ ( ( 𝐹 : 𝐵 –1-1→ 𝐶 ∧ 𝐺 : 𝐴 –1-1→ 𝐵 ) → ( 𝐹 ∘ 𝐺 ) : 𝐴 –1-1→ 𝐶 )
12		f1veqaeq	⊢ ( ( ( 𝐹 ∘ 𝐺 ) : 𝐴 –1-1→ 𝐶 ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ) → ( ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑋 ) = ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑌 ) → 𝑋 = 𝑌 ) )
13	11 12	sylan	⊢ ( ( ( 𝐹 : 𝐵 –1-1→ 𝐶 ∧ 𝐺 : 𝐴 –1-1→ 𝐵 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ) → ( ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑋 ) = ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑌 ) → 𝑋 = 𝑌 ) )
14	10 13	sylbird	⊢ ( ( ( 𝐹 : 𝐵 –1-1→ 𝐶 ∧ 𝐺 : 𝐴 –1-1→ 𝐵 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ) → ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑌 ) ) → 𝑋 = 𝑌 ) )