# 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 ( ( ( 𝑋𝑈𝑌𝑉𝑍𝑊 ) ∧ ( 𝐴𝐹𝐵𝐺𝐶𝐻 ) ∧ ( 𝑋𝑌𝑋𝑍𝑌𝑍 ) ) → { ⟨ 𝑋 , 𝐴 ⟩ , ⟨ 𝑌 , 𝐵 ⟩ , ⟨ 𝑍 , 𝐶 ⟩ } : { 𝑋 , 𝑌 , 𝑍 } ⟶ { 𝐴 , 𝐵 , 𝐶 } )

### Proof

Step Hyp Ref Expression
1 3simpa ( ( 𝑋𝑈𝑌𝑉𝑍𝑊 ) → ( 𝑋𝑈𝑌𝑉 ) )
2 3simpa ( ( 𝐴𝐹𝐵𝐺𝐶𝐻 ) → ( 𝐴𝐹𝐵𝐺 ) )
3 simp1 ( ( 𝑋𝑌𝑋𝑍𝑌𝑍 ) → 𝑋𝑌 )
4 fprg ( ( ( 𝑋𝑈𝑌𝑉 ) ∧ ( 𝐴𝐹𝐵𝐺 ) ∧ 𝑋𝑌 ) → { ⟨ 𝑋 , 𝐴 ⟩ , ⟨ 𝑌 , 𝐵 ⟩ } : { 𝑋 , 𝑌 } ⟶ { 𝐴 , 𝐵 } )
5 1 2 3 4 syl3an ( ( ( 𝑋𝑈𝑌𝑉𝑍𝑊 ) ∧ ( 𝐴𝐹𝐵𝐺𝐶𝐻 ) ∧ ( 𝑋𝑌𝑋𝑍𝑌𝑍 ) ) → { ⟨ 𝑋 , 𝐴 ⟩ , ⟨ 𝑌 , 𝐵 ⟩ } : { 𝑋 , 𝑌 } ⟶ { 𝐴 , 𝐵 } )
6 eqidd ( ( ( 𝑋𝑈𝑌𝑉𝑍𝑊 ) ∧ ( 𝐴𝐹𝐵𝐺𝐶𝐻 ) ∧ ( 𝑋𝑌𝑋𝑍𝑌𝑍 ) ) → { ⟨ 𝑍 , 𝐶 ⟩ } = { ⟨ 𝑍 , 𝐶 ⟩ } )
7 simp3 ( ( 𝑋𝑈𝑌𝑉𝑍𝑊 ) → 𝑍𝑊 )
8 simp3 ( ( 𝐴𝐹𝐵𝐺𝐶𝐻 ) → 𝐶𝐻 )
9 7 8 anim12i ( ( ( 𝑋𝑈𝑌𝑉𝑍𝑊 ) ∧ ( 𝐴𝐹𝐵𝐺𝐶𝐻 ) ) → ( 𝑍𝑊𝐶𝐻 ) )
10 9 3adant3 ( ( ( 𝑋𝑈𝑌𝑉𝑍𝑊 ) ∧ ( 𝐴𝐹𝐵𝐺𝐶𝐻 ) ∧ ( 𝑋𝑌𝑋𝑍𝑌𝑍 ) ) → ( 𝑍𝑊𝐶𝐻 ) )
11 fsng ( ( 𝑍𝑊𝐶𝐻 ) → ( { ⟨ 𝑍 , 𝐶 ⟩ } : { 𝑍 } ⟶ { 𝐶 } ↔ { ⟨ 𝑍 , 𝐶 ⟩ } = { ⟨ 𝑍 , 𝐶 ⟩ } ) )
12 10 11 syl ( ( ( 𝑋𝑈𝑌𝑉𝑍𝑊 ) ∧ ( 𝐴𝐹𝐵𝐺𝐶𝐻 ) ∧ ( 𝑋𝑌𝑋𝑍𝑌𝑍 ) ) → ( { ⟨ 𝑍 , 𝐶 ⟩ } : { 𝑍 } ⟶ { 𝐶 } ↔ { ⟨ 𝑍 , 𝐶 ⟩ } = { ⟨ 𝑍 , 𝐶 ⟩ } ) )
13 6 12 mpbird ( ( ( 𝑋𝑈𝑌𝑉𝑍𝑊 ) ∧ ( 𝐴𝐹𝐵𝐺𝐶𝐻 ) ∧ ( 𝑋𝑌𝑋𝑍𝑌𝑍 ) ) → { ⟨ 𝑍 , 𝐶 ⟩ } : { 𝑍 } ⟶ { 𝐶 } )
14 elpri ( 𝑍 ∈ { 𝑋 , 𝑌 } → ( 𝑍 = 𝑋𝑍 = 𝑌 ) )
15 eqcom ( 𝑍 = 𝑋𝑋 = 𝑍 )
16 nne ( ¬ 𝑋𝑍𝑋 = 𝑍 )
17 15 16 bitr4i ( 𝑍 = 𝑋 ↔ ¬ 𝑋𝑍 )
18 eqcom ( 𝑍 = 𝑌𝑌 = 𝑍 )
19 nne ( ¬ 𝑌𝑍𝑌 = 𝑍 )
20 18 19 bitr4i ( 𝑍 = 𝑌 ↔ ¬ 𝑌𝑍 )
21 17 20 orbi12i ( ( 𝑍 = 𝑋𝑍 = 𝑌 ) ↔ ( ¬ 𝑋𝑍 ∨ ¬ 𝑌𝑍 ) )
22 ianor ( ¬ ( 𝑋𝑍𝑌𝑍 ) ↔ ( ¬ 𝑋𝑍 ∨ ¬ 𝑌𝑍 ) )
23 21 22 sylbb2 ( ( 𝑍 = 𝑋𝑍 = 𝑌 ) → ¬ ( 𝑋𝑍𝑌𝑍 ) )
24 14 23 syl ( 𝑍 ∈ { 𝑋 , 𝑌 } → ¬ ( 𝑋𝑍𝑌𝑍 ) )
25 24 con2i ( ( 𝑋𝑍𝑌𝑍 ) → ¬ 𝑍 ∈ { 𝑋 , 𝑌 } )
26 25 3adant1 ( ( 𝑋𝑌𝑋𝑍𝑌𝑍 ) → ¬ 𝑍 ∈ { 𝑋 , 𝑌 } )
27 26 3ad2ant3 ( ( ( 𝑋𝑈𝑌𝑉𝑍𝑊 ) ∧ ( 𝐴𝐹𝐵𝐺𝐶𝐻 ) ∧ ( 𝑋𝑌𝑋𝑍𝑌𝑍 ) ) → ¬ 𝑍 ∈ { 𝑋 , 𝑌 } )
28 disjsn ( ( { 𝑋 , 𝑌 } ∩ { 𝑍 } ) = ∅ ↔ ¬ 𝑍 ∈ { 𝑋 , 𝑌 } )
29 27 28 sylibr ( ( ( 𝑋𝑈𝑌𝑉𝑍𝑊 ) ∧ ( 𝐴𝐹𝐵𝐺𝐶𝐻 ) ∧ ( 𝑋𝑌𝑋𝑍𝑌𝑍 ) ) → ( { 𝑋 , 𝑌 } ∩ { 𝑍 } ) = ∅ )
30 fun ( ( ( { ⟨ 𝑋 , 𝐴 ⟩ , ⟨ 𝑌 , 𝐵 ⟩ } : { 𝑋 , 𝑌 } ⟶ { 𝐴 , 𝐵 } ∧ { ⟨ 𝑍 , 𝐶 ⟩ } : { 𝑍 } ⟶ { 𝐶 } ) ∧ ( { 𝑋 , 𝑌 } ∩ { 𝑍 } ) = ∅ ) → ( { ⟨ 𝑋 , 𝐴 ⟩ , ⟨ 𝑌 , 𝐵 ⟩ } ∪ { ⟨ 𝑍 , 𝐶 ⟩ } ) : ( { 𝑋 , 𝑌 } ∪ { 𝑍 } ) ⟶ ( { 𝐴 , 𝐵 } ∪ { 𝐶 } ) )
31 5 13 29 30 syl21anc ( ( ( 𝑋𝑈𝑌𝑉𝑍𝑊 ) ∧ ( 𝐴𝐹𝐵𝐺𝐶𝐻 ) ∧ ( 𝑋𝑌𝑋𝑍𝑌𝑍 ) ) → ( { ⟨ 𝑋 , 𝐴 ⟩ , ⟨ 𝑌 , 𝐵 ⟩ } ∪ { ⟨ 𝑍 , 𝐶 ⟩ } ) : ( { 𝑋 , 𝑌 } ∪ { 𝑍 } ) ⟶ ( { 𝐴 , 𝐵 } ∪ { 𝐶 } ) )
32 df-tp { ⟨ 𝑋 , 𝐴 ⟩ , ⟨ 𝑌 , 𝐵 ⟩ , ⟨ 𝑍 , 𝐶 ⟩ } = ( { ⟨ 𝑋 , 𝐴 ⟩ , ⟨ 𝑌 , 𝐵 ⟩ } ∪ { ⟨ 𝑍 , 𝐶 ⟩ } )
33 32 feq1i ( { ⟨ 𝑋 , 𝐴 ⟩ , ⟨ 𝑌 , 𝐵 ⟩ , ⟨ 𝑍 , 𝐶 ⟩ } : { 𝑋 , 𝑌 , 𝑍 } ⟶ { 𝐴 , 𝐵 , 𝐶 } ↔ ( { ⟨ 𝑋 , 𝐴 ⟩ , ⟨ 𝑌 , 𝐵 ⟩ } ∪ { ⟨ 𝑍 , 𝐶 ⟩ } ) : { 𝑋 , 𝑌 , 𝑍 } ⟶ { 𝐴 , 𝐵 , 𝐶 } )
34 df-tp { 𝑋 , 𝑌 , 𝑍 } = ( { 𝑋 , 𝑌 } ∪ { 𝑍 } )
35 df-tp { 𝐴 , 𝐵 , 𝐶 } = ( { 𝐴 , 𝐵 } ∪ { 𝐶 } )
36 34 35 feq23i ( ( { ⟨ 𝑋 , 𝐴 ⟩ , ⟨ 𝑌 , 𝐵 ⟩ } ∪ { ⟨ 𝑍 , 𝐶 ⟩ } ) : { 𝑋 , 𝑌 , 𝑍 } ⟶ { 𝐴 , 𝐵 , 𝐶 } ↔ ( { ⟨ 𝑋 , 𝐴 ⟩ , ⟨ 𝑌 , 𝐵 ⟩ } ∪ { ⟨ 𝑍 , 𝐶 ⟩ } ) : ( { 𝑋 , 𝑌 } ∪ { 𝑍 } ) ⟶ ( { 𝐴 , 𝐵 } ∪ { 𝐶 } ) )
37 33 36 bitri ( { ⟨ 𝑋 , 𝐴 ⟩ , ⟨ 𝑌 , 𝐵 ⟩ , ⟨ 𝑍 , 𝐶 ⟩ } : { 𝑋 , 𝑌 , 𝑍 } ⟶ { 𝐴 , 𝐵 , 𝐶 } ↔ ( { ⟨ 𝑋 , 𝐴 ⟩ , ⟨ 𝑌 , 𝐵 ⟩ } ∪ { ⟨ 𝑍 , 𝐶 ⟩ } ) : ( { 𝑋 , 𝑌 } ∪ { 𝑍 } ) ⟶ ( { 𝐴 , 𝐵 } ∪ { 𝐶 } ) )
38 31 37 sylibr ( ( ( 𝑋𝑈𝑌𝑉𝑍𝑊 ) ∧ ( 𝐴𝐹𝐵𝐺𝐶𝐻 ) ∧ ( 𝑋𝑌𝑋𝑍𝑌𝑍 ) ) → { ⟨ 𝑋 , 𝐴 ⟩ , ⟨ 𝑌 , 𝐵 ⟩ , ⟨ 𝑍 , 𝐶 ⟩ } : { 𝑋 , 𝑌 , 𝑍 } ⟶ { 𝐴 , 𝐵 , 𝐶 } )