| Step | Hyp | Ref
| Expression |
| 1 | | oveq2 7439 |
. . . . . 6
⊢ (𝑥 = ∅ → (𝐴 ↑o 𝑥) = (𝐴 ↑o
∅)) |
| 2 | 1 | eleq2d 2827 |
. . . . 5
⊢ (𝑥 = ∅ → (∅
∈ (𝐴
↑o 𝑥)
↔ ∅ ∈ (𝐴
↑o ∅))) |
| 3 | | oveq2 7439 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝐴 ↑o 𝑥) = (𝐴 ↑o 𝑦)) |
| 4 | 3 | eleq2d 2827 |
. . . . 5
⊢ (𝑥 = 𝑦 → (∅ ∈ (𝐴 ↑o 𝑥) ↔ ∅ ∈ (𝐴 ↑o 𝑦))) |
| 5 | | oveq2 7439 |
. . . . . 6
⊢ (𝑥 = suc 𝑦 → (𝐴 ↑o 𝑥) = (𝐴 ↑o suc 𝑦)) |
| 6 | 5 | eleq2d 2827 |
. . . . 5
⊢ (𝑥 = suc 𝑦 → (∅ ∈ (𝐴 ↑o 𝑥) ↔ ∅ ∈ (𝐴 ↑o suc 𝑦))) |
| 7 | | oveq2 7439 |
. . . . . 6
⊢ (𝑥 = 𝐵 → (𝐴 ↑o 𝑥) = (𝐴 ↑o 𝐵)) |
| 8 | 7 | eleq2d 2827 |
. . . . 5
⊢ (𝑥 = 𝐵 → (∅ ∈ (𝐴 ↑o 𝑥) ↔ ∅ ∈ (𝐴 ↑o 𝐵))) |
| 9 | | 0lt1o 8542 |
. . . . . . 7
⊢ ∅
∈ 1o |
| 10 | | oe0 8560 |
. . . . . . 7
⊢ (𝐴 ∈ On → (𝐴 ↑o ∅) =
1o) |
| 11 | 9, 10 | eleqtrrid 2848 |
. . . . . 6
⊢ (𝐴 ∈ On → ∅ ∈
(𝐴 ↑o
∅)) |
| 12 | 11 | adantr 480 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ ∅ ∈
𝐴) → ∅ ∈
(𝐴 ↑o
∅)) |
| 13 | | oecl 8575 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ On ∧ 𝑦 ∈ On) → (𝐴 ↑o 𝑦) ∈ On) |
| 14 | | omordi 8604 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ On ∧ (𝐴 ↑o 𝑦) ∈ On) ∧ ∅
∈ (𝐴
↑o 𝑦))
→ (∅ ∈ 𝐴
→ ((𝐴
↑o 𝑦)
·o ∅) ∈ ((𝐴 ↑o 𝑦) ·o 𝐴))) |
| 15 | | om0 8555 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ↑o 𝑦) ∈ On → ((𝐴 ↑o 𝑦) ·o ∅)
= ∅) |
| 16 | 15 | eleq1d 2826 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ↑o 𝑦) ∈ On → (((𝐴 ↑o 𝑦) ·o ∅)
∈ ((𝐴
↑o 𝑦)
·o 𝐴)
↔ ∅ ∈ ((𝐴
↑o 𝑦)
·o 𝐴))) |
| 17 | 16 | ad2antlr 727 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ On ∧ (𝐴 ↑o 𝑦) ∈ On) ∧ ∅
∈ (𝐴
↑o 𝑦))
→ (((𝐴
↑o 𝑦)
·o ∅) ∈ ((𝐴 ↑o 𝑦) ·o 𝐴) ↔ ∅ ∈ ((𝐴 ↑o 𝑦) ·o 𝐴))) |
| 18 | 14, 17 | sylibd 239 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ On ∧ (𝐴 ↑o 𝑦) ∈ On) ∧ ∅
∈ (𝐴
↑o 𝑦))
→ (∅ ∈ 𝐴
→ ∅ ∈ ((𝐴
↑o 𝑦)
·o 𝐴))) |
| 19 | 13, 18 | syldanl 602 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ On ∧ 𝑦 ∈ On) ∧ ∅ ∈
(𝐴 ↑o 𝑦)) → (∅ ∈ 𝐴 → ∅ ∈ ((𝐴 ↑o 𝑦) ·o 𝐴))) |
| 20 | | oesuc 8565 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ On ∧ 𝑦 ∈ On) → (𝐴 ↑o suc 𝑦) = ((𝐴 ↑o 𝑦) ·o 𝐴)) |
| 21 | 20 | eleq2d 2827 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ On ∧ 𝑦 ∈ On) → (∅
∈ (𝐴
↑o suc 𝑦)
↔ ∅ ∈ ((𝐴
↑o 𝑦)
·o 𝐴))) |
| 22 | 21 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ On ∧ 𝑦 ∈ On) ∧ ∅ ∈
(𝐴 ↑o 𝑦)) → (∅ ∈ (𝐴 ↑o suc 𝑦) ↔ ∅ ∈ ((𝐴 ↑o 𝑦) ·o 𝐴))) |
| 23 | 19, 22 | sylibrd 259 |
. . . . . . . . 9
⊢ (((𝐴 ∈ On ∧ 𝑦 ∈ On) ∧ ∅ ∈
(𝐴 ↑o 𝑦)) → (∅ ∈ 𝐴 → ∅ ∈ (𝐴 ↑o suc 𝑦))) |
| 24 | 23 | exp31 419 |
. . . . . . . 8
⊢ (𝐴 ∈ On → (𝑦 ∈ On → (∅
∈ (𝐴
↑o 𝑦)
→ (∅ ∈ 𝐴
→ ∅ ∈ (𝐴
↑o suc 𝑦))))) |
| 25 | 24 | com12 32 |
. . . . . . 7
⊢ (𝑦 ∈ On → (𝐴 ∈ On → (∅
∈ (𝐴
↑o 𝑦)
→ (∅ ∈ 𝐴
→ ∅ ∈ (𝐴
↑o suc 𝑦))))) |
| 26 | 25 | com34 91 |
. . . . . 6
⊢ (𝑦 ∈ On → (𝐴 ∈ On → (∅
∈ 𝐴 → (∅
∈ (𝐴
↑o 𝑦)
→ ∅ ∈ (𝐴
↑o suc 𝑦))))) |
| 27 | 26 | impd 410 |
. . . . 5
⊢ (𝑦 ∈ On → ((𝐴 ∈ On ∧ ∅ ∈
𝐴) → (∅ ∈
(𝐴 ↑o 𝑦) → ∅ ∈ (𝐴 ↑o suc 𝑦)))) |
| 28 | | 0ellim 6447 |
. . . . . . . . . . . 12
⊢ (Lim
𝑥 → ∅ ∈
𝑥) |
| 29 | | eqimss2 4043 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ↑o ∅) =
1o → 1o ⊆ (𝐴 ↑o
∅)) |
| 30 | 10, 29 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ On → 1o
⊆ (𝐴
↑o ∅)) |
| 31 | | oveq2 7439 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = ∅ → (𝐴 ↑o 𝑦) = (𝐴 ↑o
∅)) |
| 32 | 31 | sseq2d 4016 |
. . . . . . . . . . . . 13
⊢ (𝑦 = ∅ → (1o
⊆ (𝐴
↑o 𝑦)
↔ 1o ⊆ (𝐴 ↑o
∅))) |
| 33 | 32 | rspcev 3622 |
. . . . . . . . . . . 12
⊢ ((∅
∈ 𝑥 ∧
1o ⊆ (𝐴
↑o ∅)) → ∃𝑦 ∈ 𝑥 1o ⊆ (𝐴 ↑o 𝑦)) |
| 34 | 28, 30, 33 | syl2an 596 |
. . . . . . . . . . 11
⊢ ((Lim
𝑥 ∧ 𝐴 ∈ On) → ∃𝑦 ∈ 𝑥 1o ⊆ (𝐴 ↑o 𝑦)) |
| 35 | | ssiun 5046 |
. . . . . . . . . . 11
⊢
(∃𝑦 ∈
𝑥 1o ⊆
(𝐴 ↑o 𝑦) → 1o ⊆
∪ 𝑦 ∈ 𝑥 (𝐴 ↑o 𝑦)) |
| 36 | 34, 35 | syl 17 |
. . . . . . . . . 10
⊢ ((Lim
𝑥 ∧ 𝐴 ∈ On) → 1o ⊆
∪ 𝑦 ∈ 𝑥 (𝐴 ↑o 𝑦)) |
| 37 | 36 | adantrr 717 |
. . . . . . . . 9
⊢ ((Lim
𝑥 ∧ (𝐴 ∈ On ∧ ∅ ∈ 𝐴)) → 1o ⊆
∪ 𝑦 ∈ 𝑥 (𝐴 ↑o 𝑦)) |
| 38 | | vex 3484 |
. . . . . . . . . . . 12
⊢ 𝑥 ∈ V |
| 39 | | oelim 8572 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)) ∧ ∅ ∈ 𝐴) → (𝐴 ↑o 𝑥) = ∪ 𝑦 ∈ 𝑥 (𝐴 ↑o 𝑦)) |
| 40 | 38, 39 | mpanlr1 706 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ On ∧ Lim 𝑥) ∧ ∅ ∈ 𝐴) → (𝐴 ↑o 𝑥) = ∪ 𝑦 ∈ 𝑥 (𝐴 ↑o 𝑦)) |
| 41 | 40 | anasss 466 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ On ∧ (Lim 𝑥 ∧ ∅ ∈ 𝐴)) → (𝐴 ↑o 𝑥) = ∪ 𝑦 ∈ 𝑥 (𝐴 ↑o 𝑦)) |
| 42 | 41 | an12s 649 |
. . . . . . . . 9
⊢ ((Lim
𝑥 ∧ (𝐴 ∈ On ∧ ∅ ∈ 𝐴)) → (𝐴 ↑o 𝑥) = ∪ 𝑦 ∈ 𝑥 (𝐴 ↑o 𝑦)) |
| 43 | 37, 42 | sseqtrrd 4021 |
. . . . . . . 8
⊢ ((Lim
𝑥 ∧ (𝐴 ∈ On ∧ ∅ ∈ 𝐴)) → 1o ⊆
(𝐴 ↑o 𝑥)) |
| 44 | | limelon 6448 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ V ∧ Lim 𝑥) → 𝑥 ∈ On) |
| 45 | 38, 44 | mpan 690 |
. . . . . . . . . . 11
⊢ (Lim
𝑥 → 𝑥 ∈ On) |
| 46 | | oecl 8575 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ On) → (𝐴 ↑o 𝑥) ∈ On) |
| 47 | 46 | ancoms 458 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ On ∧ 𝐴 ∈ On) → (𝐴 ↑o 𝑥) ∈ On) |
| 48 | 45, 47 | sylan 580 |
. . . . . . . . . 10
⊢ ((Lim
𝑥 ∧ 𝐴 ∈ On) → (𝐴 ↑o 𝑥) ∈ On) |
| 49 | | eloni 6394 |
. . . . . . . . . 10
⊢ ((𝐴 ↑o 𝑥) ∈ On → Ord (𝐴 ↑o 𝑥)) |
| 50 | | ordgt0ge1 8531 |
. . . . . . . . . 10
⊢ (Ord
(𝐴 ↑o 𝑥) → (∅ ∈ (𝐴 ↑o 𝑥) ↔ 1o ⊆
(𝐴 ↑o 𝑥))) |
| 51 | 48, 49, 50 | 3syl 18 |
. . . . . . . . 9
⊢ ((Lim
𝑥 ∧ 𝐴 ∈ On) → (∅ ∈ (𝐴 ↑o 𝑥) ↔ 1o ⊆
(𝐴 ↑o 𝑥))) |
| 52 | 51 | adantrr 717 |
. . . . . . . 8
⊢ ((Lim
𝑥 ∧ (𝐴 ∈ On ∧ ∅ ∈ 𝐴)) → (∅ ∈ (𝐴 ↑o 𝑥) ↔ 1o ⊆
(𝐴 ↑o 𝑥))) |
| 53 | 43, 52 | mpbird 257 |
. . . . . . 7
⊢ ((Lim
𝑥 ∧ (𝐴 ∈ On ∧ ∅ ∈ 𝐴)) → ∅ ∈ (𝐴 ↑o 𝑥)) |
| 54 | 53 | ex 412 |
. . . . . 6
⊢ (Lim
𝑥 → ((𝐴 ∈ On ∧ ∅ ∈
𝐴) → ∅ ∈
(𝐴 ↑o 𝑥))) |
| 55 | 54 | a1dd 50 |
. . . . 5
⊢ (Lim
𝑥 → ((𝐴 ∈ On ∧ ∅ ∈
𝐴) → (∀𝑦 ∈ 𝑥 ∅ ∈ (𝐴 ↑o 𝑦) → ∅ ∈ (𝐴 ↑o 𝑥)))) |
| 56 | 2, 4, 6, 8, 12, 27, 55 | tfinds3 7886 |
. . . 4
⊢ (𝐵 ∈ On → ((𝐴 ∈ On ∧ ∅ ∈
𝐴) → ∅ ∈
(𝐴 ↑o 𝐵))) |
| 57 | 56 | expd 415 |
. . 3
⊢ (𝐵 ∈ On → (𝐴 ∈ On → (∅
∈ 𝐴 → ∅
∈ (𝐴
↑o 𝐵)))) |
| 58 | 57 | com12 32 |
. 2
⊢ (𝐴 ∈ On → (𝐵 ∈ On → (∅
∈ 𝐴 → ∅
∈ (𝐴
↑o 𝐵)))) |
| 59 | 58 | imp31 417 |
1
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ ∅ ∈
𝐴) → ∅ ∈
(𝐴 ↑o 𝐵)) |