Theorem xpsntpg

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

	Ref	Expression
Assertion	xpsntpg	|- ( ( ( A e. V /\ B e. W ) /\ ( C e. U /\ D e. T ) ) -> ( { A } X. { B , C , D } ) = { <. A , B >. , <. A , C >. , <. A , D >. } )

Proof

Step	Hyp	Ref	Expression
1		xpsng	|- ( ( A e. V /\ B e. W ) -> ( { A } X. { B } ) = { <. A , B >. } )
2	1	adantr	|- ( ( ( A e. V /\ B e. W ) /\ ( C e. U /\ D e. T ) ) -> ( { A } X. { B } ) = { <. A , B >. } )
3		xpsng	|- ( ( A e. V /\ C e. U ) -> ( { A } X. { C } ) = { <. A , C >. } )
4	3	ad2ant2r	|- ( ( ( A e. V /\ B e. W ) /\ ( C e. U /\ D e. T ) ) -> ( { A } X. { C } ) = { <. A , C >. } )
5	2 4	uneq12d	|- ( ( ( A e. V /\ B e. W ) /\ ( C e. U /\ D e. T ) ) -> ( ( { A } X. { B } ) u. ( { A } X. { C } ) ) = ( { <. A , B >. } u. { <. A , C >. } ) )
6		xpsng	|- ( ( A e. V /\ D e. T ) -> ( { A } X. { D } ) = { <. A , D >. } )
7	6	ad2ant2rl	|- ( ( ( A e. V /\ B e. W ) /\ ( C e. U /\ D e. T ) ) -> ( { A } X. { D } ) = { <. A , D >. } )
8	5 7	uneq12d	|- ( ( ( A e. V /\ B e. W ) /\ ( C e. U /\ D e. T ) ) -> ( ( ( { A } X. { B } ) u. ( { A } X. { C } ) ) u. ( { A } X. { D } ) ) = ( ( { <. A , B >. } u. { <. A , C >. } ) u. { <. A , D >. } ) )
9		df-tp	|- { B , C , D } = ( { B , C } u. { D } )
10	9	xpeq2i	|- ( { A } X. { B , C , D } ) = ( { A } X. ( { B , C } u. { D } ) )
11		xpundi	|- ( { A } X. ( { B , C } u. { D } ) ) = ( ( { A } X. { B , C } ) u. ( { A } X. { D } ) )
12		df-pr	|- { B , C } = ( { B } u. { C } )
13	12	xpeq2i	|- ( { A } X. { B , C } ) = ( { A } X. ( { B } u. { C } ) )
14		xpundi	|- ( { A } X. ( { B } u. { C } ) ) = ( ( { A } X. { B } ) u. ( { A } X. { C } ) )
15	13 14	eqtri	|- ( { A } X. { B , C } ) = ( ( { A } X. { B } ) u. ( { A } X. { C } ) )
16	15	uneq1i	|- ( ( { A } X. { B , C } ) u. ( { A } X. { D } ) ) = ( ( ( { A } X. { B } ) u. ( { A } X. { C } ) ) u. ( { A } X. { D } ) )
17	11 16	eqtri	|- ( { A } X. ( { B , C } u. { D } ) ) = ( ( ( { A } X. { B } ) u. ( { A } X. { C } ) ) u. ( { A } X. { D } ) )
18	10 17	eqtri	|- ( { A } X. { B , C , D } ) = ( ( ( { A } X. { B } ) u. ( { A } X. { C } ) ) u. ( { A } X. { D } ) )
19		df-tp	|- { <. A , B >. , <. A , C >. , <. A , D >. } = ( { <. A , B >. , <. A , C >. } u. { <. A , D >. } )
20		df-pr	|- { <. A , B >. , <. A , C >. } = ( { <. A , B >. } u. { <. A , C >. } )
21	20	uneq1i	|- ( { <. A , B >. , <. A , C >. } u. { <. A , D >. } ) = ( ( { <. A , B >. } u. { <. A , C >. } ) u. { <. A , D >. } )
22	19 21	eqtri	|- { <. A , B >. , <. A , C >. , <. A , D >. } = ( ( { <. A , B >. } u. { <. A , C >. } ) u. { <. A , D >. } )
23	8 18 22	3eqtr4g	|- ( ( ( A e. V /\ B e. W ) /\ ( C e. U /\ D e. T ) ) -> ( { A } X. { B , C , D } ) = { <. A , B >. , <. A , C >. , <. A , D >. } )