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 ⊢AXBYCZ:ABC⟶XYZ

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→AXBYCZ:ABC⟶XYZ
14 10 11 12 13 mp3an ⊢AXBYCZ:ABC⟶XYZ