Metamath Proof Explorer

Theorem fvtp1g

Description: The value of a function with a domain of (at most) three elements. (Contributed by Alexander van der Vekens, 4-Dec-2017)

Ref Expression
Assertion fvtp1g ${⊢}\left(\left({A}\in {V}\wedge {D}\in {W}\right)\wedge \left({A}\ne {B}\wedge {A}\ne {C}\right)\right)\to \left\{⟨{A},{D}⟩,⟨{B},{E}⟩,⟨{C},{F}⟩\right\}\left({A}\right)={D}$

Proof

Step Hyp Ref Expression
1 df-tp ${⊢}\left\{⟨{A},{D}⟩,⟨{B},{E}⟩,⟨{C},{F}⟩\right\}=\left\{⟨{A},{D}⟩,⟨{B},{E}⟩\right\}\cup \left\{⟨{C},{F}⟩\right\}$
2 1 fveq1i ${⊢}\left\{⟨{A},{D}⟩,⟨{B},{E}⟩,⟨{C},{F}⟩\right\}\left({A}\right)=\left(\left\{⟨{A},{D}⟩,⟨{B},{E}⟩\right\}\cup \left\{⟨{C},{F}⟩\right\}\right)\left({A}\right)$
3 necom ${⊢}{A}\ne {C}↔{C}\ne {A}$
4 fvunsn ${⊢}{C}\ne {A}\to \left(\left\{⟨{A},{D}⟩,⟨{B},{E}⟩\right\}\cup \left\{⟨{C},{F}⟩\right\}\right)\left({A}\right)=\left\{⟨{A},{D}⟩,⟨{B},{E}⟩\right\}\left({A}\right)$
5 3 4 sylbi ${⊢}{A}\ne {C}\to \left(\left\{⟨{A},{D}⟩,⟨{B},{E}⟩\right\}\cup \left\{⟨{C},{F}⟩\right\}\right)\left({A}\right)=\left\{⟨{A},{D}⟩,⟨{B},{E}⟩\right\}\left({A}\right)$
6 5 ad2antll ${⊢}\left(\left({A}\in {V}\wedge {D}\in {W}\right)\wedge \left({A}\ne {B}\wedge {A}\ne {C}\right)\right)\to \left(\left\{⟨{A},{D}⟩,⟨{B},{E}⟩\right\}\cup \left\{⟨{C},{F}⟩\right\}\right)\left({A}\right)=\left\{⟨{A},{D}⟩,⟨{B},{E}⟩\right\}\left({A}\right)$
7 fvpr1g ${⊢}\left({A}\in {V}\wedge {D}\in {W}\wedge {A}\ne {B}\right)\to \left\{⟨{A},{D}⟩,⟨{B},{E}⟩\right\}\left({A}\right)={D}$
8 7 3expa ${⊢}\left(\left({A}\in {V}\wedge {D}\in {W}\right)\wedge {A}\ne {B}\right)\to \left\{⟨{A},{D}⟩,⟨{B},{E}⟩\right\}\left({A}\right)={D}$
9 8 adantrr ${⊢}\left(\left({A}\in {V}\wedge {D}\in {W}\right)\wedge \left({A}\ne {B}\wedge {A}\ne {C}\right)\right)\to \left\{⟨{A},{D}⟩,⟨{B},{E}⟩\right\}\left({A}\right)={D}$
10 6 9 eqtrd ${⊢}\left(\left({A}\in {V}\wedge {D}\in {W}\right)\wedge \left({A}\ne {B}\wedge {A}\ne {C}\right)\right)\to \left(\left\{⟨{A},{D}⟩,⟨{B},{E}⟩\right\}\cup \left\{⟨{C},{F}⟩\right\}\right)\left({A}\right)={D}$
11 2 10 syl5eq ${⊢}\left(\left({A}\in {V}\wedge {D}\in {W}\right)\wedge \left({A}\ne {B}\wedge {A}\ne {C}\right)\right)\to \left\{⟨{A},{D}⟩,⟨{B},{E}⟩,⟨{C},{F}⟩\right\}\left({A}\right)={D}$