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

Metamath Proof Explorer

Theorem xpprsng

Description: The Cartesian product of an unordered pair and a singleton. (Contributed by AV, 20-May-2019)

Ref Expression
Assertion xpprsng ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑈 ) → ( { 𝐴 , 𝐵 } × { 𝐶 } ) = { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐶 ⟩ } )

Proof

Step Hyp Ref Expression
1 df-pr ⊢ { 𝐴 , 𝐵 } = ( { 𝐴 } ∪ { 𝐵 } )
2 1 xpeq1i ⊢ ( { 𝐴 , 𝐵 } × { 𝐶 } ) = ( ( { 𝐴 } ∪ { 𝐵 } ) × { 𝐶 } )
3 xpsng ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑈 ) → ( { 𝐴 } × { 𝐶 } ) = { ⟨ 𝐴 , 𝐶 ⟩ } )
4 3 3adant2 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑈 ) → ( { 𝐴 } × { 𝐶 } ) = { ⟨ 𝐴 , 𝐶 ⟩ } )
5 xpsng ⊢ ( ( 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑈 ) → ( { 𝐵 } × { 𝐶 } ) = { ⟨ 𝐵 , 𝐶 ⟩ } )
6 5 3adant1 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑈 ) → ( { 𝐵 } × { 𝐶 } ) = { ⟨ 𝐵 , 𝐶 ⟩ } )
7 4 6 uneq12d ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑈 ) → ( ( { 𝐴 } × { 𝐶 } ) ∪ ( { 𝐵 } × { 𝐶 } ) ) = ( { ⟨ 𝐴 , 𝐶 ⟩ } ∪ { ⟨ 𝐵 , 𝐶 ⟩ } ) )
8 xpundir ⊢ ( ( { 𝐴 } ∪ { 𝐵 } ) × { 𝐶 } ) = ( ( { 𝐴 } × { 𝐶 } ) ∪ ( { 𝐵 } × { 𝐶 } ) )
9 df-pr ⊢ { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐶 ⟩ } = ( { ⟨ 𝐴 , 𝐶 ⟩ } ∪ { ⟨ 𝐵 , 𝐶 ⟩ } )
10 7 8 9 3eqtr4g ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑈 ) → ( ( { 𝐴 } ∪ { 𝐵 } ) × { 𝐶 } ) = { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐶 ⟩ } )
11 2 10 eqtrid ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑈 ) → ( { 𝐴 , 𝐵 } × { 𝐶 } ) = { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐶 ⟩ } )