Step | Hyp | Ref
| Expression |
1 | | opelxp 5070 |
. . . 4
⊢
(〈∅, 〈𝐹, 𝐿〉〉 ∈ (V × (ℤ
× ℤ)) ↔ (∅ ∈ V ∧ 〈𝐹, 𝐿〉 ∈ (ℤ ×
ℤ))) |
2 | | opelxp 5070 |
. . . . 5
⊢
(〈𝐹, 𝐿〉 ∈ (ℤ ×
ℤ) ↔ (𝐹 ∈
ℤ ∧ 𝐿 ∈
ℤ)) |
3 | | swrdval 13269 |
. . . . . . 7
⊢ ((∅
∈ V ∧ 𝐹 ∈
ℤ ∧ 𝐿 ∈
ℤ) → (∅ substr 〈𝐹, 𝐿〉) = if((𝐹..^𝐿) ⊆ dom ∅, (𝑥 ∈ (0..^(𝐿 − 𝐹)) ↦ (∅‘(𝑥 + 𝐹))), ∅)) |
4 | | fzonlt0 12360 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (¬
𝐹 < 𝐿 ↔ (𝐹..^𝐿) = ∅)) |
5 | 4 | biimprd 237 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) → ((𝐹..^𝐿) = ∅ → ¬ 𝐹 < 𝐿)) |
6 | 5 | con2d 128 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (𝐹 < 𝐿 → ¬ (𝐹..^𝐿) = ∅)) |
7 | 6 | impcom 445 |
. . . . . . . . . . . 12
⊢ ((𝐹 < 𝐿 ∧ (𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ)) → ¬ (𝐹..^𝐿) = ∅) |
8 | | ss0 3926 |
. . . . . . . . . . . 12
⊢ ((𝐹..^𝐿) ⊆ ∅ → (𝐹..^𝐿) = ∅) |
9 | 7, 8 | nsyl 134 |
. . . . . . . . . . 11
⊢ ((𝐹 < 𝐿 ∧ (𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ)) → ¬ (𝐹..^𝐿) ⊆ ∅) |
10 | | dm0 5260 |
. . . . . . . . . . . . 13
⊢ dom
∅ = ∅ |
11 | 10 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝐹 < 𝐿 ∧ (𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ)) → dom ∅ =
∅) |
12 | 11 | sseq2d 3596 |
. . . . . . . . . . 11
⊢ ((𝐹 < 𝐿 ∧ (𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ)) → ((𝐹..^𝐿) ⊆ dom ∅ ↔ (𝐹..^𝐿) ⊆ ∅)) |
13 | 9, 12 | mtbird 314 |
. . . . . . . . . 10
⊢ ((𝐹 < 𝐿 ∧ (𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ)) → ¬ (𝐹..^𝐿) ⊆ dom ∅) |
14 | 13 | iffalsed 4047 |
. . . . . . . . 9
⊢ ((𝐹 < 𝐿 ∧ (𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ)) → if((𝐹..^𝐿) ⊆ dom ∅, (𝑥 ∈ (0..^(𝐿 − 𝐹)) ↦ (∅‘(𝑥 + 𝐹))), ∅) = ∅) |
15 | | 0ss 3924 |
. . . . . . . . . . . . 13
⊢ ∅
⊆ ∅ |
16 | 15 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((¬
𝐹 < 𝐿 ∧ (𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ)) → ∅ ⊆
∅) |
17 | 4 | biimpac 502 |
. . . . . . . . . . . 12
⊢ ((¬
𝐹 < 𝐿 ∧ (𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ)) → (𝐹..^𝐿) = ∅) |
18 | 10 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((¬
𝐹 < 𝐿 ∧ (𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ)) → dom ∅ =
∅) |
19 | 16, 17, 18 | 3sstr4d 3611 |
. . . . . . . . . . 11
⊢ ((¬
𝐹 < 𝐿 ∧ (𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ)) → (𝐹..^𝐿) ⊆ dom ∅) |
20 | 19 | iftrued 4044 |
. . . . . . . . . 10
⊢ ((¬
𝐹 < 𝐿 ∧ (𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ)) → if((𝐹..^𝐿) ⊆ dom ∅, (𝑥 ∈ (0..^(𝐿 − 𝐹)) ↦ (∅‘(𝑥 + 𝐹))), ∅) = (𝑥 ∈ (0..^(𝐿 − 𝐹)) ↦ (∅‘(𝑥 + 𝐹)))) |
21 | | zre 11258 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐿 ∈ ℤ → 𝐿 ∈
ℝ) |
22 | | zre 11258 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹 ∈ ℤ → 𝐹 ∈
ℝ) |
23 | | lenlt 9995 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐿 ∈ ℝ ∧ 𝐹 ∈ ℝ) → (𝐿 ≤ 𝐹 ↔ ¬ 𝐹 < 𝐿)) |
24 | 23 | bicomd 212 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐿 ∈ ℝ ∧ 𝐹 ∈ ℝ) → (¬
𝐹 < 𝐿 ↔ 𝐿 ≤ 𝐹)) |
25 | 21, 22, 24 | syl2anr 494 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (¬
𝐹 < 𝐿 ↔ 𝐿 ≤ 𝐹)) |
26 | | fzo0n 12359 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (𝐿 ≤ 𝐹 ↔ (0..^(𝐿 − 𝐹)) = ∅)) |
27 | 25, 26 | bitrd 267 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (¬
𝐹 < 𝐿 ↔ (0..^(𝐿 − 𝐹)) = ∅)) |
28 | 27 | biimpac 502 |
. . . . . . . . . . . . . 14
⊢ ((¬
𝐹 < 𝐿 ∧ (𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ)) → (0..^(𝐿 − 𝐹)) = ∅) |
29 | 28 | mpteq1d 4666 |
. . . . . . . . . . . . 13
⊢ ((¬
𝐹 < 𝐿 ∧ (𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ)) → (𝑥 ∈ (0..^(𝐿 − 𝐹)) ↦ (∅‘(𝑥 + 𝐹))) = (𝑥 ∈ ∅ ↦ (∅‘(𝑥 + 𝐹)))) |
30 | 29 | dmeqd 5248 |
. . . . . . . . . . . 12
⊢ ((¬
𝐹 < 𝐿 ∧ (𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ)) → dom (𝑥 ∈ (0..^(𝐿 − 𝐹)) ↦ (∅‘(𝑥 + 𝐹))) = dom (𝑥 ∈ ∅ ↦ (∅‘(𝑥 + 𝐹)))) |
31 | | ral0 4028 |
. . . . . . . . . . . . 13
⊢
∀𝑥 ∈
∅ (∅‘(𝑥 +
𝐹)) ∈
V |
32 | | dmmptg 5549 |
. . . . . . . . . . . . 13
⊢
(∀𝑥 ∈
∅ (∅‘(𝑥 +
𝐹)) ∈ V → dom
(𝑥 ∈ ∅ ↦
(∅‘(𝑥 + 𝐹))) = ∅) |
33 | 31, 32 | mp1i 13 |
. . . . . . . . . . . 12
⊢ ((¬
𝐹 < 𝐿 ∧ (𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ)) → dom (𝑥 ∈ ∅ ↦
(∅‘(𝑥 + 𝐹))) = ∅) |
34 | 30, 33 | eqtrd 2644 |
. . . . . . . . . . 11
⊢ ((¬
𝐹 < 𝐿 ∧ (𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ)) → dom (𝑥 ∈ (0..^(𝐿 − 𝐹)) ↦ (∅‘(𝑥 + 𝐹))) = ∅) |
35 | | mptrel 5170 |
. . . . . . . . . . . 12
⊢ Rel
(𝑥 ∈ (0..^(𝐿 − 𝐹)) ↦ (∅‘(𝑥 + 𝐹))) |
36 | | reldm0 5264 |
. . . . . . . . . . . 12
⊢ (Rel
(𝑥 ∈ (0..^(𝐿 − 𝐹)) ↦ (∅‘(𝑥 + 𝐹))) → ((𝑥 ∈ (0..^(𝐿 − 𝐹)) ↦ (∅‘(𝑥 + 𝐹))) = ∅ ↔ dom (𝑥 ∈ (0..^(𝐿 − 𝐹)) ↦ (∅‘(𝑥 + 𝐹))) = ∅)) |
37 | 35, 36 | mp1i 13 |
. . . . . . . . . . 11
⊢ ((¬
𝐹 < 𝐿 ∧ (𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ)) → ((𝑥 ∈ (0..^(𝐿 − 𝐹)) ↦ (∅‘(𝑥 + 𝐹))) = ∅ ↔ dom (𝑥 ∈ (0..^(𝐿 − 𝐹)) ↦ (∅‘(𝑥 + 𝐹))) = ∅)) |
38 | 34, 37 | mpbird 246 |
. . . . . . . . . 10
⊢ ((¬
𝐹 < 𝐿 ∧ (𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ)) → (𝑥 ∈ (0..^(𝐿 − 𝐹)) ↦ (∅‘(𝑥 + 𝐹))) = ∅) |
39 | 20, 38 | eqtrd 2644 |
. . . . . . . . 9
⊢ ((¬
𝐹 < 𝐿 ∧ (𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ)) → if((𝐹..^𝐿) ⊆ dom ∅, (𝑥 ∈ (0..^(𝐿 − 𝐹)) ↦ (∅‘(𝑥 + 𝐹))), ∅) = ∅) |
40 | 14, 39 | pm2.61ian 827 |
. . . . . . . 8
⊢ ((𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) →
if((𝐹..^𝐿) ⊆ dom ∅, (𝑥 ∈ (0..^(𝐿 − 𝐹)) ↦ (∅‘(𝑥 + 𝐹))), ∅) = ∅) |
41 | 40 | 3adant1 1072 |
. . . . . . 7
⊢ ((∅
∈ V ∧ 𝐹 ∈
ℤ ∧ 𝐿 ∈
ℤ) → if((𝐹..^𝐿) ⊆ dom ∅, (𝑥 ∈ (0..^(𝐿 − 𝐹)) ↦ (∅‘(𝑥 + 𝐹))), ∅) = ∅) |
42 | 3, 41 | eqtrd 2644 |
. . . . . 6
⊢ ((∅
∈ V ∧ 𝐹 ∈
ℤ ∧ 𝐿 ∈
ℤ) → (∅ substr 〈𝐹, 𝐿〉) = ∅) |
43 | 42 | 3expb 1258 |
. . . . 5
⊢ ((∅
∈ V ∧ (𝐹 ∈
ℤ ∧ 𝐿 ∈
ℤ)) → (∅ substr 〈𝐹, 𝐿〉) = ∅) |
44 | 2, 43 | sylan2b 491 |
. . . 4
⊢ ((∅
∈ V ∧ 〈𝐹,
𝐿〉 ∈ (ℤ
× ℤ)) → (∅ substr 〈𝐹, 𝐿〉) = ∅) |
45 | 1, 44 | sylbi 206 |
. . 3
⊢
(〈∅, 〈𝐹, 𝐿〉〉 ∈ (V × (ℤ
× ℤ)) → (∅ substr 〈𝐹, 𝐿〉) = ∅) |
46 | | df-substr 13158 |
. . . 4
⊢ substr =
(𝑠 ∈ V, 𝑏 ∈ (ℤ ×
ℤ) ↦ if(((1st ‘𝑏)..^(2nd ‘𝑏)) ⊆ dom 𝑠, (𝑧 ∈ (0..^((2nd ‘𝑏) − (1st
‘𝑏))) ↦ (𝑠‘(𝑧 + (1st ‘𝑏)))), ∅)) |
47 | | ovex 6577 |
. . . . . 6
⊢
(0..^((2nd ‘𝑏) − (1st ‘𝑏))) ∈ V |
48 | 47 | mptex 6390 |
. . . . 5
⊢ (𝑧 ∈ (0..^((2nd
‘𝑏) −
(1st ‘𝑏)))
↦ (𝑠‘(𝑧 + (1st ‘𝑏)))) ∈ V |
49 | | 0ex 4718 |
. . . . 5
⊢ ∅
∈ V |
50 | 48, 49 | ifex 4106 |
. . . 4
⊢
if(((1st ‘𝑏)..^(2nd ‘𝑏)) ⊆ dom 𝑠, (𝑧 ∈ (0..^((2nd ‘𝑏) − (1st
‘𝑏))) ↦ (𝑠‘(𝑧 + (1st ‘𝑏)))), ∅) ∈ V |
51 | 46, 50 | dmmpt2 7129 |
. . 3
⊢ dom
substr = (V × (ℤ × ℤ)) |
52 | 45, 51 | eleq2s 2706 |
. 2
⊢
(〈∅, 〈𝐹, 𝐿〉〉 ∈ dom substr →
(∅ substr 〈𝐹,
𝐿〉) =
∅) |
53 | | df-ov 6552 |
. . 3
⊢ (∅
substr 〈𝐹, 𝐿〉) = ( substr
‘〈∅, 〈𝐹, 𝐿〉〉) |
54 | | ndmfv 6128 |
. . 3
⊢ (¬
〈∅, 〈𝐹,
𝐿〉〉 ∈ dom
substr → ( substr ‘〈∅, 〈𝐹, 𝐿〉〉) = ∅) |
55 | 53, 54 | syl5eq 2656 |
. 2
⊢ (¬
〈∅, 〈𝐹,
𝐿〉〉 ∈ dom
substr → (∅ substr 〈𝐹, 𝐿〉) = ∅) |
56 | 52, 55 | pm2.61i 175 |
1
⊢ (∅
substr 〈𝐹, 𝐿〉) =
∅ |