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 ( ( 𝐴𝑉𝐶𝑊𝐴𝐵 ) → ( { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } ‘ 𝐴 ) = 𝐶 )