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

Metamath Proof Explorer

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 { 𝐴 , 𝐵 , 𝐶 } )