Theorem fntpg

Description: Function with a domain of three different values. (Contributed by Alexander van der Vekens, 5-Dec-2017)

	Ref	Expression
Assertion	fntpg	⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ ( 𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) ) → { ⟨ 𝑋 , 𝐴 ⟩ , ⟨ 𝑌 , 𝐵 ⟩ , ⟨ 𝑍 , 𝐶 ⟩ } Fn { 𝑋 , 𝑌 , 𝑍 } )

Proof

Step	Hyp	Ref	Expression
1		funtpg	⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ ( 𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) ) → Fun { ⟨ 𝑋 , 𝐴 ⟩ , ⟨ 𝑌 , 𝐵 ⟩ , ⟨ 𝑍 , 𝐶 ⟩ } )
2		dmsnopg	⊢ ( 𝐴 ∈ 𝐹 → dom { ⟨ 𝑋 , 𝐴 ⟩ } = { 𝑋 } )
3	2	3ad2ant1	⊢ ( ( 𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻 ) → dom { ⟨ 𝑋 , 𝐴 ⟩ } = { 𝑋 } )
4		dmsnopg	⊢ ( 𝐵 ∈ 𝐺 → dom { ⟨ 𝑌 , 𝐵 ⟩ } = { 𝑌 } )
5	4	3ad2ant2	⊢ ( ( 𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻 ) → dom { ⟨ 𝑌 , 𝐵 ⟩ } = { 𝑌 } )
6	3 5	jca	⊢ ( ( 𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻 ) → ( dom { ⟨ 𝑋 , 𝐴 ⟩ } = { 𝑋 } ∧ dom { ⟨ 𝑌 , 𝐵 ⟩ } = { 𝑌 } ) )
7	6	3ad2ant2	⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ ( 𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) ) → ( dom { ⟨ 𝑋 , 𝐴 ⟩ } = { 𝑋 } ∧ dom { ⟨ 𝑌 , 𝐵 ⟩ } = { 𝑌 } ) )
8		uneq12	⊢ ( ( dom { ⟨ 𝑋 , 𝐴 ⟩ } = { 𝑋 } ∧ dom { ⟨ 𝑌 , 𝐵 ⟩ } = { 𝑌 } ) → ( dom { ⟨ 𝑋 , 𝐴 ⟩ } ∪ dom { ⟨ 𝑌 , 𝐵 ⟩ } ) = ( { 𝑋 } ∪ { 𝑌 } ) )
9	7 8	syl	⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ ( 𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) ) → ( dom { ⟨ 𝑋 , 𝐴 ⟩ } ∪ dom { ⟨ 𝑌 , 𝐵 ⟩ } ) = ( { 𝑋 } ∪ { 𝑌 } ) )
10		df-pr	⊢ { 𝑋 , 𝑌 } = ( { 𝑋 } ∪ { 𝑌 } )
11	9 10	eqtr4di	⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ ( 𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) ) → ( dom { ⟨ 𝑋 , 𝐴 ⟩ } ∪ dom { ⟨ 𝑌 , 𝐵 ⟩ } ) = { 𝑋 , 𝑌 } )
12		df-pr	⊢ { ⟨ 𝑋 , 𝐴 ⟩ , ⟨ 𝑌 , 𝐵 ⟩ } = ( { ⟨ 𝑋 , 𝐴 ⟩ } ∪ { ⟨ 𝑌 , 𝐵 ⟩ } )
13	12	dmeqi	⊢ dom { ⟨ 𝑋 , 𝐴 ⟩ , ⟨ 𝑌 , 𝐵 ⟩ } = dom ( { ⟨ 𝑋 , 𝐴 ⟩ } ∪ { ⟨ 𝑌 , 𝐵 ⟩ } )
14	13	eqeq1i	⊢ ( dom { ⟨ 𝑋 , 𝐴 ⟩ , ⟨ 𝑌 , 𝐵 ⟩ } = { 𝑋 , 𝑌 } ↔ dom ( { ⟨ 𝑋 , 𝐴 ⟩ } ∪ { ⟨ 𝑌 , 𝐵 ⟩ } ) = { 𝑋 , 𝑌 } )
15		dmun	⊢ dom ( { ⟨ 𝑋 , 𝐴 ⟩ } ∪ { ⟨ 𝑌 , 𝐵 ⟩ } ) = ( dom { ⟨ 𝑋 , 𝐴 ⟩ } ∪ dom { ⟨ 𝑌 , 𝐵 ⟩ } )
16	15	eqeq1i	⊢ ( dom ( { ⟨ 𝑋 , 𝐴 ⟩ } ∪ { ⟨ 𝑌 , 𝐵 ⟩ } ) = { 𝑋 , 𝑌 } ↔ ( dom { ⟨ 𝑋 , 𝐴 ⟩ } ∪ dom { ⟨ 𝑌 , 𝐵 ⟩ } ) = { 𝑋 , 𝑌 } )
17	14 16	bitri	⊢ ( dom { ⟨ 𝑋 , 𝐴 ⟩ , ⟨ 𝑌 , 𝐵 ⟩ } = { 𝑋 , 𝑌 } ↔ ( dom { ⟨ 𝑋 , 𝐴 ⟩ } ∪ dom { ⟨ 𝑌 , 𝐵 ⟩ } ) = { 𝑋 , 𝑌 } )
18	11 17	sylibr	⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ ( 𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) ) → dom { ⟨ 𝑋 , 𝐴 ⟩ , ⟨ 𝑌 , 𝐵 ⟩ } = { 𝑋 , 𝑌 } )
19		dmsnopg	⊢ ( 𝐶 ∈ 𝐻 → dom { ⟨ 𝑍 , 𝐶 ⟩ } = { 𝑍 } )
20	19	3ad2ant3	⊢ ( ( 𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻 ) → dom { ⟨ 𝑍 , 𝐶 ⟩ } = { 𝑍 } )
21	20	3ad2ant2	⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ ( 𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) ) → dom { ⟨ 𝑍 , 𝐶 ⟩ } = { 𝑍 } )
22	18 21	uneq12d	⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ ( 𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) ) → ( dom { ⟨ 𝑋 , 𝐴 ⟩ , ⟨ 𝑌 , 𝐵 ⟩ } ∪ dom { ⟨ 𝑍 , 𝐶 ⟩ } ) = ( { 𝑋 , 𝑌 } ∪ { 𝑍 } ) )
23		df-tp	⊢ { ⟨ 𝑋 , 𝐴 ⟩ , ⟨ 𝑌 , 𝐵 ⟩ , ⟨ 𝑍 , 𝐶 ⟩ } = ( { ⟨ 𝑋 , 𝐴 ⟩ , ⟨ 𝑌 , 𝐵 ⟩ } ∪ { ⟨ 𝑍 , 𝐶 ⟩ } )
24	23	dmeqi	⊢ dom { ⟨ 𝑋 , 𝐴 ⟩ , ⟨ 𝑌 , 𝐵 ⟩ , ⟨ 𝑍 , 𝐶 ⟩ } = dom ( { ⟨ 𝑋 , 𝐴 ⟩ , ⟨ 𝑌 , 𝐵 ⟩ } ∪ { ⟨ 𝑍 , 𝐶 ⟩ } )
25		dmun	⊢ dom ( { ⟨ 𝑋 , 𝐴 ⟩ , ⟨ 𝑌 , 𝐵 ⟩ } ∪ { ⟨ 𝑍 , 𝐶 ⟩ } ) = ( dom { ⟨ 𝑋 , 𝐴 ⟩ , ⟨ 𝑌 , 𝐵 ⟩ } ∪ dom { ⟨ 𝑍 , 𝐶 ⟩ } )
26	24 25	eqtri	⊢ dom { ⟨ 𝑋 , 𝐴 ⟩ , ⟨ 𝑌 , 𝐵 ⟩ , ⟨ 𝑍 , 𝐶 ⟩ } = ( dom { ⟨ 𝑋 , 𝐴 ⟩ , ⟨ 𝑌 , 𝐵 ⟩ } ∪ dom { ⟨ 𝑍 , 𝐶 ⟩ } )
27		df-tp	⊢ { 𝑋 , 𝑌 , 𝑍 } = ( { 𝑋 , 𝑌 } ∪ { 𝑍 } )
28	22 26 27	3eqtr4g	⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ ( 𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) ) → dom { ⟨ 𝑋 , 𝐴 ⟩ , ⟨ 𝑌 , 𝐵 ⟩ , ⟨ 𝑍 , 𝐶 ⟩ } = { 𝑋 , 𝑌 , 𝑍 } )
29		df-fn	⊢ ( { ⟨ 𝑋 , 𝐴 ⟩ , ⟨ 𝑌 , 𝐵 ⟩ , ⟨ 𝑍 , 𝐶 ⟩ } Fn { 𝑋 , 𝑌 , 𝑍 } ↔ ( Fun { ⟨ 𝑋 , 𝐴 ⟩ , ⟨ 𝑌 , 𝐵 ⟩ , ⟨ 𝑍 , 𝐶 ⟩ } ∧ dom { ⟨ 𝑋 , 𝐴 ⟩ , ⟨ 𝑌 , 𝐵 ⟩ , ⟨ 𝑍 , 𝐶 ⟩ } = { 𝑋 , 𝑌 , 𝑍 } ) )
30	1 28 29	sylanbrc	⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ ( 𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) ) → { ⟨ 𝑋 , 𝐴 ⟩ , ⟨ 𝑌 , 𝐵 ⟩ , ⟨ 𝑍 , 𝐶 ⟩ } Fn { 𝑋 , 𝑌 , 𝑍 } )