Theorem xpsntpg

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

	Ref	Expression
Assertion	xpsntpg	$$⊢\left(\left(A\in V\wedge B\in W\right)\wedge \left(C\in U\wedge D\in T\right)\right)\to \left\{A\right\}\times \left\{B,C,D\right\}=\left\{⟨A,B⟩,⟨A,C⟩,⟨A,D⟩\right\}$$

Proof

Step	Hyp	Ref	Expression
1		xpsng	$$⊢\left(A\in V\wedge B\in W\right)\to \left\{A\right\}\times \left\{B\right\}=\left\{⟨A,B⟩\right\}$$
2	1	adantr	$$⊢\left(\left(A\in V\wedge B\in W\right)\wedge \left(C\in U\wedge D\in T\right)\right)\to \left\{A\right\}\times \left\{B\right\}=\left\{⟨A,B⟩\right\}$$
3		xpsng	$$⊢\left(A\in V\wedge C\in U\right)\to \left\{A\right\}\times \left\{C\right\}=\left\{⟨A,C⟩\right\}$$
4	3	ad2ant2r	$$⊢\left(\left(A\in V\wedge B\in W\right)\wedge \left(C\in U\wedge D\in T\right)\right)\to \left\{A\right\}\times \left\{C\right\}=\left\{⟨A,C⟩\right\}$$
5	2 4	uneq12d	$$⊢\left(\left(A\in V\wedge B\in W\right)\wedge \left(C\in U\wedge D\in T\right)\right)\to \left(\left\{A\right\}\times \left\{B\right\}\right)\cup \left(\left\{A\right\}\times \left\{C\right\}\right)=\left\{⟨A,B⟩\right\}\cup \left\{⟨A,C⟩\right\}$$
6		xpsng	$$⊢\left(A\in V\wedge D\in T\right)\to \left\{A\right\}\times \left\{D\right\}=\left\{⟨A,D⟩\right\}$$
7	6	ad2ant2rl	$$⊢\left(\left(A\in V\wedge B\in W\right)\wedge \left(C\in U\wedge D\in T\right)\right)\to \left\{A\right\}\times \left\{D\right\}=\left\{⟨A,D⟩\right\}$$
8	5 7	uneq12d	$$⊢\left(\left(A\in V\wedge B\in W\right)\wedge \left(C\in U\wedge D\in T\right)\right)\to \left(\left(\left\{A\right\}\times \left\{B\right\}\right)\cup \left(\left\{A\right\}\times \left\{C\right\}\right)\right)\cup \left(\left\{A\right\}\times \left\{D\right\}\right)=\left(\left\{⟨A,B⟩\right\}\cup \left\{⟨A,C⟩\right\}\right)\cup \left\{⟨A,D⟩\right\}$$
9		df-tp	$$⊢\left\{B,C,D\right\}=\left\{B,C\right\}\cup \left\{D\right\}$$
10	9	xpeq2i	$$⊢\left\{A\right\}\times \left\{B,C,D\right\}=\left\{A\right\}\times \left(\left\{B,C\right\}\cup \left\{D\right\}\right)$$
11		xpundi	$$⊢\left\{A\right\}\times \left(\left\{B,C\right\}\cup \left\{D\right\}\right)=\left(\left\{A\right\}\times \left\{B,C\right\}\right)\cup \left(\left\{A\right\}\times \left\{D\right\}\right)$$
12		df-pr	$$⊢\left\{B,C\right\}=\left\{B\right\}\cup \left\{C\right\}$$
13	12	xpeq2i	$$⊢\left\{A\right\}\times \left\{B,C\right\}=\left\{A\right\}\times \left(\left\{B\right\}\cup \left\{C\right\}\right)$$
14		xpundi	$$⊢\left\{A\right\}\times \left(\left\{B\right\}\cup \left\{C\right\}\right)=\left(\left\{A\right\}\times \left\{B\right\}\right)\cup \left(\left\{A\right\}\times \left\{C\right\}\right)$$
15	13 14	eqtri	$$⊢\left\{A\right\}\times \left\{B,C\right\}=\left(\left\{A\right\}\times \left\{B\right\}\right)\cup \left(\left\{A\right\}\times \left\{C\right\}\right)$$
16	15	uneq1i	$$⊢\left(\left\{A\right\}\times \left\{B,C\right\}\right)\cup \left(\left\{A\right\}\times \left\{D\right\}\right)=\left(\left(\left\{A\right\}\times \left\{B\right\}\right)\cup \left(\left\{A\right\}\times \left\{C\right\}\right)\right)\cup \left(\left\{A\right\}\times \left\{D\right\}\right)$$
17	11 16	eqtri	$$⊢\left\{A\right\}\times \left(\left\{B,C\right\}\cup \left\{D\right\}\right)=\left(\left(\left\{A\right\}\times \left\{B\right\}\right)\cup \left(\left\{A\right\}\times \left\{C\right\}\right)\right)\cup \left(\left\{A\right\}\times \left\{D\right\}\right)$$
18	10 17	eqtri	$$⊢\left\{A\right\}\times \left\{B,C,D\right\}=\left(\left(\left\{A\right\}\times \left\{B\right\}\right)\cup \left(\left\{A\right\}\times \left\{C\right\}\right)\right)\cup \left(\left\{A\right\}\times \left\{D\right\}\right)$$
19		df-tp	$$⊢\left\{⟨A,B⟩,⟨A,C⟩,⟨A,D⟩\right\}=\left\{⟨A,B⟩,⟨A,C⟩\right\}\cup \left\{⟨A,D⟩\right\}$$
20		df-pr	$$⊢\left\{⟨A,B⟩,⟨A,C⟩\right\}=\left\{⟨A,B⟩\right\}\cup \left\{⟨A,C⟩\right\}$$
21	20	uneq1i	$$⊢\left\{⟨A,B⟩,⟨A,C⟩\right\}\cup \left\{⟨A,D⟩\right\}=\left(\left\{⟨A,B⟩\right\}\cup \left\{⟨A,C⟩\right\}\right)\cup \left\{⟨A,D⟩\right\}$$
22	19 21	eqtri	$$⊢\left\{⟨A,B⟩,⟨A,C⟩,⟨A,D⟩\right\}=\left(\left\{⟨A,B⟩\right\}\cup \left\{⟨A,C⟩\right\}\right)\cup \left\{⟨A,D⟩\right\}$$
23	8 18 22	3eqtr4g	$$⊢\left(\left(A\in V\wedge B\in W\right)\wedge \left(C\in U\wedge D\in T\right)\right)\to \left\{A\right\}\times \left\{B,C,D\right\}=\left\{⟨A,B⟩,⟨A,C⟩,⟨A,D⟩\right\}$$