Step | Hyp | Ref
| Expression |
1 | | oveq2 6658 |
. . . . . 6
⊢ (𝑥 = ∅ → (𝐴 ↑𝑜
𝑥) = (𝐴 ↑𝑜
∅)) |
2 | 1 | eleq2d 2687 |
. . . . 5
⊢ (𝑥 = ∅ → (∅
∈ (𝐴
↑𝑜 𝑥) ↔ ∅ ∈ (𝐴 ↑𝑜
∅))) |
3 | | oveq2 6658 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝐴 ↑𝑜 𝑥) = (𝐴 ↑𝑜 𝑦)) |
4 | 3 | eleq2d 2687 |
. . . . 5
⊢ (𝑥 = 𝑦 → (∅ ∈ (𝐴 ↑𝑜 𝑥) ↔ ∅ ∈ (𝐴 ↑𝑜
𝑦))) |
5 | | oveq2 6658 |
. . . . . 6
⊢ (𝑥 = suc 𝑦 → (𝐴 ↑𝑜 𝑥) = (𝐴 ↑𝑜 suc 𝑦)) |
6 | 5 | eleq2d 2687 |
. . . . 5
⊢ (𝑥 = suc 𝑦 → (∅ ∈ (𝐴 ↑𝑜 𝑥) ↔ ∅ ∈ (𝐴 ↑𝑜 suc
𝑦))) |
7 | | oveq2 6658 |
. . . . . 6
⊢ (𝑥 = 𝐵 → (𝐴 ↑𝑜 𝑥) = (𝐴 ↑𝑜 𝐵)) |
8 | 7 | eleq2d 2687 |
. . . . 5
⊢ (𝑥 = 𝐵 → (∅ ∈ (𝐴 ↑𝑜 𝑥) ↔ ∅ ∈ (𝐴 ↑𝑜
𝐵))) |
9 | | 0lt1o 7584 |
. . . . . . 7
⊢ ∅
∈ 1𝑜 |
10 | | oe0 7602 |
. . . . . . 7
⊢ (𝐴 ∈ On → (𝐴 ↑𝑜
∅) = 1𝑜) |
11 | 9, 10 | syl5eleqr 2708 |
. . . . . 6
⊢ (𝐴 ∈ On → ∅ ∈
(𝐴
↑𝑜 ∅)) |
12 | 11 | adantr 481 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ ∅ ∈
𝐴) → ∅ ∈
(𝐴
↑𝑜 ∅)) |
13 | | simpl 473 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ On ∧ 𝑦 ∈ On) → 𝐴 ∈ On) |
14 | | oecl 7617 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ On ∧ 𝑦 ∈ On) → (𝐴 ↑𝑜
𝑦) ∈
On) |
15 | 13, 14 | jca 554 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ On ∧ 𝑦 ∈ On) → (𝐴 ∈ On ∧ (𝐴 ↑𝑜
𝑦) ∈
On)) |
16 | | omordi 7646 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ On ∧ (𝐴 ↑𝑜
𝑦) ∈ On) ∧ ∅
∈ (𝐴
↑𝑜 𝑦)) → (∅ ∈ 𝐴 → ((𝐴 ↑𝑜 𝑦) ·𝑜
∅) ∈ ((𝐴
↑𝑜 𝑦) ·𝑜 𝐴))) |
17 | | om0 7597 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ↑𝑜
𝑦) ∈ On → ((𝐴 ↑𝑜
𝑦)
·𝑜 ∅) = ∅) |
18 | 17 | eleq1d 2686 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ↑𝑜
𝑦) ∈ On →
(((𝐴
↑𝑜 𝑦) ·𝑜 ∅)
∈ ((𝐴
↑𝑜 𝑦) ·𝑜 𝐴) ↔ ∅ ∈ ((𝐴 ↑𝑜
𝑦)
·𝑜 𝐴))) |
19 | 18 | ad2antlr 763 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ On ∧ (𝐴 ↑𝑜
𝑦) ∈ On) ∧ ∅
∈ (𝐴
↑𝑜 𝑦)) → (((𝐴 ↑𝑜 𝑦) ·𝑜
∅) ∈ ((𝐴
↑𝑜 𝑦) ·𝑜 𝐴) ↔ ∅ ∈ ((𝐴 ↑𝑜
𝑦)
·𝑜 𝐴))) |
20 | 16, 19 | sylibd 229 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ On ∧ (𝐴 ↑𝑜
𝑦) ∈ On) ∧ ∅
∈ (𝐴
↑𝑜 𝑦)) → (∅ ∈ 𝐴 → ∅ ∈ ((𝐴 ↑𝑜 𝑦) ·𝑜
𝐴))) |
21 | 15, 20 | sylan 488 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ On ∧ 𝑦 ∈ On) ∧ ∅ ∈
(𝐴
↑𝑜 𝑦)) → (∅ ∈ 𝐴 → ∅ ∈ ((𝐴 ↑𝑜 𝑦) ·𝑜
𝐴))) |
22 | | oesuc 7607 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ On ∧ 𝑦 ∈ On) → (𝐴 ↑𝑜 suc
𝑦) = ((𝐴 ↑𝑜 𝑦) ·𝑜
𝐴)) |
23 | 22 | eleq2d 2687 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ On ∧ 𝑦 ∈ On) → (∅
∈ (𝐴
↑𝑜 suc 𝑦) ↔ ∅ ∈ ((𝐴 ↑𝑜 𝑦) ·𝑜
𝐴))) |
24 | 23 | adantr 481 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ On ∧ 𝑦 ∈ On) ∧ ∅ ∈
(𝐴
↑𝑜 𝑦)) → (∅ ∈ (𝐴 ↑𝑜 suc 𝑦) ↔ ∅ ∈ ((𝐴 ↑𝑜
𝑦)
·𝑜 𝐴))) |
25 | 21, 24 | sylibrd 249 |
. . . . . . . . 9
⊢ (((𝐴 ∈ On ∧ 𝑦 ∈ On) ∧ ∅ ∈
(𝐴
↑𝑜 𝑦)) → (∅ ∈ 𝐴 → ∅ ∈ (𝐴 ↑𝑜 suc 𝑦))) |
26 | 25 | exp31 630 |
. . . . . . . 8
⊢ (𝐴 ∈ On → (𝑦 ∈ On → (∅
∈ (𝐴
↑𝑜 𝑦) → (∅ ∈ 𝐴 → ∅ ∈ (𝐴 ↑𝑜 suc 𝑦))))) |
27 | 26 | com12 32 |
. . . . . . 7
⊢ (𝑦 ∈ On → (𝐴 ∈ On → (∅
∈ (𝐴
↑𝑜 𝑦) → (∅ ∈ 𝐴 → ∅ ∈ (𝐴 ↑𝑜 suc 𝑦))))) |
28 | 27 | com34 91 |
. . . . . 6
⊢ (𝑦 ∈ On → (𝐴 ∈ On → (∅
∈ 𝐴 → (∅
∈ (𝐴
↑𝑜 𝑦) → ∅ ∈ (𝐴 ↑𝑜 suc 𝑦))))) |
29 | 28 | impd 447 |
. . . . 5
⊢ (𝑦 ∈ On → ((𝐴 ∈ On ∧ ∅ ∈
𝐴) → (∅ ∈
(𝐴
↑𝑜 𝑦) → ∅ ∈ (𝐴 ↑𝑜 suc 𝑦)))) |
30 | | 0ellim 5787 |
. . . . . . . . . . . 12
⊢ (Lim
𝑥 → ∅ ∈
𝑥) |
31 | | eqimss2 3658 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ↑𝑜
∅) = 1𝑜 → 1𝑜 ⊆ (𝐴 ↑𝑜
∅)) |
32 | 10, 31 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ On →
1𝑜 ⊆ (𝐴 ↑𝑜
∅)) |
33 | | oveq2 6658 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = ∅ → (𝐴 ↑𝑜
𝑦) = (𝐴 ↑𝑜
∅)) |
34 | 33 | sseq2d 3633 |
. . . . . . . . . . . . 13
⊢ (𝑦 = ∅ →
(1𝑜 ⊆ (𝐴 ↑𝑜 𝑦) ↔ 1𝑜
⊆ (𝐴
↑𝑜 ∅))) |
35 | 34 | rspcev 3309 |
. . . . . . . . . . . 12
⊢ ((∅
∈ 𝑥 ∧
1𝑜 ⊆ (𝐴 ↑𝑜 ∅)) →
∃𝑦 ∈ 𝑥 1𝑜 ⊆
(𝐴
↑𝑜 𝑦)) |
36 | 30, 32, 35 | syl2an 494 |
. . . . . . . . . . 11
⊢ ((Lim
𝑥 ∧ 𝐴 ∈ On) → ∃𝑦 ∈ 𝑥 1𝑜 ⊆ (𝐴 ↑𝑜
𝑦)) |
37 | | ssiun 4562 |
. . . . . . . . . . 11
⊢
(∃𝑦 ∈
𝑥 1𝑜
⊆ (𝐴
↑𝑜 𝑦) → 1𝑜 ⊆
∪ 𝑦 ∈ 𝑥 (𝐴 ↑𝑜 𝑦)) |
38 | 36, 37 | syl 17 |
. . . . . . . . . 10
⊢ ((Lim
𝑥 ∧ 𝐴 ∈ On) → 1𝑜
⊆ ∪ 𝑦 ∈ 𝑥 (𝐴 ↑𝑜 𝑦)) |
39 | 38 | adantrr 753 |
. . . . . . . . 9
⊢ ((Lim
𝑥 ∧ (𝐴 ∈ On ∧ ∅ ∈ 𝐴)) → 1𝑜
⊆ ∪ 𝑦 ∈ 𝑥 (𝐴 ↑𝑜 𝑦)) |
40 | | vex 3203 |
. . . . . . . . . . . 12
⊢ 𝑥 ∈ V |
41 | | oelim 7614 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)) ∧ ∅ ∈ 𝐴) → (𝐴 ↑𝑜 𝑥) = ∪ 𝑦 ∈ 𝑥 (𝐴 ↑𝑜 𝑦)) |
42 | 40, 41 | mpanlr1 722 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ On ∧ Lim 𝑥) ∧ ∅ ∈ 𝐴) → (𝐴 ↑𝑜 𝑥) = ∪ 𝑦 ∈ 𝑥 (𝐴 ↑𝑜 𝑦)) |
43 | 42 | anasss 679 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ On ∧ (Lim 𝑥 ∧ ∅ ∈ 𝐴)) → (𝐴 ↑𝑜 𝑥) = ∪ 𝑦 ∈ 𝑥 (𝐴 ↑𝑜 𝑦)) |
44 | 43 | an12s 843 |
. . . . . . . . 9
⊢ ((Lim
𝑥 ∧ (𝐴 ∈ On ∧ ∅ ∈ 𝐴)) → (𝐴 ↑𝑜 𝑥) = ∪ 𝑦 ∈ 𝑥 (𝐴 ↑𝑜 𝑦)) |
45 | 39, 44 | sseqtr4d 3642 |
. . . . . . . 8
⊢ ((Lim
𝑥 ∧ (𝐴 ∈ On ∧ ∅ ∈ 𝐴)) → 1𝑜
⊆ (𝐴
↑𝑜 𝑥)) |
46 | | limelon 5788 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ V ∧ Lim 𝑥) → 𝑥 ∈ On) |
47 | 40, 46 | mpan 706 |
. . . . . . . . . . 11
⊢ (Lim
𝑥 → 𝑥 ∈ On) |
48 | | oecl 7617 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ On) → (𝐴 ↑𝑜
𝑥) ∈
On) |
49 | 48 | ancoms 469 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ On ∧ 𝐴 ∈ On) → (𝐴 ↑𝑜
𝑥) ∈
On) |
50 | 47, 49 | sylan 488 |
. . . . . . . . . 10
⊢ ((Lim
𝑥 ∧ 𝐴 ∈ On) → (𝐴 ↑𝑜 𝑥) ∈ On) |
51 | | eloni 5733 |
. . . . . . . . . 10
⊢ ((𝐴 ↑𝑜
𝑥) ∈ On → Ord
(𝐴
↑𝑜 𝑥)) |
52 | | ordgt0ge1 7577 |
. . . . . . . . . 10
⊢ (Ord
(𝐴
↑𝑜 𝑥) → (∅ ∈ (𝐴 ↑𝑜 𝑥) ↔ 1𝑜
⊆ (𝐴
↑𝑜 𝑥))) |
53 | 50, 51, 52 | 3syl 18 |
. . . . . . . . 9
⊢ ((Lim
𝑥 ∧ 𝐴 ∈ On) → (∅ ∈ (𝐴 ↑𝑜
𝑥) ↔
1𝑜 ⊆ (𝐴 ↑𝑜 𝑥))) |
54 | 53 | adantrr 753 |
. . . . . . . 8
⊢ ((Lim
𝑥 ∧ (𝐴 ∈ On ∧ ∅ ∈ 𝐴)) → (∅ ∈ (𝐴 ↑𝑜
𝑥) ↔
1𝑜 ⊆ (𝐴 ↑𝑜 𝑥))) |
55 | 45, 54 | mpbird 247 |
. . . . . . 7
⊢ ((Lim
𝑥 ∧ (𝐴 ∈ On ∧ ∅ ∈ 𝐴)) → ∅ ∈ (𝐴 ↑𝑜
𝑥)) |
56 | 55 | ex 450 |
. . . . . 6
⊢ (Lim
𝑥 → ((𝐴 ∈ On ∧ ∅ ∈
𝐴) → ∅ ∈
(𝐴
↑𝑜 𝑥))) |
57 | 56 | a1dd 50 |
. . . . 5
⊢ (Lim
𝑥 → ((𝐴 ∈ On ∧ ∅ ∈
𝐴) → (∀𝑦 ∈ 𝑥 ∅ ∈ (𝐴 ↑𝑜 𝑦) → ∅ ∈ (𝐴 ↑𝑜
𝑥)))) |
58 | 2, 4, 6, 8, 12, 29, 57 | tfinds3 7064 |
. . . 4
⊢ (𝐵 ∈ On → ((𝐴 ∈ On ∧ ∅ ∈
𝐴) → ∅ ∈
(𝐴
↑𝑜 𝐵))) |
59 | 58 | expd 452 |
. . 3
⊢ (𝐵 ∈ On → (𝐴 ∈ On → (∅
∈ 𝐴 → ∅
∈ (𝐴
↑𝑜 𝐵)))) |
60 | 59 | com12 32 |
. 2
⊢ (𝐴 ∈ On → (𝐵 ∈ On → (∅
∈ 𝐴 → ∅
∈ (𝐴
↑𝑜 𝐵)))) |
61 | 60 | imp31 448 |
1
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ ∅ ∈
𝐴) → ∅ ∈
(𝐴
↑𝑜 𝐵)) |