Proof of Theorem strlemor1
Step | Hyp | Ref
| Expression |
1 | | strlemor.f |
. . . . . 6
⊢ (Fun
◡◡𝐹 ∧ dom 𝐹 ⊆ (1...𝐼)) |
2 | 1 | simpli 473 |
. . . . 5
⊢ Fun ◡◡𝐹 |
3 | | funcnvsn 5850 |
. . . . 5
⊢ Fun ◡{〈𝑋, 𝐽〉} |
4 | 2, 3 | pm3.2i 470 |
. . . 4
⊢ (Fun
◡◡𝐹 ∧ Fun ◡{〈𝑋, 𝐽〉}) |
5 | | cnvcnvss 5507 |
. . . . . . 7
⊢ ◡◡𝐹 ⊆ 𝐹 |
6 | | dmss 5245 |
. . . . . . 7
⊢ (◡◡𝐹 ⊆ 𝐹 → dom ◡◡𝐹 ⊆ dom 𝐹) |
7 | 5, 6 | ax-mp 5 |
. . . . . 6
⊢ dom ◡◡𝐹 ⊆ dom 𝐹 |
8 | | cnvcnvsn 5530 |
. . . . . . . . 9
⊢ ◡◡{〈𝐽, 𝑋〉} = ◡{〈𝑋, 𝐽〉} |
9 | | cnvcnvss 5507 |
. . . . . . . . 9
⊢ ◡◡{〈𝐽, 𝑋〉} ⊆ {〈𝐽, 𝑋〉} |
10 | 8, 9 | eqsstr3i 3599 |
. . . . . . . 8
⊢ ◡{〈𝑋, 𝐽〉} ⊆ {〈𝐽, 𝑋〉} |
11 | | dmss 5245 |
. . . . . . . 8
⊢ (◡{〈𝑋, 𝐽〉} ⊆ {〈𝐽, 𝑋〉} → dom ◡{〈𝑋, 𝐽〉} ⊆ dom {〈𝐽, 𝑋〉}) |
12 | 10, 11 | ax-mp 5 |
. . . . . . 7
⊢ dom ◡{〈𝑋, 𝐽〉} ⊆ dom {〈𝐽, 𝑋〉} |
13 | | dmsnopss 5525 |
. . . . . . 7
⊢ dom
{〈𝐽, 𝑋〉} ⊆ {𝐽} |
14 | 12, 13 | sstri 3577 |
. . . . . 6
⊢ dom ◡{〈𝑋, 𝐽〉} ⊆ {𝐽} |
15 | | ss2in 3802 |
. . . . . 6
⊢ ((dom
◡◡𝐹 ⊆ dom 𝐹 ∧ dom ◡{〈𝑋, 𝐽〉} ⊆ {𝐽}) → (dom ◡◡𝐹 ∩ dom ◡{〈𝑋, 𝐽〉}) ⊆ (dom 𝐹 ∩ {𝐽})) |
16 | 7, 14, 15 | mp2an 704 |
. . . . 5
⊢ (dom
◡◡𝐹 ∩ dom ◡{〈𝑋, 𝐽〉}) ⊆ (dom 𝐹 ∩ {𝐽}) |
17 | | strlemor.o |
. . . . . . . . 9
⊢ 𝐼 < 𝐽 |
18 | | strlemor.i |
. . . . . . . . . . 11
⊢ 𝐼 ∈
ℕ0 |
19 | 18 | nn0rei 11180 |
. . . . . . . . . 10
⊢ 𝐼 ∈ ℝ |
20 | | strlemor.j |
. . . . . . . . . . 11
⊢ 𝐽 ∈ ℕ |
21 | 20 | nnrei 10906 |
. . . . . . . . . 10
⊢ 𝐽 ∈ ℝ |
22 | 19, 21 | ltnlei 10037 |
. . . . . . . . 9
⊢ (𝐼 < 𝐽 ↔ ¬ 𝐽 ≤ 𝐼) |
23 | 17, 22 | mpbi 219 |
. . . . . . . 8
⊢ ¬
𝐽 ≤ 𝐼 |
24 | | elfzle2 12216 |
. . . . . . . 8
⊢ (𝐽 ∈ (1...𝐼) → 𝐽 ≤ 𝐼) |
25 | 23, 24 | mto 187 |
. . . . . . 7
⊢ ¬
𝐽 ∈ (1...𝐼) |
26 | 1 | simpri 477 |
. . . . . . . 8
⊢ dom 𝐹 ⊆ (1...𝐼) |
27 | 26 | sseli 3564 |
. . . . . . 7
⊢ (𝐽 ∈ dom 𝐹 → 𝐽 ∈ (1...𝐼)) |
28 | 25, 27 | mto 187 |
. . . . . 6
⊢ ¬
𝐽 ∈ dom 𝐹 |
29 | | disjsn 4192 |
. . . . . 6
⊢ ((dom
𝐹 ∩ {𝐽}) = ∅ ↔ ¬ 𝐽 ∈ dom 𝐹) |
30 | 28, 29 | mpbir 220 |
. . . . 5
⊢ (dom
𝐹 ∩ {𝐽}) = ∅ |
31 | | sseq0 3927 |
. . . . 5
⊢ (((dom
◡◡𝐹 ∩ dom ◡{〈𝑋, 𝐽〉}) ⊆ (dom 𝐹 ∩ {𝐽}) ∧ (dom 𝐹 ∩ {𝐽}) = ∅) → (dom ◡◡𝐹 ∩ dom ◡{〈𝑋, 𝐽〉}) = ∅) |
32 | 16, 30, 31 | mp2an 704 |
. . . 4
⊢ (dom
◡◡𝐹 ∩ dom ◡{〈𝑋, 𝐽〉}) = ∅ |
33 | | funun 5846 |
. . . 4
⊢ (((Fun
◡◡𝐹 ∧ Fun ◡{〈𝑋, 𝐽〉}) ∧ (dom ◡◡𝐹 ∩ dom ◡{〈𝑋, 𝐽〉}) = ∅) → Fun (◡◡𝐹 ∪ ◡{〈𝑋, 𝐽〉})) |
34 | 4, 32, 33 | mp2an 704 |
. . 3
⊢ Fun
(◡◡𝐹 ∪ ◡{〈𝑋, 𝐽〉}) |
35 | | strlemor1.g |
. . . . . . . . 9
⊢ 𝐺 = (𝐹 ∪ {〈𝐴, 𝑋〉}) |
36 | | strlemor.a |
. . . . . . . . . . . 12
⊢ 𝐴 = 𝐽 |
37 | 36 | opeq1i 4343 |
. . . . . . . . . . 11
⊢
〈𝐴, 𝑋〉 = 〈𝐽, 𝑋〉 |
38 | 37 | sneqi 4136 |
. . . . . . . . . 10
⊢
{〈𝐴, 𝑋〉} = {〈𝐽, 𝑋〉} |
39 | 38 | uneq2i 3726 |
. . . . . . . . 9
⊢ (𝐹 ∪ {〈𝐴, 𝑋〉}) = (𝐹 ∪ {〈𝐽, 𝑋〉}) |
40 | 35, 39 | eqtri 2632 |
. . . . . . . 8
⊢ 𝐺 = (𝐹 ∪ {〈𝐽, 𝑋〉}) |
41 | 40 | cnveqi 5219 |
. . . . . . 7
⊢ ◡𝐺 = ◡(𝐹 ∪ {〈𝐽, 𝑋〉}) |
42 | | cnvun 5457 |
. . . . . . 7
⊢ ◡(𝐹 ∪ {〈𝐽, 𝑋〉}) = (◡𝐹 ∪ ◡{〈𝐽, 𝑋〉}) |
43 | 41, 42 | eqtri 2632 |
. . . . . 6
⊢ ◡𝐺 = (◡𝐹 ∪ ◡{〈𝐽, 𝑋〉}) |
44 | 43 | cnveqi 5219 |
. . . . 5
⊢ ◡◡𝐺 = ◡(◡𝐹 ∪ ◡{〈𝐽, 𝑋〉}) |
45 | | cnvun 5457 |
. . . . . 6
⊢ ◡(◡𝐹 ∪ ◡{〈𝐽, 𝑋〉}) = (◡◡𝐹 ∪ ◡◡{〈𝐽, 𝑋〉}) |
46 | 8 | uneq2i 3726 |
. . . . . 6
⊢ (◡◡𝐹 ∪ ◡◡{〈𝐽, 𝑋〉}) = (◡◡𝐹 ∪ ◡{〈𝑋, 𝐽〉}) |
47 | 45, 46 | eqtri 2632 |
. . . . 5
⊢ ◡(◡𝐹 ∪ ◡{〈𝐽, 𝑋〉}) = (◡◡𝐹 ∪ ◡{〈𝑋, 𝐽〉}) |
48 | 44, 47 | eqtri 2632 |
. . . 4
⊢ ◡◡𝐺 = (◡◡𝐹 ∪ ◡{〈𝑋, 𝐽〉}) |
49 | 48 | funeqi 5824 |
. . 3
⊢ (Fun
◡◡𝐺 ↔ Fun (◡◡𝐹 ∪ ◡{〈𝑋, 𝐽〉})) |
50 | 34, 49 | mpbir 220 |
. 2
⊢ Fun ◡◡𝐺 |
51 | 40 | dmeqi 5247 |
. . . 4
⊢ dom 𝐺 = dom (𝐹 ∪ {〈𝐽, 𝑋〉}) |
52 | | dmun 5253 |
. . . 4
⊢ dom
(𝐹 ∪ {〈𝐽, 𝑋〉}) = (dom 𝐹 ∪ dom {〈𝐽, 𝑋〉}) |
53 | 51, 52 | eqtri 2632 |
. . 3
⊢ dom 𝐺 = (dom 𝐹 ∪ dom {〈𝐽, 𝑋〉}) |
54 | 18 | nn0zi 11279 |
. . . . . . 7
⊢ 𝐼 ∈ ℤ |
55 | 20 | nnzi 11278 |
. . . . . . 7
⊢ 𝐽 ∈ ℤ |
56 | 19, 21, 17 | ltleii 10039 |
. . . . . . 7
⊢ 𝐼 ≤ 𝐽 |
57 | | eluz2 11569 |
. . . . . . 7
⊢ (𝐽 ∈
(ℤ≥‘𝐼) ↔ (𝐼 ∈ ℤ ∧ 𝐽 ∈ ℤ ∧ 𝐼 ≤ 𝐽)) |
58 | 54, 55, 56, 57 | mpbir3an 1237 |
. . . . . 6
⊢ 𝐽 ∈
(ℤ≥‘𝐼) |
59 | | fzss2 12252 |
. . . . . 6
⊢ (𝐽 ∈
(ℤ≥‘𝐼) → (1...𝐼) ⊆ (1...𝐽)) |
60 | 58, 59 | ax-mp 5 |
. . . . 5
⊢
(1...𝐼) ⊆
(1...𝐽) |
61 | 26, 60 | sstri 3577 |
. . . 4
⊢ dom 𝐹 ⊆ (1...𝐽) |
62 | | elfz1end 12242 |
. . . . . . 7
⊢ (𝐽 ∈ ℕ ↔ 𝐽 ∈ (1...𝐽)) |
63 | 20, 62 | mpbi 219 |
. . . . . 6
⊢ 𝐽 ∈ (1...𝐽) |
64 | | snssi 4280 |
. . . . . 6
⊢ (𝐽 ∈ (1...𝐽) → {𝐽} ⊆ (1...𝐽)) |
65 | 63, 64 | ax-mp 5 |
. . . . 5
⊢ {𝐽} ⊆ (1...𝐽) |
66 | 13, 65 | sstri 3577 |
. . . 4
⊢ dom
{〈𝐽, 𝑋〉} ⊆ (1...𝐽) |
67 | 61, 66 | unssi 3750 |
. . 3
⊢ (dom
𝐹 ∪ dom {〈𝐽, 𝑋〉}) ⊆ (1...𝐽) |
68 | 53, 67 | eqsstri 3598 |
. 2
⊢ dom 𝐺 ⊆ (1...𝐽) |
69 | 50, 68 | pm3.2i 470 |
1
⊢ (Fun
◡◡𝐺 ∧ dom 𝐺 ⊆ (1...𝐽)) |