strle3

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

Step	Hyp	Ref	Expression
1		strle1.i	$⊢ I \in ℕ$
2		strle1.a	$⊢ A = I$
3		strle2.j	$⊢ I < J$
4		strle2.k	$⊢ J \in ℕ$
5		strle2.b	$⊢ B = J$
6		strle3.k	$⊢ J < K$
7		strle3.l	$⊢ K \in ℕ$
8		strle3.c	$⊢ C = K$
9		df-tp	$⊢ \{⟨A, X⟩, ⟨B, Y⟩, ⟨C, Z⟩\} = \{⟨A, X⟩, ⟨B, Y⟩\} \cup \{⟨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⟩\} \cup \{⟨C, Z⟩\}) Struct ⟨I, K⟩$
13	9 12	eqbrtri	$⊢ \{⟨A, X⟩, ⟨B, Y⟩, ⟨C, Z⟩\} Struct ⟨I, K⟩$

Metamath Proof Explorer