Metamath Proof Explorer

Theorem ftp

Description: A function with a domain of three elements. (Contributed by Stefan O'Rear, 17-Oct-2014) (Proof shortened by Alexander van der Vekens, 23-Jan-2018)

Ref Expression
Hypotheses ftp.a ⊢ A ∈ V
ftp.b ⊢ B ∈ V
ftp.c ⊢ C ∈ V
ftp.d ⊢ X ∈ V
ftp.e ⊢ Y ∈ V
ftp.f ⊢ Z ∈ V
ftp.g ⊢ A ≠ B
ftp.h ⊢ A ≠ C
ftp.i ⊢ B ≠ C
Assertion ftp ⊢ A X B Y C Z : A B C ⟶ X Y Z

Proof

Step Hyp Ref Expression
1 ftp.a ⊢ A ∈ V
2 ftp.b ⊢ B ∈ V
3 ftp.c ⊢ C ∈ V
4 ftp.d ⊢ X ∈ V
5 ftp.e ⊢ Y ∈ V
6 ftp.f ⊢ Z ∈ V
7 ftp.g ⊢ A ≠ B
8 ftp.h ⊢ A ≠ C
9 ftp.i ⊢ B ≠ C
10 1 2 3 3pm3.2i ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V
11 4 5 6 3pm3.2i ⊢ X ∈ V ∧ Y ∈ V ∧ Z ∈ V
12 7 8 9 3pm3.2i ⊢ A ≠ B ∧ A ≠ C ∧ B ≠ C
13 ftpg ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ X ∈ V ∧ Y ∈ V ∧ Z ∈ V ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C → A X B Y C Z : A B C ⟶ X Y Z
14 10 11 12 13 mp3an ⊢ A X B Y C Z : A B C ⟶ X Y Z