Step | Hyp | Ref
| Expression |
1 | | oveq2 6557 |
. . . . . . . 8
⊢ (𝐵 = ∅ → (∅
↑𝑜 𝐵) = (∅ ↑𝑜
∅)) |
2 | | oe0m0 7487 |
. . . . . . . . 9
⊢ (∅
↑𝑜 ∅) = 1𝑜 |
3 | | 1on 7454 |
. . . . . . . . 9
⊢
1𝑜 ∈ On |
4 | 2, 3 | eqeltri 2684 |
. . . . . . . 8
⊢ (∅
↑𝑜 ∅) ∈ On |
5 | 1, 4 | syl6eqel 2696 |
. . . . . . 7
⊢ (𝐵 = ∅ → (∅
↑𝑜 𝐵) ∈ On) |
6 | 5 | adantl 481 |
. . . . . 6
⊢ ((𝐵 ∈ On ∧ 𝐵 = ∅) → (∅
↑𝑜 𝐵) ∈ On) |
7 | | oe0m1 7488 |
. . . . . . . . 9
⊢ (𝐵 ∈ On → (∅
∈ 𝐵 ↔ (∅
↑𝑜 𝐵) = ∅)) |
8 | 7 | biimpa 500 |
. . . . . . . 8
⊢ ((𝐵 ∈ On ∧ ∅ ∈
𝐵) → (∅
↑𝑜 𝐵) = ∅) |
9 | | 0elon 5695 |
. . . . . . . 8
⊢ ∅
∈ On |
10 | 8, 9 | syl6eqel 2696 |
. . . . . . 7
⊢ ((𝐵 ∈ On ∧ ∅ ∈
𝐵) → (∅
↑𝑜 𝐵) ∈ On) |
11 | 10 | adantll 746 |
. . . . . 6
⊢ (((𝐵 ∈ On ∧ 𝐵 ∈ On) ∧ ∅ ∈
𝐵) → (∅
↑𝑜 𝐵) ∈ On) |
12 | 6, 11 | oe0lem 7480 |
. . . . 5
⊢ ((𝐵 ∈ On ∧ 𝐵 ∈ On) → (∅
↑𝑜 𝐵) ∈ On) |
13 | 12 | anidms 675 |
. . . 4
⊢ (𝐵 ∈ On → (∅
↑𝑜 𝐵) ∈ On) |
14 | | oveq1 6556 |
. . . . 5
⊢ (𝐴 = ∅ → (𝐴 ↑𝑜
𝐵) = (∅
↑𝑜 𝐵)) |
15 | 14 | eleq1d 2672 |
. . . 4
⊢ (𝐴 = ∅ → ((𝐴 ↑𝑜
𝐵) ∈ On ↔
(∅ ↑𝑜 𝐵) ∈ On)) |
16 | 13, 15 | syl5ibr 235 |
. . 3
⊢ (𝐴 = ∅ → (𝐵 ∈ On → (𝐴 ↑𝑜
𝐵) ∈
On)) |
17 | 16 | impcom 445 |
. 2
⊢ ((𝐵 ∈ On ∧ 𝐴 = ∅) → (𝐴 ↑𝑜
𝐵) ∈
On) |
18 | | oveq2 6557 |
. . . . . . 7
⊢ (𝑥 = ∅ → (𝐴 ↑𝑜
𝑥) = (𝐴 ↑𝑜
∅)) |
19 | 18 | eleq1d 2672 |
. . . . . 6
⊢ (𝑥 = ∅ → ((𝐴 ↑𝑜
𝑥) ∈ On ↔ (𝐴 ↑𝑜
∅) ∈ On)) |
20 | | oveq2 6557 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝐴 ↑𝑜 𝑥) = (𝐴 ↑𝑜 𝑦)) |
21 | 20 | eleq1d 2672 |
. . . . . 6
⊢ (𝑥 = 𝑦 → ((𝐴 ↑𝑜 𝑥) ∈ On ↔ (𝐴 ↑𝑜
𝑦) ∈
On)) |
22 | | oveq2 6557 |
. . . . . . 7
⊢ (𝑥 = suc 𝑦 → (𝐴 ↑𝑜 𝑥) = (𝐴 ↑𝑜 suc 𝑦)) |
23 | 22 | eleq1d 2672 |
. . . . . 6
⊢ (𝑥 = suc 𝑦 → ((𝐴 ↑𝑜 𝑥) ∈ On ↔ (𝐴 ↑𝑜 suc
𝑦) ∈
On)) |
24 | | oveq2 6557 |
. . . . . . 7
⊢ (𝑥 = 𝐵 → (𝐴 ↑𝑜 𝑥) = (𝐴 ↑𝑜 𝐵)) |
25 | 24 | eleq1d 2672 |
. . . . . 6
⊢ (𝑥 = 𝐵 → ((𝐴 ↑𝑜 𝑥) ∈ On ↔ (𝐴 ↑𝑜
𝐵) ∈
On)) |
26 | | oe0 7489 |
. . . . . . . 8
⊢ (𝐴 ∈ On → (𝐴 ↑𝑜
∅) = 1𝑜) |
27 | 26, 3 | syl6eqel 2696 |
. . . . . . 7
⊢ (𝐴 ∈ On → (𝐴 ↑𝑜
∅) ∈ On) |
28 | 27 | adantr 480 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ ∅ ∈
𝐴) → (𝐴 ↑𝑜
∅) ∈ On) |
29 | | omcl 7503 |
. . . . . . . . . . 11
⊢ (((𝐴 ↑𝑜
𝑦) ∈ On ∧ 𝐴 ∈ On) → ((𝐴 ↑𝑜
𝑦)
·𝑜 𝐴) ∈ On) |
30 | 29 | expcom 450 |
. . . . . . . . . 10
⊢ (𝐴 ∈ On → ((𝐴 ↑𝑜
𝑦) ∈ On → ((𝐴 ↑𝑜
𝑦)
·𝑜 𝐴) ∈ On)) |
31 | 30 | adantr 480 |
. . . . . . . . 9
⊢ ((𝐴 ∈ On ∧ 𝑦 ∈ On) → ((𝐴 ↑𝑜
𝑦) ∈ On → ((𝐴 ↑𝑜
𝑦)
·𝑜 𝐴) ∈ On)) |
32 | | oesuc 7494 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ On ∧ 𝑦 ∈ On) → (𝐴 ↑𝑜 suc
𝑦) = ((𝐴 ↑𝑜 𝑦) ·𝑜
𝐴)) |
33 | 32 | eleq1d 2672 |
. . . . . . . . 9
⊢ ((𝐴 ∈ On ∧ 𝑦 ∈ On) → ((𝐴 ↑𝑜 suc
𝑦) ∈ On ↔ ((𝐴 ↑𝑜
𝑦)
·𝑜 𝐴) ∈ On)) |
34 | 31, 33 | sylibrd 248 |
. . . . . . . 8
⊢ ((𝐴 ∈ On ∧ 𝑦 ∈ On) → ((𝐴 ↑𝑜
𝑦) ∈ On → (𝐴 ↑𝑜 suc
𝑦) ∈
On)) |
35 | 34 | expcom 450 |
. . . . . . 7
⊢ (𝑦 ∈ On → (𝐴 ∈ On → ((𝐴 ↑𝑜
𝑦) ∈ On → (𝐴 ↑𝑜 suc
𝑦) ∈
On))) |
36 | 35 | adantrd 483 |
. . . . . 6
⊢ (𝑦 ∈ On → ((𝐴 ∈ On ∧ ∅ ∈
𝐴) → ((𝐴 ↑𝑜
𝑦) ∈ On → (𝐴 ↑𝑜 suc
𝑦) ∈
On))) |
37 | | vex 3176 |
. . . . . . . . 9
⊢ 𝑥 ∈ V |
38 | | iunon 7323 |
. . . . . . . . 9
⊢ ((𝑥 ∈ V ∧ ∀𝑦 ∈ 𝑥 (𝐴 ↑𝑜 𝑦) ∈ On) → ∪ 𝑦 ∈ 𝑥 (𝐴 ↑𝑜 𝑦) ∈ On) |
39 | 37, 38 | mpan 702 |
. . . . . . . 8
⊢
(∀𝑦 ∈
𝑥 (𝐴 ↑𝑜 𝑦) ∈ On → ∪ 𝑦 ∈ 𝑥 (𝐴 ↑𝑜 𝑦) ∈ On) |
40 | | oelim 7501 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)) ∧ ∅ ∈ 𝐴) → (𝐴 ↑𝑜 𝑥) = ∪ 𝑦 ∈ 𝑥 (𝐴 ↑𝑜 𝑦)) |
41 | 37, 40 | mpanlr1 718 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ On ∧ Lim 𝑥) ∧ ∅ ∈ 𝐴) → (𝐴 ↑𝑜 𝑥) = ∪ 𝑦 ∈ 𝑥 (𝐴 ↑𝑜 𝑦)) |
42 | 41 | anasss 677 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ On ∧ (Lim 𝑥 ∧ ∅ ∈ 𝐴)) → (𝐴 ↑𝑜 𝑥) = ∪ 𝑦 ∈ 𝑥 (𝐴 ↑𝑜 𝑦)) |
43 | 42 | an12s 839 |
. . . . . . . . 9
⊢ ((Lim
𝑥 ∧ (𝐴 ∈ On ∧ ∅ ∈ 𝐴)) → (𝐴 ↑𝑜 𝑥) = ∪ 𝑦 ∈ 𝑥 (𝐴 ↑𝑜 𝑦)) |
44 | 43 | eleq1d 2672 |
. . . . . . . 8
⊢ ((Lim
𝑥 ∧ (𝐴 ∈ On ∧ ∅ ∈ 𝐴)) → ((𝐴 ↑𝑜 𝑥) ∈ On ↔ ∪ 𝑦 ∈ 𝑥 (𝐴 ↑𝑜 𝑦) ∈ On)) |
45 | 39, 44 | syl5ibr 235 |
. . . . . . 7
⊢ ((Lim
𝑥 ∧ (𝐴 ∈ On ∧ ∅ ∈ 𝐴)) → (∀𝑦 ∈ 𝑥 (𝐴 ↑𝑜 𝑦) ∈ On → (𝐴 ↑𝑜
𝑥) ∈
On)) |
46 | 45 | ex 449 |
. . . . . 6
⊢ (Lim
𝑥 → ((𝐴 ∈ On ∧ ∅ ∈
𝐴) → (∀𝑦 ∈ 𝑥 (𝐴 ↑𝑜 𝑦) ∈ On → (𝐴 ↑𝑜
𝑥) ∈
On))) |
47 | 19, 21, 23, 25, 28, 36, 46 | tfinds3 6956 |
. . . . 5
⊢ (𝐵 ∈ On → ((𝐴 ∈ On ∧ ∅ ∈
𝐴) → (𝐴 ↑𝑜
𝐵) ∈
On)) |
48 | 47 | expd 451 |
. . . 4
⊢ (𝐵 ∈ On → (𝐴 ∈ On → (∅
∈ 𝐴 → (𝐴 ↑𝑜
𝐵) ∈
On))) |
49 | 48 | com12 32 |
. . 3
⊢ (𝐴 ∈ On → (𝐵 ∈ On → (∅
∈ 𝐴 → (𝐴 ↑𝑜
𝐵) ∈
On))) |
50 | 49 | imp31 447 |
. 2
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ ∅ ∈
𝐴) → (𝐴 ↑𝑜
𝐵) ∈
On) |
51 | 17, 50 | oe0lem 7480 |
1
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ↑𝑜
𝐵) ∈
On) |