Metamath Proof Explorer

Theorem xpsntpg

Description: The Cartesian product of a singleton and an unordered triple. (Contributed by AV, 18-Aug-2026)

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

Proof

Step Hyp Ref Expression
1 xpsng ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( { 𝐴 } × { 𝐵 } ) = { ⟨ 𝐴 , 𝐵 ⟩ } )
2 1 adantr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝐶 ∈ 𝑈 ∧ 𝐷 ∈ 𝑇 ) ) → ( { 𝐴 } × { 𝐵 } ) = { ⟨ 𝐴 , 𝐵 ⟩ } )
3 xpsng ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑈 ) → ( { 𝐴 } × { 𝐶 } ) = { ⟨ 𝐴 , 𝐶 ⟩ } )
4 3 ad2ant2r ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝐶 ∈ 𝑈 ∧ 𝐷 ∈ 𝑇 ) ) → ( { 𝐴 } × { 𝐶 } ) = { ⟨ 𝐴 , 𝐶 ⟩ } )
5 2 4 uneq12d ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝐶 ∈ 𝑈 ∧ 𝐷 ∈ 𝑇 ) ) → ( ( { 𝐴 } × { 𝐵 } ) ∪ ( { 𝐴 } × { 𝐶 } ) ) = ( { ⟨ 𝐴 , 𝐵 ⟩ } ∪ { ⟨ 𝐴 , 𝐶 ⟩ } ) )
6 xpsng ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐷 ∈ 𝑇 ) → ( { 𝐴 } × { 𝐷 } ) = { ⟨ 𝐴 , 𝐷 ⟩ } )
7 6 ad2ant2rl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝐶 ∈ 𝑈 ∧ 𝐷 ∈ 𝑇 ) ) → ( { 𝐴 } × { 𝐷 } ) = { ⟨ 𝐴 , 𝐷 ⟩ } )
8 5 7 uneq12d ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝐶 ∈ 𝑈 ∧ 𝐷 ∈ 𝑇 ) ) → ( ( ( { 𝐴 } × { 𝐵 } ) ∪ ( { 𝐴 } × { 𝐶 } ) ) ∪ ( { 𝐴 } × { 𝐷 } ) ) = ( ( { ⟨ 𝐴 , 𝐵 ⟩ } ∪ { ⟨ 𝐴 , 𝐶 ⟩ } ) ∪ { ⟨ 𝐴 , 𝐷 ⟩ } ) )
9 df-tp ⊢ { 𝐵 , 𝐶 , 𝐷 } = ( { 𝐵 , 𝐶 } ∪ { 𝐷 } )
10 9 xpeq2i ⊢ ( { 𝐴 } × { 𝐵 , 𝐶 , 𝐷 } ) = ( { 𝐴 } × ( { 𝐵 , 𝐶 } ∪ { 𝐷 } ) )
11 xpundi ⊢ ( { 𝐴 } × ( { 𝐵 , 𝐶 } ∪ { 𝐷 } ) ) = ( ( { 𝐴 } × { 𝐵 , 𝐶 } ) ∪ ( { 𝐴 } × { 𝐷 } ) )
12 df-pr ⊢ { 𝐵 , 𝐶 } = ( { 𝐵 } ∪ { 𝐶 } )
13 12 xpeq2i ⊢ ( { 𝐴 } × { 𝐵 , 𝐶 } ) = ( { 𝐴 } × ( { 𝐵 } ∪ { 𝐶 } ) )
14 xpundi ⊢ ( { 𝐴 } × ( { 𝐵 } ∪ { 𝐶 } ) ) = ( ( { 𝐴 } × { 𝐵 } ) ∪ ( { 𝐴 } × { 𝐶 } ) )
15 13 14 eqtri ⊢ ( { 𝐴 } × { 𝐵 , 𝐶 } ) = ( ( { 𝐴 } × { 𝐵 } ) ∪ ( { 𝐴 } × { 𝐶 } ) )
16 15 uneq1i ⊢ ( ( { 𝐴 } × { 𝐵 , 𝐶 } ) ∪ ( { 𝐴 } × { 𝐷 } ) ) = ( ( ( { 𝐴 } × { 𝐵 } ) ∪ ( { 𝐴 } × { 𝐶 } ) ) ∪ ( { 𝐴 } × { 𝐷 } ) )
17 11 16 eqtri ⊢ ( { 𝐴 } × ( { 𝐵 , 𝐶 } ∪ { 𝐷 } ) ) = ( ( ( { 𝐴 } × { 𝐵 } ) ∪ ( { 𝐴 } × { 𝐶 } ) ) ∪ ( { 𝐴 } × { 𝐷 } ) )
18 10 17 eqtri ⊢ ( { 𝐴 } × { 𝐵 , 𝐶 , 𝐷 } ) = ( ( ( { 𝐴 } × { 𝐵 } ) ∪ ( { 𝐴 } × { 𝐶 } ) ) ∪ ( { 𝐴 } × { 𝐷 } ) )
19 df-tp ⊢ { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐴 , 𝐷 ⟩ } = ( { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐴 , 𝐶 ⟩ } ∪ { ⟨ 𝐴 , 𝐷 ⟩ } )
20 df-pr ⊢ { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐴 , 𝐶 ⟩ } = ( { ⟨ 𝐴 , 𝐵 ⟩ } ∪ { ⟨ 𝐴 , 𝐶 ⟩ } )
21 20 uneq1i ⊢ ( { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐴 , 𝐶 ⟩ } ∪ { ⟨ 𝐴 , 𝐷 ⟩ } ) = ( ( { ⟨ 𝐴 , 𝐵 ⟩ } ∪ { ⟨ 𝐴 , 𝐶 ⟩ } ) ∪ { ⟨ 𝐴 , 𝐷 ⟩ } )
22 19 21 eqtri ⊢ { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐴 , 𝐷 ⟩ } = ( ( { ⟨ 𝐴 , 𝐵 ⟩ } ∪ { ⟨ 𝐴 , 𝐶 ⟩ } ) ∪ { ⟨ 𝐴 , 𝐷 ⟩ } )
23 8 18 22 3eqtr4g ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝐶 ∈ 𝑈 ∧ 𝐷 ∈ 𝑇 ) ) → ( { 𝐴 } × { 𝐵 , 𝐶 , 𝐷 } ) = { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐴 , 𝐷 ⟩ } )