Metamath Proof Explorer

Theorem strleun

Description: Combine two structures into one. (Contributed by Mario Carneiro, 29-Aug-2015)

Ref Expression
Hypotheses strleun.f 
|- F Struct <. A , B >.
strleun.g 
|- G Struct <. C , D >.
strleun.l 
|- B < C
Assertion strleun 
|- ( F u. G ) Struct <. A , D >.

Proof

Step Hyp Ref Expression
1 strleun.f 
 |-  F Struct <. A , B >.
2 strleun.g 
 |-  G Struct <. C , D >.
3 strleun.l 
 |-  B < C
4 isstruct 
 |-  ( F Struct <. A , B >. <-> ( ( A e. NN /\ B e. NN /\ A <_ B ) /\ Fun ( F \ { (/) } ) /\ dom F C_ ( A ... B ) ) )
5 1 4 mpbi 
 |-  ( ( A e. NN /\ B e. NN /\ A <_ B ) /\ Fun ( F \ { (/) } ) /\ dom F C_ ( A ... B ) )
6 5 simp1i 
 |-  ( A e. NN /\ B e. NN /\ A <_ B )
7 6 simp1i 
 |-  A e. NN
8 isstruct 
 |-  ( G Struct <. C , D >. <-> ( ( C e. NN /\ D e. NN /\ C <_ D ) /\ Fun ( G \ { (/) } ) /\ dom G C_ ( C ... D ) ) )
9 2 8 mpbi 
 |-  ( ( C e. NN /\ D e. NN /\ C <_ D ) /\ Fun ( G \ { (/) } ) /\ dom G C_ ( C ... D ) )
10 9 simp1i 
 |-  ( C e. NN /\ D e. NN /\ C <_ D )
11 10 simp2i 
 |-  D e. NN
12 6 simp3i 
 |-  A <_ B
13 6 simp2i 
 |-  B e. NN
14 13 nnrei 
 |-  B e. RR
15 10 simp1i 
 |-  C e. NN
16 15 nnrei 
 |-  C e. RR
17 14 16 3 ltleii 
 |-  B <_ C
18 7 nnrei 
 |-  A e. RR
19 18 14 16 letri 
 |-  ( ( A <_ B /\ B <_ C ) -> A <_ C )
20 12 17 19 mp2an 
 |-  A <_ C
21 10 simp3i 
 |-  C <_ D
22 11 nnrei 
 |-  D e. RR
23 18 16 22 letri 
 |-  ( ( A <_ C /\ C <_ D ) -> A <_ D )
24 20 21 23 mp2an 
 |-  A <_ D
25 7 11 24 3pm3.2i 
 |-  ( A e. NN /\ D e. NN /\ A <_ D )
26 5 simp2i 
 |-  Fun ( F \ { (/) } )
27 9 simp2i 
 |-  Fun ( G \ { (/) } )
28 26 27 pm3.2i 
 |-  ( Fun ( F \ { (/) } ) /\ Fun ( G \ { (/) } ) )
29 difss 
 |-  ( F \ { (/) } ) C_ F
30 dmss 
 |-  ( ( F \ { (/) } ) C_ F -> dom ( F \ { (/) } ) C_ dom F )
31 29 30 ax-mp 
 |-  dom ( F \ { (/) } ) C_ dom F
32 5 simp3i 
 |-  dom F C_ ( A ... B )
33 31 32 sstri 
 |-  dom ( F \ { (/) } ) C_ ( A ... B )
34 difss 
 |-  ( G \ { (/) } ) C_ G
35 dmss 
 |-  ( ( G \ { (/) } ) C_ G -> dom ( G \ { (/) } ) C_ dom G )
36 34 35 ax-mp 
 |-  dom ( G \ { (/) } ) C_ dom G
37 9 simp3i 
 |-  dom G C_ ( C ... D )
38 36 37 sstri 
 |-  dom ( G \ { (/) } ) C_ ( C ... D )
39 ss2in 
 |-  ( ( dom ( F \ { (/) } ) C_ ( A ... B ) /\ dom ( G \ { (/) } ) C_ ( C ... D ) ) -> ( dom ( F \ { (/) } ) i^i dom ( G \ { (/) } ) ) C_ ( ( A ... B ) i^i ( C ... D ) ) )
40 33 38 39 mp2an 
 |-  ( dom ( F \ { (/) } ) i^i dom ( G \ { (/) } ) ) C_ ( ( A ... B ) i^i ( C ... D ) )
41 fzdisj 
 |-  ( B < C -> ( ( A ... B ) i^i ( C ... D ) ) = (/) )
42 3 41 ax-mp 
 |-  ( ( A ... B ) i^i ( C ... D ) ) = (/)
43 sseq0 
 |-  ( ( ( dom ( F \ { (/) } ) i^i dom ( G \ { (/) } ) ) C_ ( ( A ... B ) i^i ( C ... D ) ) /\ ( ( A ... B ) i^i ( C ... D ) ) = (/) ) -> ( dom ( F \ { (/) } ) i^i dom ( G \ { (/) } ) ) = (/) )
44 40 42 43 mp2an 
 |-  ( dom ( F \ { (/) } ) i^i dom ( G \ { (/) } ) ) = (/)
45 funun 
 |-  ( ( ( Fun ( F \ { (/) } ) /\ Fun ( G \ { (/) } ) ) /\ ( dom ( F \ { (/) } ) i^i dom ( G \ { (/) } ) ) = (/) ) -> Fun ( ( F \ { (/) } ) u. ( G \ { (/) } ) ) )
46 28 44 45 mp2an 
 |-  Fun ( ( F \ { (/) } ) u. ( G \ { (/) } ) )
47 difundir 
 |-  ( ( F u. G ) \ { (/) } ) = ( ( F \ { (/) } ) u. ( G \ { (/) } ) )
48 47 funeqi 
 |-  ( Fun ( ( F u. G ) \ { (/) } ) <-> Fun ( ( F \ { (/) } ) u. ( G \ { (/) } ) ) )
49 46 48 mpbir 
 |-  Fun ( ( F u. G ) \ { (/) } )
50 dmun 
 |-  dom ( F u. G ) = ( dom F u. dom G )
51 13 nnzi 
 |-  B e. ZZ
52 11 nnzi 
 |-  D e. ZZ
53 14 16 22 letri 
 |-  ( ( B <_ C /\ C <_ D ) -> B <_ D )
54 17 21 53 mp2an 
 |-  B <_ D
55 eluz2 
 |-  ( D e. ( ZZ>= ` B ) <-> ( B e. ZZ /\ D e. ZZ /\ B <_ D ) )
56 51 52 54 55 mpbir3an 
 |-  D e. ( ZZ>= ` B )
57 fzss2 
 |-  ( D e. ( ZZ>= ` B ) -> ( A ... B ) C_ ( A ... D ) )
58 56 57 ax-mp 
 |-  ( A ... B ) C_ ( A ... D )
59 32 58 sstri 
 |-  dom F C_ ( A ... D )
60 7 nnzi 
 |-  A e. ZZ
61 15 nnzi 
 |-  C e. ZZ
62 eluz2 
 |-  ( C e. ( ZZ>= ` A ) <-> ( A e. ZZ /\ C e. ZZ /\ A <_ C ) )
63 60 61 20 62 mpbir3an 
 |-  C e. ( ZZ>= ` A )
64 fzss1 
 |-  ( C e. ( ZZ>= ` A ) -> ( C ... D ) C_ ( A ... D ) )
65 63 64 ax-mp 
 |-  ( C ... D ) C_ ( A ... D )
66 37 65 sstri 
 |-  dom G C_ ( A ... D )
67 59 66 unssi 
 |-  ( dom F u. dom G ) C_ ( A ... D )
68 50 67 eqsstri 
 |-  dom ( F u. G ) C_ ( A ... D )
69 isstruct 
 |-  ( ( F u. G ) Struct <. A , D >. <-> ( ( A e. NN /\ D e. NN /\ A <_ D ) /\ Fun ( ( F u. G ) \ { (/) } ) /\ dom ( F u. G ) C_ ( A ... D ) ) )
70 25 49 68 69 mpbir3an 
 |-  ( F u. G ) Struct <. A , D >.