Step | Hyp | Ref
| Expression |
1 | | omelon 9623 |
. . . 4
⊢ ω
∈ On |
2 | | onun2 6461 |
. . . 4
⊢ ((𝐴 ∈ On ∧ ω ∈
On) → (𝐴 ∪
ω) ∈ On) |
3 | 1, 2 | mpan2 689 |
. . 3
⊢ (𝐴 ∈ On → (𝐴 ∪ ω) ∈
On) |
4 | | onexomgt 41761 |
. . 3
⊢ ((𝐴 ∪ ω) ∈ On →
∃𝑎 ∈ On (𝐴 ∪ ω) ∈ (ω
·o 𝑎)) |
5 | 3, 4 | syl 17 |
. 2
⊢ (𝐴 ∈ On → ∃𝑎 ∈ On (𝐴 ∪ ω) ∈ (ω
·o 𝑎)) |
6 | | simp2 1137 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝑎 ∈ On ∧ (𝐴 ∪ ω) ∈ (ω
·o 𝑎))
→ 𝑎 ∈
On) |
7 | | omcl 8518 |
. . . . 5
⊢ ((ω
∈ On ∧ 𝑎 ∈
On) → (ω ·o 𝑎) ∈ On) |
8 | 1, 6, 7 | sylancr 587 |
. . . 4
⊢ ((𝐴 ∈ On ∧ 𝑎 ∈ On ∧ (𝐴 ∪ ω) ∈ (ω
·o 𝑎))
→ (ω ·o 𝑎) ∈ On) |
9 | | noel 4326 |
. . . . . . . . . 10
⊢ ¬
(𝐴 ∪ ω) ∈
∅ |
10 | | oveq2 7401 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = ∅ → (ω
·o 𝑎) =
(ω ·o ∅)) |
11 | | om0 8499 |
. . . . . . . . . . . . . . 15
⊢ (ω
∈ On → (ω ·o ∅) =
∅) |
12 | 1, 11 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ (ω
·o ∅) = ∅ |
13 | 10, 12 | eqtrdi 2787 |
. . . . . . . . . . . . 13
⊢ (𝑎 = ∅ → (ω
·o 𝑎) =
∅) |
14 | 13 | eleq2d 2818 |
. . . . . . . . . . . 12
⊢ (𝑎 = ∅ → ((𝐴 ∪ ω) ∈ (ω
·o 𝑎)
↔ (𝐴 ∪ ω)
∈ ∅)) |
15 | 14 | notbid 317 |
. . . . . . . . . . 11
⊢ (𝑎 = ∅ → (¬ (𝐴 ∪ ω) ∈ (ω
·o 𝑎)
↔ ¬ (𝐴 ∪
ω) ∈ ∅)) |
16 | 15 | adantl 482 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ On ∧ 𝑎 ∈ On) ∧ 𝑎 = ∅) → (¬ (𝐴 ∪ ω) ∈ (ω
·o 𝑎)
↔ ¬ (𝐴 ∪
ω) ∈ ∅)) |
17 | 9, 16 | mpbiri 257 |
. . . . . . . . 9
⊢ (((𝐴 ∈ On ∧ 𝑎 ∈ On) ∧ 𝑎 = ∅) → ¬ (𝐴 ∪ ω) ∈ (ω
·o 𝑎)) |
18 | 17 | pm2.21d 121 |
. . . . . . . 8
⊢ (((𝐴 ∈ On ∧ 𝑎 ∈ On) ∧ 𝑎 = ∅) → ((𝐴 ∪ ω) ∈ (ω
·o 𝑎)
→ Lim (ω ·o 𝑎))) |
19 | 18 | ex 413 |
. . . . . . 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 7854 |
. . . . . . . . 9
⊢ Lim
ω |
23 | 1, 22 | pm3.2i 471 |
. . . . . . . 8
⊢ (ω
∈ On ∧ Lim ω) |
24 | 6, 23 | jctir 521 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ 𝑎 ∈ On ∧ (𝐴 ∪ ω) ∈ (ω
·o 𝑎))
→ (𝑎 ∈ On ∧
(ω ∈ On ∧ Lim ω))) |
25 | | omlimcl2 41762 |
. . . . . . 7
⊢ (((𝑎 ∈ On ∧ (ω ∈
On ∧ Lim ω)) ∧ ∅ ∈ 𝑎) → Lim (ω ·o
𝑎)) |
26 | 24, 25 | sylan 580 |
. . . . . 6
⊢ (((𝐴 ∈ On ∧ 𝑎 ∈ On ∧ (𝐴 ∪ ω) ∈ (ω
·o 𝑎))
∧ ∅ ∈ 𝑎)
→ Lim (ω ·o 𝑎)) |
27 | 26 | ex 413 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝑎 ∈ On ∧ (𝐴 ∪ ω) ∈ (ω
·o 𝑎))
→ (∅ ∈ 𝑎
→ Lim (ω ·o 𝑎))) |
28 | | on0eqel 6477 |
. . . . . 6
⊢ (𝑎 ∈ On → (𝑎 = ∅ ∨ ∅ ∈
𝑎)) |
29 | 6, 28 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝑎 ∈ On ∧ (𝐴 ∪ ω) ∈ (ω
·o 𝑎))
→ (𝑎 = ∅ ∨
∅ ∈ 𝑎)) |
30 | 21, 27, 29 | mpjaod 858 |
. . . 4
⊢ ((𝐴 ∈ On ∧ 𝑎 ∈ On ∧ (𝐴 ∪ ω) ∈ (ω
·o 𝑎))
→ Lim (ω ·o 𝑎)) |
31 | | simp1 1136 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝑎 ∈ On ∧ (𝐴 ∪ ω) ∈ (ω
·o 𝑎))
→ 𝐴 ∈
On) |
32 | 31, 8 | jca 512 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝑎 ∈ On ∧ (𝐴 ∪ ω) ∈ (ω
·o 𝑎))
→ (𝐴 ∈ On ∧
(ω ·o 𝑎) ∈ On)) |
33 | | simp3 1138 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝑎 ∈ On ∧ (𝐴 ∪ ω) ∈ (ω
·o 𝑎))
→ (𝐴 ∪ ω)
∈ (ω ·o 𝑎)) |
34 | | ssun1 4168 |
. . . . . 6
⊢ 𝐴 ⊆ (𝐴 ∪ ω) |
35 | 33, 34 | jctil 520 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝑎 ∈ On ∧ (𝐴 ∪ ω) ∈ (ω
·o 𝑎))
→ (𝐴 ⊆ (𝐴 ∪ ω) ∧ (𝐴 ∪ ω) ∈ (ω
·o 𝑎))) |
36 | | ontr2 6400 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ (ω
·o 𝑎)
∈ On) → ((𝐴
⊆ (𝐴 ∪ ω)
∧ (𝐴 ∪ ω)
∈ (ω ·o 𝑎)) → 𝐴 ∈ (ω ·o 𝑎))) |
37 | 32, 35, 36 | sylc 65 |
. . . 4
⊢ ((𝐴 ∈ On ∧ 𝑎 ∈ On ∧ (𝐴 ∪ ω) ∈ (ω
·o 𝑎))
→ 𝐴 ∈ (ω
·o 𝑎)) |
38 | | limeq 6365 |
. . . . . 6
⊢ (𝑥 = (ω ·o
𝑎) → (Lim 𝑥 ↔ Lim (ω
·o 𝑎))) |
39 | | eleq2 2821 |
. . . . . 6
⊢ (𝑥 = (ω ·o
𝑎) → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ (ω ·o 𝑎))) |
40 | 38, 39 | anbi12d 631 |
. . . . 5
⊢ (𝑥 = (ω ·o
𝑎) → ((Lim 𝑥 ∧ 𝐴 ∈ 𝑥) ↔ (Lim (ω ·o
𝑎) ∧ 𝐴 ∈ (ω ·o 𝑎)))) |
41 | 40 | rspcev 3609 |
. . . 4
⊢
(((ω ·o 𝑎) ∈ On ∧ (Lim (ω
·o 𝑎)
∧ 𝐴 ∈ (ω
·o 𝑎)))
→ ∃𝑥 ∈ On
(Lim 𝑥 ∧ 𝐴 ∈ 𝑥)) |
42 | 8, 30, 37, 41 | syl12anc 835 |
. . 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 𝑥 ∧ 𝐴 ∈ 𝑥)) |