Theorem fntp

Description: A function with a domain of three elements. (Contributed by NM, 14-Sep-2011) (Revised by Mario Carneiro, 26-Apr-2015)

	Ref	Expression
Hypotheses	fntp.1	⊢ 𝐴 ∈ V
	fntp.2	⊢ 𝐵 ∈ V
	fntp.3	⊢ 𝐶 ∈ V
	fntp.4	⊢ 𝐷 ∈ V
	fntp.5	⊢ 𝐸 ∈ V
	fntp.6	⊢ 𝐹 ∈ V
Assertion	fntp	⊢ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) → { ⟨ 𝐴 , 𝐷 ⟩ , ⟨ 𝐵 , 𝐸 ⟩ , ⟨ 𝐶 , 𝐹 ⟩ } Fn { 𝐴 , 𝐵 , 𝐶 } )

Proof

Step	Hyp	Ref	Expression
1		fntp.1	⊢ 𝐴 ∈ V
2		fntp.2	⊢ 𝐵 ∈ V
3		fntp.3	⊢ 𝐶 ∈ V
4		fntp.4	⊢ 𝐷 ∈ V
5		fntp.5	⊢ 𝐸 ∈ V
6		fntp.6	⊢ 𝐹 ∈ V
7	1 2 3 4 5 6	funtp	⊢ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) → Fun { ⟨ 𝐴 , 𝐷 ⟩ , ⟨ 𝐵 , 𝐸 ⟩ , ⟨ 𝐶 , 𝐹 ⟩ } )
8	4 5 6	dmtpop	⊢ dom { ⟨ 𝐴 , 𝐷 ⟩ , ⟨ 𝐵 , 𝐸 ⟩ , ⟨ 𝐶 , 𝐹 ⟩ } = { 𝐴 , 𝐵 , 𝐶 }
9		df-fn	⊢ ( { ⟨ 𝐴 , 𝐷 ⟩ , ⟨ 𝐵 , 𝐸 ⟩ , ⟨ 𝐶 , 𝐹 ⟩ } Fn { 𝐴 , 𝐵 , 𝐶 } ↔ ( Fun { ⟨ 𝐴 , 𝐷 ⟩ , ⟨ 𝐵 , 𝐸 ⟩ , ⟨ 𝐶 , 𝐹 ⟩ } ∧ dom { ⟨ 𝐴 , 𝐷 ⟩ , ⟨ 𝐵 , 𝐸 ⟩ , ⟨ 𝐶 , 𝐹 ⟩ } = { 𝐴 , 𝐵 , 𝐶 } ) )
10	7 8 9	sylanblrc	⊢ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) → { ⟨ 𝐴 , 𝐷 ⟩ , ⟨ 𝐵 , 𝐸 ⟩ , ⟨ 𝐶 , 𝐹 ⟩ } Fn { 𝐴 , 𝐵 , 𝐶 } )