Theorem strle2

Description: Make a structure from a pair. (Contributed by Mario Carneiro, 29-Aug-2015)

	Ref	Expression
Hypotheses	strle1.i	|- I e. NN
	strle1.a	|- A = I
	strle2.j	|- I < J
	strle2.k	|- J e. NN
	strle2.b	|- B = J
Assertion	strle2	|- { <. A , X >. , <. B , Y >. } Struct <. I , J >.

Proof

Step	Hyp	Ref	Expression
1		strle1.i	|- I e. NN
2		strle1.a	|- A = I
3		strle2.j	|- I < J
4		strle2.k	|- J e. NN
5		strle2.b	|- B = J
6		df-pr	|- { <. A , X >. , <. B , Y >. } = ( { <. A , X >. } u. { <. B , Y >. } )
7	1 2	strle1	|- { <. A , X >. } Struct <. I , I >.
8	4 5	strle1	|- { <. B , Y >. } Struct <. J , J >.
9	7 8 3	strleun	|- ( { <. A , X >. } u. { <. B , Y >. } ) Struct <. I , J >.
10	6 9	eqbrtri	|- { <. A , X >. , <. B , Y >. } Struct <. I , J >.