Step | Hyp | Ref
| Expression |
1 | | p0ex 4072 |
. . . . . . . . . . 11
⊢ {∅}
∈ V |
2 | 1 | ssex 4025 |
. . . . . . . . . 10
⊢ (𝑦 ⊆ {∅} → 𝑦 ∈ V) |
3 | 2 | adantl 273 |
. . . . . . . . 9
⊢
(((∀𝑥((𝑥 ≼ ω ∧ ω
≼ 𝑥) → 𝑥 ≈ ω) ∧ ω
∈ Omni) ∧ 𝑦
⊆ {∅}) → 𝑦
∈ V) |
4 | | omex 4467 |
. . . . . . . . 9
⊢ ω
∈ V |
5 | | djuex 6880 |
. . . . . . . . 9
⊢ ((𝑦 ∈ V ∧ ω ∈
V) → (𝑦 ⊔
ω) ∈ V) |
6 | 3, 4, 5 | sylancl 407 |
. . . . . . . 8
⊢
(((∀𝑥((𝑥 ≼ ω ∧ ω
≼ 𝑥) → 𝑥 ≈ ω) ∧ ω
∈ Omni) ∧ 𝑦
⊆ {∅}) → (𝑦 ⊔ ω) ∈ V) |
7 | | simpll 501 |
. . . . . . . 8
⊢
(((∀𝑥((𝑥 ≼ ω ∧ ω
≼ 𝑥) → 𝑥 ≈ ω) ∧ ω
∈ Omni) ∧ 𝑦
⊆ {∅}) → ∀𝑥((𝑥 ≼ ω ∧ ω ≼ 𝑥) → 𝑥 ≈ ω)) |
8 | | ssdomg 6626 |
. . . . . . . . . . . 12
⊢
({∅} ∈ V → (𝑦 ⊆ {∅} → 𝑦 ≼ {∅})) |
9 | 1, 8 | ax-mp 7 |
. . . . . . . . . . 11
⊢ (𝑦 ⊆ {∅} → 𝑦 ≼
{∅}) |
10 | | domrefg 6615 |
. . . . . . . . . . . . . 14
⊢ (ω
∈ V → ω ≼ ω) |
11 | 4, 10 | ax-mp 7 |
. . . . . . . . . . . . 13
⊢ ω
≼ ω |
12 | | djudom 6930 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ≼ {∅} ∧ ω
≼ ω) → (𝑦
⊔ ω) ≼ ({∅} ⊔ ω)) |
13 | 11, 12 | mpan2 419 |
. . . . . . . . . . . 12
⊢ (𝑦 ≼ {∅} → (𝑦 ⊔ ω) ≼
({∅} ⊔ ω)) |
14 | | df1o2 6280 |
. . . . . . . . . . . . 13
⊢
1o = {∅} |
15 | | djueq1 6877 |
. . . . . . . . . . . . 13
⊢
(1o = {∅} → (1o ⊔ ω) =
({∅} ⊔ ω)) |
16 | 14, 15 | ax-mp 7 |
. . . . . . . . . . . 12
⊢
(1o ⊔ ω) = ({∅} ⊔
ω) |
17 | 13, 16 | syl6breqr 3935 |
. . . . . . . . . . 11
⊢ (𝑦 ≼ {∅} → (𝑦 ⊔ ω) ≼
(1o ⊔ ω)) |
18 | | 1onn 6370 |
. . . . . . . . . . . . . 14
⊢
1o ∈ ω |
19 | | endjusym 6933 |
. . . . . . . . . . . . . 14
⊢ ((ω
∈ V ∧ 1o ∈ ω) → (ω ⊔
1o) ≈ (1o ⊔ ω)) |
20 | 4, 18, 19 | mp2an 420 |
. . . . . . . . . . . . 13
⊢ (ω
⊔ 1o) ≈ (1o ⊔
ω) |
21 | | omp1eom 6932 |
. . . . . . . . . . . . 13
⊢ (ω
⊔ 1o) ≈ ω |
22 | 20, 21 | entr3i 6636 |
. . . . . . . . . . . 12
⊢
(1o ⊔ ω) ≈ ω |
23 | | domentr 6639 |
. . . . . . . . . . . 12
⊢ (((𝑦 ⊔ ω) ≼
(1o ⊔ ω) ∧ (1o ⊔ ω) ≈
ω) → (𝑦 ⊔
ω) ≼ ω) |
24 | 22, 23 | mpan2 419 |
. . . . . . . . . . 11
⊢ ((𝑦 ⊔ ω) ≼
(1o ⊔ ω) → (𝑦 ⊔ ω) ≼
ω) |
25 | 9, 17, 24 | 3syl 17 |
. . . . . . . . . 10
⊢ (𝑦 ⊆ {∅} → (𝑦 ⊔ ω) ≼
ω) |
26 | 25 | adantl 273 |
. . . . . . . . 9
⊢
(((∀𝑥((𝑥 ≼ ω ∧ ω
≼ 𝑥) → 𝑥 ≈ ω) ∧ ω
∈ Omni) ∧ 𝑦
⊆ {∅}) → (𝑦 ⊔ ω) ≼
ω) |
27 | | djudomr 7024 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ V ∧ ω ∈
V) → ω ≼ (𝑦 ⊔ ω)) |
28 | 3, 4, 27 | sylancl 407 |
. . . . . . . . 9
⊢
(((∀𝑥((𝑥 ≼ ω ∧ ω
≼ 𝑥) → 𝑥 ≈ ω) ∧ ω
∈ Omni) ∧ 𝑦
⊆ {∅}) → ω ≼ (𝑦 ⊔ ω)) |
29 | 26, 28 | jca 302 |
. . . . . . . 8
⊢
(((∀𝑥((𝑥 ≼ ω ∧ ω
≼ 𝑥) → 𝑥 ≈ ω) ∧ ω
∈ Omni) ∧ 𝑦
⊆ {∅}) → ((𝑦 ⊔ ω) ≼ ω ∧
ω ≼ (𝑦 ⊔
ω))) |
30 | | breq1 3898 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑦 ⊔ ω) → (𝑥 ≼ ω ↔ (𝑦 ⊔ ω) ≼
ω)) |
31 | | breq2 3899 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑦 ⊔ ω) → (ω ≼
𝑥 ↔ ω ≼
(𝑦 ⊔
ω))) |
32 | 30, 31 | anbi12d 462 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑦 ⊔ ω) → ((𝑥 ≼ ω ∧ ω
≼ 𝑥) ↔ ((𝑦 ⊔ ω) ≼
ω ∧ ω ≼ (𝑦 ⊔ ω)))) |
33 | | breq1 3898 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑦 ⊔ ω) → (𝑥 ≈ ω ↔ (𝑦 ⊔ ω) ≈
ω)) |
34 | 32, 33 | imbi12d 233 |
. . . . . . . . 9
⊢ (𝑥 = (𝑦 ⊔ ω) → (((𝑥 ≼ ω ∧ ω
≼ 𝑥) → 𝑥 ≈ ω) ↔
(((𝑦 ⊔ ω)
≼ ω ∧ ω ≼ (𝑦 ⊔ ω)) → (𝑦 ⊔ ω) ≈
ω))) |
35 | 34 | spcgv 2744 |
. . . . . . . 8
⊢ ((𝑦 ⊔ ω) ∈ V
→ (∀𝑥((𝑥 ≼ ω ∧ ω
≼ 𝑥) → 𝑥 ≈ ω) →
(((𝑦 ⊔ ω)
≼ ω ∧ ω ≼ (𝑦 ⊔ ω)) → (𝑦 ⊔ ω) ≈
ω))) |
36 | 6, 7, 29, 35 | syl3c 63 |
. . . . . . 7
⊢
(((∀𝑥((𝑥 ≼ ω ∧ ω
≼ 𝑥) → 𝑥 ≈ ω) ∧ ω
∈ Omni) ∧ 𝑦
⊆ {∅}) → (𝑦 ⊔ ω) ≈
ω) |
37 | 36 | ensymd 6631 |
. . . . . 6
⊢
(((∀𝑥((𝑥 ≼ ω ∧ ω
≼ 𝑥) → 𝑥 ≈ ω) ∧ ω
∈ Omni) ∧ 𝑦
⊆ {∅}) → ω ≈ (𝑦 ⊔ ω)) |
38 | | bren 6595 |
. . . . . 6
⊢ (ω
≈ (𝑦 ⊔
ω) ↔ ∃𝑓
𝑓:ω–1-1-onto→(𝑦 ⊔ ω)) |
39 | 37, 38 | sylib 121 |
. . . . 5
⊢
(((∀𝑥((𝑥 ≼ ω ∧ ω
≼ 𝑥) → 𝑥 ≈ ω) ∧ ω
∈ Omni) ∧ 𝑦
⊆ {∅}) → ∃𝑓 𝑓:ω–1-1-onto→(𝑦 ⊔ ω)) |
40 | | simpllr 506 |
. . . . . 6
⊢
((((∀𝑥((𝑥 ≼ ω ∧ ω
≼ 𝑥) → 𝑥 ≈ ω) ∧ ω
∈ Omni) ∧ 𝑦
⊆ {∅}) ∧ 𝑓:ω–1-1-onto→(𝑦 ⊔ ω)) → ω ∈
Omni) |
41 | | simplr 502 |
. . . . . 6
⊢
((((∀𝑥((𝑥 ≼ ω ∧ ω
≼ 𝑥) → 𝑥 ≈ ω) ∧ ω
∈ Omni) ∧ 𝑦
⊆ {∅}) ∧ 𝑓:ω–1-1-onto→(𝑦 ⊔ ω)) → 𝑦 ⊆ {∅}) |
42 | | simpr 109 |
. . . . . 6
⊢
((((∀𝑥((𝑥 ≼ ω ∧ ω
≼ 𝑥) → 𝑥 ≈ ω) ∧ ω
∈ Omni) ∧ 𝑦
⊆ {∅}) ∧ 𝑓:ω–1-1-onto→(𝑦 ⊔ ω)) → 𝑓:ω–1-1-onto→(𝑦 ⊔ ω)) |
43 | 40, 41, 42 | sbthomlem 12912 |
. . . . 5
⊢
((((∀𝑥((𝑥 ≼ ω ∧ ω
≼ 𝑥) → 𝑥 ≈ ω) ∧ ω
∈ Omni) ∧ 𝑦
⊆ {∅}) ∧ 𝑓:ω–1-1-onto→(𝑦 ⊔ ω)) → (𝑦 = ∅ ∨ 𝑦 = {∅})) |
44 | 39, 43 | exlimddv 1852 |
. . . 4
⊢
(((∀𝑥((𝑥 ≼ ω ∧ ω
≼ 𝑥) → 𝑥 ≈ ω) ∧ ω
∈ Omni) ∧ 𝑦
⊆ {∅}) → (𝑦 = ∅ ∨ 𝑦 = {∅})) |
45 | 44 | ex 114 |
. . 3
⊢
((∀𝑥((𝑥 ≼ ω ∧ ω
≼ 𝑥) → 𝑥 ≈ ω) ∧ ω
∈ Omni) → (𝑦
⊆ {∅} → (𝑦
= ∅ ∨ 𝑦 =
{∅}))) |
46 | 45 | alrimiv 1828 |
. 2
⊢
((∀𝑥((𝑥 ≼ ω ∧ ω
≼ 𝑥) → 𝑥 ≈ ω) ∧ ω
∈ Omni) → ∀𝑦(𝑦 ⊆ {∅} → (𝑦 = ∅ ∨ 𝑦 = {∅}))) |
47 | | exmid01 4081 |
. 2
⊢
(EXMID ↔ ∀𝑦(𝑦 ⊆ {∅} → (𝑦 = ∅ ∨ 𝑦 = {∅}))) |
48 | 46, 47 | sylibr 133 |
1
⊢
((∀𝑥((𝑥 ≼ ω ∧ ω
≼ 𝑥) → 𝑥 ≈ ω) ∧ ω
∈ Omni) → EXMID) |