Step | Hyp | Ref
| Expression |
1 | | oveq2 5540 |
. . . . . . . . 9
⊢ (𝑥 = 𝐶 → (𝐴 +𝑜 𝑥) = (𝐴 +𝑜 𝐶)) |
2 | | oveq2 5540 |
. . . . . . . . 9
⊢ (𝑥 = 𝐶 → (𝐵 +𝑜 𝑥) = (𝐵 +𝑜 𝐶)) |
3 | 1, 2 | eleq12d 2149 |
. . . . . . . 8
⊢ (𝑥 = 𝐶 → ((𝐴 +𝑜 𝑥) ∈ (𝐵 +𝑜 𝑥) ↔ (𝐴 +𝑜 𝐶) ∈ (𝐵 +𝑜 𝐶))) |
4 | 3 | imbi2d 228 |
. . . . . . 7
⊢ (𝑥 = 𝐶 → (((𝐵 ∈ ω ∧ 𝐴 ∈ 𝐵) → (𝐴 +𝑜 𝑥) ∈ (𝐵 +𝑜 𝑥)) ↔ ((𝐵 ∈ ω ∧ 𝐴 ∈ 𝐵) → (𝐴 +𝑜 𝐶) ∈ (𝐵 +𝑜 𝐶)))) |
5 | | oveq2 5540 |
. . . . . . . . 9
⊢ (𝑥 = ∅ → (𝐴 +𝑜 𝑥) = (𝐴 +𝑜
∅)) |
6 | | oveq2 5540 |
. . . . . . . . 9
⊢ (𝑥 = ∅ → (𝐵 +𝑜 𝑥) = (𝐵 +𝑜
∅)) |
7 | 5, 6 | eleq12d 2149 |
. . . . . . . 8
⊢ (𝑥 = ∅ → ((𝐴 +𝑜 𝑥) ∈ (𝐵 +𝑜 𝑥) ↔ (𝐴 +𝑜 ∅) ∈
(𝐵 +𝑜
∅))) |
8 | | oveq2 5540 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝐴 +𝑜 𝑥) = (𝐴 +𝑜 𝑦)) |
9 | | oveq2 5540 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝐵 +𝑜 𝑥) = (𝐵 +𝑜 𝑦)) |
10 | 8, 9 | eleq12d 2149 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → ((𝐴 +𝑜 𝑥) ∈ (𝐵 +𝑜 𝑥) ↔ (𝐴 +𝑜 𝑦) ∈ (𝐵 +𝑜 𝑦))) |
11 | | oveq2 5540 |
. . . . . . . . 9
⊢ (𝑥 = suc 𝑦 → (𝐴 +𝑜 𝑥) = (𝐴 +𝑜 suc 𝑦)) |
12 | | oveq2 5540 |
. . . . . . . . 9
⊢ (𝑥 = suc 𝑦 → (𝐵 +𝑜 𝑥) = (𝐵 +𝑜 suc 𝑦)) |
13 | 11, 12 | eleq12d 2149 |
. . . . . . . 8
⊢ (𝑥 = suc 𝑦 → ((𝐴 +𝑜 𝑥) ∈ (𝐵 +𝑜 𝑥) ↔ (𝐴 +𝑜 suc 𝑦) ∈ (𝐵 +𝑜 suc 𝑦))) |
14 | | simpr 108 |
. . . . . . . . 9
⊢ ((𝐵 ∈ ω ∧ 𝐴 ∈ 𝐵) → 𝐴 ∈ 𝐵) |
15 | | elnn 4346 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ ω) → 𝐴 ∈ ω) |
16 | 15 | ancoms 264 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ ω ∧ 𝐴 ∈ 𝐵) → 𝐴 ∈ ω) |
17 | | nna0 6076 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ω → (𝐴 +𝑜 ∅)
= 𝐴) |
18 | 16, 17 | syl 14 |
. . . . . . . . 9
⊢ ((𝐵 ∈ ω ∧ 𝐴 ∈ 𝐵) → (𝐴 +𝑜 ∅) = 𝐴) |
19 | | nna0 6076 |
. . . . . . . . . 10
⊢ (𝐵 ∈ ω → (𝐵 +𝑜 ∅)
= 𝐵) |
20 | 19 | adantr 270 |
. . . . . . . . 9
⊢ ((𝐵 ∈ ω ∧ 𝐴 ∈ 𝐵) → (𝐵 +𝑜 ∅) = 𝐵) |
21 | 14, 18, 20 | 3eltr4d 2162 |
. . . . . . . 8
⊢ ((𝐵 ∈ ω ∧ 𝐴 ∈ 𝐵) → (𝐴 +𝑜 ∅) ∈
(𝐵 +𝑜
∅)) |
22 | | simprl 497 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ω ∧ (𝐵 ∈ ω ∧ 𝐴 ∈ 𝐵)) → 𝐵 ∈ ω) |
23 | | simpl 107 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ω ∧ (𝐵 ∈ ω ∧ 𝐴 ∈ 𝐵)) → 𝑦 ∈ ω) |
24 | | nnacl 6082 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ ω ∧ 𝑦 ∈ ω) → (𝐵 +𝑜 𝑦) ∈
ω) |
25 | 22, 23, 24 | syl2anc 403 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ω ∧ (𝐵 ∈ ω ∧ 𝐴 ∈ 𝐵)) → (𝐵 +𝑜 𝑦) ∈ ω) |
26 | | nnsucelsuc 6093 |
. . . . . . . . . . . 12
⊢ ((𝐵 +𝑜 𝑦) ∈ ω → ((𝐴 +𝑜 𝑦) ∈ (𝐵 +𝑜 𝑦) ↔ suc (𝐴 +𝑜 𝑦) ∈ suc (𝐵 +𝑜 𝑦))) |
27 | 25, 26 | syl 14 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ω ∧ (𝐵 ∈ ω ∧ 𝐴 ∈ 𝐵)) → ((𝐴 +𝑜 𝑦) ∈ (𝐵 +𝑜 𝑦) ↔ suc (𝐴 +𝑜 𝑦) ∈ suc (𝐵 +𝑜 𝑦))) |
28 | 16 | adantl 271 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ω ∧ (𝐵 ∈ ω ∧ 𝐴 ∈ 𝐵)) → 𝐴 ∈ ω) |
29 | | nnon 4350 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ω → 𝐴 ∈ On) |
30 | 28, 29 | syl 14 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ω ∧ (𝐵 ∈ ω ∧ 𝐴 ∈ 𝐵)) → 𝐴 ∈ On) |
31 | | nnon 4350 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ω → 𝑦 ∈ On) |
32 | 31 | adantr 270 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ω ∧ (𝐵 ∈ ω ∧ 𝐴 ∈ 𝐵)) → 𝑦 ∈ On) |
33 | | oasuc 6067 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ On ∧ 𝑦 ∈ On) → (𝐴 +𝑜 suc 𝑦) = suc (𝐴 +𝑜 𝑦)) |
34 | 30, 32, 33 | syl2anc 403 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ω ∧ (𝐵 ∈ ω ∧ 𝐴 ∈ 𝐵)) → (𝐴 +𝑜 suc 𝑦) = suc (𝐴 +𝑜 𝑦)) |
35 | | nnon 4350 |
. . . . . . . . . . . . . 14
⊢ (𝐵 ∈ ω → 𝐵 ∈ On) |
36 | 35 | ad2antrl 473 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ω ∧ (𝐵 ∈ ω ∧ 𝐴 ∈ 𝐵)) → 𝐵 ∈ On) |
37 | | oasuc 6067 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐵 +𝑜 suc 𝑦) = suc (𝐵 +𝑜 𝑦)) |
38 | 36, 32, 37 | syl2anc 403 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ω ∧ (𝐵 ∈ ω ∧ 𝐴 ∈ 𝐵)) → (𝐵 +𝑜 suc 𝑦) = suc (𝐵 +𝑜 𝑦)) |
39 | 34, 38 | eleq12d 2149 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ω ∧ (𝐵 ∈ ω ∧ 𝐴 ∈ 𝐵)) → ((𝐴 +𝑜 suc 𝑦) ∈ (𝐵 +𝑜 suc 𝑦) ↔ suc (𝐴 +𝑜 𝑦) ∈ suc (𝐵 +𝑜 𝑦))) |
40 | 27, 39 | bitr4d 189 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ω ∧ (𝐵 ∈ ω ∧ 𝐴 ∈ 𝐵)) → ((𝐴 +𝑜 𝑦) ∈ (𝐵 +𝑜 𝑦) ↔ (𝐴 +𝑜 suc 𝑦) ∈ (𝐵 +𝑜 suc 𝑦))) |
41 | 40 | biimpd 142 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ω ∧ (𝐵 ∈ ω ∧ 𝐴 ∈ 𝐵)) → ((𝐴 +𝑜 𝑦) ∈ (𝐵 +𝑜 𝑦) → (𝐴 +𝑜 suc 𝑦) ∈ (𝐵 +𝑜 suc 𝑦))) |
42 | 41 | ex 113 |
. . . . . . . 8
⊢ (𝑦 ∈ ω → ((𝐵 ∈ ω ∧ 𝐴 ∈ 𝐵) → ((𝐴 +𝑜 𝑦) ∈ (𝐵 +𝑜 𝑦) → (𝐴 +𝑜 suc 𝑦) ∈ (𝐵 +𝑜 suc 𝑦)))) |
43 | 7, 10, 13, 21, 42 | finds2 4342 |
. . . . . . 7
⊢ (𝑥 ∈ ω → ((𝐵 ∈ ω ∧ 𝐴 ∈ 𝐵) → (𝐴 +𝑜 𝑥) ∈ (𝐵 +𝑜 𝑥))) |
44 | 4, 43 | vtoclga 2664 |
. . . . . 6
⊢ (𝐶 ∈ ω → ((𝐵 ∈ ω ∧ 𝐴 ∈ 𝐵) → (𝐴 +𝑜 𝐶) ∈ (𝐵 +𝑜 𝐶))) |
45 | 44 | imp 122 |
. . . . 5
⊢ ((𝐶 ∈ ω ∧ (𝐵 ∈ ω ∧ 𝐴 ∈ 𝐵)) → (𝐴 +𝑜 𝐶) ∈ (𝐵 +𝑜 𝐶)) |
46 | 16 | adantl 271 |
. . . . . 6
⊢ ((𝐶 ∈ ω ∧ (𝐵 ∈ ω ∧ 𝐴 ∈ 𝐵)) → 𝐴 ∈ ω) |
47 | | simpl 107 |
. . . . . 6
⊢ ((𝐶 ∈ ω ∧ (𝐵 ∈ ω ∧ 𝐴 ∈ 𝐵)) → 𝐶 ∈ ω) |
48 | | nnacom 6086 |
. . . . . 6
⊢ ((𝐴 ∈ ω ∧ 𝐶 ∈ ω) → (𝐴 +𝑜 𝐶) = (𝐶 +𝑜 𝐴)) |
49 | 46, 47, 48 | syl2anc 403 |
. . . . 5
⊢ ((𝐶 ∈ ω ∧ (𝐵 ∈ ω ∧ 𝐴 ∈ 𝐵)) → (𝐴 +𝑜 𝐶) = (𝐶 +𝑜 𝐴)) |
50 | | nnacom 6086 |
. . . . . . 7
⊢ ((𝐵 ∈ ω ∧ 𝐶 ∈ ω) → (𝐵 +𝑜 𝐶) = (𝐶 +𝑜 𝐵)) |
51 | 50 | ancoms 264 |
. . . . . 6
⊢ ((𝐶 ∈ ω ∧ 𝐵 ∈ ω) → (𝐵 +𝑜 𝐶) = (𝐶 +𝑜 𝐵)) |
52 | 51 | adantrr 462 |
. . . . 5
⊢ ((𝐶 ∈ ω ∧ (𝐵 ∈ ω ∧ 𝐴 ∈ 𝐵)) → (𝐵 +𝑜 𝐶) = (𝐶 +𝑜 𝐵)) |
53 | 45, 49, 52 | 3eltr3d 2161 |
. . . 4
⊢ ((𝐶 ∈ ω ∧ (𝐵 ∈ ω ∧ 𝐴 ∈ 𝐵)) → (𝐶 +𝑜 𝐴) ∈ (𝐶 +𝑜 𝐵)) |
54 | 53 | 3impb 1134 |
. . 3
⊢ ((𝐶 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐴 ∈ 𝐵) → (𝐶 +𝑜 𝐴) ∈ (𝐶 +𝑜 𝐵)) |
55 | 54 | 3com12 1142 |
. 2
⊢ ((𝐵 ∈ ω ∧ 𝐶 ∈ ω ∧ 𝐴 ∈ 𝐵) → (𝐶 +𝑜 𝐴) ∈ (𝐶 +𝑜 𝐵)) |
56 | 55 | 3expia 1140 |
1
⊢ ((𝐵 ∈ ω ∧ 𝐶 ∈ ω) → (𝐴 ∈ 𝐵 → (𝐶 +𝑜 𝐴) ∈ (𝐶 +𝑜 𝐵))) |