This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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