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 >. |
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 >. |