# 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 ${⊢}\left(\left({X}\in {U}\wedge {Y}\in {V}\wedge {Z}\in {W}\right)\wedge \left({A}\in {F}\wedge {B}\in {G}\wedge {C}\in {H}\right)\wedge \left({X}\ne {Y}\wedge {X}\ne {Z}\wedge {Y}\ne {Z}\right)\right)\to \left\{⟨{X},{A}⟩,⟨{Y},{B}⟩,⟨{Z},{C}⟩\right\}:\left\{{X},{Y},{Z}\right\}⟶\left\{{A},{B},{C}\right\}$

### Proof

Step Hyp Ref Expression
1 3simpa ${⊢}\left({X}\in {U}\wedge {Y}\in {V}\wedge {Z}\in {W}\right)\to \left({X}\in {U}\wedge {Y}\in {V}\right)$
2 3simpa ${⊢}\left({A}\in {F}\wedge {B}\in {G}\wedge {C}\in {H}\right)\to \left({A}\in {F}\wedge {B}\in {G}\right)$
3 simp1 ${⊢}\left({X}\ne {Y}\wedge {X}\ne {Z}\wedge {Y}\ne {Z}\right)\to {X}\ne {Y}$
4 fprg ${⊢}\left(\left({X}\in {U}\wedge {Y}\in {V}\right)\wedge \left({A}\in {F}\wedge {B}\in {G}\right)\wedge {X}\ne {Y}\right)\to \left\{⟨{X},{A}⟩,⟨{Y},{B}⟩\right\}:\left\{{X},{Y}\right\}⟶\left\{{A},{B}\right\}$
5 1 2 3 4 syl3an ${⊢}\left(\left({X}\in {U}\wedge {Y}\in {V}\wedge {Z}\in {W}\right)\wedge \left({A}\in {F}\wedge {B}\in {G}\wedge {C}\in {H}\right)\wedge \left({X}\ne {Y}\wedge {X}\ne {Z}\wedge {Y}\ne {Z}\right)\right)\to \left\{⟨{X},{A}⟩,⟨{Y},{B}⟩\right\}:\left\{{X},{Y}\right\}⟶\left\{{A},{B}\right\}$
6 eqidd ${⊢}\left(\left({X}\in {U}\wedge {Y}\in {V}\wedge {Z}\in {W}\right)\wedge \left({A}\in {F}\wedge {B}\in {G}\wedge {C}\in {H}\right)\wedge \left({X}\ne {Y}\wedge {X}\ne {Z}\wedge {Y}\ne {Z}\right)\right)\to \left\{⟨{Z},{C}⟩\right\}=\left\{⟨{Z},{C}⟩\right\}$
7 simp3 ${⊢}\left({X}\in {U}\wedge {Y}\in {V}\wedge {Z}\in {W}\right)\to {Z}\in {W}$
8 simp3 ${⊢}\left({A}\in {F}\wedge {B}\in {G}\wedge {C}\in {H}\right)\to {C}\in {H}$
9 7 8 anim12i ${⊢}\left(\left({X}\in {U}\wedge {Y}\in {V}\wedge {Z}\in {W}\right)\wedge \left({A}\in {F}\wedge {B}\in {G}\wedge {C}\in {H}\right)\right)\to \left({Z}\in {W}\wedge {C}\in {H}\right)$
10 9 3adant3 ${⊢}\left(\left({X}\in {U}\wedge {Y}\in {V}\wedge {Z}\in {W}\right)\wedge \left({A}\in {F}\wedge {B}\in {G}\wedge {C}\in {H}\right)\wedge \left({X}\ne {Y}\wedge {X}\ne {Z}\wedge {Y}\ne {Z}\right)\right)\to \left({Z}\in {W}\wedge {C}\in {H}\right)$
11 fsng ${⊢}\left({Z}\in {W}\wedge {C}\in {H}\right)\to \left(\left\{⟨{Z},{C}⟩\right\}:\left\{{Z}\right\}⟶\left\{{C}\right\}↔\left\{⟨{Z},{C}⟩\right\}=\left\{⟨{Z},{C}⟩\right\}\right)$
12 10 11 syl ${⊢}\left(\left({X}\in {U}\wedge {Y}\in {V}\wedge {Z}\in {W}\right)\wedge \left({A}\in {F}\wedge {B}\in {G}\wedge {C}\in {H}\right)\wedge \left({X}\ne {Y}\wedge {X}\ne {Z}\wedge {Y}\ne {Z}\right)\right)\to \left(\left\{⟨{Z},{C}⟩\right\}:\left\{{Z}\right\}⟶\left\{{C}\right\}↔\left\{⟨{Z},{C}⟩\right\}=\left\{⟨{Z},{C}⟩\right\}\right)$
13 6 12 mpbird ${⊢}\left(\left({X}\in {U}\wedge {Y}\in {V}\wedge {Z}\in {W}\right)\wedge \left({A}\in {F}\wedge {B}\in {G}\wedge {C}\in {H}\right)\wedge \left({X}\ne {Y}\wedge {X}\ne {Z}\wedge {Y}\ne {Z}\right)\right)\to \left\{⟨{Z},{C}⟩\right\}:\left\{{Z}\right\}⟶\left\{{C}\right\}$
14 elpri ${⊢}{Z}\in \left\{{X},{Y}\right\}\to \left({Z}={X}\vee {Z}={Y}\right)$
15 eqcom ${⊢}{Z}={X}↔{X}={Z}$
16 nne ${⊢}¬{X}\ne {Z}↔{X}={Z}$
17 15 16 bitr4i ${⊢}{Z}={X}↔¬{X}\ne {Z}$
18 eqcom ${⊢}{Z}={Y}↔{Y}={Z}$
19 nne ${⊢}¬{Y}\ne {Z}↔{Y}={Z}$
20 18 19 bitr4i ${⊢}{Z}={Y}↔¬{Y}\ne {Z}$
21 17 20 orbi12i ${⊢}\left({Z}={X}\vee {Z}={Y}\right)↔\left(¬{X}\ne {Z}\vee ¬{Y}\ne {Z}\right)$
22 ianor ${⊢}¬\left({X}\ne {Z}\wedge {Y}\ne {Z}\right)↔\left(¬{X}\ne {Z}\vee ¬{Y}\ne {Z}\right)$
23 21 22 sylbb2 ${⊢}\left({Z}={X}\vee {Z}={Y}\right)\to ¬\left({X}\ne {Z}\wedge {Y}\ne {Z}\right)$
24 14 23 syl ${⊢}{Z}\in \left\{{X},{Y}\right\}\to ¬\left({X}\ne {Z}\wedge {Y}\ne {Z}\right)$
25 24 con2i ${⊢}\left({X}\ne {Z}\wedge {Y}\ne {Z}\right)\to ¬{Z}\in \left\{{X},{Y}\right\}$
26 25 3adant1 ${⊢}\left({X}\ne {Y}\wedge {X}\ne {Z}\wedge {Y}\ne {Z}\right)\to ¬{Z}\in \left\{{X},{Y}\right\}$
27 26 3ad2ant3 ${⊢}\left(\left({X}\in {U}\wedge {Y}\in {V}\wedge {Z}\in {W}\right)\wedge \left({A}\in {F}\wedge {B}\in {G}\wedge {C}\in {H}\right)\wedge \left({X}\ne {Y}\wedge {X}\ne {Z}\wedge {Y}\ne {Z}\right)\right)\to ¬{Z}\in \left\{{X},{Y}\right\}$
28 disjsn ${⊢}\left\{{X},{Y}\right\}\cap \left\{{Z}\right\}=\varnothing ↔¬{Z}\in \left\{{X},{Y}\right\}$
29 27 28 sylibr ${⊢}\left(\left({X}\in {U}\wedge {Y}\in {V}\wedge {Z}\in {W}\right)\wedge \left({A}\in {F}\wedge {B}\in {G}\wedge {C}\in {H}\right)\wedge \left({X}\ne {Y}\wedge {X}\ne {Z}\wedge {Y}\ne {Z}\right)\right)\to \left\{{X},{Y}\right\}\cap \left\{{Z}\right\}=\varnothing$
30 fun ${⊢}\left(\left(\left\{⟨{X},{A}⟩,⟨{Y},{B}⟩\right\}:\left\{{X},{Y}\right\}⟶\left\{{A},{B}\right\}\wedge \left\{⟨{Z},{C}⟩\right\}:\left\{{Z}\right\}⟶\left\{{C}\right\}\right)\wedge \left\{{X},{Y}\right\}\cap \left\{{Z}\right\}=\varnothing \right)\to \left(\left\{⟨{X},{A}⟩,⟨{Y},{B}⟩\right\}\cup \left\{⟨{Z},{C}⟩\right\}\right):\left\{{X},{Y}\right\}\cup \left\{{Z}\right\}⟶\left\{{A},{B}\right\}\cup \left\{{C}\right\}$
31 5 13 29 30 syl21anc ${⊢}\left(\left({X}\in {U}\wedge {Y}\in {V}\wedge {Z}\in {W}\right)\wedge \left({A}\in {F}\wedge {B}\in {G}\wedge {C}\in {H}\right)\wedge \left({X}\ne {Y}\wedge {X}\ne {Z}\wedge {Y}\ne {Z}\right)\right)\to \left(\left\{⟨{X},{A}⟩,⟨{Y},{B}⟩\right\}\cup \left\{⟨{Z},{C}⟩\right\}\right):\left\{{X},{Y}\right\}\cup \left\{{Z}\right\}⟶\left\{{A},{B}\right\}\cup \left\{{C}\right\}$
32 df-tp ${⊢}\left\{⟨{X},{A}⟩,⟨{Y},{B}⟩,⟨{Z},{C}⟩\right\}=\left\{⟨{X},{A}⟩,⟨{Y},{B}⟩\right\}\cup \left\{⟨{Z},{C}⟩\right\}$
33 32 feq1i ${⊢}\left\{⟨{X},{A}⟩,⟨{Y},{B}⟩,⟨{Z},{C}⟩\right\}:\left\{{X},{Y},{Z}\right\}⟶\left\{{A},{B},{C}\right\}↔\left(\left\{⟨{X},{A}⟩,⟨{Y},{B}⟩\right\}\cup \left\{⟨{Z},{C}⟩\right\}\right):\left\{{X},{Y},{Z}\right\}⟶\left\{{A},{B},{C}\right\}$
34 df-tp ${⊢}\left\{{X},{Y},{Z}\right\}=\left\{{X},{Y}\right\}\cup \left\{{Z}\right\}$
35 df-tp ${⊢}\left\{{A},{B},{C}\right\}=\left\{{A},{B}\right\}\cup \left\{{C}\right\}$
36 34 35 feq23i ${⊢}\left(\left\{⟨{X},{A}⟩,⟨{Y},{B}⟩\right\}\cup \left\{⟨{Z},{C}⟩\right\}\right):\left\{{X},{Y},{Z}\right\}⟶\left\{{A},{B},{C}\right\}↔\left(\left\{⟨{X},{A}⟩,⟨{Y},{B}⟩\right\}\cup \left\{⟨{Z},{C}⟩\right\}\right):\left\{{X},{Y}\right\}\cup \left\{{Z}\right\}⟶\left\{{A},{B}\right\}\cup \left\{{C}\right\}$
37 33 36 bitri ${⊢}\left\{⟨{X},{A}⟩,⟨{Y},{B}⟩,⟨{Z},{C}⟩\right\}:\left\{{X},{Y},{Z}\right\}⟶\left\{{A},{B},{C}\right\}↔\left(\left\{⟨{X},{A}⟩,⟨{Y},{B}⟩\right\}\cup \left\{⟨{Z},{C}⟩\right\}\right):\left\{{X},{Y}\right\}\cup \left\{{Z}\right\}⟶\left\{{A},{B}\right\}\cup \left\{{C}\right\}$
38 31 37 sylibr ${⊢}\left(\left({X}\in {U}\wedge {Y}\in {V}\wedge {Z}\in {W}\right)\wedge \left({A}\in {F}\wedge {B}\in {G}\wedge {C}\in {H}\right)\wedge \left({X}\ne {Y}\wedge {X}\ne {Z}\wedge {Y}\ne {Z}\right)\right)\to \left\{⟨{X},{A}⟩,⟨{Y},{B}⟩,⟨{Z},{C}⟩\right\}:\left\{{X},{Y},{Z}\right\}⟶\left\{{A},{B},{C}\right\}$