This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem strle2

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

Ref Expression
Hypotheses strle1.i ⊢ I ∈ ℕ
strle1.a ⊢ A = I
strle2.j ⊢ I < J
strle2.k ⊢ J ∈ ℕ
strle2.b ⊢ B = J
Assertion strle2 ⊢ A X B Y Struct I J

Proof

Step Hyp Ref Expression
1 strle1.i ⊢ I ∈ ℕ
2 strle1.a ⊢ A = I
3 strle2.j ⊢ I < J
4 strle2.k ⊢ J ∈ ℕ
5 strle2.b ⊢ B = J
6 df-pr ⊢ A X B Y = A X ∪ 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 ∪ B Y Struct I J
10 6 9 eqbrtri ⊢ A X B Y Struct I J