Theorem strle3

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

	Ref	Expression
Hypotheses	strle1.i	$$⊢I\in \mathbb{N}$$
	strle1.a	$$⊢A=I$$
	strle2.j	$$⊢I<J$$
	strle2.k	$$⊢J\in \mathbb{N}$$
	strle2.b	$$⊢B=J$$
	strle3.k	$$⊢J<K$$
	strle3.l	$$⊢K\in \mathbb{N}$$
	strle3.c	$$⊢C=K$$
Assertion	strle3	$$⊢\left\{⟨A,X⟩,⟨B,Y⟩,⟨C,Z⟩\right\}\mathrm{Struct}⟨I,K⟩$$

Proof

Step	Hyp	Ref	Expression
1		strle1.i	$$⊢I\in \mathbb{N}$$
2		strle1.a	$$⊢A=I$$
3		strle2.j	$$⊢I<J$$
4		strle2.k	$$⊢J\in \mathbb{N}$$
5		strle2.b	$$⊢B=J$$
6		strle3.k	$$⊢J<K$$
7		strle3.l	$$⊢K\in \mathbb{N}$$
8		strle3.c	$$⊢C=K$$
9		df-tp	$$⊢\left\{⟨A,X⟩,⟨B,Y⟩,⟨C,Z⟩\right\}=\left\{⟨A,X⟩,⟨B,Y⟩\right\}\cup \left\{⟨C,Z⟩\right\}$$
10	1 2 3 4 5	strle2	$$⊢\left\{⟨A,X⟩,⟨B,Y⟩\right\}\mathrm{Struct}⟨I,J⟩$$
11	7 8	strle1	$$⊢\left\{⟨C,Z⟩\right\}\mathrm{Struct}⟨K,K⟩$$
12	10 11 6	strleun	$$⊢\left(\left\{⟨A,X⟩,⟨B,Y⟩\right\}\cup \left\{⟨C,Z⟩\right\}\right)\mathrm{Struct}⟨I,K⟩$$
13	9 12	eqbrtri	$$⊢\left\{⟨A,X⟩,⟨B,Y⟩,⟨C,Z⟩\right\}\mathrm{Struct}⟨I,K⟩$$