Step | Hyp | Ref
| Expression |
1 | | oveq1 7419 |
. . . . 5
⊢ (𝐴 = ∅ → (𝐴 ·o 𝑁) = (∅
·o 𝑁)) |
2 | | simp3 1137 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑁 ∈ ω) → 𝑁 ∈
ω) |
3 | | nnon 7865 |
. . . . . 6
⊢ (𝑁 ∈ ω → 𝑁 ∈ On) |
4 | | om0r 8545 |
. . . . . 6
⊢ (𝑁 ∈ On → (∅
·o 𝑁) =
∅) |
5 | 2, 3, 4 | 3syl 18 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑁 ∈ ω) → (∅
·o 𝑁) =
∅) |
6 | 1, 5 | sylan9eqr 2793 |
. . . 4
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑁 ∈ ω) ∧ 𝐴 = ∅) → (𝐴 ·o 𝑁) = ∅) |
7 | | simpl2 1191 |
. . . . . 6
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑁 ∈ ω) ∧ 𝐴 = ∅) → 𝐵 ∈ On) |
8 | | omelon 9647 |
. . . . . 6
⊢ ω
∈ On |
9 | 7, 8 | jctil 519 |
. . . . 5
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑁 ∈ ω) ∧ 𝐴 = ∅) → (ω
∈ On ∧ 𝐵 ∈
On)) |
10 | | peano1 7883 |
. . . . 5
⊢ ∅
∈ ω |
11 | | oen0 8592 |
. . . . 5
⊢
(((ω ∈ On ∧ 𝐵 ∈ On) ∧ ∅ ∈ ω)
→ ∅ ∈ (ω ↑o 𝐵)) |
12 | 9, 10, 11 | sylancl 585 |
. . . 4
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑁 ∈ ω) ∧ 𝐴 = ∅) → ∅
∈ (ω ↑o 𝐵)) |
13 | 6, 12 | eqeltrd 2832 |
. . 3
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑁 ∈ ω) ∧ 𝐴 = ∅) → (𝐴 ·o 𝑁) ∈ (ω
↑o 𝐵)) |
14 | 13 | a1d 25 |
. 2
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑁 ∈ ω) ∧ 𝐴 = ∅) → (𝐴 ∈ (ω
↑o 𝐵)
→ (𝐴
·o 𝑁)
∈ (ω ↑o 𝐵))) |
15 | 2 | adantr 480 |
. . 3
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑁 ∈ ω) ∧ ∅
∈ 𝐴) → 𝑁 ∈
ω) |
16 | | simp1 1135 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑁 ∈ ω) → 𝐴 ∈ On) |
17 | 16 | anim1i 614 |
. . . 4
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑁 ∈ ω) ∧ ∅
∈ 𝐴) → (𝐴 ∈ On ∧ ∅ ∈
𝐴)) |
18 | | ondif1 8507 |
. . . 4
⊢ (𝐴 ∈ (On ∖
1o) ↔ (𝐴
∈ On ∧ ∅ ∈ 𝐴)) |
19 | 17, 18 | sylibr 233 |
. . 3
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑁 ∈ ω) ∧ ∅
∈ 𝐴) → 𝐴 ∈ (On ∖
1o)) |
20 | | simpl2 1191 |
. . 3
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑁 ∈ ω) ∧ ∅
∈ 𝐴) → 𝐵 ∈ On) |
21 | | oveq2 7420 |
. . . . . . 7
⊢ (𝑥 = ∅ → (𝐴 ·o 𝑥) = (𝐴 ·o
∅)) |
22 | 21 | eleq1d 2817 |
. . . . . 6
⊢ (𝑥 = ∅ → ((𝐴 ·o 𝑥) ∈ (ω
↑o 𝐵)
↔ (𝐴
·o ∅) ∈ (ω ↑o 𝐵))) |
23 | 22 | imbi2d 340 |
. . . . 5
⊢ (𝑥 = ∅ → ((((𝐴 ∈ (On ∖
1o) ∧ 𝐵
∈ On) ∧ 𝐴 ∈
(ω ↑o 𝐵)) → (𝐴 ·o 𝑥) ∈ (ω ↑o 𝐵)) ↔ (((𝐴 ∈ (On ∖ 1o) ∧
𝐵 ∈ On) ∧ 𝐴 ∈ (ω
↑o 𝐵))
→ (𝐴
·o ∅) ∈ (ω ↑o 𝐵)))) |
24 | | oveq2 7420 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝐴 ·o 𝑥) = (𝐴 ·o 𝑦)) |
25 | 24 | eleq1d 2817 |
. . . . . 6
⊢ (𝑥 = 𝑦 → ((𝐴 ·o 𝑥) ∈ (ω ↑o 𝐵) ↔ (𝐴 ·o 𝑦) ∈ (ω ↑o 𝐵))) |
26 | 25 | imbi2d 340 |
. . . . 5
⊢ (𝑥 = 𝑦 → ((((𝐴 ∈ (On ∖ 1o) ∧
𝐵 ∈ On) ∧ 𝐴 ∈ (ω
↑o 𝐵))
→ (𝐴
·o 𝑥)
∈ (ω ↑o 𝐵)) ↔ (((𝐴 ∈ (On ∖ 1o) ∧
𝐵 ∈ On) ∧ 𝐴 ∈ (ω
↑o 𝐵))
→ (𝐴
·o 𝑦)
∈ (ω ↑o 𝐵)))) |
27 | | oveq2 7420 |
. . . . . . 7
⊢ (𝑥 = suc 𝑦 → (𝐴 ·o 𝑥) = (𝐴 ·o suc 𝑦)) |
28 | 27 | eleq1d 2817 |
. . . . . 6
⊢ (𝑥 = suc 𝑦 → ((𝐴 ·o 𝑥) ∈ (ω ↑o 𝐵) ↔ (𝐴 ·o suc 𝑦) ∈ (ω ↑o 𝐵))) |
29 | 28 | imbi2d 340 |
. . . . 5
⊢ (𝑥 = suc 𝑦 → ((((𝐴 ∈ (On ∖ 1o) ∧
𝐵 ∈ On) ∧ 𝐴 ∈ (ω
↑o 𝐵))
→ (𝐴
·o 𝑥)
∈ (ω ↑o 𝐵)) ↔ (((𝐴 ∈ (On ∖ 1o) ∧
𝐵 ∈ On) ∧ 𝐴 ∈ (ω
↑o 𝐵))
→ (𝐴
·o suc 𝑦)
∈ (ω ↑o 𝐵)))) |
30 | | oveq2 7420 |
. . . . . . 7
⊢ (𝑥 = 𝑁 → (𝐴 ·o 𝑥) = (𝐴 ·o 𝑁)) |
31 | 30 | eleq1d 2817 |
. . . . . 6
⊢ (𝑥 = 𝑁 → ((𝐴 ·o 𝑥) ∈ (ω ↑o 𝐵) ↔ (𝐴 ·o 𝑁) ∈ (ω ↑o 𝐵))) |
32 | 31 | imbi2d 340 |
. . . . 5
⊢ (𝑥 = 𝑁 → ((((𝐴 ∈ (On ∖ 1o) ∧
𝐵 ∈ On) ∧ 𝐴 ∈ (ω
↑o 𝐵))
→ (𝐴
·o 𝑥)
∈ (ω ↑o 𝐵)) ↔ (((𝐴 ∈ (On ∖ 1o) ∧
𝐵 ∈ On) ∧ 𝐴 ∈ (ω
↑o 𝐵))
→ (𝐴
·o 𝑁)
∈ (ω ↑o 𝐵)))) |
33 | | eldifi 4126 |
. . . . . . . . 9
⊢ (𝐴 ∈ (On ∖
1o) → 𝐴
∈ On) |
34 | | om0 8523 |
. . . . . . . . 9
⊢ (𝐴 ∈ On → (𝐴 ·o ∅) =
∅) |
35 | 33, 34 | syl 17 |
. . . . . . . 8
⊢ (𝐴 ∈ (On ∖
1o) → (𝐴
·o ∅) = ∅) |
36 | 35 | adantr 480 |
. . . . . . 7
⊢ ((𝐴 ∈ (On ∖
1o) ∧ 𝐵
∈ On) → (𝐴
·o ∅) = ∅) |
37 | 8 | jctl 523 |
. . . . . . . . 9
⊢ (𝐵 ∈ On → (ω
∈ On ∧ 𝐵 ∈
On)) |
38 | 37, 10, 11 | sylancl 585 |
. . . . . . . 8
⊢ (𝐵 ∈ On → ∅ ∈
(ω ↑o 𝐵)) |
39 | 38 | adantl 481 |
. . . . . . 7
⊢ ((𝐴 ∈ (On ∖
1o) ∧ 𝐵
∈ On) → ∅ ∈ (ω ↑o 𝐵)) |
40 | 36, 39 | eqeltrd 2832 |
. . . . . 6
⊢ ((𝐴 ∈ (On ∖
1o) ∧ 𝐵
∈ On) → (𝐴
·o ∅) ∈ (ω ↑o 𝐵)) |
41 | 40 | adantr 480 |
. . . . 5
⊢ (((𝐴 ∈ (On ∖
1o) ∧ 𝐵
∈ On) ∧ 𝐴 ∈
(ω ↑o 𝐵)) → (𝐴 ·o ∅) ∈
(ω ↑o 𝐵)) |
42 | 33 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ (On ∖
1o) ∧ 𝐵
∈ On) → 𝐴 ∈
On) |
43 | 42 | ad2antrl 725 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ω ∧ ((𝐴 ∈ (On ∖
1o) ∧ 𝐵
∈ On) ∧ 𝐴 ∈
(ω ↑o 𝐵))) → 𝐴 ∈ On) |
44 | | simpll 764 |
. . . . . . . . 9
⊢ (((𝑦 ∈ ω ∧ ((𝐴 ∈ (On ∖
1o) ∧ 𝐵
∈ On) ∧ 𝐴 ∈
(ω ↑o 𝐵))) ∧ (𝐴 ·o 𝑦) ∈ (ω ↑o 𝐵)) → 𝑦 ∈ ω) |
45 | | onmsuc 8535 |
. . . . . . . . 9
⊢ ((𝐴 ∈ On ∧ 𝑦 ∈ ω) → (𝐴 ·o suc 𝑦) = ((𝐴 ·o 𝑦) +o 𝐴)) |
46 | 43, 44, 45 | syl2an2r 682 |
. . . . . . . 8
⊢ (((𝑦 ∈ ω ∧ ((𝐴 ∈ (On ∖
1o) ∧ 𝐵
∈ On) ∧ 𝐴 ∈
(ω ↑o 𝐵))) ∧ (𝐴 ·o 𝑦) ∈ (ω ↑o 𝐵)) → (𝐴 ·o suc 𝑦) = ((𝐴 ·o 𝑦) +o 𝐴)) |
47 | | simpr 484 |
. . . . . . . . 9
⊢ (((𝑦 ∈ ω ∧ ((𝐴 ∈ (On ∖
1o) ∧ 𝐵
∈ On) ∧ 𝐴 ∈
(ω ↑o 𝐵))) ∧ (𝐴 ·o 𝑦) ∈ (ω ↑o 𝐵)) → (𝐴 ·o 𝑦) ∈ (ω ↑o 𝐵)) |
48 | | simplrr 775 |
. . . . . . . . 9
⊢ (((𝑦 ∈ ω ∧ ((𝐴 ∈ (On ∖
1o) ∧ 𝐵
∈ On) ∧ 𝐴 ∈
(ω ↑o 𝐵))) ∧ (𝐴 ·o 𝑦) ∈ (ω ↑o 𝐵)) → 𝐴 ∈ (ω ↑o 𝐵)) |
49 | | eqid 2731 |
. . . . . . . . . . . . . 14
⊢ (ω
↑o 𝐵) =
(ω ↑o 𝐵) |
50 | 49 | jctl 523 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∈ On → ((ω
↑o 𝐵) =
(ω ↑o 𝐵) ∧ 𝐵 ∈ On)) |
51 | 50 | olcd 871 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈ On → ((ω
↑o 𝐵) =
∅ ∨ ((ω ↑o 𝐵) = (ω ↑o 𝐵) ∧ 𝐵 ∈ On))) |
52 | 51 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ (On ∖
1o) ∧ 𝐵
∈ On) → ((ω ↑o 𝐵) = ∅ ∨ ((ω
↑o 𝐵) =
(ω ↑o 𝐵) ∧ 𝐵 ∈ On))) |
53 | 52 | ad2antrl 725 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ω ∧ ((𝐴 ∈ (On ∖
1o) ∧ 𝐵
∈ On) ∧ 𝐴 ∈
(ω ↑o 𝐵))) → ((ω ↑o
𝐵) = ∅ ∨ ((ω
↑o 𝐵) =
(ω ↑o 𝐵) ∧ 𝐵 ∈ On))) |
54 | 53 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑦 ∈ ω ∧ ((𝐴 ∈ (On ∖
1o) ∧ 𝐵
∈ On) ∧ 𝐴 ∈
(ω ↑o 𝐵))) ∧ (𝐴 ·o 𝑦) ∈ (ω ↑o 𝐵)) → ((ω
↑o 𝐵) =
∅ ∨ ((ω ↑o 𝐵) = (ω ↑o 𝐵) ∧ 𝐵 ∈ On))) |
55 | | oacl2g 42395 |
. . . . . . . . 9
⊢ ((((𝐴 ·o 𝑦) ∈ (ω
↑o 𝐵) ∧
𝐴 ∈ (ω
↑o 𝐵))
∧ ((ω ↑o 𝐵) = ∅ ∨ ((ω
↑o 𝐵) =
(ω ↑o 𝐵) ∧ 𝐵 ∈ On))) → ((𝐴 ·o 𝑦) +o 𝐴) ∈ (ω ↑o 𝐵)) |
56 | 47, 48, 54, 55 | syl21anc 835 |
. . . . . . . 8
⊢ (((𝑦 ∈ ω ∧ ((𝐴 ∈ (On ∖
1o) ∧ 𝐵
∈ On) ∧ 𝐴 ∈
(ω ↑o 𝐵))) ∧ (𝐴 ·o 𝑦) ∈ (ω ↑o 𝐵)) → ((𝐴 ·o 𝑦) +o 𝐴) ∈ (ω ↑o 𝐵)) |
57 | 46, 56 | eqeltrd 2832 |
. . . . . . 7
⊢ (((𝑦 ∈ ω ∧ ((𝐴 ∈ (On ∖
1o) ∧ 𝐵
∈ On) ∧ 𝐴 ∈
(ω ↑o 𝐵))) ∧ (𝐴 ·o 𝑦) ∈ (ω ↑o 𝐵)) → (𝐴 ·o suc 𝑦) ∈ (ω ↑o 𝐵)) |
58 | 57 | exp31 419 |
. . . . . 6
⊢ (𝑦 ∈ ω → (((𝐴 ∈ (On ∖
1o) ∧ 𝐵
∈ On) ∧ 𝐴 ∈
(ω ↑o 𝐵)) → ((𝐴 ·o 𝑦) ∈ (ω ↑o 𝐵) → (𝐴 ·o suc 𝑦) ∈ (ω ↑o 𝐵)))) |
59 | 58 | a2d 29 |
. . . . 5
⊢ (𝑦 ∈ ω → ((((𝐴 ∈ (On ∖
1o) ∧ 𝐵
∈ On) ∧ 𝐴 ∈
(ω ↑o 𝐵)) → (𝐴 ·o 𝑦) ∈ (ω ↑o 𝐵)) → (((𝐴 ∈ (On ∖ 1o) ∧
𝐵 ∈ On) ∧ 𝐴 ∈ (ω
↑o 𝐵))
→ (𝐴
·o suc 𝑦)
∈ (ω ↑o 𝐵)))) |
60 | 23, 26, 29, 32, 41, 59 | finds 7893 |
. . . 4
⊢ (𝑁 ∈ ω → (((𝐴 ∈ (On ∖
1o) ∧ 𝐵
∈ On) ∧ 𝐴 ∈
(ω ↑o 𝐵)) → (𝐴 ·o 𝑁) ∈ (ω ↑o 𝐵))) |
61 | 60 | expdimp 452 |
. . 3
⊢ ((𝑁 ∈ ω ∧ (𝐴 ∈ (On ∖
1o) ∧ 𝐵
∈ On)) → (𝐴
∈ (ω ↑o 𝐵) → (𝐴 ·o 𝑁) ∈ (ω ↑o 𝐵))) |
62 | 15, 19, 20, 61 | syl12anc 834 |
. 2
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑁 ∈ ω) ∧ ∅
∈ 𝐴) → (𝐴 ∈ (ω
↑o 𝐵)
→ (𝐴
·o 𝑁)
∈ (ω ↑o 𝐵))) |
63 | | on0eqel 6488 |
. . 3
⊢ (𝐴 ∈ On → (𝐴 = ∅ ∨ ∅ ∈
𝐴)) |
64 | 16, 63 | syl 17 |
. 2
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑁 ∈ ω) → (𝐴 = ∅ ∨ ∅ ∈
𝐴)) |
65 | 14, 62, 64 | mpjaodan 956 |
1
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑁 ∈ ω) → (𝐴 ∈ (ω
↑o 𝐵)
→ (𝐴
·o 𝑁)
∈ (ω ↑o 𝐵))) |