Proof of Theorem cantnftermord
Step | Hyp | Ref
| Expression |
1 | | simplll 774 |
. . . . . 6
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ (ω ∖
1o) ∧ 𝐷
∈ (ω ∖ 1o))) ∧ 𝐴 ∈ 𝐵) → 𝐴 ∈ On) |
2 | | onsuc 7793 |
. . . . . 6
⊢ (𝐴 ∈ On → suc 𝐴 ∈ On) |
3 | 1, 2 | syl 17 |
. . . . 5
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ (ω ∖
1o) ∧ 𝐷
∈ (ω ∖ 1o))) ∧ 𝐴 ∈ 𝐵) → suc 𝐴 ∈ On) |
4 | | simpllr 775 |
. . . . 5
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ (ω ∖
1o) ∧ 𝐷
∈ (ω ∖ 1o))) ∧ 𝐴 ∈ 𝐵) → 𝐵 ∈ On) |
5 | | omelon 9636 |
. . . . . . 7
⊢ ω
∈ On |
6 | | 1onn 8634 |
. . . . . . 7
⊢
1o ∈ ω |
7 | | ondif2 8496 |
. . . . . . 7
⊢ (ω
∈ (On ∖ 2o) ↔ (ω ∈ On ∧ 1o
∈ ω)) |
8 | 5, 6, 7 | mpbir2an 710 |
. . . . . 6
⊢ ω
∈ (On ∖ 2o) |
9 | 8 | a1i 11 |
. . . . 5
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ (ω ∖
1o) ∧ 𝐷
∈ (ω ∖ 1o))) ∧ 𝐴 ∈ 𝐵) → ω ∈ (On ∖
2o)) |
10 | | onsucss 41948 |
. . . . . . 7
⊢ (𝐵 ∈ On → (𝐴 ∈ 𝐵 → suc 𝐴 ⊆ 𝐵)) |
11 | 10 | ad2antlr 726 |
. . . . . 6
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ (ω ∖
1o) ∧ 𝐷
∈ (ω ∖ 1o))) → (𝐴 ∈ 𝐵 → suc 𝐴 ⊆ 𝐵)) |
12 | 11 | imp 408 |
. . . . 5
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ (ω ∖
1o) ∧ 𝐷
∈ (ω ∖ 1o))) ∧ 𝐴 ∈ 𝐵) → suc 𝐴 ⊆ 𝐵) |
13 | | oeword 8585 |
. . . . . 6
⊢ ((suc
𝐴 ∈ On ∧ 𝐵 ∈ On ∧ ω ∈
(On ∖ 2o)) → (suc 𝐴 ⊆ 𝐵 ↔ (ω ↑o suc
𝐴) ⊆ (ω
↑o 𝐵))) |
14 | 13 | biimpa 478 |
. . . . 5
⊢ (((suc
𝐴 ∈ On ∧ 𝐵 ∈ On ∧ ω ∈
(On ∖ 2o)) ∧ suc 𝐴 ⊆ 𝐵) → (ω ↑o suc
𝐴) ⊆ (ω
↑o 𝐵)) |
15 | 3, 4, 9, 12, 14 | syl31anc 1374 |
. . . 4
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ (ω ∖
1o) ∧ 𝐷
∈ (ω ∖ 1o))) ∧ 𝐴 ∈ 𝐵) → (ω ↑o suc
𝐴) ⊆ (ω
↑o 𝐵)) |
16 | 5 | a1i 11 |
. . . . . . . . 9
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ω
∈ On) |
17 | | oecl 8531 |
. . . . . . . . 9
⊢ ((ω
∈ On ∧ 𝐵 ∈
On) → (ω ↑o 𝐵) ∈ On) |
18 | 16, 17 | sylancom 589 |
. . . . . . . 8
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (ω
↑o 𝐵)
∈ On) |
19 | | omsson 7853 |
. . . . . . . . . . . 12
⊢ ω
⊆ On |
20 | | ssdif 4137 |
. . . . . . . . . . . 12
⊢ (ω
⊆ On → (ω ∖ 1o) ⊆ (On ∖
1o)) |
21 | 19, 20 | ax-mp 5 |
. . . . . . . . . . 11
⊢ (ω
∖ 1o) ⊆ (On ∖ 1o) |
22 | 21 | sseli 3976 |
. . . . . . . . . 10
⊢ (𝐷 ∈ (ω ∖
1o) → 𝐷
∈ (On ∖ 1o)) |
23 | | ondif1 8495 |
. . . . . . . . . 10
⊢ (𝐷 ∈ (On ∖
1o) ↔ (𝐷
∈ On ∧ ∅ ∈ 𝐷)) |
24 | 22, 23 | sylib 217 |
. . . . . . . . 9
⊢ (𝐷 ∈ (ω ∖
1o) → (𝐷
∈ On ∧ ∅ ∈ 𝐷)) |
25 | 24 | adantl 483 |
. . . . . . . 8
⊢ ((𝐶 ∈ (ω ∖
1o) ∧ 𝐷
∈ (ω ∖ 1o)) → (𝐷 ∈ On ∧ ∅ ∈ 𝐷)) |
26 | 18, 25 | anim12i 614 |
. . . . . . 7
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ (ω ∖
1o) ∧ 𝐷
∈ (ω ∖ 1o))) → ((ω ↑o
𝐵) ∈ On ∧ (𝐷 ∈ On ∧ ∅ ∈
𝐷))) |
27 | 26 | adantr 482 |
. . . . . 6
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ (ω ∖
1o) ∧ 𝐷
∈ (ω ∖ 1o))) ∧ 𝐴 ∈ 𝐵) → ((ω ↑o 𝐵) ∈ On ∧ (𝐷 ∈ On ∧ ∅ ∈
𝐷))) |
28 | | anass 470 |
. . . . . 6
⊢
((((ω ↑o 𝐵) ∈ On ∧ 𝐷 ∈ On) ∧ ∅ ∈ 𝐷) ↔ ((ω
↑o 𝐵)
∈ On ∧ (𝐷 ∈
On ∧ ∅ ∈ 𝐷))) |
29 | 27, 28 | sylibr 233 |
. . . . 5
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ (ω ∖
1o) ∧ 𝐷
∈ (ω ∖ 1o))) ∧ 𝐴 ∈ 𝐵) → (((ω ↑o 𝐵) ∈ On ∧ 𝐷 ∈ On) ∧ ∅ ∈
𝐷)) |
30 | | omword1 8568 |
. . . . 5
⊢
((((ω ↑o 𝐵) ∈ On ∧ 𝐷 ∈ On) ∧ ∅ ∈ 𝐷) → (ω
↑o 𝐵)
⊆ ((ω ↑o 𝐵) ·o 𝐷)) |
31 | 29, 30 | syl 17 |
. . . 4
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ (ω ∖
1o) ∧ 𝐷
∈ (ω ∖ 1o))) ∧ 𝐴 ∈ 𝐵) → (ω ↑o 𝐵) ⊆ ((ω
↑o 𝐵)
·o 𝐷)) |
32 | 15, 31 | sstrd 3990 |
. . 3
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ (ω ∖
1o) ∧ 𝐷
∈ (ω ∖ 1o))) ∧ 𝐴 ∈ 𝐵) → (ω ↑o suc
𝐴) ⊆ ((ω
↑o 𝐵)
·o 𝐷)) |
33 | 5 | a1i 11 |
. . . . 5
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ (ω ∖
1o) ∧ 𝐷
∈ (ω ∖ 1o))) ∧ 𝐴 ∈ 𝐵) → ω ∈ On) |
34 | 1, 5 | jctil 521 |
. . . . . 6
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ (ω ∖
1o) ∧ 𝐷
∈ (ω ∖ 1o))) ∧ 𝐴 ∈ 𝐵) → (ω ∈ On ∧ 𝐴 ∈ On)) |
35 | | oecl 8531 |
. . . . . 6
⊢ ((ω
∈ On ∧ 𝐴 ∈
On) → (ω ↑o 𝐴) ∈ On) |
36 | 34, 35 | syl 17 |
. . . . 5
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ (ω ∖
1o) ∧ 𝐷
∈ (ω ∖ 1o))) ∧ 𝐴 ∈ 𝐵) → (ω ↑o 𝐴) ∈ On) |
37 | | peano1 7873 |
. . . . . 6
⊢ ∅
∈ ω |
38 | | oen0 8581 |
. . . . . 6
⊢
(((ω ∈ On ∧ 𝐴 ∈ On) ∧ ∅ ∈ ω)
→ ∅ ∈ (ω ↑o 𝐴)) |
39 | 34, 37, 38 | sylancl 587 |
. . . . 5
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ (ω ∖
1o) ∧ 𝐷
∈ (ω ∖ 1o))) ∧ 𝐴 ∈ 𝐵) → ∅ ∈ (ω
↑o 𝐴)) |
40 | | simplrl 776 |
. . . . . 6
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ (ω ∖
1o) ∧ 𝐷
∈ (ω ∖ 1o))) ∧ 𝐴 ∈ 𝐵) → 𝐶 ∈ (ω ∖
1o)) |
41 | 40 | eldifad 3958 |
. . . . 5
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ (ω ∖
1o) ∧ 𝐷
∈ (ω ∖ 1o))) ∧ 𝐴 ∈ 𝐵) → 𝐶 ∈ ω) |
42 | | omordi 8561 |
. . . . . 6
⊢
(((ω ∈ On ∧ (ω ↑o 𝐴) ∈ On) ∧ ∅ ∈ (ω
↑o 𝐴))
→ (𝐶 ∈ ω
→ ((ω ↑o 𝐴) ·o 𝐶) ∈ ((ω ↑o 𝐴) ·o
ω))) |
43 | 42 | imp 408 |
. . . . 5
⊢
((((ω ∈ On ∧ (ω ↑o 𝐴) ∈ On) ∧ ∅
∈ (ω ↑o 𝐴)) ∧ 𝐶 ∈ ω) → ((ω
↑o 𝐴)
·o 𝐶)
∈ ((ω ↑o 𝐴) ·o
ω)) |
44 | 33, 36, 39, 41, 43 | syl1111anc 839 |
. . . 4
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ (ω ∖
1o) ∧ 𝐷
∈ (ω ∖ 1o))) ∧ 𝐴 ∈ 𝐵) → ((ω ↑o 𝐴) ·o 𝐶) ∈ ((ω
↑o 𝐴)
·o ω)) |
45 | | oesuc 8521 |
. . . . 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 2837 |
. . 3
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ (ω ∖
1o) ∧ 𝐷
∈ (ω ∖ 1o))) ∧ 𝐴 ∈ 𝐵) → ((ω ↑o 𝐴) ·o 𝐶) ∈ (ω
↑o suc 𝐴)) |
48 | 32, 47 | sseldd 3981 |
. 2
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ (ω ∖
1o) ∧ 𝐷
∈ (ω ∖ 1o))) ∧ 𝐴 ∈ 𝐵) → ((ω ↑o 𝐴) ·o 𝐶) ∈ ((ω
↑o 𝐵)
·o 𝐷)) |
49 | 48 | ex 414 |
1
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ (ω ∖
1o) ∧ 𝐷
∈ (ω ∖ 1o))) → (𝐴 ∈ 𝐵 → ((ω ↑o 𝐴) ·o 𝐶) ∈ ((ω
↑o 𝐵)
·o 𝐷))) |