Step | Hyp | Ref
| Expression |
1 | | onelon 5748 |
. . . . 5
⊢ ((𝐵 ∈ On ∧ 𝐴 ∈ 𝐵) → 𝐴 ∈ On) |
2 | 1 | adantll 750 |
. . . 4
⊢ (((𝐶 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐴 ∈ 𝐵) → 𝐴 ∈ On) |
3 | | eloni 5733 |
. . . . . . . . 9
⊢ (𝐵 ∈ On → Ord 𝐵) |
4 | | ordsucss 7018 |
. . . . . . . . 9
⊢ (Ord
𝐵 → (𝐴 ∈ 𝐵 → suc 𝐴 ⊆ 𝐵)) |
5 | 3, 4 | syl 17 |
. . . . . . . 8
⊢ (𝐵 ∈ On → (𝐴 ∈ 𝐵 → suc 𝐴 ⊆ 𝐵)) |
6 | 5 | ad2antlr 763 |
. . . . . . 7
⊢ (((𝐶 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐴 ∈ On) → (𝐴 ∈ 𝐵 → suc 𝐴 ⊆ 𝐵)) |
7 | | sucelon 7017 |
. . . . . . . . . 10
⊢ (𝐴 ∈ On ↔ suc 𝐴 ∈ On) |
8 | | oveq2 6658 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = suc 𝐴 → (𝐶 +𝑜 𝑥) = (𝐶 +𝑜 suc 𝐴)) |
9 | 8 | sseq2d 3633 |
. . . . . . . . . . . . 13
⊢ (𝑥 = suc 𝐴 → ((𝐶 +𝑜 suc 𝐴) ⊆ (𝐶 +𝑜 𝑥) ↔ (𝐶 +𝑜 suc 𝐴) ⊆ (𝐶 +𝑜 suc 𝐴))) |
10 | 9 | imbi2d 330 |
. . . . . . . . . . . 12
⊢ (𝑥 = suc 𝐴 → ((𝐶 ∈ On → (𝐶 +𝑜 suc 𝐴) ⊆ (𝐶 +𝑜 𝑥)) ↔ (𝐶 ∈ On → (𝐶 +𝑜 suc 𝐴) ⊆ (𝐶 +𝑜 suc 𝐴)))) |
11 | | oveq2 6658 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑦 → (𝐶 +𝑜 𝑥) = (𝐶 +𝑜 𝑦)) |
12 | 11 | sseq2d 3633 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → ((𝐶 +𝑜 suc 𝐴) ⊆ (𝐶 +𝑜 𝑥) ↔ (𝐶 +𝑜 suc 𝐴) ⊆ (𝐶 +𝑜 𝑦))) |
13 | 12 | imbi2d 330 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → ((𝐶 ∈ On → (𝐶 +𝑜 suc 𝐴) ⊆ (𝐶 +𝑜 𝑥)) ↔ (𝐶 ∈ On → (𝐶 +𝑜 suc 𝐴) ⊆ (𝐶 +𝑜 𝑦)))) |
14 | | oveq2 6658 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = suc 𝑦 → (𝐶 +𝑜 𝑥) = (𝐶 +𝑜 suc 𝑦)) |
15 | 14 | sseq2d 3633 |
. . . . . . . . . . . . 13
⊢ (𝑥 = suc 𝑦 → ((𝐶 +𝑜 suc 𝐴) ⊆ (𝐶 +𝑜 𝑥) ↔ (𝐶 +𝑜 suc 𝐴) ⊆ (𝐶 +𝑜 suc 𝑦))) |
16 | 15 | imbi2d 330 |
. . . . . . . . . . . 12
⊢ (𝑥 = suc 𝑦 → ((𝐶 ∈ On → (𝐶 +𝑜 suc 𝐴) ⊆ (𝐶 +𝑜 𝑥)) ↔ (𝐶 ∈ On → (𝐶 +𝑜 suc 𝐴) ⊆ (𝐶 +𝑜 suc 𝑦)))) |
17 | | oveq2 6658 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝐵 → (𝐶 +𝑜 𝑥) = (𝐶 +𝑜 𝐵)) |
18 | 17 | sseq2d 3633 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝐵 → ((𝐶 +𝑜 suc 𝐴) ⊆ (𝐶 +𝑜 𝑥) ↔ (𝐶 +𝑜 suc 𝐴) ⊆ (𝐶 +𝑜 𝐵))) |
19 | 18 | imbi2d 330 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝐵 → ((𝐶 ∈ On → (𝐶 +𝑜 suc 𝐴) ⊆ (𝐶 +𝑜 𝑥)) ↔ (𝐶 ∈ On → (𝐶 +𝑜 suc 𝐴) ⊆ (𝐶 +𝑜 𝐵)))) |
20 | | ssid 3624 |
. . . . . . . . . . . . 13
⊢ (𝐶 +𝑜 suc 𝐴) ⊆ (𝐶 +𝑜 suc 𝐴) |
21 | 20 | 2a1i 12 |
. . . . . . . . . . . 12
⊢ (suc
𝐴 ∈ On → (𝐶 ∈ On → (𝐶 +𝑜 suc 𝐴) ⊆ (𝐶 +𝑜 suc 𝐴))) |
22 | | sssucid 5802 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐶 +𝑜 𝑦) ⊆ suc (𝐶 +𝑜 𝑦) |
23 | | sstr2 3610 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐶 +𝑜 suc 𝐴) ⊆ (𝐶 +𝑜 𝑦) → ((𝐶 +𝑜 𝑦) ⊆ suc (𝐶 +𝑜 𝑦) → (𝐶 +𝑜 suc 𝐴) ⊆ suc (𝐶 +𝑜 𝑦))) |
24 | 22, 23 | mpi 20 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐶 +𝑜 suc 𝐴) ⊆ (𝐶 +𝑜 𝑦) → (𝐶 +𝑜 suc 𝐴) ⊆ suc (𝐶 +𝑜 𝑦)) |
25 | | oasuc 7604 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐶 ∈ On ∧ 𝑦 ∈ On) → (𝐶 +𝑜 suc 𝑦) = suc (𝐶 +𝑜 𝑦)) |
26 | 25 | ancoms 469 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ On ∧ 𝐶 ∈ On) → (𝐶 +𝑜 suc 𝑦) = suc (𝐶 +𝑜 𝑦)) |
27 | 26 | sseq2d 3633 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ On ∧ 𝐶 ∈ On) → ((𝐶 +𝑜 suc 𝐴) ⊆ (𝐶 +𝑜 suc 𝑦) ↔ (𝐶 +𝑜 suc 𝐴) ⊆ suc (𝐶 +𝑜 𝑦))) |
28 | 24, 27 | syl5ibr 236 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ On ∧ 𝐶 ∈ On) → ((𝐶 +𝑜 suc 𝐴) ⊆ (𝐶 +𝑜 𝑦) → (𝐶 +𝑜 suc 𝐴) ⊆ (𝐶 +𝑜 suc 𝑦))) |
29 | 28 | ex 450 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ On → (𝐶 ∈ On → ((𝐶 +𝑜 suc 𝐴) ⊆ (𝐶 +𝑜 𝑦) → (𝐶 +𝑜 suc 𝐴) ⊆ (𝐶 +𝑜 suc 𝑦)))) |
30 | 29 | ad2antrr 762 |
. . . . . . . . . . . . 13
⊢ (((𝑦 ∈ On ∧ suc 𝐴 ∈ On) ∧ suc 𝐴 ⊆ 𝑦) → (𝐶 ∈ On → ((𝐶 +𝑜 suc 𝐴) ⊆ (𝐶 +𝑜 𝑦) → (𝐶 +𝑜 suc 𝐴) ⊆ (𝐶 +𝑜 suc 𝑦)))) |
31 | 30 | a2d 29 |
. . . . . . . . . . . 12
⊢ (((𝑦 ∈ On ∧ suc 𝐴 ∈ On) ∧ suc 𝐴 ⊆ 𝑦) → ((𝐶 ∈ On → (𝐶 +𝑜 suc 𝐴) ⊆ (𝐶 +𝑜 𝑦)) → (𝐶 ∈ On → (𝐶 +𝑜 suc 𝐴) ⊆ (𝐶 +𝑜 suc 𝑦)))) |
32 | | sucssel 5819 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐴 ∈ On → (suc 𝐴 ⊆ 𝑥 → 𝐴 ∈ 𝑥)) |
33 | 7, 32 | sylbir 225 |
. . . . . . . . . . . . . . . . . . 19
⊢ (suc
𝐴 ∈ On → (suc
𝐴 ⊆ 𝑥 → 𝐴 ∈ 𝑥)) |
34 | | limsuc 7049 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (Lim
𝑥 → (𝐴 ∈ 𝑥 ↔ suc 𝐴 ∈ 𝑥)) |
35 | 34 | biimpd 219 |
. . . . . . . . . . . . . . . . . . 19
⊢ (Lim
𝑥 → (𝐴 ∈ 𝑥 → suc 𝐴 ∈ 𝑥)) |
36 | 33, 35 | sylan9r 690 |
. . . . . . . . . . . . . . . . . 18
⊢ ((Lim
𝑥 ∧ suc 𝐴 ∈ On) → (suc 𝐴 ⊆ 𝑥 → suc 𝐴 ∈ 𝑥)) |
37 | 36 | imp 445 |
. . . . . . . . . . . . . . . . 17
⊢ (((Lim
𝑥 ∧ suc 𝐴 ∈ On) ∧ suc 𝐴 ⊆ 𝑥) → suc 𝐴 ∈ 𝑥) |
38 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = suc 𝐴 → (𝐶 +𝑜 𝑦) = (𝐶 +𝑜 suc 𝐴)) |
39 | 38 | ssiun2s 4564 |
. . . . . . . . . . . . . . . . 17
⊢ (suc
𝐴 ∈ 𝑥 → (𝐶 +𝑜 suc 𝐴) ⊆ ∪ 𝑦 ∈ 𝑥 (𝐶 +𝑜 𝑦)) |
40 | 37, 39 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((Lim
𝑥 ∧ suc 𝐴 ∈ On) ∧ suc 𝐴 ⊆ 𝑥) → (𝐶 +𝑜 suc 𝐴) ⊆ ∪ 𝑦 ∈ 𝑥 (𝐶 +𝑜 𝑦)) |
41 | 40 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((((Lim
𝑥 ∧ suc 𝐴 ∈ On) ∧ suc 𝐴 ⊆ 𝑥) ∧ 𝐶 ∈ On) → (𝐶 +𝑜 suc 𝐴) ⊆ ∪ 𝑦 ∈ 𝑥 (𝐶 +𝑜 𝑦)) |
42 | | vex 3203 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑥 ∈ V |
43 | | oalim 7612 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐶 ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)) → (𝐶 +𝑜 𝑥) = ∪ 𝑦 ∈ 𝑥 (𝐶 +𝑜 𝑦)) |
44 | 42, 43 | mpanr1 719 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐶 ∈ On ∧ Lim 𝑥) → (𝐶 +𝑜 𝑥) = ∪ 𝑦 ∈ 𝑥 (𝐶 +𝑜 𝑦)) |
45 | 44 | ancoms 469 |
. . . . . . . . . . . . . . . . 17
⊢ ((Lim
𝑥 ∧ 𝐶 ∈ On) → (𝐶 +𝑜 𝑥) = ∪ 𝑦 ∈ 𝑥 (𝐶 +𝑜 𝑦)) |
46 | 45 | adantlr 751 |
. . . . . . . . . . . . . . . 16
⊢ (((Lim
𝑥 ∧ suc 𝐴 ∈ On) ∧ 𝐶 ∈ On) → (𝐶 +𝑜 𝑥) = ∪ 𝑦 ∈ 𝑥 (𝐶 +𝑜 𝑦)) |
47 | 46 | adantlr 751 |
. . . . . . . . . . . . . . 15
⊢ ((((Lim
𝑥 ∧ suc 𝐴 ∈ On) ∧ suc 𝐴 ⊆ 𝑥) ∧ 𝐶 ∈ On) → (𝐶 +𝑜 𝑥) = ∪ 𝑦 ∈ 𝑥 (𝐶 +𝑜 𝑦)) |
48 | 41, 47 | sseqtr4d 3642 |
. . . . . . . . . . . . . 14
⊢ ((((Lim
𝑥 ∧ suc 𝐴 ∈ On) ∧ suc 𝐴 ⊆ 𝑥) ∧ 𝐶 ∈ On) → (𝐶 +𝑜 suc 𝐴) ⊆ (𝐶 +𝑜 𝑥)) |
49 | 48 | ex 450 |
. . . . . . . . . . . . 13
⊢ (((Lim
𝑥 ∧ suc 𝐴 ∈ On) ∧ suc 𝐴 ⊆ 𝑥) → (𝐶 ∈ On → (𝐶 +𝑜 suc 𝐴) ⊆ (𝐶 +𝑜 𝑥))) |
50 | 49 | a1d 25 |
. . . . . . . . . . . 12
⊢ (((Lim
𝑥 ∧ suc 𝐴 ∈ On) ∧ suc 𝐴 ⊆ 𝑥) → (∀𝑦 ∈ 𝑥 (suc 𝐴 ⊆ 𝑦 → (𝐶 ∈ On → (𝐶 +𝑜 suc 𝐴) ⊆ (𝐶 +𝑜 𝑦))) → (𝐶 ∈ On → (𝐶 +𝑜 suc 𝐴) ⊆ (𝐶 +𝑜 𝑥)))) |
51 | 10, 13, 16, 19, 21, 31, 50 | tfindsg 7060 |
. . . . . . . . . . 11
⊢ (((𝐵 ∈ On ∧ suc 𝐴 ∈ On) ∧ suc 𝐴 ⊆ 𝐵) → (𝐶 ∈ On → (𝐶 +𝑜 suc 𝐴) ⊆ (𝐶 +𝑜 𝐵))) |
52 | 51 | exp31 630 |
. . . . . . . . . 10
⊢ (𝐵 ∈ On → (suc 𝐴 ∈ On → (suc 𝐴 ⊆ 𝐵 → (𝐶 ∈ On → (𝐶 +𝑜 suc 𝐴) ⊆ (𝐶 +𝑜 𝐵))))) |
53 | 7, 52 | syl5bi 232 |
. . . . . . . . 9
⊢ (𝐵 ∈ On → (𝐴 ∈ On → (suc 𝐴 ⊆ 𝐵 → (𝐶 ∈ On → (𝐶 +𝑜 suc 𝐴) ⊆ (𝐶 +𝑜 𝐵))))) |
54 | 53 | com4r 94 |
. . . . . . . 8
⊢ (𝐶 ∈ On → (𝐵 ∈ On → (𝐴 ∈ On → (suc 𝐴 ⊆ 𝐵 → (𝐶 +𝑜 suc 𝐴) ⊆ (𝐶 +𝑜 𝐵))))) |
55 | 54 | imp31 448 |
. . . . . . 7
⊢ (((𝐶 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐴 ∈ On) → (suc 𝐴 ⊆ 𝐵 → (𝐶 +𝑜 suc 𝐴) ⊆ (𝐶 +𝑜 𝐵))) |
56 | | oasuc 7604 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ On ∧ 𝐴 ∈ On) → (𝐶 +𝑜 suc 𝐴) = suc (𝐶 +𝑜 𝐴)) |
57 | 56 | sseq1d 3632 |
. . . . . . . . 9
⊢ ((𝐶 ∈ On ∧ 𝐴 ∈ On) → ((𝐶 +𝑜 suc 𝐴) ⊆ (𝐶 +𝑜 𝐵) ↔ suc (𝐶 +𝑜 𝐴) ⊆ (𝐶 +𝑜 𝐵))) |
58 | | ovex 6678 |
. . . . . . . . . 10
⊢ (𝐶 +𝑜 𝐴) ∈ V |
59 | | sucssel 5819 |
. . . . . . . . . 10
⊢ ((𝐶 +𝑜 𝐴) ∈ V → (suc (𝐶 +𝑜 𝐴) ⊆ (𝐶 +𝑜 𝐵) → (𝐶 +𝑜 𝐴) ∈ (𝐶 +𝑜 𝐵))) |
60 | 58, 59 | ax-mp 5 |
. . . . . . . . 9
⊢ (suc
(𝐶 +𝑜
𝐴) ⊆ (𝐶 +𝑜 𝐵) → (𝐶 +𝑜 𝐴) ∈ (𝐶 +𝑜 𝐵)) |
61 | 57, 60 | syl6bi 243 |
. . . . . . . 8
⊢ ((𝐶 ∈ On ∧ 𝐴 ∈ On) → ((𝐶 +𝑜 suc 𝐴) ⊆ (𝐶 +𝑜 𝐵) → (𝐶 +𝑜 𝐴) ∈ (𝐶 +𝑜 𝐵))) |
62 | 61 | adantlr 751 |
. . . . . . 7
⊢ (((𝐶 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐴 ∈ On) → ((𝐶 +𝑜 suc 𝐴) ⊆ (𝐶 +𝑜 𝐵) → (𝐶 +𝑜 𝐴) ∈ (𝐶 +𝑜 𝐵))) |
63 | 6, 55, 62 | 3syld 60 |
. . . . . 6
⊢ (((𝐶 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐴 ∈ On) → (𝐴 ∈ 𝐵 → (𝐶 +𝑜 𝐴) ∈ (𝐶 +𝑜 𝐵))) |
64 | 63 | imp 445 |
. . . . 5
⊢ ((((𝐶 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐴 ∈ On) ∧ 𝐴 ∈ 𝐵) → (𝐶 +𝑜 𝐴) ∈ (𝐶 +𝑜 𝐵)) |
65 | 64 | an32s 846 |
. . . 4
⊢ ((((𝐶 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐴 ∈ 𝐵) ∧ 𝐴 ∈ On) → (𝐶 +𝑜 𝐴) ∈ (𝐶 +𝑜 𝐵)) |
66 | 2, 65 | mpdan 702 |
. . 3
⊢ (((𝐶 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐴 ∈ 𝐵) → (𝐶 +𝑜 𝐴) ∈ (𝐶 +𝑜 𝐵)) |
67 | 66 | ex 450 |
. 2
⊢ ((𝐶 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ∈ 𝐵 → (𝐶 +𝑜 𝐴) ∈ (𝐶 +𝑜 𝐵))) |
68 | 67 | ancoms 469 |
1
⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ∈ 𝐵 → (𝐶 +𝑜 𝐴) ∈ (𝐶 +𝑜 𝐵))) |