| Step | Hyp | Ref
| Expression |
| 1 | | limelon 6448 |
. . 3
⊢ ((𝐵 ∈ 𝐶 ∧ Lim 𝐵) → 𝐵 ∈ On) |
| 2 | | oacl 8573 |
. . . 4
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +o 𝐵) ∈ On) |
| 3 | | eloni 6394 |
. . . 4
⊢ ((𝐴 +o 𝐵) ∈ On → Ord (𝐴 +o 𝐵)) |
| 4 | 2, 3 | syl 17 |
. . 3
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → Ord (𝐴 +o 𝐵)) |
| 5 | 1, 4 | sylan2 593 |
. 2
⊢ ((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) → Ord (𝐴 +o 𝐵)) |
| 6 | | 0ellim 6447 |
. . . . . 6
⊢ (Lim
𝐵 → ∅ ∈
𝐵) |
| 7 | | n0i 4340 |
. . . . . 6
⊢ (∅
∈ 𝐵 → ¬ 𝐵 = ∅) |
| 8 | 6, 7 | syl 17 |
. . . . 5
⊢ (Lim
𝐵 → ¬ 𝐵 = ∅) |
| 9 | 8 | ad2antll 729 |
. . . 4
⊢ ((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) → ¬ 𝐵 = ∅) |
| 10 | | oa00 8597 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 +o 𝐵) = ∅ ↔ (𝐴 = ∅ ∧ 𝐵 = ∅))) |
| 11 | | simpr 484 |
. . . . . . 7
⊢ ((𝐴 = ∅ ∧ 𝐵 = ∅) → 𝐵 = ∅) |
| 12 | 10, 11 | biimtrdi 253 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 +o 𝐵) = ∅ → 𝐵 = ∅)) |
| 13 | 12 | con3d 152 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (¬ 𝐵 = ∅ → ¬ (𝐴 +o 𝐵) = ∅)) |
| 14 | 1, 13 | sylan2 593 |
. . . 4
⊢ ((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) → (¬ 𝐵 = ∅ → ¬ (𝐴 +o 𝐵) = ∅)) |
| 15 | 9, 14 | mpd 15 |
. . 3
⊢ ((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) → ¬ (𝐴 +o 𝐵) = ∅) |
| 16 | | vex 3484 |
. . . . . . . . . . 11
⊢ 𝑦 ∈ V |
| 17 | 16 | sucid 6466 |
. . . . . . . . . 10
⊢ 𝑦 ∈ suc 𝑦 |
| 18 | | oalim 8570 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) → (𝐴 +o 𝐵) = ∪
𝑥 ∈ 𝐵 (𝐴 +o 𝑥)) |
| 19 | | eqeq1 2741 |
. . . . . . . . . . . 12
⊢ ((𝐴 +o 𝐵) = suc 𝑦 → ((𝐴 +o 𝐵) = ∪
𝑥 ∈ 𝐵 (𝐴 +o 𝑥) ↔ suc 𝑦 = ∪ 𝑥 ∈ 𝐵 (𝐴 +o 𝑥))) |
| 20 | 18, 19 | imbitrid 244 |
. . . . . . . . . . 11
⊢ ((𝐴 +o 𝐵) = suc 𝑦 → ((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) → suc 𝑦 = ∪ 𝑥 ∈ 𝐵 (𝐴 +o 𝑥))) |
| 21 | 20 | imp 406 |
. . . . . . . . . 10
⊢ (((𝐴 +o 𝐵) = suc 𝑦 ∧ (𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵))) → suc 𝑦 = ∪ 𝑥 ∈ 𝐵 (𝐴 +o 𝑥)) |
| 22 | 17, 21 | eleqtrid 2847 |
. . . . . . . . 9
⊢ (((𝐴 +o 𝐵) = suc 𝑦 ∧ (𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵))) → 𝑦 ∈ ∪
𝑥 ∈ 𝐵 (𝐴 +o 𝑥)) |
| 23 | | eliun 4995 |
. . . . . . . . 9
⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐵 (𝐴 +o 𝑥) ↔ ∃𝑥 ∈ 𝐵 𝑦 ∈ (𝐴 +o 𝑥)) |
| 24 | 22, 23 | sylib 218 |
. . . . . . . 8
⊢ (((𝐴 +o 𝐵) = suc 𝑦 ∧ (𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵))) → ∃𝑥 ∈ 𝐵 𝑦 ∈ (𝐴 +o 𝑥)) |
| 25 | | onelon 6409 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐵 ∈ On ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ On) |
| 26 | 1, 25 | sylan 580 |
. . . . . . . . . . . . . . 15
⊢ (((𝐵 ∈ 𝐶 ∧ Lim 𝐵) ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ On) |
| 27 | | onnbtwn 6478 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ On → ¬ (𝑥 ∈ 𝐵 ∧ 𝐵 ∈ suc 𝑥)) |
| 28 | | imnan 399 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ 𝐵 → ¬ 𝐵 ∈ suc 𝑥) ↔ ¬ (𝑥 ∈ 𝐵 ∧ 𝐵 ∈ suc 𝑥)) |
| 29 | 27, 28 | sylibr 234 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ On → (𝑥 ∈ 𝐵 → ¬ 𝐵 ∈ suc 𝑥)) |
| 30 | 29 | com12 32 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ 𝐵 → (𝑥 ∈ On → ¬ 𝐵 ∈ suc 𝑥)) |
| 31 | 30 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝐵 ∈ 𝐶 ∧ Lim 𝐵) ∧ 𝑥 ∈ 𝐵) → (𝑥 ∈ On → ¬ 𝐵 ∈ suc 𝑥)) |
| 32 | 26, 31 | mpd 15 |
. . . . . . . . . . . . . 14
⊢ (((𝐵 ∈ 𝐶 ∧ Lim 𝐵) ∧ 𝑥 ∈ 𝐵) → ¬ 𝐵 ∈ suc 𝑥) |
| 33 | 32 | ad2antrl 728 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ On ∧ (((𝐵 ∈ 𝐶 ∧ Lim 𝐵) ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ (𝐴 +o 𝑥))) → ¬ 𝐵 ∈ suc 𝑥) |
| 34 | | oacl 8573 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ On) → (𝐴 +o 𝑥) ∈ On) |
| 35 | | eloni 6394 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 +o 𝑥) ∈ On → Ord (𝐴 +o 𝑥)) |
| 36 | | ordsucelsuc 7842 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (Ord
(𝐴 +o 𝑥) → (𝑦 ∈ (𝐴 +o 𝑥) ↔ suc 𝑦 ∈ suc (𝐴 +o 𝑥))) |
| 37 | 34, 35, 36 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ On) → (𝑦 ∈ (𝐴 +o 𝑥) ↔ suc 𝑦 ∈ suc (𝐴 +o 𝑥))) |
| 38 | | oasuc 8562 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ On) → (𝐴 +o suc 𝑥) = suc (𝐴 +o 𝑥)) |
| 39 | 38 | eleq2d 2827 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ On) → (suc 𝑦 ∈ (𝐴 +o suc 𝑥) ↔ suc 𝑦 ∈ suc (𝐴 +o 𝑥))) |
| 40 | 37, 39 | bitr4d 282 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ On) → (𝑦 ∈ (𝐴 +o 𝑥) ↔ suc 𝑦 ∈ (𝐴 +o suc 𝑥))) |
| 41 | 26, 40 | sylan2 593 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ On ∧ ((𝐵 ∈ 𝐶 ∧ Lim 𝐵) ∧ 𝑥 ∈ 𝐵)) → (𝑦 ∈ (𝐴 +o 𝑥) ↔ suc 𝑦 ∈ (𝐴 +o suc 𝑥))) |
| 42 | | eleq1 2829 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 +o 𝐵) = suc 𝑦 → ((𝐴 +o 𝐵) ∈ (𝐴 +o suc 𝑥) ↔ suc 𝑦 ∈ (𝐴 +o suc 𝑥))) |
| 43 | 42 | bicomd 223 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 +o 𝐵) = suc 𝑦 → (suc 𝑦 ∈ (𝐴 +o suc 𝑥) ↔ (𝐴 +o 𝐵) ∈ (𝐴 +o suc 𝑥))) |
| 44 | 41, 43 | sylan9bbr 510 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 +o 𝐵) = suc 𝑦 ∧ (𝐴 ∈ On ∧ ((𝐵 ∈ 𝐶 ∧ Lim 𝐵) ∧ 𝑥 ∈ 𝐵))) → (𝑦 ∈ (𝐴 +o 𝑥) ↔ (𝐴 +o 𝐵) ∈ (𝐴 +o suc 𝑥))) |
| 45 | 1 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐵 ∈ 𝐶 ∧ Lim 𝐵) ∧ 𝑥 ∈ 𝐵) → 𝐵 ∈ On) |
| 46 | | onsucb 7837 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 ∈ On ↔ suc 𝑥 ∈ On) |
| 47 | 26, 46 | sylib 218 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐵 ∈ 𝐶 ∧ Lim 𝐵) ∧ 𝑥 ∈ 𝐵) → suc 𝑥 ∈ On) |
| 48 | 45, 47 | jca 511 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐵 ∈ 𝐶 ∧ Lim 𝐵) ∧ 𝑥 ∈ 𝐵) → (𝐵 ∈ On ∧ suc 𝑥 ∈ On)) |
| 49 | | oaord 8585 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐵 ∈ On ∧ suc 𝑥 ∈ On ∧ 𝐴 ∈ On) → (𝐵 ∈ suc 𝑥 ↔ (𝐴 +o 𝐵) ∈ (𝐴 +o suc 𝑥))) |
| 50 | 49 | 3expa 1119 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐵 ∈ On ∧ suc 𝑥 ∈ On) ∧ 𝐴 ∈ On) → (𝐵 ∈ suc 𝑥 ↔ (𝐴 +o 𝐵) ∈ (𝐴 +o suc 𝑥))) |
| 51 | 48, 50 | sylan 580 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐵 ∈ 𝐶 ∧ Lim 𝐵) ∧ 𝑥 ∈ 𝐵) ∧ 𝐴 ∈ On) → (𝐵 ∈ suc 𝑥 ↔ (𝐴 +o 𝐵) ∈ (𝐴 +o suc 𝑥))) |
| 52 | 51 | ancoms 458 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ On ∧ ((𝐵 ∈ 𝐶 ∧ Lim 𝐵) ∧ 𝑥 ∈ 𝐵)) → (𝐵 ∈ suc 𝑥 ↔ (𝐴 +o 𝐵) ∈ (𝐴 +o suc 𝑥))) |
| 53 | 52 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 +o 𝐵) = suc 𝑦 ∧ (𝐴 ∈ On ∧ ((𝐵 ∈ 𝐶 ∧ Lim 𝐵) ∧ 𝑥 ∈ 𝐵))) → (𝐵 ∈ suc 𝑥 ↔ (𝐴 +o 𝐵) ∈ (𝐴 +o suc 𝑥))) |
| 54 | 44, 53 | bitr4d 282 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 +o 𝐵) = suc 𝑦 ∧ (𝐴 ∈ On ∧ ((𝐵 ∈ 𝐶 ∧ Lim 𝐵) ∧ 𝑥 ∈ 𝐵))) → (𝑦 ∈ (𝐴 +o 𝑥) ↔ 𝐵 ∈ suc 𝑥)) |
| 55 | 54 | biimpd 229 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 +o 𝐵) = suc 𝑦 ∧ (𝐴 ∈ On ∧ ((𝐵 ∈ 𝐶 ∧ Lim 𝐵) ∧ 𝑥 ∈ 𝐵))) → (𝑦 ∈ (𝐴 +o 𝑥) → 𝐵 ∈ suc 𝑥)) |
| 56 | 55 | exp32 420 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 +o 𝐵) = suc 𝑦 → (𝐴 ∈ On → (((𝐵 ∈ 𝐶 ∧ Lim 𝐵) ∧ 𝑥 ∈ 𝐵) → (𝑦 ∈ (𝐴 +o 𝑥) → 𝐵 ∈ suc 𝑥)))) |
| 57 | 56 | com4l 92 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ On → (((𝐵 ∈ 𝐶 ∧ Lim 𝐵) ∧ 𝑥 ∈ 𝐵) → (𝑦 ∈ (𝐴 +o 𝑥) → ((𝐴 +o 𝐵) = suc 𝑦 → 𝐵 ∈ suc 𝑥)))) |
| 58 | 57 | imp32 418 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ On ∧ (((𝐵 ∈ 𝐶 ∧ Lim 𝐵) ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ (𝐴 +o 𝑥))) → ((𝐴 +o 𝐵) = suc 𝑦 → 𝐵 ∈ suc 𝑥)) |
| 59 | 33, 58 | mtod 198 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ On ∧ (((𝐵 ∈ 𝐶 ∧ Lim 𝐵) ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ (𝐴 +o 𝑥))) → ¬ (𝐴 +o 𝐵) = suc 𝑦) |
| 60 | 59 | exp44 437 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ On → ((𝐵 ∈ 𝐶 ∧ Lim 𝐵) → (𝑥 ∈ 𝐵 → (𝑦 ∈ (𝐴 +o 𝑥) → ¬ (𝐴 +o 𝐵) = suc 𝑦)))) |
| 61 | 60 | imp 406 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) → (𝑥 ∈ 𝐵 → (𝑦 ∈ (𝐴 +o 𝑥) → ¬ (𝐴 +o 𝐵) = suc 𝑦))) |
| 62 | 61 | rexlimdv 3153 |
. . . . . . . . 9
⊢ ((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) → (∃𝑥 ∈ 𝐵 𝑦 ∈ (𝐴 +o 𝑥) → ¬ (𝐴 +o 𝐵) = suc 𝑦)) |
| 63 | 62 | adantl 481 |
. . . . . . . 8
⊢ (((𝐴 +o 𝐵) = suc 𝑦 ∧ (𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵))) → (∃𝑥 ∈ 𝐵 𝑦 ∈ (𝐴 +o 𝑥) → ¬ (𝐴 +o 𝐵) = suc 𝑦)) |
| 64 | 24, 63 | mpd 15 |
. . . . . . 7
⊢ (((𝐴 +o 𝐵) = suc 𝑦 ∧ (𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵))) → ¬ (𝐴 +o 𝐵) = suc 𝑦) |
| 65 | 64 | expcom 413 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) → ((𝐴 +o 𝐵) = suc 𝑦 → ¬ (𝐴 +o 𝐵) = suc 𝑦)) |
| 66 | 65 | pm2.01d 190 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) → ¬ (𝐴 +o 𝐵) = suc 𝑦) |
| 67 | 66 | adantr 480 |
. . . 4
⊢ (((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) ∧ 𝑦 ∈ On) → ¬ (𝐴 +o 𝐵) = suc 𝑦) |
| 68 | 67 | nrexdv 3149 |
. . 3
⊢ ((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) → ¬ ∃𝑦 ∈ On (𝐴 +o 𝐵) = suc 𝑦) |
| 69 | | ioran 986 |
. . 3
⊢ (¬
((𝐴 +o 𝐵) = ∅ ∨ ∃𝑦 ∈ On (𝐴 +o 𝐵) = suc 𝑦) ↔ (¬ (𝐴 +o 𝐵) = ∅ ∧ ¬ ∃𝑦 ∈ On (𝐴 +o 𝐵) = suc 𝑦)) |
| 70 | 15, 68, 69 | sylanbrc 583 |
. 2
⊢ ((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) → ¬ ((𝐴 +o 𝐵) = ∅ ∨ ∃𝑦 ∈ On (𝐴 +o 𝐵) = suc 𝑦)) |
| 71 | | dflim3 7868 |
. 2
⊢ (Lim
(𝐴 +o 𝐵) ↔ (Ord (𝐴 +o 𝐵) ∧ ¬ ((𝐴 +o 𝐵) = ∅ ∨ ∃𝑦 ∈ On (𝐴 +o 𝐵) = suc 𝑦))) |
| 72 | 5, 70, 71 | sylanbrc 583 |
1
⊢ ((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) → Lim (𝐴 +o 𝐵)) |