Metamath Proof Explorer

Theorem 2f1fvneq

Description: If two one-to-one functions are applied on different arguments, also the values are different. (Contributed by Alexander van der Vekens, 25-Jan-2018)

Ref Expression
Assertion 2f1fvneq ( ( ( 𝐸 : 𝐷 –1-1→ 𝑅 ∧ 𝐹 : 𝐶 –1-1→ 𝐷 ) ∧ ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ∧ 𝐴 ≠ 𝐵 ) → ( ( ( 𝐸 ‘ ( 𝐹 ‘ 𝐴 ) ) = 𝑋 ∧ ( 𝐸 ‘ ( 𝐹 ‘ 𝐵 ) ) = 𝑌 ) → 𝑋 ≠ 𝑌 ) )

Proof

Step Hyp Ref Expression
1 f1veqaeq ⊢ ( ( 𝐹 : 𝐶 –1-1→ 𝐷 ∧ ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ) → ( ( 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ 𝐵 ) → 𝐴 = 𝐵 ) )
2 1 adantll ⊢ ( ( ( 𝐸 : 𝐷 –1-1→ 𝑅 ∧ 𝐹 : 𝐶 –1-1→ 𝐷 ) ∧ ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ) → ( ( 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ 𝐵 ) → 𝐴 = 𝐵 ) )
3 2 necon3ad ⊢ ( ( ( 𝐸 : 𝐷 –1-1→ 𝑅 ∧ 𝐹 : 𝐶 –1-1→ 𝐷 ) ∧ ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ) → ( 𝐴 ≠ 𝐵 → ¬ ( 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ 𝐵 ) ) )
4 3 3impia ⊢ ( ( ( 𝐸 : 𝐷 –1-1→ 𝑅 ∧ 𝐹 : 𝐶 –1-1→ 𝐷 ) ∧ ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ∧ 𝐴 ≠ 𝐵 ) → ¬ ( 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ 𝐵 ) )
5 simpll ⊢ ( ( ( 𝐸 : 𝐷 –1-1→ 𝑅 ∧ 𝐹 : 𝐶 –1-1→ 𝐷 ) ∧ ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ) → 𝐸 : 𝐷 –1-1→ 𝑅 )
6 f1f ⊢ ( 𝐹 : 𝐶 –1-1→ 𝐷 → 𝐹 : 𝐶 ⟶ 𝐷 )
7 ffvelcdm ⊢ ( ( 𝐹 : 𝐶 ⟶ 𝐷 ∧ 𝐴 ∈ 𝐶 ) → ( 𝐹 ‘ 𝐴 ) ∈ 𝐷 )
8 ffvelcdm ⊢ ( ( 𝐹 : 𝐶 ⟶ 𝐷 ∧ 𝐵 ∈ 𝐶 ) → ( 𝐹 ‘ 𝐵 ) ∈ 𝐷 )
9 7 8 anim12dan ⊢ ( ( 𝐹 : 𝐶 ⟶ 𝐷 ∧ ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ) → ( ( 𝐹 ‘ 𝐴 ) ∈ 𝐷 ∧ ( 𝐹 ‘ 𝐵 ) ∈ 𝐷 ) )
10 9 ex ⊢ ( 𝐹 : 𝐶 ⟶ 𝐷 → ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) → ( ( 𝐹 ‘ 𝐴 ) ∈ 𝐷 ∧ ( 𝐹 ‘ 𝐵 ) ∈ 𝐷 ) ) )
11 6 10 syl ⊢ ( 𝐹 : 𝐶 –1-1→ 𝐷 → ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) → ( ( 𝐹 ‘ 𝐴 ) ∈ 𝐷 ∧ ( 𝐹 ‘ 𝐵 ) ∈ 𝐷 ) ) )
12 11 adantl ⊢ ( ( 𝐸 : 𝐷 –1-1→ 𝑅 ∧ 𝐹 : 𝐶 –1-1→ 𝐷 ) → ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) → ( ( 𝐹 ‘ 𝐴 ) ∈ 𝐷 ∧ ( 𝐹 ‘ 𝐵 ) ∈ 𝐷 ) ) )
13 12 imp ⊢ ( ( ( 𝐸 : 𝐷 –1-1→ 𝑅 ∧ 𝐹 : 𝐶 –1-1→ 𝐷 ) ∧ ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ) → ( ( 𝐹 ‘ 𝐴 ) ∈ 𝐷 ∧ ( 𝐹 ‘ 𝐵 ) ∈ 𝐷 ) )
14 f1veqaeq ⊢ ( ( 𝐸 : 𝐷 –1-1→ 𝑅 ∧ ( ( 𝐹 ‘ 𝐴 ) ∈ 𝐷 ∧ ( 𝐹 ‘ 𝐵 ) ∈ 𝐷 ) ) → ( ( 𝐸 ‘ ( 𝐹 ‘ 𝐴 ) ) = ( 𝐸 ‘ ( 𝐹 ‘ 𝐵 ) ) → ( 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ 𝐵 ) ) )
15 5 13 14 syl2anc ⊢ ( ( ( 𝐸 : 𝐷 –1-1→ 𝑅 ∧ 𝐹 : 𝐶 –1-1→ 𝐷 ) ∧ ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ) → ( ( 𝐸 ‘ ( 𝐹 ‘ 𝐴 ) ) = ( 𝐸 ‘ ( 𝐹 ‘ 𝐵 ) ) → ( 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ 𝐵 ) ) )
16 15 con3dimp ⊢ ( ( ( ( 𝐸 : 𝐷 –1-1→ 𝑅 ∧ 𝐹 : 𝐶 –1-1→ 𝐷 ) ∧ ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ) ∧ ¬ ( 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ 𝐵 ) ) → ¬ ( 𝐸 ‘ ( 𝐹 ‘ 𝐴 ) ) = ( 𝐸 ‘ ( 𝐹 ‘ 𝐵 ) ) )
17 eqeq12 ⊢ ( ( ( 𝐸 ‘ ( 𝐹 ‘ 𝐴 ) ) = 𝑋 ∧ ( 𝐸 ‘ ( 𝐹 ‘ 𝐵 ) ) = 𝑌 ) → ( ( 𝐸 ‘ ( 𝐹 ‘ 𝐴 ) ) = ( 𝐸 ‘ ( 𝐹 ‘ 𝐵 ) ) ↔ 𝑋 = 𝑌 ) )
18 17 notbid ⊢ ( ( ( 𝐸 ‘ ( 𝐹 ‘ 𝐴 ) ) = 𝑋 ∧ ( 𝐸 ‘ ( 𝐹 ‘ 𝐵 ) ) = 𝑌 ) → ( ¬ ( 𝐸 ‘ ( 𝐹 ‘ 𝐴 ) ) = ( 𝐸 ‘ ( 𝐹 ‘ 𝐵 ) ) ↔ ¬ 𝑋 = 𝑌 ) )
19 neqne ⊢ ( ¬ 𝑋 = 𝑌 → 𝑋 ≠ 𝑌 )
20 18 19 biimtrdi ⊢ ( ( ( 𝐸 ‘ ( 𝐹 ‘ 𝐴 ) ) = 𝑋 ∧ ( 𝐸 ‘ ( 𝐹 ‘ 𝐵 ) ) = 𝑌 ) → ( ¬ ( 𝐸 ‘ ( 𝐹 ‘ 𝐴 ) ) = ( 𝐸 ‘ ( 𝐹 ‘ 𝐵 ) ) → 𝑋 ≠ 𝑌 ) )
21 16 20 syl5com ⊢ ( ( ( ( 𝐸 : 𝐷 –1-1→ 𝑅 ∧ 𝐹 : 𝐶 –1-1→ 𝐷 ) ∧ ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ) ∧ ¬ ( 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ 𝐵 ) ) → ( ( ( 𝐸 ‘ ( 𝐹 ‘ 𝐴 ) ) = 𝑋 ∧ ( 𝐸 ‘ ( 𝐹 ‘ 𝐵 ) ) = 𝑌 ) → 𝑋 ≠ 𝑌 ) )
22 21 ex ⊢ ( ( ( 𝐸 : 𝐷 –1-1→ 𝑅 ∧ 𝐹 : 𝐶 –1-1→ 𝐷 ) ∧ ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ) → ( ¬ ( 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ 𝐵 ) → ( ( ( 𝐸 ‘ ( 𝐹 ‘ 𝐴 ) ) = 𝑋 ∧ ( 𝐸 ‘ ( 𝐹 ‘ 𝐵 ) ) = 𝑌 ) → 𝑋 ≠ 𝑌 ) ) )
23 22 3adant3 ⊢ ( ( ( 𝐸 : 𝐷 –1-1→ 𝑅 ∧ 𝐹 : 𝐶 –1-1→ 𝐷 ) ∧ ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ∧ 𝐴 ≠ 𝐵 ) → ( ¬ ( 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ 𝐵 ) → ( ( ( 𝐸 ‘ ( 𝐹 ‘ 𝐴 ) ) = 𝑋 ∧ ( 𝐸 ‘ ( 𝐹 ‘ 𝐵 ) ) = 𝑌 ) → 𝑋 ≠ 𝑌 ) ) )
24 4 23 mpd ⊢ ( ( ( 𝐸 : 𝐷 –1-1→ 𝑅 ∧ 𝐹 : 𝐶 –1-1→ 𝐷 ) ∧ ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ∧ 𝐴 ≠ 𝐵 ) → ( ( ( 𝐸 ‘ ( 𝐹 ‘ 𝐴 ) ) = 𝑋 ∧ ( 𝐸 ‘ ( 𝐹 ‘ 𝐵 ) ) = 𝑌 ) → 𝑋 ≠ 𝑌 ) )