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) (Proof shortened by AV, 30-Oct-2025)

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

Proof

Step Hyp Ref Expression
1 simp1l ⊢ ( ( ( 𝐸 : 𝐷 –1-1→ 𝑅 ∧ 𝐹 : 𝐶 –1-1→ 𝐷 ) ∧ ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ∧ 𝐴 ≠ 𝐵 ) → 𝐸 : 𝐷 –1-1→ 𝑅 )
2 f1f ⊢ ( 𝐹 : 𝐶 –1-1→ 𝐷 → 𝐹 : 𝐶 ⟶ 𝐷 )
3 2 adantl ⊢ ( ( 𝐸 : 𝐷 –1-1→ 𝑅 ∧ 𝐹 : 𝐶 –1-1→ 𝐷 ) → 𝐹 : 𝐶 ⟶ 𝐷 )
4 3 adantr ⊢ ( ( ( 𝐸 : 𝐷 –1-1→ 𝑅 ∧ 𝐹 : 𝐶 –1-1→ 𝐷 ) ∧ ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ) → 𝐹 : 𝐶 ⟶ 𝐷 )
5 simpl ⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) → 𝐴 ∈ 𝐶 )
6 5 adantl ⊢ ( ( ( 𝐸 : 𝐷 –1-1→ 𝑅 ∧ 𝐹 : 𝐶 –1-1→ 𝐷 ) ∧ ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ) → 𝐴 ∈ 𝐶 )
7 4 6 ffvelcdmd ⊢ ( ( ( 𝐸 : 𝐷 –1-1→ 𝑅 ∧ 𝐹 : 𝐶 –1-1→ 𝐷 ) ∧ ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ) → ( 𝐹 ‘ 𝐴 ) ∈ 𝐷 )
8 7 3adant3 ⊢ ( ( ( 𝐸 : 𝐷 –1-1→ 𝑅 ∧ 𝐹 : 𝐶 –1-1→ 𝐷 ) ∧ ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ∧ 𝐴 ≠ 𝐵 ) → ( 𝐹 ‘ 𝐴 ) ∈ 𝐷 )
9 simpr ⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) → 𝐵 ∈ 𝐶 )
10 9 adantl ⊢ ( ( ( 𝐸 : 𝐷 –1-1→ 𝑅 ∧ 𝐹 : 𝐶 –1-1→ 𝐷 ) ∧ ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ) → 𝐵 ∈ 𝐶 )
11 4 10 ffvelcdmd ⊢ ( ( ( 𝐸 : 𝐷 –1-1→ 𝑅 ∧ 𝐹 : 𝐶 –1-1→ 𝐷 ) ∧ ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ) → ( 𝐹 ‘ 𝐵 ) ∈ 𝐷 )
12 11 3adant3 ⊢ ( ( ( 𝐸 : 𝐷 –1-1→ 𝑅 ∧ 𝐹 : 𝐶 –1-1→ 𝐷 ) ∧ ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ∧ 𝐴 ≠ 𝐵 ) → ( 𝐹 ‘ 𝐵 ) ∈ 𝐷 )
13 simpr ⊢ ( ( 𝐸 : 𝐷 –1-1→ 𝑅 ∧ 𝐹 : 𝐶 –1-1→ 𝐷 ) → 𝐹 : 𝐶 –1-1→ 𝐷 )
14 df-3an ⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ∧ 𝐴 ≠ 𝐵 ) ↔ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ∧ 𝐴 ≠ 𝐵 ) )
15 14 biimpri ⊢ ( ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ∧ 𝐴 ≠ 𝐵 ) → ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ∧ 𝐴 ≠ 𝐵 ) )
16 dff14i ⊢ ( ( 𝐹 : 𝐶 –1-1→ 𝐷 ∧ ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ∧ 𝐴 ≠ 𝐵 ) ) → ( 𝐹 ‘ 𝐴 ) ≠ ( 𝐹 ‘ 𝐵 ) )
17 13 15 16 syl3an132 ⊢ ( ( ( 𝐸 : 𝐷 –1-1→ 𝑅 ∧ 𝐹 : 𝐶 –1-1→ 𝐷 ) ∧ ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ∧ 𝐴 ≠ 𝐵 ) → ( 𝐹 ‘ 𝐴 ) ≠ ( 𝐹 ‘ 𝐵 ) )
18 dff14i ⊢ ( ( 𝐸 : 𝐷 –1-1→ 𝑅 ∧ ( ( 𝐹 ‘ 𝐴 ) ∈ 𝐷 ∧ ( 𝐹 ‘ 𝐵 ) ∈ 𝐷 ∧ ( 𝐹 ‘ 𝐴 ) ≠ ( 𝐹 ‘ 𝐵 ) ) ) → ( 𝐸 ‘ ( 𝐹 ‘ 𝐴 ) ) ≠ ( 𝐸 ‘ ( 𝐹 ‘ 𝐵 ) ) )
19 1 8 12 17 18 syl13anc ⊢ ( ( ( 𝐸 : 𝐷 –1-1→ 𝑅 ∧ 𝐹 : 𝐶 –1-1→ 𝐷 ) ∧ ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ∧ 𝐴 ≠ 𝐵 ) → ( 𝐸 ‘ ( 𝐹 ‘ 𝐴 ) ) ≠ ( 𝐸 ‘ ( 𝐹 ‘ 𝐵 ) ) )
20 simpl ⊢ ( ( ( 𝐸 ‘ ( 𝐹 ‘ 𝐴 ) ) = 𝑋 ∧ ( 𝐸 ‘ ( 𝐹 ‘ 𝐵 ) ) = 𝑌 ) → ( 𝐸 ‘ ( 𝐹 ‘ 𝐴 ) ) = 𝑋 )
21 simpr ⊢ ( ( ( 𝐸 ‘ ( 𝐹 ‘ 𝐴 ) ) = 𝑋 ∧ ( 𝐸 ‘ ( 𝐹 ‘ 𝐵 ) ) = 𝑌 ) → ( 𝐸 ‘ ( 𝐹 ‘ 𝐵 ) ) = 𝑌 )
22 20 21 neeq12d ⊢ ( ( ( 𝐸 ‘ ( 𝐹 ‘ 𝐴 ) ) = 𝑋 ∧ ( 𝐸 ‘ ( 𝐹 ‘ 𝐵 ) ) = 𝑌 ) → ( ( 𝐸 ‘ ( 𝐹 ‘ 𝐴 ) ) ≠ ( 𝐸 ‘ ( 𝐹 ‘ 𝐵 ) ) ↔ 𝑋 ≠ 𝑌 ) )
23 19 22 syl5ibcom ⊢ ( ( ( 𝐸 : 𝐷 –1-1→ 𝑅 ∧ 𝐹 : 𝐶 –1-1→ 𝐷 ) ∧ ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ∧ 𝐴 ≠ 𝐵 ) → ( ( ( 𝐸 ‘ ( 𝐹 ‘ 𝐴 ) ) = 𝑋 ∧ ( 𝐸 ‘ ( 𝐹 ‘ 𝐵 ) ) = 𝑌 ) → 𝑋 ≠ 𝑌 ) )