| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | omelon 9687 | . . . 4
⊢ ω
∈ On | 
| 2 |  | onun2 6491 | . . . 4
⊢ ((𝐴 ∈ On ∧ ω ∈
On) → (𝐴 ∪
ω) ∈ On) | 
| 3 | 1, 2 | mpan2 691 | . . 3
⊢ (𝐴 ∈ On → (𝐴 ∪ ω) ∈
On) | 
| 4 |  | onexomgt 43258 | . . 3
⊢ ((𝐴 ∪ ω) ∈ On →
∃𝑎 ∈ On (𝐴 ∪ ω) ∈ (ω
·o 𝑎)) | 
| 5 | 3, 4 | syl 17 | . 2
⊢ (𝐴 ∈ On → ∃𝑎 ∈ On (𝐴 ∪ ω) ∈ (ω
·o 𝑎)) | 
| 6 |  | simp2 1137 | . . . . 5
⊢ ((𝐴 ∈ On ∧ 𝑎 ∈ On ∧ (𝐴 ∪ ω) ∈ (ω
·o 𝑎))
→ 𝑎 ∈
On) | 
| 7 |  | omcl 8575 | . . . . 5
⊢ ((ω
∈ On ∧ 𝑎 ∈
On) → (ω ·o 𝑎) ∈ On) | 
| 8 | 1, 6, 7 | sylancr 587 | . . . 4
⊢ ((𝐴 ∈ On ∧ 𝑎 ∈ On ∧ (𝐴 ∪ ω) ∈ (ω
·o 𝑎))
→ (ω ·o 𝑎) ∈ On) | 
| 9 |  | noel 4337 | . . . . . . . . . 10
⊢  ¬
(𝐴 ∪ ω) ∈
∅ | 
| 10 |  | oveq2 7440 | . . . . . . . . . . . . . 14
⊢ (𝑎 = ∅ → (ω
·o 𝑎) =
(ω ·o ∅)) | 
| 11 |  | om0 8556 | . . . . . . . . . . . . . . 15
⊢ (ω
∈ On → (ω ·o ∅) =
∅) | 
| 12 | 1, 11 | ax-mp 5 | . . . . . . . . . . . . . 14
⊢ (ω
·o ∅) = ∅ | 
| 13 | 10, 12 | eqtrdi 2792 | . . . . . . . . . . . . 13
⊢ (𝑎 = ∅ → (ω
·o 𝑎) =
∅) | 
| 14 | 13 | eleq2d 2826 | . . . . . . . . . . . 12
⊢ (𝑎 = ∅ → ((𝐴 ∪ ω) ∈ (ω
·o 𝑎)
↔ (𝐴 ∪ ω)
∈ ∅)) | 
| 15 | 14 | notbid 318 | . . . . . . . . . . 11
⊢ (𝑎 = ∅ → (¬ (𝐴 ∪ ω) ∈ (ω
·o 𝑎)
↔ ¬ (𝐴 ∪
ω) ∈ ∅)) | 
| 16 | 15 | adantl 481 | . . . . . . . . . 10
⊢ (((𝐴 ∈ On ∧ 𝑎 ∈ On) ∧ 𝑎 = ∅) → (¬ (𝐴 ∪ ω) ∈ (ω
·o 𝑎)
↔ ¬ (𝐴 ∪
ω) ∈ ∅)) | 
| 17 | 9, 16 | mpbiri 258 | . . . . . . . . 9
⊢ (((𝐴 ∈ On ∧ 𝑎 ∈ On) ∧ 𝑎 = ∅) → ¬ (𝐴 ∪ ω) ∈ (ω
·o 𝑎)) | 
| 18 | 17 | pm2.21d 121 | . . . . . . . 8
⊢ (((𝐴 ∈ On ∧ 𝑎 ∈ On) ∧ 𝑎 = ∅) → ((𝐴 ∪ ω) ∈ (ω
·o 𝑎)
→ Lim (ω ·o 𝑎))) | 
| 19 | 18 | ex 412 | . . . . . . 7
⊢ ((𝐴 ∈ On ∧ 𝑎 ∈ On) → (𝑎 = ∅ → ((𝐴 ∪ ω) ∈ (ω
·o 𝑎)
→ Lim (ω ·o 𝑎)))) | 
| 20 | 19 | com23 86 | . . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝑎 ∈ On) → ((𝐴 ∪ ω) ∈ (ω
·o 𝑎)
→ (𝑎 = ∅ →
Lim (ω ·o 𝑎)))) | 
| 21 | 20 | 3impia 1117 | . . . . 5
⊢ ((𝐴 ∈ On ∧ 𝑎 ∈ On ∧ (𝐴 ∪ ω) ∈ (ω
·o 𝑎))
→ (𝑎 = ∅ →
Lim (ω ·o 𝑎))) | 
| 22 |  | limom 7904 | . . . . . . . . 9
⊢ Lim
ω | 
| 23 | 1, 22 | pm3.2i 470 | . . . . . . . 8
⊢ (ω
∈ On ∧ Lim ω) | 
| 24 | 6, 23 | jctir 520 | . . . . . . 7
⊢ ((𝐴 ∈ On ∧ 𝑎 ∈ On ∧ (𝐴 ∪ ω) ∈ (ω
·o 𝑎))
→ (𝑎 ∈ On ∧
(ω ∈ On ∧ Lim ω))) | 
| 25 |  | omlimcl2 43259 | . . . . . . 7
⊢ (((𝑎 ∈ On ∧ (ω ∈
On ∧ Lim ω)) ∧ ∅ ∈ 𝑎) → Lim (ω ·o
𝑎)) | 
| 26 | 24, 25 | sylan 580 | . . . . . 6
⊢ (((𝐴 ∈ On ∧ 𝑎 ∈ On ∧ (𝐴 ∪ ω) ∈ (ω
·o 𝑎))
∧ ∅ ∈ 𝑎)
→ Lim (ω ·o 𝑎)) | 
| 27 | 26 | ex 412 | . . . . 5
⊢ ((𝐴 ∈ On ∧ 𝑎 ∈ On ∧ (𝐴 ∪ ω) ∈ (ω
·o 𝑎))
→ (∅ ∈ 𝑎
→ Lim (ω ·o 𝑎))) | 
| 28 |  | on0eqel 6507 | . . . . . 6
⊢ (𝑎 ∈ On → (𝑎 = ∅ ∨ ∅ ∈
𝑎)) | 
| 29 | 6, 28 | syl 17 | . . . . 5
⊢ ((𝐴 ∈ On ∧ 𝑎 ∈ On ∧ (𝐴 ∪ ω) ∈ (ω
·o 𝑎))
→ (𝑎 = ∅ ∨
∅ ∈ 𝑎)) | 
| 30 | 21, 27, 29 | mpjaod 860 | . . . 4
⊢ ((𝐴 ∈ On ∧ 𝑎 ∈ On ∧ (𝐴 ∪ ω) ∈ (ω
·o 𝑎))
→ Lim (ω ·o 𝑎)) | 
| 31 |  | simp1 1136 | . . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝑎 ∈ On ∧ (𝐴 ∪ ω) ∈ (ω
·o 𝑎))
→ 𝐴 ∈
On) | 
| 32 | 31, 8 | jca 511 | . . . . 5
⊢ ((𝐴 ∈ On ∧ 𝑎 ∈ On ∧ (𝐴 ∪ ω) ∈ (ω
·o 𝑎))
→ (𝐴 ∈ On ∧
(ω ·o 𝑎) ∈ On)) | 
| 33 |  | simp3 1138 | . . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝑎 ∈ On ∧ (𝐴 ∪ ω) ∈ (ω
·o 𝑎))
→ (𝐴 ∪ ω)
∈ (ω ·o 𝑎)) | 
| 34 |  | ssun1 4177 | . . . . . 6
⊢ 𝐴 ⊆ (𝐴 ∪ ω) | 
| 35 | 33, 34 | jctil 519 | . . . . 5
⊢ ((𝐴 ∈ On ∧ 𝑎 ∈ On ∧ (𝐴 ∪ ω) ∈ (ω
·o 𝑎))
→ (𝐴 ⊆ (𝐴 ∪ ω) ∧ (𝐴 ∪ ω) ∈ (ω
·o 𝑎))) | 
| 36 |  | ontr2 6430 | . . . . 5
⊢ ((𝐴 ∈ On ∧ (ω
·o 𝑎)
∈ On) → ((𝐴
⊆ (𝐴 ∪ ω)
∧ (𝐴 ∪ ω)
∈ (ω ·o 𝑎)) → 𝐴 ∈ (ω ·o 𝑎))) | 
| 37 | 32, 35, 36 | sylc 65 | . . . 4
⊢ ((𝐴 ∈ On ∧ 𝑎 ∈ On ∧ (𝐴 ∪ ω) ∈ (ω
·o 𝑎))
→ 𝐴 ∈ (ω
·o 𝑎)) | 
| 38 |  | limeq 6395 | . . . . . 6
⊢ (𝑥 = (ω ·o
𝑎) → (Lim 𝑥 ↔ Lim (ω
·o 𝑎))) | 
| 39 |  | eleq2 2829 | . . . . . 6
⊢ (𝑥 = (ω ·o
𝑎) → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ (ω ·o 𝑎))) | 
| 40 | 38, 39 | anbi12d 632 | . . . . 5
⊢ (𝑥 = (ω ·o
𝑎) → ((Lim 𝑥 ∧ 𝐴 ∈ 𝑥) ↔ (Lim (ω ·o
𝑎) ∧ 𝐴 ∈ (ω ·o 𝑎)))) | 
| 41 | 40 | rspcev 3621 | . . . 4
⊢
(((ω ·o 𝑎) ∈ On ∧ (Lim (ω
·o 𝑎)
∧ 𝐴 ∈ (ω
·o 𝑎)))
→ ∃𝑥 ∈ On
(Lim 𝑥 ∧ 𝐴 ∈ 𝑥)) | 
| 42 | 8, 30, 37, 41 | syl12anc 836 | . . 3
⊢ ((𝐴 ∈ On ∧ 𝑎 ∈ On ∧ (𝐴 ∪ ω) ∈ (ω
·o 𝑎))
→ ∃𝑥 ∈ On
(Lim 𝑥 ∧ 𝐴 ∈ 𝑥)) | 
| 43 | 42 | rexlimdv3a 3158 | . 2
⊢ (𝐴 ∈ On → (∃𝑎 ∈ On (𝐴 ∪ ω) ∈ (ω
·o 𝑎)
→ ∃𝑥 ∈ On
(Lim 𝑥 ∧ 𝐴 ∈ 𝑥))) | 
| 44 | 5, 43 | mpd 15 | 1
⊢ (𝐴 ∈ On → ∃𝑥 ∈ On (Lim 𝑥 ∧ 𝐴 ∈ 𝑥)) |