Proof of Theorem strleun
Step | Hyp | Ref
| Expression |
1 | | strleun.f |
. . . . . 6
⊢ 𝐹 Struct 〈𝐴, 𝐵〉 |
2 | | isstruct 16851 |
. . . . . 6
⊢ (𝐹 Struct 〈𝐴, 𝐵〉 ↔ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐴 ≤ 𝐵) ∧ Fun (𝐹 ∖ {∅}) ∧ dom 𝐹 ⊆ (𝐴...𝐵))) |
3 | 1, 2 | mpbi 229 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐴 ≤ 𝐵) ∧ Fun (𝐹 ∖ {∅}) ∧ dom 𝐹 ⊆ (𝐴...𝐵)) |
4 | 3 | simp1i 1138 |
. . . 4
⊢ (𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐴 ≤ 𝐵) |
5 | 4 | simp1i 1138 |
. . 3
⊢ 𝐴 ∈ ℕ |
6 | | strleun.g |
. . . . . 6
⊢ 𝐺 Struct 〈𝐶, 𝐷〉 |
7 | | isstruct 16851 |
. . . . . 6
⊢ (𝐺 Struct 〈𝐶, 𝐷〉 ↔ ((𝐶 ∈ ℕ ∧ 𝐷 ∈ ℕ ∧ 𝐶 ≤ 𝐷) ∧ Fun (𝐺 ∖ {∅}) ∧ dom 𝐺 ⊆ (𝐶...𝐷))) |
8 | 6, 7 | mpbi 229 |
. . . . 5
⊢ ((𝐶 ∈ ℕ ∧ 𝐷 ∈ ℕ ∧ 𝐶 ≤ 𝐷) ∧ Fun (𝐺 ∖ {∅}) ∧ dom 𝐺 ⊆ (𝐶...𝐷)) |
9 | 8 | simp1i 1138 |
. . . 4
⊢ (𝐶 ∈ ℕ ∧ 𝐷 ∈ ℕ ∧ 𝐶 ≤ 𝐷) |
10 | 9 | simp2i 1139 |
. . 3
⊢ 𝐷 ∈ ℕ |
11 | 4 | simp3i 1140 |
. . . . 5
⊢ 𝐴 ≤ 𝐵 |
12 | 4 | simp2i 1139 |
. . . . . . 7
⊢ 𝐵 ∈ ℕ |
13 | 12 | nnrei 11980 |
. . . . . 6
⊢ 𝐵 ∈ ℝ |
14 | 9 | simp1i 1138 |
. . . . . . 7
⊢ 𝐶 ∈ ℕ |
15 | 14 | nnrei 11980 |
. . . . . 6
⊢ 𝐶 ∈ ℝ |
16 | | strleun.l |
. . . . . 6
⊢ 𝐵 < 𝐶 |
17 | 13, 15, 16 | ltleii 11096 |
. . . . 5
⊢ 𝐵 ≤ 𝐶 |
18 | 5 | nnrei 11980 |
. . . . . 6
⊢ 𝐴 ∈ ℝ |
19 | 18, 13, 15 | letri 11102 |
. . . . 5
⊢ ((𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 ≤ 𝐶) |
20 | 11, 17, 19 | mp2an 689 |
. . . 4
⊢ 𝐴 ≤ 𝐶 |
21 | 9 | simp3i 1140 |
. . . 4
⊢ 𝐶 ≤ 𝐷 |
22 | 10 | nnrei 11980 |
. . . . 5
⊢ 𝐷 ∈ ℝ |
23 | 18, 15, 22 | letri 11102 |
. . . 4
⊢ ((𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐷) → 𝐴 ≤ 𝐷) |
24 | 20, 21, 23 | mp2an 689 |
. . 3
⊢ 𝐴 ≤ 𝐷 |
25 | 5, 10, 24 | 3pm3.2i 1338 |
. 2
⊢ (𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ∧ 𝐴 ≤ 𝐷) |
26 | 3 | simp2i 1139 |
. . . . 5
⊢ Fun
(𝐹 ∖
{∅}) |
27 | 8 | simp2i 1139 |
. . . . 5
⊢ Fun
(𝐺 ∖
{∅}) |
28 | 26, 27 | pm3.2i 471 |
. . . 4
⊢ (Fun
(𝐹 ∖ {∅}) ∧
Fun (𝐺 ∖
{∅})) |
29 | | difss 4067 |
. . . . . . . 8
⊢ (𝐹 ∖ {∅}) ⊆
𝐹 |
30 | | dmss 5813 |
. . . . . . . 8
⊢ ((𝐹 ∖ {∅}) ⊆
𝐹 → dom (𝐹 ∖ {∅}) ⊆ dom
𝐹) |
31 | 29, 30 | ax-mp 5 |
. . . . . . 7
⊢ dom
(𝐹 ∖ {∅})
⊆ dom 𝐹 |
32 | 3 | simp3i 1140 |
. . . . . . 7
⊢ dom 𝐹 ⊆ (𝐴...𝐵) |
33 | 31, 32 | sstri 3931 |
. . . . . 6
⊢ dom
(𝐹 ∖ {∅})
⊆ (𝐴...𝐵) |
34 | | difss 4067 |
. . . . . . . 8
⊢ (𝐺 ∖ {∅}) ⊆
𝐺 |
35 | | dmss 5813 |
. . . . . . . 8
⊢ ((𝐺 ∖ {∅}) ⊆
𝐺 → dom (𝐺 ∖ {∅}) ⊆ dom
𝐺) |
36 | 34, 35 | ax-mp 5 |
. . . . . . 7
⊢ dom
(𝐺 ∖ {∅})
⊆ dom 𝐺 |
37 | 8 | simp3i 1140 |
. . . . . . 7
⊢ dom 𝐺 ⊆ (𝐶...𝐷) |
38 | 36, 37 | sstri 3931 |
. . . . . 6
⊢ dom
(𝐺 ∖ {∅})
⊆ (𝐶...𝐷) |
39 | | ss2in 4172 |
. . . . . 6
⊢ ((dom
(𝐹 ∖ {∅})
⊆ (𝐴...𝐵) ∧ dom (𝐺 ∖ {∅}) ⊆ (𝐶...𝐷)) → (dom (𝐹 ∖ {∅}) ∩ dom (𝐺 ∖ {∅})) ⊆
((𝐴...𝐵) ∩ (𝐶...𝐷))) |
40 | 33, 38, 39 | mp2an 689 |
. . . . 5
⊢ (dom
(𝐹 ∖ {∅}) ∩
dom (𝐺 ∖ {∅}))
⊆ ((𝐴...𝐵) ∩ (𝐶...𝐷)) |
41 | | fzdisj 13281 |
. . . . . 6
⊢ (𝐵 < 𝐶 → ((𝐴...𝐵) ∩ (𝐶...𝐷)) = ∅) |
42 | 16, 41 | ax-mp 5 |
. . . . 5
⊢ ((𝐴...𝐵) ∩ (𝐶...𝐷)) = ∅ |
43 | | sseq0 4335 |
. . . . 5
⊢ (((dom
(𝐹 ∖ {∅}) ∩
dom (𝐺 ∖ {∅}))
⊆ ((𝐴...𝐵) ∩ (𝐶...𝐷)) ∧ ((𝐴...𝐵) ∩ (𝐶...𝐷)) = ∅) → (dom (𝐹 ∖ {∅}) ∩ dom (𝐺 ∖ {∅})) =
∅) |
44 | 40, 42, 43 | mp2an 689 |
. . . 4
⊢ (dom
(𝐹 ∖ {∅}) ∩
dom (𝐺 ∖ {∅}))
= ∅ |
45 | | funun 6482 |
. . . 4
⊢ (((Fun
(𝐹 ∖ {∅}) ∧
Fun (𝐺 ∖ {∅}))
∧ (dom (𝐹 ∖
{∅}) ∩ dom (𝐺
∖ {∅})) = ∅) → Fun ((𝐹 ∖ {∅}) ∪ (𝐺 ∖ {∅}))) |
46 | 28, 44, 45 | mp2an 689 |
. . 3
⊢ Fun
((𝐹 ∖ {∅})
∪ (𝐺 ∖
{∅})) |
47 | | difundir 4216 |
. . . 4
⊢ ((𝐹 ∪ 𝐺) ∖ {∅}) = ((𝐹 ∖ {∅}) ∪ (𝐺 ∖ {∅})) |
48 | 47 | funeqi 6457 |
. . 3
⊢ (Fun
((𝐹 ∪ 𝐺) ∖ {∅}) ↔ Fun ((𝐹 ∖ {∅}) ∪ (𝐺 ∖
{∅}))) |
49 | 46, 48 | mpbir 230 |
. 2
⊢ Fun
((𝐹 ∪ 𝐺) ∖ {∅}) |
50 | | dmun 5821 |
. . 3
⊢ dom
(𝐹 ∪ 𝐺) = (dom 𝐹 ∪ dom 𝐺) |
51 | 12 | nnzi 12342 |
. . . . . . 7
⊢ 𝐵 ∈ ℤ |
52 | 10 | nnzi 12342 |
. . . . . . 7
⊢ 𝐷 ∈ ℤ |
53 | 13, 15, 22 | letri 11102 |
. . . . . . . 8
⊢ ((𝐵 ≤ 𝐶 ∧ 𝐶 ≤ 𝐷) → 𝐵 ≤ 𝐷) |
54 | 17, 21, 53 | mp2an 689 |
. . . . . . 7
⊢ 𝐵 ≤ 𝐷 |
55 | | eluz2 12586 |
. . . . . . 7
⊢ (𝐷 ∈
(ℤ≥‘𝐵) ↔ (𝐵 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐵 ≤ 𝐷)) |
56 | 51, 52, 54, 55 | mpbir3an 1340 |
. . . . . 6
⊢ 𝐷 ∈
(ℤ≥‘𝐵) |
57 | | fzss2 13294 |
. . . . . 6
⊢ (𝐷 ∈
(ℤ≥‘𝐵) → (𝐴...𝐵) ⊆ (𝐴...𝐷)) |
58 | 56, 57 | ax-mp 5 |
. . . . 5
⊢ (𝐴...𝐵) ⊆ (𝐴...𝐷) |
59 | 32, 58 | sstri 3931 |
. . . 4
⊢ dom 𝐹 ⊆ (𝐴...𝐷) |
60 | 5 | nnzi 12342 |
. . . . . . 7
⊢ 𝐴 ∈ ℤ |
61 | 14 | nnzi 12342 |
. . . . . . 7
⊢ 𝐶 ∈ ℤ |
62 | | eluz2 12586 |
. . . . . . 7
⊢ (𝐶 ∈
(ℤ≥‘𝐴) ↔ (𝐴 ∈ ℤ ∧ 𝐶 ∈ ℤ ∧ 𝐴 ≤ 𝐶)) |
63 | 60, 61, 20, 62 | mpbir3an 1340 |
. . . . . 6
⊢ 𝐶 ∈
(ℤ≥‘𝐴) |
64 | | fzss1 13293 |
. . . . . 6
⊢ (𝐶 ∈
(ℤ≥‘𝐴) → (𝐶...𝐷) ⊆ (𝐴...𝐷)) |
65 | 63, 64 | ax-mp 5 |
. . . . 5
⊢ (𝐶...𝐷) ⊆ (𝐴...𝐷) |
66 | 37, 65 | sstri 3931 |
. . . 4
⊢ dom 𝐺 ⊆ (𝐴...𝐷) |
67 | 59, 66 | unssi 4120 |
. . 3
⊢ (dom
𝐹 ∪ dom 𝐺) ⊆ (𝐴...𝐷) |
68 | 50, 67 | eqsstri 3956 |
. 2
⊢ dom
(𝐹 ∪ 𝐺) ⊆ (𝐴...𝐷) |
69 | | isstruct 16851 |
. 2
⊢ ((𝐹 ∪ 𝐺) Struct 〈𝐴, 𝐷〉 ↔ ((𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ∧ 𝐴 ≤ 𝐷) ∧ Fun ((𝐹 ∪ 𝐺) ∖ {∅}) ∧ dom (𝐹 ∪ 𝐺) ⊆ (𝐴...𝐷))) |
70 | 25, 49, 68, 69 | mpbir3an 1340 |
1
⊢ (𝐹 ∪ 𝐺) Struct 〈𝐴, 𝐷〉 |