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

Metamath Proof Explorer

Theorem ftp

Description: A function with a domain of three elements. (Contributed by Stefan O'Rear, 17-Oct-2014) (Proof shortened by Alexander van der Vekens, 23-Jan-2018)

Ref Expression
Hypotheses ftp.a ⊢ 𝐴 ∈ V
ftp.b ⊢ 𝐵 ∈ V
ftp.c ⊢ 𝐶 ∈ V
ftp.d ⊢ 𝑋 ∈ V
ftp.e ⊢ 𝑌 ∈ V
ftp.f ⊢ 𝑍 ∈ V
ftp.g ⊢ 𝐴 ≠ 𝐵
ftp.h ⊢ 𝐴 ≠ 𝐶
ftp.i ⊢ 𝐵 ≠ 𝐶
Assertion ftp { ⟨ 𝐴 , 𝑋 ⟩ , ⟨ 𝐵 , 𝑌 ⟩ , ⟨ 𝐶 , 𝑍 ⟩ } : { 𝐴 , 𝐵 , 𝐶 } ⟶ { 𝑋 , 𝑌 , 𝑍 }

Proof

Step Hyp Ref Expression
1 ftp.a ⊢ 𝐴 ∈ V
2 ftp.b ⊢ 𝐵 ∈ V
3 ftp.c ⊢ 𝐶 ∈ V
4 ftp.d ⊢ 𝑋 ∈ V
5 ftp.e ⊢ 𝑌 ∈ V
6 ftp.f ⊢ 𝑍 ∈ V
7 ftp.g ⊢ 𝐴 ≠ 𝐵
8 ftp.h ⊢ 𝐴 ≠ 𝐶
9 ftp.i ⊢ 𝐵 ≠ 𝐶
10 1 2 3 3pm3.2i ⊢ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V )
11 4 5 6 3pm3.2i ⊢ ( 𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ V )
12 7 8 9 3pm3.2i ⊢ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 )
13 ftpg ⊢ ( ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V ) ∧ ( 𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ V ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → { ⟨ 𝐴 , 𝑋 ⟩ , ⟨ 𝐵 , 𝑌 ⟩ , ⟨ 𝐶 , 𝑍 ⟩ } : { 𝐴 , 𝐵 , 𝐶 } ⟶ { 𝑋 , 𝑌 , 𝑍 } )
14 10 11 12 13 mp3an ⊢ { ⟨ 𝐴 , 𝑋 ⟩ , ⟨ 𝐵 , 𝑌 ⟩ , ⟨ 𝐶 , 𝑍 ⟩ } : { 𝐴 , 𝐵 , 𝐶 } ⟶ { 𝑋 , 𝑌 , 𝑍 }