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 ⟨ 𝐴 , 𝐷 ⟩