Step | Hyp | Ref
| Expression |
1 | | oveq2 6557 |
. . . . . . 7
⊢ (𝑥 = ∅ → (𝐴 +𝑜 𝑥) = (𝐴 +𝑜
∅)) |
2 | | oveq2 6557 |
. . . . . . 7
⊢ (𝑥 = ∅ → (𝐵 +𝑜 𝑥) = (𝐵 +𝑜
∅)) |
3 | 1, 2 | sseq12d 3597 |
. . . . . 6
⊢ (𝑥 = ∅ → ((𝐴 +𝑜 𝑥) ⊆ (𝐵 +𝑜 𝑥) ↔ (𝐴 +𝑜 ∅) ⊆
(𝐵 +𝑜
∅))) |
4 | 3 | imbi2d 329 |
. . . . 5
⊢ (𝑥 = ∅ → ((𝐴 ⊆ 𝐵 → (𝐴 +𝑜 𝑥) ⊆ (𝐵 +𝑜 𝑥)) ↔ (𝐴 ⊆ 𝐵 → (𝐴 +𝑜 ∅) ⊆
(𝐵 +𝑜
∅)))) |
5 | 4 | imbi2d 329 |
. . . 4
⊢ (𝑥 = ∅ → (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ⊆ 𝐵 → (𝐴 +𝑜 𝑥) ⊆ (𝐵 +𝑜 𝑥))) ↔ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ⊆ 𝐵 → (𝐴 +𝑜 ∅) ⊆
(𝐵 +𝑜
∅))))) |
6 | | oveq2 6557 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝐴 +𝑜 𝑥) = (𝐴 +𝑜 𝑦)) |
7 | | oveq2 6557 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝐵 +𝑜 𝑥) = (𝐵 +𝑜 𝑦)) |
8 | 6, 7 | sseq12d 3597 |
. . . . . 6
⊢ (𝑥 = 𝑦 → ((𝐴 +𝑜 𝑥) ⊆ (𝐵 +𝑜 𝑥) ↔ (𝐴 +𝑜 𝑦) ⊆ (𝐵 +𝑜 𝑦))) |
9 | 8 | imbi2d 329 |
. . . . 5
⊢ (𝑥 = 𝑦 → ((𝐴 ⊆ 𝐵 → (𝐴 +𝑜 𝑥) ⊆ (𝐵 +𝑜 𝑥)) ↔ (𝐴 ⊆ 𝐵 → (𝐴 +𝑜 𝑦) ⊆ (𝐵 +𝑜 𝑦)))) |
10 | 9 | imbi2d 329 |
. . . 4
⊢ (𝑥 = 𝑦 → (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ⊆ 𝐵 → (𝐴 +𝑜 𝑥) ⊆ (𝐵 +𝑜 𝑥))) ↔ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ⊆ 𝐵 → (𝐴 +𝑜 𝑦) ⊆ (𝐵 +𝑜 𝑦))))) |
11 | | oveq2 6557 |
. . . . . . 7
⊢ (𝑥 = suc 𝑦 → (𝐴 +𝑜 𝑥) = (𝐴 +𝑜 suc 𝑦)) |
12 | | oveq2 6557 |
. . . . . . 7
⊢ (𝑥 = suc 𝑦 → (𝐵 +𝑜 𝑥) = (𝐵 +𝑜 suc 𝑦)) |
13 | 11, 12 | sseq12d 3597 |
. . . . . 6
⊢ (𝑥 = suc 𝑦 → ((𝐴 +𝑜 𝑥) ⊆ (𝐵 +𝑜 𝑥) ↔ (𝐴 +𝑜 suc 𝑦) ⊆ (𝐵 +𝑜 suc 𝑦))) |
14 | 13 | imbi2d 329 |
. . . . 5
⊢ (𝑥 = suc 𝑦 → ((𝐴 ⊆ 𝐵 → (𝐴 +𝑜 𝑥) ⊆ (𝐵 +𝑜 𝑥)) ↔ (𝐴 ⊆ 𝐵 → (𝐴 +𝑜 suc 𝑦) ⊆ (𝐵 +𝑜 suc 𝑦)))) |
15 | 14 | imbi2d 329 |
. . . 4
⊢ (𝑥 = suc 𝑦 → (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ⊆ 𝐵 → (𝐴 +𝑜 𝑥) ⊆ (𝐵 +𝑜 𝑥))) ↔ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ⊆ 𝐵 → (𝐴 +𝑜 suc 𝑦) ⊆ (𝐵 +𝑜 suc 𝑦))))) |
16 | | oveq2 6557 |
. . . . . . 7
⊢ (𝑥 = 𝐶 → (𝐴 +𝑜 𝑥) = (𝐴 +𝑜 𝐶)) |
17 | | oveq2 6557 |
. . . . . . 7
⊢ (𝑥 = 𝐶 → (𝐵 +𝑜 𝑥) = (𝐵 +𝑜 𝐶)) |
18 | 16, 17 | sseq12d 3597 |
. . . . . 6
⊢ (𝑥 = 𝐶 → ((𝐴 +𝑜 𝑥) ⊆ (𝐵 +𝑜 𝑥) ↔ (𝐴 +𝑜 𝐶) ⊆ (𝐵 +𝑜 𝐶))) |
19 | 18 | imbi2d 329 |
. . . . 5
⊢ (𝑥 = 𝐶 → ((𝐴 ⊆ 𝐵 → (𝐴 +𝑜 𝑥) ⊆ (𝐵 +𝑜 𝑥)) ↔ (𝐴 ⊆ 𝐵 → (𝐴 +𝑜 𝐶) ⊆ (𝐵 +𝑜 𝐶)))) |
20 | 19 | imbi2d 329 |
. . . 4
⊢ (𝑥 = 𝐶 → (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ⊆ 𝐵 → (𝐴 +𝑜 𝑥) ⊆ (𝐵 +𝑜 𝑥))) ↔ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ⊆ 𝐵 → (𝐴 +𝑜 𝐶) ⊆ (𝐵 +𝑜 𝐶))))) |
21 | | nnon 6963 |
. . . . 5
⊢ (𝐴 ∈ ω → 𝐴 ∈ On) |
22 | | nnon 6963 |
. . . . 5
⊢ (𝐵 ∈ ω → 𝐵 ∈ On) |
23 | | oa0 7483 |
. . . . . . . 8
⊢ (𝐴 ∈ On → (𝐴 +𝑜 ∅)
= 𝐴) |
24 | 23 | adantr 480 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +𝑜 ∅)
= 𝐴) |
25 | | oa0 7483 |
. . . . . . . 8
⊢ (𝐵 ∈ On → (𝐵 +𝑜 ∅)
= 𝐵) |
26 | 25 | adantl 481 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐵 +𝑜 ∅)
= 𝐵) |
27 | 24, 26 | sseq12d 3597 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 +𝑜 ∅)
⊆ (𝐵
+𝑜 ∅) ↔ 𝐴 ⊆ 𝐵)) |
28 | 27 | biimprd 237 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ⊆ 𝐵 → (𝐴 +𝑜 ∅) ⊆
(𝐵 +𝑜
∅))) |
29 | 21, 22, 28 | syl2an 493 |
. . . 4
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ⊆ 𝐵 → (𝐴 +𝑜 ∅) ⊆
(𝐵 +𝑜
∅))) |
30 | | nnacl 7578 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ω ∧ 𝑦 ∈ ω) → (𝐴 +𝑜 𝑦) ∈
ω) |
31 | 30 | ancoms 468 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ω ∧ 𝐴 ∈ ω) → (𝐴 +𝑜 𝑦) ∈
ω) |
32 | 31 | adantrr 749 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ω ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) → (𝐴 +𝑜 𝑦) ∈
ω) |
33 | | nnon 6963 |
. . . . . . . . . . . 12
⊢ ((𝐴 +𝑜 𝑦) ∈ ω → (𝐴 +𝑜 𝑦) ∈ On) |
34 | | eloni 5650 |
. . . . . . . . . . . 12
⊢ ((𝐴 +𝑜 𝑦) ∈ On → Ord (𝐴 +𝑜 𝑦)) |
35 | 32, 33, 34 | 3syl 18 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ω ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) → Ord
(𝐴 +𝑜
𝑦)) |
36 | | nnacl 7578 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 ∈ ω ∧ 𝑦 ∈ ω) → (𝐵 +𝑜 𝑦) ∈
ω) |
37 | 36 | ancoms 468 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ω ∧ 𝐵 ∈ ω) → (𝐵 +𝑜 𝑦) ∈
ω) |
38 | 37 | adantrl 748 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ω ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) → (𝐵 +𝑜 𝑦) ∈
ω) |
39 | | nnon 6963 |
. . . . . . . . . . . 12
⊢ ((𝐵 +𝑜 𝑦) ∈ ω → (𝐵 +𝑜 𝑦) ∈ On) |
40 | | eloni 5650 |
. . . . . . . . . . . 12
⊢ ((𝐵 +𝑜 𝑦) ∈ On → Ord (𝐵 +𝑜 𝑦)) |
41 | 38, 39, 40 | 3syl 18 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ω ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) → Ord
(𝐵 +𝑜
𝑦)) |
42 | | ordsucsssuc 6915 |
. . . . . . . . . . 11
⊢ ((Ord
(𝐴 +𝑜
𝑦) ∧ Ord (𝐵 +𝑜 𝑦)) → ((𝐴 +𝑜 𝑦) ⊆ (𝐵 +𝑜 𝑦) ↔ suc (𝐴 +𝑜 𝑦) ⊆ suc (𝐵 +𝑜 𝑦))) |
43 | 35, 41, 42 | syl2anc 691 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ω ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) → ((𝐴 +𝑜 𝑦) ⊆ (𝐵 +𝑜 𝑦) ↔ suc (𝐴 +𝑜 𝑦) ⊆ suc (𝐵 +𝑜 𝑦))) |
44 | 43 | biimpa 500 |
. . . . . . . . 9
⊢ (((𝑦 ∈ ω ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) ∧ (𝐴 +𝑜 𝑦) ⊆ (𝐵 +𝑜 𝑦)) → suc (𝐴 +𝑜 𝑦) ⊆ suc (𝐵 +𝑜 𝑦)) |
45 | | nnasuc 7573 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ω ∧ 𝑦 ∈ ω) → (𝐴 +𝑜 suc 𝑦) = suc (𝐴 +𝑜 𝑦)) |
46 | 45 | ancoms 468 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ω ∧ 𝐴 ∈ ω) → (𝐴 +𝑜 suc 𝑦) = suc (𝐴 +𝑜 𝑦)) |
47 | 46 | adantrr 749 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ω ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) → (𝐴 +𝑜 suc 𝑦) = suc (𝐴 +𝑜 𝑦)) |
48 | | nnasuc 7573 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ ω ∧ 𝑦 ∈ ω) → (𝐵 +𝑜 suc 𝑦) = suc (𝐵 +𝑜 𝑦)) |
49 | 48 | ancoms 468 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ω ∧ 𝐵 ∈ ω) → (𝐵 +𝑜 suc 𝑦) = suc (𝐵 +𝑜 𝑦)) |
50 | 49 | adantrl 748 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ω ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) → (𝐵 +𝑜 suc 𝑦) = suc (𝐵 +𝑜 𝑦)) |
51 | 47, 50 | sseq12d 3597 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ω ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) → ((𝐴 +𝑜 suc 𝑦) ⊆ (𝐵 +𝑜 suc 𝑦) ↔ suc (𝐴 +𝑜 𝑦) ⊆ suc (𝐵 +𝑜 𝑦))) |
52 | 51 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑦 ∈ ω ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) ∧ (𝐴 +𝑜 𝑦) ⊆ (𝐵 +𝑜 𝑦)) → ((𝐴 +𝑜 suc 𝑦) ⊆ (𝐵 +𝑜 suc 𝑦) ↔ suc (𝐴 +𝑜 𝑦) ⊆ suc (𝐵 +𝑜 𝑦))) |
53 | 44, 52 | mpbird 246 |
. . . . . . . 8
⊢ (((𝑦 ∈ ω ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) ∧ (𝐴 +𝑜 𝑦) ⊆ (𝐵 +𝑜 𝑦)) → (𝐴 +𝑜 suc 𝑦) ⊆ (𝐵 +𝑜 suc 𝑦)) |
54 | 53 | ex 449 |
. . . . . . 7
⊢ ((𝑦 ∈ ω ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) → ((𝐴 +𝑜 𝑦) ⊆ (𝐵 +𝑜 𝑦) → (𝐴 +𝑜 suc 𝑦) ⊆ (𝐵 +𝑜 suc 𝑦))) |
55 | 54 | imim2d 55 |
. . . . . 6
⊢ ((𝑦 ∈ ω ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) → ((𝐴 ⊆ 𝐵 → (𝐴 +𝑜 𝑦) ⊆ (𝐵 +𝑜 𝑦)) → (𝐴 ⊆ 𝐵 → (𝐴 +𝑜 suc 𝑦) ⊆ (𝐵 +𝑜 suc 𝑦)))) |
56 | 55 | ex 449 |
. . . . 5
⊢ (𝑦 ∈ ω → ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → ((𝐴 ⊆ 𝐵 → (𝐴 +𝑜 𝑦) ⊆ (𝐵 +𝑜 𝑦)) → (𝐴 ⊆ 𝐵 → (𝐴 +𝑜 suc 𝑦) ⊆ (𝐵 +𝑜 suc 𝑦))))) |
57 | 56 | a2d 29 |
. . . 4
⊢ (𝑦 ∈ ω → (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ⊆ 𝐵 → (𝐴 +𝑜 𝑦) ⊆ (𝐵 +𝑜 𝑦))) → ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ⊆ 𝐵 → (𝐴 +𝑜 suc 𝑦) ⊆ (𝐵 +𝑜 suc 𝑦))))) |
58 | 5, 10, 15, 20, 29, 57 | finds 6984 |
. . 3
⊢ (𝐶 ∈ ω → ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ⊆ 𝐵 → (𝐴 +𝑜 𝐶) ⊆ (𝐵 +𝑜 𝐶)))) |
59 | 58 | com12 32 |
. 2
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐶 ∈ ω → (𝐴 ⊆ 𝐵 → (𝐴 +𝑜 𝐶) ⊆ (𝐵 +𝑜 𝐶)))) |
60 | 59 | 3impia 1253 |
1
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) → (𝐴 ⊆ 𝐵 → (𝐴 +𝑜 𝐶) ⊆ (𝐵 +𝑜 𝐶))) |