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 e. NN
strle1.a
|- A = I
strle2.j
|- I < J
strle2.k
|- J e. NN
strle2.b
|- B = J
Assertion strle2
|- { <. A , X >. , <. B , Y >. } Struct <. I , J >.

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 df-pr
 |-  { <. A , X >. , <. B , Y >. } = ( { <. A , X >. } u. { <. 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 >. } u. { <. B , Y >. } ) Struct <. I , J >.
10 6 9 eqbrtri
 |-  { <. A , X >. , <. B , Y >. } Struct <. I , J >.