Step | Hyp | Ref
| Expression |
1 | | elnn 7075 |
. . . . . 6
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ ω) → 𝐴 ∈ ω) |
2 | 1 | ancoms 469 |
. . . . 5
⊢ ((𝐵 ∈ ω ∧ 𝐴 ∈ 𝐵) → 𝐴 ∈ ω) |
3 | 2 | adantll 750 |
. . . 4
⊢ (((𝐶 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ∈ 𝐵) → 𝐴 ∈ ω) |
4 | | nnord 7073 |
. . . . . . . . 9
⊢ (𝐵 ∈ ω → Ord 𝐵) |
5 | | ordsucss 7018 |
. . . . . . . . 9
⊢ (Ord
𝐵 → (𝐴 ∈ 𝐵 → suc 𝐴 ⊆ 𝐵)) |
6 | 4, 5 | syl 17 |
. . . . . . . 8
⊢ (𝐵 ∈ ω → (𝐴 ∈ 𝐵 → suc 𝐴 ⊆ 𝐵)) |
7 | 6 | ad2antlr 763 |
. . . . . . 7
⊢ (((𝐶 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ∈ ω) → (𝐴 ∈ 𝐵 → suc 𝐴 ⊆ 𝐵)) |
8 | | peano2b 7081 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ω ↔ suc 𝐴 ∈
ω) |
9 | | oveq2 6658 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = suc 𝐴 → (𝐶 +𝑜 𝑥) = (𝐶 +𝑜 suc 𝐴)) |
10 | 9 | sseq2d 3633 |
. . . . . . . . . . . . 13
⊢ (𝑥 = suc 𝐴 → ((𝐶 +𝑜 suc 𝐴) ⊆ (𝐶 +𝑜 𝑥) ↔ (𝐶 +𝑜 suc 𝐴) ⊆ (𝐶 +𝑜 suc 𝐴))) |
11 | 10 | imbi2d 330 |
. . . . . . . . . . . 12
⊢ (𝑥 = suc 𝐴 → ((𝐶 ∈ ω → (𝐶 +𝑜 suc 𝐴) ⊆ (𝐶 +𝑜 𝑥)) ↔ (𝐶 ∈ ω → (𝐶 +𝑜 suc 𝐴) ⊆ (𝐶 +𝑜 suc 𝐴)))) |
12 | | oveq2 6658 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑦 → (𝐶 +𝑜 𝑥) = (𝐶 +𝑜 𝑦)) |
13 | 12 | sseq2d 3633 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → ((𝐶 +𝑜 suc 𝐴) ⊆ (𝐶 +𝑜 𝑥) ↔ (𝐶 +𝑜 suc 𝐴) ⊆ (𝐶 +𝑜 𝑦))) |
14 | 13 | imbi2d 330 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → ((𝐶 ∈ ω → (𝐶 +𝑜 suc 𝐴) ⊆ (𝐶 +𝑜 𝑥)) ↔ (𝐶 ∈ ω → (𝐶 +𝑜 suc 𝐴) ⊆ (𝐶 +𝑜 𝑦)))) |
15 | | oveq2 6658 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = suc 𝑦 → (𝐶 +𝑜 𝑥) = (𝐶 +𝑜 suc 𝑦)) |
16 | 15 | sseq2d 3633 |
. . . . . . . . . . . . 13
⊢ (𝑥 = suc 𝑦 → ((𝐶 +𝑜 suc 𝐴) ⊆ (𝐶 +𝑜 𝑥) ↔ (𝐶 +𝑜 suc 𝐴) ⊆ (𝐶 +𝑜 suc 𝑦))) |
17 | 16 | imbi2d 330 |
. . . . . . . . . . . 12
⊢ (𝑥 = suc 𝑦 → ((𝐶 ∈ ω → (𝐶 +𝑜 suc 𝐴) ⊆ (𝐶 +𝑜 𝑥)) ↔ (𝐶 ∈ ω → (𝐶 +𝑜 suc 𝐴) ⊆ (𝐶 +𝑜 suc 𝑦)))) |
18 | | oveq2 6658 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝐵 → (𝐶 +𝑜 𝑥) = (𝐶 +𝑜 𝐵)) |
19 | 18 | sseq2d 3633 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝐵 → ((𝐶 +𝑜 suc 𝐴) ⊆ (𝐶 +𝑜 𝑥) ↔ (𝐶 +𝑜 suc 𝐴) ⊆ (𝐶 +𝑜 𝐵))) |
20 | 19 | imbi2d 330 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝐵 → ((𝐶 ∈ ω → (𝐶 +𝑜 suc 𝐴) ⊆ (𝐶 +𝑜 𝑥)) ↔ (𝐶 ∈ ω → (𝐶 +𝑜 suc 𝐴) ⊆ (𝐶 +𝑜 𝐵)))) |
21 | | ssid 3624 |
. . . . . . . . . . . . 13
⊢ (𝐶 +𝑜 suc 𝐴) ⊆ (𝐶 +𝑜 suc 𝐴) |
22 | 21 | 2a1i 12 |
. . . . . . . . . . . 12
⊢ (suc
𝐴 ∈ ω →
(𝐶 ∈ ω →
(𝐶 +𝑜
suc 𝐴) ⊆ (𝐶 +𝑜 suc 𝐴))) |
23 | | sssucid 5802 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐶 +𝑜 𝑦) ⊆ suc (𝐶 +𝑜 𝑦) |
24 | | sstr2 3610 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐶 +𝑜 suc 𝐴) ⊆ (𝐶 +𝑜 𝑦) → ((𝐶 +𝑜 𝑦) ⊆ suc (𝐶 +𝑜 𝑦) → (𝐶 +𝑜 suc 𝐴) ⊆ suc (𝐶 +𝑜 𝑦))) |
25 | 23, 24 | mpi 20 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐶 +𝑜 suc 𝐴) ⊆ (𝐶 +𝑜 𝑦) → (𝐶 +𝑜 suc 𝐴) ⊆ suc (𝐶 +𝑜 𝑦)) |
26 | | nnasuc 7686 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐶 ∈ ω ∧ 𝑦 ∈ ω) → (𝐶 +𝑜 suc 𝑦) = suc (𝐶 +𝑜 𝑦)) |
27 | 26 | ancoms 469 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ω ∧ 𝐶 ∈ ω) → (𝐶 +𝑜 suc 𝑦) = suc (𝐶 +𝑜 𝑦)) |
28 | 27 | sseq2d 3633 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ ω ∧ 𝐶 ∈ ω) → ((𝐶 +𝑜 suc 𝐴) ⊆ (𝐶 +𝑜 suc 𝑦) ↔ (𝐶 +𝑜 suc 𝐴) ⊆ suc (𝐶 +𝑜 𝑦))) |
29 | 25, 28 | syl5ibr 236 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ω ∧ 𝐶 ∈ ω) → ((𝐶 +𝑜 suc 𝐴) ⊆ (𝐶 +𝑜 𝑦) → (𝐶 +𝑜 suc 𝐴) ⊆ (𝐶 +𝑜 suc 𝑦))) |
30 | 29 | ex 450 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ω → (𝐶 ∈ ω → ((𝐶 +𝑜 suc 𝐴) ⊆ (𝐶 +𝑜 𝑦) → (𝐶 +𝑜 suc 𝐴) ⊆ (𝐶 +𝑜 suc 𝑦)))) |
31 | 30 | ad2antrr 762 |
. . . . . . . . . . . . 13
⊢ (((𝑦 ∈ ω ∧ suc 𝐴 ∈ ω) ∧ suc 𝐴 ⊆ 𝑦) → (𝐶 ∈ ω → ((𝐶 +𝑜 suc 𝐴) ⊆ (𝐶 +𝑜 𝑦) → (𝐶 +𝑜 suc 𝐴) ⊆ (𝐶 +𝑜 suc 𝑦)))) |
32 | 31 | a2d 29 |
. . . . . . . . . . . 12
⊢ (((𝑦 ∈ ω ∧ suc 𝐴 ∈ ω) ∧ suc 𝐴 ⊆ 𝑦) → ((𝐶 ∈ ω → (𝐶 +𝑜 suc 𝐴) ⊆ (𝐶 +𝑜 𝑦)) → (𝐶 ∈ ω → (𝐶 +𝑜 suc 𝐴) ⊆ (𝐶 +𝑜 suc 𝑦)))) |
33 | 11, 14, 17, 20, 22, 32 | findsg 7093 |
. . . . . . . . . . 11
⊢ (((𝐵 ∈ ω ∧ suc 𝐴 ∈ ω) ∧ suc 𝐴 ⊆ 𝐵) → (𝐶 ∈ ω → (𝐶 +𝑜 suc 𝐴) ⊆ (𝐶 +𝑜 𝐵))) |
34 | 33 | exp31 630 |
. . . . . . . . . 10
⊢ (𝐵 ∈ ω → (suc
𝐴 ∈ ω →
(suc 𝐴 ⊆ 𝐵 → (𝐶 ∈ ω → (𝐶 +𝑜 suc 𝐴) ⊆ (𝐶 +𝑜 𝐵))))) |
35 | 8, 34 | syl5bi 232 |
. . . . . . . . 9
⊢ (𝐵 ∈ ω → (𝐴 ∈ ω → (suc
𝐴 ⊆ 𝐵 → (𝐶 ∈ ω → (𝐶 +𝑜 suc 𝐴) ⊆ (𝐶 +𝑜 𝐵))))) |
36 | 35 | com4r 94 |
. . . . . . . 8
⊢ (𝐶 ∈ ω → (𝐵 ∈ ω → (𝐴 ∈ ω → (suc
𝐴 ⊆ 𝐵 → (𝐶 +𝑜 suc 𝐴) ⊆ (𝐶 +𝑜 𝐵))))) |
37 | 36 | imp31 448 |
. . . . . . 7
⊢ (((𝐶 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ∈ ω) → (suc
𝐴 ⊆ 𝐵 → (𝐶 +𝑜 suc 𝐴) ⊆ (𝐶 +𝑜 𝐵))) |
38 | | nnasuc 7686 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ ω ∧ 𝐴 ∈ ω) → (𝐶 +𝑜 suc 𝐴) = suc (𝐶 +𝑜 𝐴)) |
39 | 38 | sseq1d 3632 |
. . . . . . . . 9
⊢ ((𝐶 ∈ ω ∧ 𝐴 ∈ ω) → ((𝐶 +𝑜 suc 𝐴) ⊆ (𝐶 +𝑜 𝐵) ↔ suc (𝐶 +𝑜 𝐴) ⊆ (𝐶 +𝑜 𝐵))) |
40 | | ovex 6678 |
. . . . . . . . . 10
⊢ (𝐶 +𝑜 𝐴) ∈ V |
41 | | sucssel 5819 |
. . . . . . . . . 10
⊢ ((𝐶 +𝑜 𝐴) ∈ V → (suc (𝐶 +𝑜 𝐴) ⊆ (𝐶 +𝑜 𝐵) → (𝐶 +𝑜 𝐴) ∈ (𝐶 +𝑜 𝐵))) |
42 | 40, 41 | ax-mp 5 |
. . . . . . . . 9
⊢ (suc
(𝐶 +𝑜
𝐴) ⊆ (𝐶 +𝑜 𝐵) → (𝐶 +𝑜 𝐴) ∈ (𝐶 +𝑜 𝐵)) |
43 | 39, 42 | syl6bi 243 |
. . . . . . . 8
⊢ ((𝐶 ∈ ω ∧ 𝐴 ∈ ω) → ((𝐶 +𝑜 suc 𝐴) ⊆ (𝐶 +𝑜 𝐵) → (𝐶 +𝑜 𝐴) ∈ (𝐶 +𝑜 𝐵))) |
44 | 43 | adantlr 751 |
. . . . . . 7
⊢ (((𝐶 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ∈ ω) → ((𝐶 +𝑜 suc 𝐴) ⊆ (𝐶 +𝑜 𝐵) → (𝐶 +𝑜 𝐴) ∈ (𝐶 +𝑜 𝐵))) |
45 | 7, 37, 44 | 3syld 60 |
. . . . . 6
⊢ (((𝐶 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ∈ ω) → (𝐴 ∈ 𝐵 → (𝐶 +𝑜 𝐴) ∈ (𝐶 +𝑜 𝐵))) |
46 | 45 | imp 445 |
. . . . 5
⊢ ((((𝐶 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ∈ ω) ∧ 𝐴 ∈ 𝐵) → (𝐶 +𝑜 𝐴) ∈ (𝐶 +𝑜 𝐵)) |
47 | 46 | an32s 846 |
. . . 4
⊢ ((((𝐶 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ∈ 𝐵) ∧ 𝐴 ∈ ω) → (𝐶 +𝑜 𝐴) ∈ (𝐶 +𝑜 𝐵)) |
48 | 3, 47 | mpdan 702 |
. . 3
⊢ (((𝐶 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ∈ 𝐵) → (𝐶 +𝑜 𝐴) ∈ (𝐶 +𝑜 𝐵)) |
49 | 48 | ex 450 |
. 2
⊢ ((𝐶 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ∈ 𝐵 → (𝐶 +𝑜 𝐴) ∈ (𝐶 +𝑜 𝐵))) |
50 | 49 | ancoms 469 |
1
⊢ ((𝐵 ∈ ω ∧ 𝐶 ∈ ω) → (𝐴 ∈ 𝐵 → (𝐶 +𝑜 𝐴) ∈ (𝐶 +𝑜 𝐵))) |