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

Metamath Proof Explorer

Theorem strleun

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

Ref Expression
Hypotheses strleun.f ⊢ 𝐹 Struct ⟨ 𝐴 , 𝐵 ⟩
strleun.g ⊢ 𝐺 Struct ⟨ 𝐶 , 𝐷 ⟩
strleun.l ⊢ 𝐵 < 𝐶
Assertion strleun ( 𝐹 ∪ 𝐺 ) Struct ⟨ 𝐴 , 𝐷 ⟩

Proof

Step Hyp Ref Expression
1 strleun.f ⊢ 𝐹 Struct ⟨ 𝐴 , 𝐵 ⟩
2 strleun.g ⊢ 𝐺 Struct ⟨ 𝐶 , 𝐷 ⟩
3 strleun.l ⊢ 𝐵 < 𝐶
4 isstruct ⊢ ( 𝐹 Struct ⟨ 𝐴 , 𝐵 ⟩ ↔ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐴 ≤ 𝐵 ) ∧ Fun ( 𝐹 ∖ { ∅ } ) ∧ dom 𝐹 ⊆ ( 𝐴 ... 𝐵 ) ) )
5 1 4 mpbi ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐴 ≤ 𝐵 ) ∧ Fun ( 𝐹 ∖ { ∅ } ) ∧ dom 𝐹 ⊆ ( 𝐴 ... 𝐵 ) )
6 5 simp1i ⊢ ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐴 ≤ 𝐵 )
7 6 simp1i ⊢ 𝐴 ∈ ℕ
8 isstruct ⊢ ( 𝐺 Struct ⟨ 𝐶 , 𝐷 ⟩ ↔ ( ( 𝐶 ∈ ℕ ∧ 𝐷 ∈ ℕ ∧ 𝐶 ≤ 𝐷 ) ∧ Fun ( 𝐺 ∖ { ∅ } ) ∧ dom 𝐺 ⊆ ( 𝐶 ... 𝐷 ) ) )
9 2 8 mpbi ⊢ ( ( 𝐶 ∈ ℕ ∧ 𝐷 ∈ ℕ ∧ 𝐶 ≤ 𝐷 ) ∧ Fun ( 𝐺 ∖ { ∅ } ) ∧ dom 𝐺 ⊆ ( 𝐶 ... 𝐷 ) )
10 9 simp1i ⊢ ( 𝐶 ∈ ℕ ∧ 𝐷 ∈ ℕ ∧ 𝐶 ≤ 𝐷 )
11 10 simp2i ⊢ 𝐷 ∈ ℕ
12 6 simp3i ⊢ 𝐴 ≤ 𝐵
13 6 simp2i ⊢ 𝐵 ∈ ℕ
14 13 nnrei ⊢ 𝐵 ∈ ℝ
15 10 simp1i ⊢ 𝐶 ∈ ℕ
16 15 nnrei ⊢ 𝐶 ∈ ℝ
17 14 16 3 ltleii ⊢ 𝐵 ≤ 𝐶
18 7 nnrei ⊢ 𝐴 ∈ ℝ
19 18 14 16 letri ⊢ ( ( 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶 ) → 𝐴 ≤ 𝐶 )
20 12 17 19 mp2an ⊢ 𝐴 ≤ 𝐶
21 10 simp3i ⊢ 𝐶 ≤ 𝐷
22 11 nnrei ⊢ 𝐷 ∈ ℝ
23 18 16 22 letri ⊢ ( ( 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐷 ) → 𝐴 ≤ 𝐷 )
24 20 21 23 mp2an ⊢ 𝐴 ≤ 𝐷
25 7 11 24 3pm3.2i ⊢ ( 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ∧ 𝐴 ≤ 𝐷 )
26 5 simp2i ⊢ Fun ( 𝐹 ∖ { ∅ } )
27 9 simp2i ⊢ Fun ( 𝐺 ∖ { ∅ } )
28 26 27 pm3.2i ⊢ ( Fun ( 𝐹 ∖ { ∅ } ) ∧ Fun ( 𝐺 ∖ { ∅ } ) )
29 difss ⊢ ( 𝐹 ∖ { ∅ } ) ⊆ 𝐹
30 dmss ⊢ ( ( 𝐹 ∖ { ∅ } ) ⊆ 𝐹 → dom ( 𝐹 ∖ { ∅ } ) ⊆ dom 𝐹 )
31 29 30 ax-mp ⊢ dom ( 𝐹 ∖ { ∅ } ) ⊆ dom 𝐹
32 5 simp3i ⊢ dom 𝐹 ⊆ ( 𝐴 ... 𝐵 )
33 31 32 sstri ⊢ dom ( 𝐹 ∖ { ∅ } ) ⊆ ( 𝐴 ... 𝐵 )
34 difss ⊢ ( 𝐺 ∖ { ∅ } ) ⊆ 𝐺
35 dmss ⊢ ( ( 𝐺 ∖ { ∅ } ) ⊆ 𝐺 → dom ( 𝐺 ∖ { ∅ } ) ⊆ dom 𝐺 )
36 34 35 ax-mp ⊢ dom ( 𝐺 ∖ { ∅ } ) ⊆ dom 𝐺
37 9 simp3i ⊢ dom 𝐺 ⊆ ( 𝐶 ... 𝐷 )
38 36 37 sstri ⊢ dom ( 𝐺 ∖ { ∅ } ) ⊆ ( 𝐶 ... 𝐷 )
39 ss2in ⊢ ( ( dom ( 𝐹 ∖ { ∅ } ) ⊆ ( 𝐴 ... 𝐵 ) ∧ dom ( 𝐺 ∖ { ∅ } ) ⊆ ( 𝐶 ... 𝐷 ) ) → ( dom ( 𝐹 ∖ { ∅ } ) ∩ dom ( 𝐺 ∖ { ∅ } ) ) ⊆ ( ( 𝐴 ... 𝐵 ) ∩ ( 𝐶 ... 𝐷 ) ) )
40 33 38 39 mp2an ⊢ ( dom ( 𝐹 ∖ { ∅ } ) ∩ dom ( 𝐺 ∖ { ∅ } ) ) ⊆ ( ( 𝐴 ... 𝐵 ) ∩ ( 𝐶 ... 𝐷 ) )
41 fzdisj ⊢ ( 𝐵 < 𝐶 → ( ( 𝐴 ... 𝐵 ) ∩ ( 𝐶 ... 𝐷 ) ) = ∅ )
42 3 41 ax-mp ⊢ ( ( 𝐴 ... 𝐵 ) ∩ ( 𝐶 ... 𝐷 ) ) = ∅
43 sseq0 ⊢ ( ( ( dom ( 𝐹 ∖ { ∅ } ) ∩ dom ( 𝐺 ∖ { ∅ } ) ) ⊆ ( ( 𝐴 ... 𝐵 ) ∩ ( 𝐶 ... 𝐷 ) ) ∧ ( ( 𝐴 ... 𝐵 ) ∩ ( 𝐶 ... 𝐷 ) ) = ∅ ) → ( dom ( 𝐹 ∖ { ∅ } ) ∩ dom ( 𝐺 ∖ { ∅ } ) ) = ∅ )
44 40 42 43 mp2an ⊢ ( dom ( 𝐹 ∖ { ∅ } ) ∩ dom ( 𝐺 ∖ { ∅ } ) ) = ∅
45 funun ⊢ ( ( ( Fun ( 𝐹 ∖ { ∅ } ) ∧ Fun ( 𝐺 ∖ { ∅ } ) ) ∧ ( dom ( 𝐹 ∖ { ∅ } ) ∩ dom ( 𝐺 ∖ { ∅ } ) ) = ∅ ) → Fun ( ( 𝐹 ∖ { ∅ } ) ∪ ( 𝐺 ∖ { ∅ } ) ) )
46 28 44 45 mp2an ⊢ Fun ( ( 𝐹 ∖ { ∅ } ) ∪ ( 𝐺 ∖ { ∅ } ) )
47 difundir ⊢ ( ( 𝐹 ∪ 𝐺 ) ∖ { ∅ } ) = ( ( 𝐹 ∖ { ∅ } ) ∪ ( 𝐺 ∖ { ∅ } ) )
48 47 funeqi ⊢ ( Fun ( ( 𝐹 ∪ 𝐺 ) ∖ { ∅ } ) ↔ Fun ( ( 𝐹 ∖ { ∅ } ) ∪ ( 𝐺 ∖ { ∅ } ) ) )
49 46 48 mpbir ⊢ Fun ( ( 𝐹 ∪ 𝐺 ) ∖ { ∅ } )
50 dmun ⊢ dom ( 𝐹 ∪ 𝐺 ) = ( dom 𝐹 ∪ dom 𝐺 )
51 13 nnzi ⊢ 𝐵 ∈ ℤ
52 11 nnzi ⊢ 𝐷 ∈ ℤ
53 14 16 22 letri ⊢ ( ( 𝐵 ≤ 𝐶 ∧ 𝐶 ≤ 𝐷 ) → 𝐵 ≤ 𝐷 )
54 17 21 53 mp2an ⊢ 𝐵 ≤ 𝐷
55 eluz2 ⊢ ( 𝐷 ∈ ( ℤ≥ ‘ 𝐵 ) ↔ ( 𝐵 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐵 ≤ 𝐷 ) )
56 51 52 54 55 mpbir3an ⊢ 𝐷 ∈ ( ℤ≥ ‘ 𝐵 )
57 fzss2 ⊢ ( 𝐷 ∈ ( ℤ≥ ‘ 𝐵 ) → ( 𝐴 ... 𝐵 ) ⊆ ( 𝐴 ... 𝐷 ) )
58 56 57 ax-mp ⊢ ( 𝐴 ... 𝐵 ) ⊆ ( 𝐴 ... 𝐷 )
59 32 58 sstri ⊢ dom 𝐹 ⊆ ( 𝐴 ... 𝐷 )
60 7 nnzi ⊢ 𝐴 ∈ ℤ
61 15 nnzi ⊢ 𝐶 ∈ ℤ
62 eluz2 ⊢ ( 𝐶 ∈ ( ℤ≥ ‘ 𝐴 ) ↔ ( 𝐴 ∈ ℤ ∧ 𝐶 ∈ ℤ ∧ 𝐴 ≤ 𝐶 ) )
63 60 61 20 62 mpbir3an ⊢ 𝐶 ∈ ( ℤ≥ ‘ 𝐴 )
64 fzss1 ⊢ ( 𝐶 ∈ ( ℤ≥ ‘ 𝐴 ) → ( 𝐶 ... 𝐷 ) ⊆ ( 𝐴 ... 𝐷 ) )
65 63 64 ax-mp ⊢ ( 𝐶 ... 𝐷 ) ⊆ ( 𝐴 ... 𝐷 )
66 37 65 sstri ⊢ dom 𝐺 ⊆ ( 𝐴 ... 𝐷 )
67 59 66 unssi ⊢ ( dom 𝐹 ∪ dom 𝐺 ) ⊆ ( 𝐴 ... 𝐷 )
68 50 67 eqsstri ⊢ dom ( 𝐹 ∪ 𝐺 ) ⊆ ( 𝐴 ... 𝐷 )
69 isstruct ⊢ ( ( 𝐹 ∪ 𝐺 ) Struct ⟨ 𝐴 , 𝐷 ⟩ ↔ ( ( 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ∧ 𝐴 ≤ 𝐷 ) ∧ Fun ( ( 𝐹 ∪ 𝐺 ) ∖ { ∅ } ) ∧ dom ( 𝐹 ∪ 𝐺 ) ⊆ ( 𝐴 ... 𝐷 ) ) )
70 25 49 68 69 mpbir3an ⊢ ( 𝐹 ∪ 𝐺 ) Struct ⟨ 𝐴 , 𝐷 ⟩