Step | Hyp | Ref
| Expression |
1 | | oveq1 5539 |
. . . . . . 7
⊢ (𝑥 = 𝐶 → (𝑥 +𝑜 𝐴) = (𝐶 +𝑜 𝐴)) |
2 | | oveq1 5539 |
. . . . . . 7
⊢ (𝑥 = 𝐶 → (𝑥 +𝑜 𝐵) = (𝐶 +𝑜 𝐵)) |
3 | 1, 2 | sseq12d 3028 |
. . . . . 6
⊢ (𝑥 = 𝐶 → ((𝑥 +𝑜 𝐴) ⊆ (𝑥 +𝑜 𝐵) ↔ (𝐶 +𝑜 𝐴) ⊆ (𝐶 +𝑜 𝐵))) |
4 | 3 | bibi2d 230 |
. . . . 5
⊢ (𝑥 = 𝐶 → ((𝐴 ⊆ 𝐵 ↔ (𝑥 +𝑜 𝐴) ⊆ (𝑥 +𝑜 𝐵)) ↔ (𝐴 ⊆ 𝐵 ↔ (𝐶 +𝑜 𝐴) ⊆ (𝐶 +𝑜 𝐵)))) |
5 | 4 | imbi2d 228 |
. . . 4
⊢ (𝑥 = 𝐶 → (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ⊆ 𝐵 ↔ (𝑥 +𝑜 𝐴) ⊆ (𝑥 +𝑜 𝐵))) ↔ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ⊆ 𝐵 ↔ (𝐶 +𝑜 𝐴) ⊆ (𝐶 +𝑜 𝐵))))) |
6 | | oveq1 5539 |
. . . . . . 7
⊢ (𝑥 = ∅ → (𝑥 +𝑜 𝐴) = (∅
+𝑜 𝐴)) |
7 | | oveq1 5539 |
. . . . . . 7
⊢ (𝑥 = ∅ → (𝑥 +𝑜 𝐵) = (∅
+𝑜 𝐵)) |
8 | 6, 7 | sseq12d 3028 |
. . . . . 6
⊢ (𝑥 = ∅ → ((𝑥 +𝑜 𝐴) ⊆ (𝑥 +𝑜 𝐵) ↔ (∅ +𝑜
𝐴) ⊆ (∅
+𝑜 𝐵))) |
9 | 8 | bibi2d 230 |
. . . . 5
⊢ (𝑥 = ∅ → ((𝐴 ⊆ 𝐵 ↔ (𝑥 +𝑜 𝐴) ⊆ (𝑥 +𝑜 𝐵)) ↔ (𝐴 ⊆ 𝐵 ↔ (∅ +𝑜 𝐴) ⊆ (∅
+𝑜 𝐵)))) |
10 | | oveq1 5539 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑥 +𝑜 𝐴) = (𝑦 +𝑜 𝐴)) |
11 | | oveq1 5539 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑥 +𝑜 𝐵) = (𝑦 +𝑜 𝐵)) |
12 | 10, 11 | sseq12d 3028 |
. . . . . 6
⊢ (𝑥 = 𝑦 → ((𝑥 +𝑜 𝐴) ⊆ (𝑥 +𝑜 𝐵) ↔ (𝑦 +𝑜 𝐴) ⊆ (𝑦 +𝑜 𝐵))) |
13 | 12 | bibi2d 230 |
. . . . 5
⊢ (𝑥 = 𝑦 → ((𝐴 ⊆ 𝐵 ↔ (𝑥 +𝑜 𝐴) ⊆ (𝑥 +𝑜 𝐵)) ↔ (𝐴 ⊆ 𝐵 ↔ (𝑦 +𝑜 𝐴) ⊆ (𝑦 +𝑜 𝐵)))) |
14 | | oveq1 5539 |
. . . . . . 7
⊢ (𝑥 = suc 𝑦 → (𝑥 +𝑜 𝐴) = (suc 𝑦 +𝑜 𝐴)) |
15 | | oveq1 5539 |
. . . . . . 7
⊢ (𝑥 = suc 𝑦 → (𝑥 +𝑜 𝐵) = (suc 𝑦 +𝑜 𝐵)) |
16 | 14, 15 | sseq12d 3028 |
. . . . . 6
⊢ (𝑥 = suc 𝑦 → ((𝑥 +𝑜 𝐴) ⊆ (𝑥 +𝑜 𝐵) ↔ (suc 𝑦 +𝑜 𝐴) ⊆ (suc 𝑦 +𝑜 𝐵))) |
17 | 16 | bibi2d 230 |
. . . . 5
⊢ (𝑥 = suc 𝑦 → ((𝐴 ⊆ 𝐵 ↔ (𝑥 +𝑜 𝐴) ⊆ (𝑥 +𝑜 𝐵)) ↔ (𝐴 ⊆ 𝐵 ↔ (suc 𝑦 +𝑜 𝐴) ⊆ (suc 𝑦 +𝑜 𝐵)))) |
18 | | nna0r 6080 |
. . . . . . . 8
⊢ (𝐴 ∈ ω → (∅
+𝑜 𝐴) =
𝐴) |
19 | 18 | eqcomd 2086 |
. . . . . . 7
⊢ (𝐴 ∈ ω → 𝐴 = (∅
+𝑜 𝐴)) |
20 | 19 | adantr 270 |
. . . . . 6
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → 𝐴 = (∅
+𝑜 𝐴)) |
21 | | nna0r 6080 |
. . . . . . . 8
⊢ (𝐵 ∈ ω → (∅
+𝑜 𝐵) =
𝐵) |
22 | 21 | eqcomd 2086 |
. . . . . . 7
⊢ (𝐵 ∈ ω → 𝐵 = (∅
+𝑜 𝐵)) |
23 | 22 | adantl 271 |
. . . . . 6
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → 𝐵 = (∅
+𝑜 𝐵)) |
24 | 20, 23 | sseq12d 3028 |
. . . . 5
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ⊆ 𝐵 ↔ (∅ +𝑜 𝐴) ⊆ (∅
+𝑜 𝐵))) |
25 | | nnacl 6082 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ω ∧ 𝐴 ∈ ω) → (𝑦 +𝑜 𝐴) ∈
ω) |
26 | 25 | 3adant3 958 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ω ∧ 𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝑦 +𝑜 𝐴) ∈
ω) |
27 | | nnacl 6082 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ω ∧ 𝐵 ∈ ω) → (𝑦 +𝑜 𝐵) ∈
ω) |
28 | 27 | 3adant2 957 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ω ∧ 𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝑦 +𝑜 𝐵) ∈
ω) |
29 | | nnsucsssuc 6094 |
. . . . . . . . . 10
⊢ (((𝑦 +𝑜 𝐴) ∈ ω ∧ (𝑦 +𝑜 𝐵) ∈ ω) → ((𝑦 +𝑜 𝐴) ⊆ (𝑦 +𝑜 𝐵) ↔ suc (𝑦 +𝑜 𝐴) ⊆ suc (𝑦 +𝑜 𝐵))) |
30 | 26, 28, 29 | syl2anc 403 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ω ∧ 𝐴 ∈ ω ∧ 𝐵 ∈ ω) → ((𝑦 +𝑜 𝐴) ⊆ (𝑦 +𝑜 𝐵) ↔ suc (𝑦 +𝑜 𝐴) ⊆ suc (𝑦 +𝑜 𝐵))) |
31 | | nnasuc 6078 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ω ∧ 𝑦 ∈ ω) → (𝐴 +𝑜 suc 𝑦) = suc (𝐴 +𝑜 𝑦)) |
32 | | peano2 4336 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ω → suc 𝑦 ∈
ω) |
33 | | nnacom 6086 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ω ∧ suc 𝑦 ∈ ω) → (𝐴 +𝑜 suc 𝑦) = (suc 𝑦 +𝑜 𝐴)) |
34 | 32, 33 | sylan2 280 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ω ∧ 𝑦 ∈ ω) → (𝐴 +𝑜 suc 𝑦) = (suc 𝑦 +𝑜 𝐴)) |
35 | | nnacom 6086 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ω ∧ 𝑦 ∈ ω) → (𝐴 +𝑜 𝑦) = (𝑦 +𝑜 𝐴)) |
36 | | suceq 4157 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 +𝑜 𝑦) = (𝑦 +𝑜 𝐴) → suc (𝐴 +𝑜 𝑦) = suc (𝑦 +𝑜 𝐴)) |
37 | 35, 36 | syl 14 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ω ∧ 𝑦 ∈ ω) → suc
(𝐴 +𝑜
𝑦) = suc (𝑦 +𝑜 𝐴)) |
38 | 31, 34, 37 | 3eqtr3rd 2122 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ω ∧ 𝑦 ∈ ω) → suc
(𝑦 +𝑜
𝐴) = (suc 𝑦 +𝑜 𝐴)) |
39 | 38 | ancoms 264 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ω ∧ 𝐴 ∈ ω) → suc
(𝑦 +𝑜
𝐴) = (suc 𝑦 +𝑜 𝐴)) |
40 | 39 | 3adant3 958 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ω ∧ 𝐴 ∈ ω ∧ 𝐵 ∈ ω) → suc
(𝑦 +𝑜
𝐴) = (suc 𝑦 +𝑜 𝐴)) |
41 | | nnasuc 6078 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ ω ∧ 𝑦 ∈ ω) → (𝐵 +𝑜 suc 𝑦) = suc (𝐵 +𝑜 𝑦)) |
42 | | nnacom 6086 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 ∈ ω ∧ suc 𝑦 ∈ ω) → (𝐵 +𝑜 suc 𝑦) = (suc 𝑦 +𝑜 𝐵)) |
43 | 32, 42 | sylan2 280 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ ω ∧ 𝑦 ∈ ω) → (𝐵 +𝑜 suc 𝑦) = (suc 𝑦 +𝑜 𝐵)) |
44 | | nnacom 6086 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 ∈ ω ∧ 𝑦 ∈ ω) → (𝐵 +𝑜 𝑦) = (𝑦 +𝑜 𝐵)) |
45 | | suceq 4157 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 +𝑜 𝑦) = (𝑦 +𝑜 𝐵) → suc (𝐵 +𝑜 𝑦) = suc (𝑦 +𝑜 𝐵)) |
46 | 44, 45 | syl 14 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ ω ∧ 𝑦 ∈ ω) → suc
(𝐵 +𝑜
𝑦) = suc (𝑦 +𝑜 𝐵)) |
47 | 41, 43, 46 | 3eqtr3rd 2122 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ ω ∧ 𝑦 ∈ ω) → suc
(𝑦 +𝑜
𝐵) = (suc 𝑦 +𝑜 𝐵)) |
48 | 47 | ancoms 264 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ω ∧ 𝐵 ∈ ω) → suc
(𝑦 +𝑜
𝐵) = (suc 𝑦 +𝑜 𝐵)) |
49 | 48 | 3adant2 957 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ω ∧ 𝐴 ∈ ω ∧ 𝐵 ∈ ω) → suc
(𝑦 +𝑜
𝐵) = (suc 𝑦 +𝑜 𝐵)) |
50 | 40, 49 | sseq12d 3028 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ω ∧ 𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (suc
(𝑦 +𝑜
𝐴) ⊆ suc (𝑦 +𝑜 𝐵) ↔ (suc 𝑦 +𝑜 𝐴) ⊆ (suc 𝑦 +𝑜 𝐵))) |
51 | 30, 50 | bitrd 186 |
. . . . . . . 8
⊢ ((𝑦 ∈ ω ∧ 𝐴 ∈ ω ∧ 𝐵 ∈ ω) → ((𝑦 +𝑜 𝐴) ⊆ (𝑦 +𝑜 𝐵) ↔ (suc 𝑦 +𝑜 𝐴) ⊆ (suc 𝑦 +𝑜 𝐵))) |
52 | 51 | bibi2d 230 |
. . . . . . 7
⊢ ((𝑦 ∈ ω ∧ 𝐴 ∈ ω ∧ 𝐵 ∈ ω) → ((𝐴 ⊆ 𝐵 ↔ (𝑦 +𝑜 𝐴) ⊆ (𝑦 +𝑜 𝐵)) ↔ (𝐴 ⊆ 𝐵 ↔ (suc 𝑦 +𝑜 𝐴) ⊆ (suc 𝑦 +𝑜 𝐵)))) |
53 | 52 | biimpd 142 |
. . . . . 6
⊢ ((𝑦 ∈ ω ∧ 𝐴 ∈ ω ∧ 𝐵 ∈ ω) → ((𝐴 ⊆ 𝐵 ↔ (𝑦 +𝑜 𝐴) ⊆ (𝑦 +𝑜 𝐵)) → (𝐴 ⊆ 𝐵 ↔ (suc 𝑦 +𝑜 𝐴) ⊆ (suc 𝑦 +𝑜 𝐵)))) |
54 | 53 | 3expib 1141 |
. . . . 5
⊢ (𝑦 ∈ ω → ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → ((𝐴 ⊆ 𝐵 ↔ (𝑦 +𝑜 𝐴) ⊆ (𝑦 +𝑜 𝐵)) → (𝐴 ⊆ 𝐵 ↔ (suc 𝑦 +𝑜 𝐴) ⊆ (suc 𝑦 +𝑜 𝐵))))) |
55 | 9, 13, 17, 24, 54 | finds2 4342 |
. . . 4
⊢ (𝑥 ∈ ω → ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ⊆ 𝐵 ↔ (𝑥 +𝑜 𝐴) ⊆ (𝑥 +𝑜 𝐵)))) |
56 | 5, 55 | vtoclga 2664 |
. . 3
⊢ (𝐶 ∈ ω → ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ⊆ 𝐵 ↔ (𝐶 +𝑜 𝐴) ⊆ (𝐶 +𝑜 𝐵)))) |
57 | 56 | impcom 123 |
. 2
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐶 ∈ ω) → (𝐴 ⊆ 𝐵 ↔ (𝐶 +𝑜 𝐴) ⊆ (𝐶 +𝑜 𝐵))) |
58 | 57 | 3impa 1133 |
1
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) → (𝐴 ⊆ 𝐵 ↔ (𝐶 +𝑜 𝐴) ⊆ (𝐶 +𝑜 𝐵))) |