Metamath Proof Explorer


Theorem ftpg

Description: A function with a domain of three elements. (Contributed by Alexander van der Vekens, 4-Dec-2017)

Ref Expression
Assertion ftpg XUYVZWAFBGCHXYXZYZXAYBZC:XYZABC

Proof

Step Hyp Ref Expression
1 3simpa XUYVZWXUYV
2 3simpa AFBGCHAFBG
3 simp1 XYXZYZXY
4 fprg XUYVAFBGXYXAYB:XYAB
5 1 2 3 4 syl3an XUYVZWAFBGCHXYXZYZXAYB:XYAB
6 eqidd XUYVZWAFBGCHXYXZYZZC=ZC
7 simp3 XUYVZWZW
8 simp3 AFBGCHCH
9 7 8 anim12i XUYVZWAFBGCHZWCH
10 9 3adant3 XUYVZWAFBGCHXYXZYZZWCH
11 fsng ZWCHZC:ZCZC=ZC
12 10 11 syl XUYVZWAFBGCHXYXZYZZC:ZCZC=ZC
13 6 12 mpbird XUYVZWAFBGCHXYXZYZZC:ZC
14 elpri ZXYZ=XZ=Y
15 eqcom Z=XX=Z
16 nne ¬XZX=Z
17 15 16 bitr4i Z=X¬XZ
18 eqcom Z=YY=Z
19 nne ¬YZY=Z
20 18 19 bitr4i Z=Y¬YZ
21 17 20 orbi12i Z=XZ=Y¬XZ¬YZ
22 ianor ¬XZYZ¬XZ¬YZ
23 21 22 sylbb2 Z=XZ=Y¬XZYZ
24 14 23 syl ZXY¬XZYZ
25 24 con2i XZYZ¬ZXY
26 25 3adant1 XYXZYZ¬ZXY
27 26 3ad2ant3 XUYVZWAFBGCHXYXZYZ¬ZXY
28 disjsn XYZ=¬ZXY
29 27 28 sylibr XUYVZWAFBGCHXYXZYZXYZ=
30 fun XAYB:XYABZC:ZCXYZ=XAYBZC:XYZABC
31 5 13 29 30 syl21anc XUYVZWAFBGCHXYXZYZXAYBZC:XYZABC
32 df-tp XAYBZC=XAYBZC
33 32 feq1i XAYBZC:XYZABCXAYBZC:XYZABC
34 df-tp XYZ=XYZ
35 df-tp ABC=ABC
36 34 35 feq23i XAYBZC:XYZABCXAYBZC:XYZABC
37 33 36 bitri XAYBZC:XYZABCXAYBZC:XYZABC
38 31 37 sylibr XUYVZWAFBGCHXYXZYZXAYBZC:XYZABC