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