Proof of Theorem cantnftermord
| Step | Hyp | Ref
| Expression |
| 1 | | simplll 775 |
. . . . . 6
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ (ω ∖
1o) ∧ 𝐷
∈ (ω ∖ 1o))) ∧ 𝐴 ∈ 𝐵) → 𝐴 ∈ On) |
| 2 | | onsuc 7831 |
. . . . . 6
⊢ (𝐴 ∈ On → suc 𝐴 ∈ On) |
| 3 | 1, 2 | syl 17 |
. . . . 5
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ (ω ∖
1o) ∧ 𝐷
∈ (ω ∖ 1o))) ∧ 𝐴 ∈ 𝐵) → suc 𝐴 ∈ On) |
| 4 | | simpllr 776 |
. . . . 5
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ (ω ∖
1o) ∧ 𝐷
∈ (ω ∖ 1o))) ∧ 𝐴 ∈ 𝐵) → 𝐵 ∈ On) |
| 5 | | omelon 9686 |
. . . . . . 7
⊢ ω
∈ On |
| 6 | | 1onn 8678 |
. . . . . . 7
⊢
1o ∈ ω |
| 7 | | ondif2 8540 |
. . . . . . 7
⊢ (ω
∈ (On ∖ 2o) ↔ (ω ∈ On ∧ 1o
∈ ω)) |
| 8 | 5, 6, 7 | mpbir2an 711 |
. . . . . 6
⊢ ω
∈ (On ∖ 2o) |
| 9 | 8 | a1i 11 |
. . . . 5
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ (ω ∖
1o) ∧ 𝐷
∈ (ω ∖ 1o))) ∧ 𝐴 ∈ 𝐵) → ω ∈ (On ∖
2o)) |
| 10 | | onsucss 43279 |
. . . . . . 7
⊢ (𝐵 ∈ On → (𝐴 ∈ 𝐵 → suc 𝐴 ⊆ 𝐵)) |
| 11 | 10 | ad2antlr 727 |
. . . . . 6
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ (ω ∖
1o) ∧ 𝐷
∈ (ω ∖ 1o))) → (𝐴 ∈ 𝐵 → suc 𝐴 ⊆ 𝐵)) |
| 12 | 11 | imp 406 |
. . . . 5
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ (ω ∖
1o) ∧ 𝐷
∈ (ω ∖ 1o))) ∧ 𝐴 ∈ 𝐵) → suc 𝐴 ⊆ 𝐵) |
| 13 | | oeword 8628 |
. . . . . 6
⊢ ((suc
𝐴 ∈ On ∧ 𝐵 ∈ On ∧ ω ∈
(On ∖ 2o)) → (suc 𝐴 ⊆ 𝐵 ↔ (ω ↑o suc
𝐴) ⊆ (ω
↑o 𝐵))) |
| 14 | 13 | biimpa 476 |
. . . . 5
⊢ (((suc
𝐴 ∈ On ∧ 𝐵 ∈ On ∧ ω ∈
(On ∖ 2o)) ∧ suc 𝐴 ⊆ 𝐵) → (ω ↑o suc
𝐴) ⊆ (ω
↑o 𝐵)) |
| 15 | 3, 4, 9, 12, 14 | syl31anc 1375 |
. . . 4
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ (ω ∖
1o) ∧ 𝐷
∈ (ω ∖ 1o))) ∧ 𝐴 ∈ 𝐵) → (ω ↑o suc
𝐴) ⊆ (ω
↑o 𝐵)) |
| 16 | 5 | a1i 11 |
. . . . . . . . 9
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ω
∈ On) |
| 17 | | oecl 8575 |
. . . . . . . . 9
⊢ ((ω
∈ On ∧ 𝐵 ∈
On) → (ω ↑o 𝐵) ∈ On) |
| 18 | 16, 17 | sylancom 588 |
. . . . . . . 8
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (ω
↑o 𝐵)
∈ On) |
| 19 | | omsson 7891 |
. . . . . . . . . . . 12
⊢ ω
⊆ On |
| 20 | | ssdif 4144 |
. . . . . . . . . . . 12
⊢ (ω
⊆ On → (ω ∖ 1o) ⊆ (On ∖
1o)) |
| 21 | 19, 20 | ax-mp 5 |
. . . . . . . . . . 11
⊢ (ω
∖ 1o) ⊆ (On ∖ 1o) |
| 22 | 21 | sseli 3979 |
. . . . . . . . . 10
⊢ (𝐷 ∈ (ω ∖
1o) → 𝐷
∈ (On ∖ 1o)) |
| 23 | | ondif1 8539 |
. . . . . . . . . 10
⊢ (𝐷 ∈ (On ∖
1o) ↔ (𝐷
∈ On ∧ ∅ ∈ 𝐷)) |
| 24 | 22, 23 | sylib 218 |
. . . . . . . . 9
⊢ (𝐷 ∈ (ω ∖
1o) → (𝐷
∈ On ∧ ∅ ∈ 𝐷)) |
| 25 | 24 | adantl 481 |
. . . . . . . 8
⊢ ((𝐶 ∈ (ω ∖
1o) ∧ 𝐷
∈ (ω ∖ 1o)) → (𝐷 ∈ On ∧ ∅ ∈ 𝐷)) |
| 26 | 18, 25 | anim12i 613 |
. . . . . . 7
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ (ω ∖
1o) ∧ 𝐷
∈ (ω ∖ 1o))) → ((ω ↑o
𝐵) ∈ On ∧ (𝐷 ∈ On ∧ ∅ ∈
𝐷))) |
| 27 | 26 | adantr 480 |
. . . . . 6
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ (ω ∖
1o) ∧ 𝐷
∈ (ω ∖ 1o))) ∧ 𝐴 ∈ 𝐵) → ((ω ↑o 𝐵) ∈ On ∧ (𝐷 ∈ On ∧ ∅ ∈
𝐷))) |
| 28 | | anass 468 |
. . . . . 6
⊢
((((ω ↑o 𝐵) ∈ On ∧ 𝐷 ∈ On) ∧ ∅ ∈ 𝐷) ↔ ((ω
↑o 𝐵)
∈ On ∧ (𝐷 ∈
On ∧ ∅ ∈ 𝐷))) |
| 29 | 27, 28 | sylibr 234 |
. . . . 5
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ (ω ∖
1o) ∧ 𝐷
∈ (ω ∖ 1o))) ∧ 𝐴 ∈ 𝐵) → (((ω ↑o 𝐵) ∈ On ∧ 𝐷 ∈ On) ∧ ∅ ∈
𝐷)) |
| 30 | | omword1 8611 |
. . . . 5
⊢
((((ω ↑o 𝐵) ∈ On ∧ 𝐷 ∈ On) ∧ ∅ ∈ 𝐷) → (ω
↑o 𝐵)
⊆ ((ω ↑o 𝐵) ·o 𝐷)) |
| 31 | 29, 30 | syl 17 |
. . . 4
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ (ω ∖
1o) ∧ 𝐷
∈ (ω ∖ 1o))) ∧ 𝐴 ∈ 𝐵) → (ω ↑o 𝐵) ⊆ ((ω
↑o 𝐵)
·o 𝐷)) |
| 32 | 15, 31 | sstrd 3994 |
. . 3
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ (ω ∖
1o) ∧ 𝐷
∈ (ω ∖ 1o))) ∧ 𝐴 ∈ 𝐵) → (ω ↑o suc
𝐴) ⊆ ((ω
↑o 𝐵)
·o 𝐷)) |
| 33 | 5 | a1i 11 |
. . . . 5
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ (ω ∖
1o) ∧ 𝐷
∈ (ω ∖ 1o))) ∧ 𝐴 ∈ 𝐵) → ω ∈ On) |
| 34 | 1, 5 | jctil 519 |
. . . . . 6
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ (ω ∖
1o) ∧ 𝐷
∈ (ω ∖ 1o))) ∧ 𝐴 ∈ 𝐵) → (ω ∈ On ∧ 𝐴 ∈ On)) |
| 35 | | oecl 8575 |
. . . . . 6
⊢ ((ω
∈ On ∧ 𝐴 ∈
On) → (ω ↑o 𝐴) ∈ On) |
| 36 | 34, 35 | syl 17 |
. . . . 5
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ (ω ∖
1o) ∧ 𝐷
∈ (ω ∖ 1o))) ∧ 𝐴 ∈ 𝐵) → (ω ↑o 𝐴) ∈ On) |
| 37 | | peano1 7910 |
. . . . . 6
⊢ ∅
∈ ω |
| 38 | | oen0 8624 |
. . . . . 6
⊢
(((ω ∈ On ∧ 𝐴 ∈ On) ∧ ∅ ∈ ω)
→ ∅ ∈ (ω ↑o 𝐴)) |
| 39 | 34, 37, 38 | sylancl 586 |
. . . . 5
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ (ω ∖
1o) ∧ 𝐷
∈ (ω ∖ 1o))) ∧ 𝐴 ∈ 𝐵) → ∅ ∈ (ω
↑o 𝐴)) |
| 40 | | simplrl 777 |
. . . . . 6
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ (ω ∖
1o) ∧ 𝐷
∈ (ω ∖ 1o))) ∧ 𝐴 ∈ 𝐵) → 𝐶 ∈ (ω ∖
1o)) |
| 41 | 40 | eldifad 3963 |
. . . . 5
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ (ω ∖
1o) ∧ 𝐷
∈ (ω ∖ 1o))) ∧ 𝐴 ∈ 𝐵) → 𝐶 ∈ ω) |
| 42 | | omordi 8604 |
. . . . . 6
⊢
(((ω ∈ On ∧ (ω ↑o 𝐴) ∈ On) ∧ ∅ ∈ (ω
↑o 𝐴))
→ (𝐶 ∈ ω
→ ((ω ↑o 𝐴) ·o 𝐶) ∈ ((ω ↑o 𝐴) ·o
ω))) |
| 43 | 42 | imp 406 |
. . . . 5
⊢
((((ω ∈ On ∧ (ω ↑o 𝐴) ∈ On) ∧ ∅
∈ (ω ↑o 𝐴)) ∧ 𝐶 ∈ ω) → ((ω
↑o 𝐴)
·o 𝐶)
∈ ((ω ↑o 𝐴) ·o
ω)) |
| 44 | 33, 36, 39, 41, 43 | syl1111anc 841 |
. . . 4
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ (ω ∖
1o) ∧ 𝐷
∈ (ω ∖ 1o))) ∧ 𝐴 ∈ 𝐵) → ((ω ↑o 𝐴) ·o 𝐶) ∈ ((ω
↑o 𝐴)
·o ω)) |
| 45 | | oesuc 8565 |
. . . . 5
⊢ ((ω
∈ On ∧ 𝐴 ∈
On) → (ω ↑o suc 𝐴) = ((ω ↑o 𝐴) ·o
ω)) |
| 46 | 34, 45 | syl 17 |
. . . 4
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ (ω ∖
1o) ∧ 𝐷
∈ (ω ∖ 1o))) ∧ 𝐴 ∈ 𝐵) → (ω ↑o suc
𝐴) = ((ω
↑o 𝐴)
·o ω)) |
| 47 | 44, 46 | eleqtrrd 2844 |
. . 3
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ (ω ∖
1o) ∧ 𝐷
∈ (ω ∖ 1o))) ∧ 𝐴 ∈ 𝐵) → ((ω ↑o 𝐴) ·o 𝐶) ∈ (ω
↑o suc 𝐴)) |
| 48 | 32, 47 | sseldd 3984 |
. 2
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ (ω ∖
1o) ∧ 𝐷
∈ (ω ∖ 1o))) ∧ 𝐴 ∈ 𝐵) → ((ω ↑o 𝐴) ·o 𝐶) ∈ ((ω
↑o 𝐵)
·o 𝐷)) |
| 49 | 48 | ex 412 |
1
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ (ω ∖
1o) ∧ 𝐷
∈ (ω ∖ 1o))) → (𝐴 ∈ 𝐵 → ((ω ↑o 𝐴) ·o 𝐶) ∈ ((ω
↑o 𝐵)
·o 𝐷))) |