Proof of Theorem oe0suclim
Step | Hyp | Ref
| Expression |
1 | | oe0 8517 |
. 2
⊢ (𝐴 ∈ On → (𝐴 ↑o ∅) =
1o) |
2 | | oesuc 8522 |
. 2
⊢ ((𝐴 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ↑o suc 𝐶) = ((𝐴 ↑o 𝐶) ·o 𝐴)) |
3 | | oelim 8529 |
. . . . 5
⊢ (((𝐴 ∈ On ∧ (𝐵 ∈ On ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) → (𝐴 ↑o 𝐵) = ∪
𝑐 ∈ 𝐵 (𝐴 ↑o 𝑐)) |
4 | | simpr 486 |
. . . . . 6
⊢ (((𝐴 ∈ On ∧ (𝐵 ∈ On ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) → ∅ ∈ 𝐴) |
5 | 4 | iftrued 4535 |
. . . . 5
⊢ (((𝐴 ∈ On ∧ (𝐵 ∈ On ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) → if(∅ ∈ 𝐴, ∪ 𝑐 ∈ 𝐵 (𝐴 ↑o 𝑐), ∅) = ∪ 𝑐 ∈ 𝐵 (𝐴 ↑o 𝑐)) |
6 | 3, 5 | eqtr4d 2776 |
. . . 4
⊢ (((𝐴 ∈ On ∧ (𝐵 ∈ On ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) → (𝐴 ↑o 𝐵) = if(∅ ∈ 𝐴, ∪ 𝑐 ∈ 𝐵 (𝐴 ↑o 𝑐), ∅)) |
7 | | simpl 484 |
. . . . . . . 8
⊢ ((𝐴 ∈ On ∧ (𝐵 ∈ On ∧ Lim 𝐵)) → 𝐴 ∈ On) |
8 | | 0elon 6415 |
. . . . . . . 8
⊢ ∅
∈ On |
9 | | ontri1 6395 |
. . . . . . . . 9
⊢ ((𝐴 ∈ On ∧ ∅ ∈
On) → (𝐴 ⊆
∅ ↔ ¬ ∅ ∈ 𝐴)) |
10 | | ss0 4397 |
. . . . . . . . 9
⊢ (𝐴 ⊆ ∅ → 𝐴 = ∅) |
11 | 9, 10 | syl6bir 254 |
. . . . . . . 8
⊢ ((𝐴 ∈ On ∧ ∅ ∈
On) → (¬ ∅ ∈ 𝐴 → 𝐴 = ∅)) |
12 | 7, 8, 11 | sylancl 587 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ (𝐵 ∈ On ∧ Lim 𝐵)) → (¬ ∅ ∈
𝐴 → 𝐴 = ∅)) |
13 | | oveq1 7411 |
. . . . . . . . 9
⊢ (𝐴 = ∅ → (𝐴 ↑o 𝐵) = (∅ ↑o
𝐵)) |
14 | | oe0m1 8516 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈ On → (∅
∈ 𝐵 ↔ (∅
↑o 𝐵) =
∅)) |
15 | 14 | biimpd 228 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ On → (∅
∈ 𝐵 → (∅
↑o 𝐵) =
∅)) |
16 | | 0ellim 6424 |
. . . . . . . . . . 11
⊢ (Lim
𝐵 → ∅ ∈
𝐵) |
17 | 15, 16 | impel 507 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ On ∧ Lim 𝐵) → (∅
↑o 𝐵) =
∅) |
18 | 17 | adantl 483 |
. . . . . . . . 9
⊢ ((𝐴 ∈ On ∧ (𝐵 ∈ On ∧ Lim 𝐵)) → (∅
↑o 𝐵) =
∅) |
19 | 13, 18 | sylan9eqr 2795 |
. . . . . . . 8
⊢ (((𝐴 ∈ On ∧ (𝐵 ∈ On ∧ Lim 𝐵)) ∧ 𝐴 = ∅) → (𝐴 ↑o 𝐵) = ∅) |
20 | 19 | ex 414 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ (𝐵 ∈ On ∧ Lim 𝐵)) → (𝐴 = ∅ → (𝐴 ↑o 𝐵) = ∅)) |
21 | 12, 20 | syld 47 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ (𝐵 ∈ On ∧ Lim 𝐵)) → (¬ ∅ ∈
𝐴 → (𝐴 ↑o 𝐵) = ∅)) |
22 | 21 | imp 408 |
. . . . 5
⊢ (((𝐴 ∈ On ∧ (𝐵 ∈ On ∧ Lim 𝐵)) ∧ ¬ ∅ ∈
𝐴) → (𝐴 ↑o 𝐵) = ∅) |
23 | | simpr 486 |
. . . . . 6
⊢ (((𝐴 ∈ On ∧ (𝐵 ∈ On ∧ Lim 𝐵)) ∧ ¬ ∅ ∈
𝐴) → ¬ ∅
∈ 𝐴) |
24 | 23 | iffalsed 4538 |
. . . . 5
⊢ (((𝐴 ∈ On ∧ (𝐵 ∈ On ∧ Lim 𝐵)) ∧ ¬ ∅ ∈
𝐴) → if(∅ ∈
𝐴, ∪ 𝑐 ∈ 𝐵 (𝐴 ↑o 𝑐), ∅) = ∅) |
25 | 22, 24 | eqtr4d 2776 |
. . . 4
⊢ (((𝐴 ∈ On ∧ (𝐵 ∈ On ∧ Lim 𝐵)) ∧ ¬ ∅ ∈
𝐴) → (𝐴 ↑o 𝐵) = if(∅ ∈ 𝐴, ∪ 𝑐 ∈ 𝐵 (𝐴 ↑o 𝑐), ∅)) |
26 | 6, 25 | pm2.61dan 812 |
. . 3
⊢ ((𝐴 ∈ On ∧ (𝐵 ∈ On ∧ Lim 𝐵)) → (𝐴 ↑o 𝐵) = if(∅ ∈ 𝐴, ∪ 𝑐 ∈ 𝐵 (𝐴 ↑o 𝑐), ∅)) |
27 | 26 | anassrs 469 |
. 2
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ Lim 𝐵) → (𝐴 ↑o 𝐵) = if(∅ ∈ 𝐴, ∪ 𝑐 ∈ 𝐵 (𝐴 ↑o 𝑐), ∅)) |
28 | 1, 2, 27 | onov0suclim 41957 |
1
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐵 = ∅ → (𝐴 ↑o 𝐵) = 1o) ∧ ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → (𝐴 ↑o 𝐵) = ((𝐴 ↑o 𝐶) ·o 𝐴)) ∧ (Lim 𝐵 → (𝐴 ↑o 𝐵) = if(∅ ∈ 𝐴, ∪ 𝑐 ∈ 𝐵 (𝐴 ↑o 𝑐), ∅)))) |