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

Metamath Proof Explorer

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 { 𝑋 , 𝑌 , 𝑍 } )