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	⊢ { ⟨ 𝐴 , 𝑋 ⟩ , ⟨ 𝐵 , 𝑌 ⟩ , ⟨ 𝐶 , 𝑍 ⟩ } : { 𝐴 , 𝐵 , 𝐶 } ⟶ { 𝑋 , 𝑌 , 𝑍 }