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

Metamath Proof Explorer

Theorem strle3

Description: Make a structure from a triple. (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
strle3.k 
|- J < K
strle3.l 
|- K e. NN
strle3.c 
|- C = K
Assertion strle3 
|- { <. A , X >. , <. B , Y >. , <. C , Z >. } Struct <. I , K >.

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 strle3.k 
 |-  J < K
7 strle3.l 
 |-  K e. NN
8 strle3.c 
 |-  C = K
9 df-tp 
 |-  { <. A , X >. , <. B , Y >. , <. C , Z >. } = ( { <. A , X >. , <. B , Y >. } u. { <. 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 >. } u. { <. C , Z >. } ) Struct <. I , K >.
13 9 12 eqbrtri 
 |-  { <. A , X >. , <. B , Y >. , <. C , Z >. } Struct <. I , K >.