Theorem strle2

Description: Make a structure from a pair. (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$$
Assertion	strle2	$$⊢\left\{⟨A,X⟩,⟨B,Y⟩\right\}\mathrm{Struct}⟨I,J⟩$$

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		df-pr	$$⊢\left\{⟨A,X⟩,⟨B,Y⟩\right\}=\left\{⟨A,X⟩\right\}\cup \left\{⟨B,Y⟩\right\}$$
7	1 2	strle1	$$⊢\left\{⟨A,X⟩\right\}\mathrm{Struct}⟨I,I⟩$$
8	4 5	strle1	$$⊢\left\{⟨B,Y⟩\right\}\mathrm{Struct}⟨J,J⟩$$
9	7 8 3	strleun	$$⊢\left(\left\{⟨A,X⟩\right\}\cup \left\{⟨B,Y⟩\right\}\right)\mathrm{Struct}⟨I,J⟩$$
10	6 9	eqbrtri	$$⊢\left\{⟨A,X⟩,⟨B,Y⟩\right\}\mathrm{Struct}⟨I,J⟩$$