Theorem strle3

Description: Make a structure from a triple. (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
	strle3.k	|- J < K
	strle3.l	|- K e. NN
	strle3.c	|- C = K
Assertion	strle3	|- { <. A , X >. , <. B , Y >. , <. C , Z >. } Struct <. I , K >.

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		strle3.k	|- J < K
7		strle3.l	|- K e. NN
8		strle3.c	|- C = K
9		df-tp	|- { <. A , X >. , <. B , Y >. , <. C , Z >. } = ( { <. A , X >. , <. B , Y >. } u. { <. C , Z >. } )
10	1 2 3 4 5	strle2	|- { <. A , X >. , <. B , Y >. } Struct <. I , J >.
11	7 8	strle1	|- { <. C , Z >. } Struct <. K , K >.
12	10 11 6	strleun	|- ( { <. A , X >. , <. B , Y >. } u. { <. C , Z >. } ) Struct <. I , K >.
13	9 12	eqbrtri	|- { <. A , X >. , <. B , Y >. , <. C , Z >. } Struct <. I , K >.