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

Metamath Proof Explorer

Theorem fvpr1g

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

Ref Expression
Assertion fvpr1g ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → ( { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } ‘ 𝐴 ) = 𝐶 )

Proof

Step Hyp Ref Expression
1 df-pr ⊢ { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } = ( { ⟨ 𝐴 , 𝐶 ⟩ } ∪ { ⟨ 𝐵 , 𝐷 ⟩ } )
2 1 fveq1i ⊢ ( { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } ‘ 𝐴 ) = ( ( { ⟨ 𝐴 , 𝐶 ⟩ } ∪ { ⟨ 𝐵 , 𝐷 ⟩ } ) ‘ 𝐴 )
3 necom ⊢ ( 𝐴 ≠ 𝐵 ↔ 𝐵 ≠ 𝐴 )
4 fvunsn ⊢ ( 𝐵 ≠ 𝐴 → ( ( { ⟨ 𝐴 , 𝐶 ⟩ } ∪ { ⟨ 𝐵 , 𝐷 ⟩ } ) ‘ 𝐴 ) = ( { ⟨ 𝐴 , 𝐶 ⟩ } ‘ 𝐴 ) )
5 3 4 sylbi ⊢ ( 𝐴 ≠ 𝐵 → ( ( { ⟨ 𝐴 , 𝐶 ⟩ } ∪ { ⟨ 𝐵 , 𝐷 ⟩ } ) ‘ 𝐴 ) = ( { ⟨ 𝐴 , 𝐶 ⟩ } ‘ 𝐴 ) )
6 2 5 eqtrid ⊢ ( 𝐴 ≠ 𝐵 → ( { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } ‘ 𝐴 ) = ( { ⟨ 𝐴 , 𝐶 ⟩ } ‘ 𝐴 ) )
7 6 3ad2ant3 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → ( { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } ‘ 𝐴 ) = ( { ⟨ 𝐴 , 𝐶 ⟩ } ‘ 𝐴 ) )
8 fvsng ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ) → ( { ⟨ 𝐴 , 𝐶 ⟩ } ‘ 𝐴 ) = 𝐶 )
9 8 3adant3 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → ( { ⟨ 𝐴 , 𝐶 ⟩ } ‘ 𝐴 ) = 𝐶 )
10 7 9 eqtrd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → ( { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } ‘ 𝐴 ) = 𝐶 )