| Step | Hyp | Ref
| Expression |
| 1 | | vex 2766 |
. . . . . . . . . . 11
⊢ 𝑦 ∈ V |
| 2 | 1 | enref 6824 |
. . . . . . . . . 10
⊢ 𝑦 ≈ 𝑦 |
| 3 | | 2z 9354 |
. . . . . . . . . . 11
⊢ 2 ∈
ℤ |
| 4 | | uzennn 10528 |
. . . . . . . . . . 11
⊢ (2 ∈
ℤ → (ℤ≥‘2) ≈
ℕ) |
| 5 | 3, 4 | ax-mp 5 |
. . . . . . . . . 10
⊢
(ℤ≥‘2) ≈ ℕ |
| 6 | | djuen 7278 |
. . . . . . . . . 10
⊢ ((𝑦 ≈ 𝑦 ∧ (ℤ≥‘2)
≈ ℕ) → (𝑦
⊔ (ℤ≥‘2)) ≈ (𝑦 ⊔ ℕ)) |
| 7 | 2, 5, 6 | mp2an 426 |
. . . . . . . . 9
⊢ (𝑦 ⊔
(ℤ≥‘2)) ≈ (𝑦 ⊔ ℕ) |
| 8 | 7 | ensymi 6841 |
. . . . . . . 8
⊢ (𝑦 ⊔ ℕ) ≈
(𝑦 ⊔
(ℤ≥‘2)) |
| 9 | | zex 9335 |
. . . . . . . . . . 11
⊢ ℤ
∈ V |
| 10 | | uzssz 9621 |
. . . . . . . . . . 11
⊢
(ℤ≥‘2) ⊆ ℤ |
| 11 | 9, 10 | ssexi 4171 |
. . . . . . . . . 10
⊢
(ℤ≥‘2) ∈ V |
| 12 | | 1re 8025 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
ℝ |
| 13 | 12 | ltnri 8119 |
. . . . . . . . . . . . . 14
⊢ ¬ 1
< 1 |
| 14 | | simplr 528 |
. . . . . . . . . . . . . . . . 17
⊢
((((∀𝑥((𝑥 ⊆ ℕ ∧
∀𝑚 ∈ ℕ
∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni)
∧ 𝑦 ⊆ {1}) ∧
𝑧 ∈ 𝑦) → 𝑦 ⊆ {1}) |
| 15 | | simpr 110 |
. . . . . . . . . . . . . . . . 17
⊢
((((∀𝑥((𝑥 ⊆ ℕ ∧
∀𝑚 ∈ ℕ
∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni)
∧ 𝑦 ⊆ {1}) ∧
𝑧 ∈ 𝑦) → 𝑧 ∈ 𝑦) |
| 16 | 14, 15 | sseldd 3184 |
. . . . . . . . . . . . . . . 16
⊢
((((∀𝑥((𝑥 ⊆ ℕ ∧
∀𝑚 ∈ ℕ
∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni)
∧ 𝑦 ⊆ {1}) ∧
𝑧 ∈ 𝑦) → 𝑧 ∈ {1}) |
| 17 | | elsni 3640 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ {1} → 𝑧 = 1) |
| 18 | 16, 17 | syl 14 |
. . . . . . . . . . . . . . 15
⊢
((((∀𝑥((𝑥 ⊆ ℕ ∧
∀𝑚 ∈ ℕ
∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni)
∧ 𝑦 ⊆ {1}) ∧
𝑧 ∈ 𝑦) → 𝑧 = 1) |
| 19 | 18 | breq2d 4045 |
. . . . . . . . . . . . . 14
⊢
((((∀𝑥((𝑥 ⊆ ℕ ∧
∀𝑚 ∈ ℕ
∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni)
∧ 𝑦 ⊆ {1}) ∧
𝑧 ∈ 𝑦) → (1 < 𝑧 ↔ 1 < 1)) |
| 20 | 13, 19 | mtbiri 676 |
. . . . . . . . . . . . 13
⊢
((((∀𝑥((𝑥 ⊆ ℕ ∧
∀𝑚 ∈ ℕ
∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni)
∧ 𝑦 ⊆ {1}) ∧
𝑧 ∈ 𝑦) → ¬ 1 < 𝑧) |
| 21 | | eluz2gt1 9676 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈
(ℤ≥‘2) → 1 < 𝑧) |
| 22 | 20, 21 | nsyl 629 |
. . . . . . . . . . . 12
⊢
((((∀𝑥((𝑥 ⊆ ℕ ∧
∀𝑚 ∈ ℕ
∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni)
∧ 𝑦 ⊆ {1}) ∧
𝑧 ∈ 𝑦) → ¬ 𝑧 ∈
(ℤ≥‘2)) |
| 23 | 22 | ralrimiva 2570 |
. . . . . . . . . . 11
⊢
(((∀𝑥((𝑥 ⊆ ℕ ∧
∀𝑚 ∈ ℕ
∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni)
∧ 𝑦 ⊆ {1}) →
∀𝑧 ∈ 𝑦 ¬ 𝑧 ∈
(ℤ≥‘2)) |
| 24 | | disj 3499 |
. . . . . . . . . . 11
⊢ ((𝑦 ∩
(ℤ≥‘2)) = ∅ ↔ ∀𝑧 ∈ 𝑦 ¬ 𝑧 ∈
(ℤ≥‘2)) |
| 25 | 23, 24 | sylibr 134 |
. . . . . . . . . 10
⊢
(((∀𝑥((𝑥 ⊆ ℕ ∧
∀𝑚 ∈ ℕ
∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni)
∧ 𝑦 ⊆ {1}) →
(𝑦 ∩
(ℤ≥‘2)) = ∅) |
| 26 | | endjudisj 7277 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ V ∧
(ℤ≥‘2) ∈ V ∧ (𝑦 ∩ (ℤ≥‘2)) =
∅) → (𝑦 ⊔
(ℤ≥‘2)) ≈ (𝑦 ∪
(ℤ≥‘2))) |
| 27 | 1, 11, 25, 26 | mp3an12i 1352 |
. . . . . . . . 9
⊢
(((∀𝑥((𝑥 ⊆ ℕ ∧
∀𝑚 ∈ ℕ
∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni)
∧ 𝑦 ⊆ {1}) →
(𝑦 ⊔
(ℤ≥‘2)) ≈ (𝑦 ∪
(ℤ≥‘2))) |
| 28 | | simpr 110 |
. . . . . . . . . . . 12
⊢
(((∀𝑥((𝑥 ⊆ ℕ ∧
∀𝑚 ∈ ℕ
∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni)
∧ 𝑦 ⊆ {1}) →
𝑦 ⊆
{1}) |
| 29 | | 1nn 9001 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℕ |
| 30 | | snssi 3766 |
. . . . . . . . . . . . 13
⊢ (1 ∈
ℕ → {1} ⊆ ℕ) |
| 31 | 29, 30 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ {1}
⊆ ℕ |
| 32 | 28, 31 | sstrdi 3195 |
. . . . . . . . . . 11
⊢
(((∀𝑥((𝑥 ⊆ ℕ ∧
∀𝑚 ∈ ℕ
∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni)
∧ 𝑦 ⊆ {1}) →
𝑦 ⊆
ℕ) |
| 33 | | 2nn 9152 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℕ |
| 34 | | uznnssnn 9651 |
. . . . . . . . . . . 12
⊢ (2 ∈
ℕ → (ℤ≥‘2) ⊆
ℕ) |
| 35 | 33, 34 | mp1i 10 |
. . . . . . . . . . 11
⊢
(((∀𝑥((𝑥 ⊆ ℕ ∧
∀𝑚 ∈ ℕ
∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni)
∧ 𝑦 ⊆ {1}) →
(ℤ≥‘2) ⊆ ℕ) |
| 36 | 32, 35 | unssd 3339 |
. . . . . . . . . 10
⊢
(((∀𝑥((𝑥 ⊆ ℕ ∧
∀𝑚 ∈ ℕ
∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni)
∧ 𝑦 ⊆ {1}) →
(𝑦 ∪
(ℤ≥‘2)) ⊆ ℕ) |
| 37 | | nfv 1542 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑚 𝑥 ⊆
ℕ |
| 38 | | nfra1 2528 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑚∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝑥 𝑚 < 𝑛 |
| 39 | 37, 38 | nfan 1579 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑚(𝑥 ⊆ ℕ ∧
∀𝑚 ∈ ℕ
∃𝑛 ∈ 𝑥 𝑚 < 𝑛) |
| 40 | | nfv 1542 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑚 𝑥 ≈
ℕ |
| 41 | 39, 40 | nfim 1586 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑚((𝑥 ⊆ ℕ ∧
∀𝑚 ∈ ℕ
∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) |
| 42 | 41 | nfal 1590 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑚∀𝑥((𝑥 ⊆ ℕ ∧ ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) |
| 43 | | nfv 1542 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑚ω
∈ Omni |
| 44 | 42, 43 | nfan 1579 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑚(∀𝑥((𝑥 ⊆ ℕ ∧ ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈
Omni) |
| 45 | | nfv 1542 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑚 𝑦 ⊆ {1} |
| 46 | 44, 45 | nfan 1579 |
. . . . . . . . . . 11
⊢
Ⅎ𝑚((∀𝑥((𝑥 ⊆ ℕ ∧ ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni)
∧ 𝑦 ⊆
{1}) |
| 47 | | simpr 110 |
. . . . . . . . . . . . . . . . 17
⊢
((((∀𝑥((𝑥 ⊆ ℕ ∧
∀𝑚 ∈ ℕ
∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni)
∧ 𝑦 ⊆ {1}) ∧
𝑚 ∈ ℕ) →
𝑚 ∈
ℕ) |
| 48 | 47 | peano2nnd 9005 |
. . . . . . . . . . . . . . . 16
⊢
((((∀𝑥((𝑥 ⊆ ℕ ∧
∀𝑚 ∈ ℕ
∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni)
∧ 𝑦 ⊆ {1}) ∧
𝑚 ∈ ℕ) →
(𝑚 + 1) ∈
ℕ) |
| 49 | 48 | nnzd 9447 |
. . . . . . . . . . . . . . 15
⊢
((((∀𝑥((𝑥 ⊆ ℕ ∧
∀𝑚 ∈ ℕ
∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni)
∧ 𝑦 ⊆ {1}) ∧
𝑚 ∈ ℕ) →
(𝑚 + 1) ∈
ℤ) |
| 50 | | 0p1e1 9104 |
. . . . . . . . . . . . . . . . 17
⊢ (0 + 1) =
1 |
| 51 | | 0red 8027 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑚 ∈ ℕ → 0 ∈
ℝ) |
| 52 | | nnre 8997 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑚 ∈ ℕ → 𝑚 ∈
ℝ) |
| 53 | | 1red 8041 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑚 ∈ ℕ → 1 ∈
ℝ) |
| 54 | | nngt0 9015 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑚 ∈ ℕ → 0 <
𝑚) |
| 55 | 51, 52, 53, 54 | ltadd1dd 8583 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 ∈ ℕ → (0 + 1)
< (𝑚 +
1)) |
| 56 | 50, 55 | eqbrtrrid 4069 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 ∈ ℕ → 1 <
(𝑚 + 1)) |
| 57 | 56 | adantl 277 |
. . . . . . . . . . . . . . 15
⊢
((((∀𝑥((𝑥 ⊆ ℕ ∧
∀𝑚 ∈ ℕ
∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni)
∧ 𝑦 ⊆ {1}) ∧
𝑚 ∈ ℕ) → 1
< (𝑚 +
1)) |
| 58 | | eluz2b1 9675 |
. . . . . . . . . . . . . . 15
⊢ ((𝑚 + 1) ∈
(ℤ≥‘2) ↔ ((𝑚 + 1) ∈ ℤ ∧ 1 < (𝑚 + 1))) |
| 59 | 49, 57, 58 | sylanbrc 417 |
. . . . . . . . . . . . . 14
⊢
((((∀𝑥((𝑥 ⊆ ℕ ∧
∀𝑚 ∈ ℕ
∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni)
∧ 𝑦 ⊆ {1}) ∧
𝑚 ∈ ℕ) →
(𝑚 + 1) ∈
(ℤ≥‘2)) |
| 60 | | elun2 3331 |
. . . . . . . . . . . . . 14
⊢ ((𝑚 + 1) ∈
(ℤ≥‘2) → (𝑚 + 1) ∈ (𝑦 ∪
(ℤ≥‘2))) |
| 61 | 59, 60 | syl 14 |
. . . . . . . . . . . . 13
⊢
((((∀𝑥((𝑥 ⊆ ℕ ∧
∀𝑚 ∈ ℕ
∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni)
∧ 𝑦 ⊆ {1}) ∧
𝑚 ∈ ℕ) →
(𝑚 + 1) ∈ (𝑦 ∪
(ℤ≥‘2))) |
| 62 | 47 | nnred 9003 |
. . . . . . . . . . . . . 14
⊢
((((∀𝑥((𝑥 ⊆ ℕ ∧
∀𝑚 ∈ ℕ
∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni)
∧ 𝑦 ⊆ {1}) ∧
𝑚 ∈ ℕ) →
𝑚 ∈
ℝ) |
| 63 | 62 | ltp1d 8957 |
. . . . . . . . . . . . 13
⊢
((((∀𝑥((𝑥 ⊆ ℕ ∧
∀𝑚 ∈ ℕ
∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni)
∧ 𝑦 ⊆ {1}) ∧
𝑚 ∈ ℕ) →
𝑚 < (𝑚 + 1)) |
| 64 | | breq2 4037 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = (𝑚 + 1) → (𝑚 < 𝑛 ↔ 𝑚 < (𝑚 + 1))) |
| 65 | 64 | rspcev 2868 |
. . . . . . . . . . . . 13
⊢ (((𝑚 + 1) ∈ (𝑦 ∪ (ℤ≥‘2))
∧ 𝑚 < (𝑚 + 1)) → ∃𝑛 ∈ (𝑦 ∪ (ℤ≥‘2))𝑚 < 𝑛) |
| 66 | 61, 63, 65 | syl2anc 411 |
. . . . . . . . . . . 12
⊢
((((∀𝑥((𝑥 ⊆ ℕ ∧
∀𝑚 ∈ ℕ
∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni)
∧ 𝑦 ⊆ {1}) ∧
𝑚 ∈ ℕ) →
∃𝑛 ∈ (𝑦 ∪
(ℤ≥‘2))𝑚 < 𝑛) |
| 67 | 66 | ex 115 |
. . . . . . . . . . 11
⊢
(((∀𝑥((𝑥 ⊆ ℕ ∧
∀𝑚 ∈ ℕ
∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni)
∧ 𝑦 ⊆ {1}) →
(𝑚 ∈ ℕ →
∃𝑛 ∈ (𝑦 ∪
(ℤ≥‘2))𝑚 < 𝑛)) |
| 68 | 46, 67 | ralrimi 2568 |
. . . . . . . . . 10
⊢
(((∀𝑥((𝑥 ⊆ ℕ ∧
∀𝑚 ∈ ℕ
∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni)
∧ 𝑦 ⊆ {1}) →
∀𝑚 ∈ ℕ
∃𝑛 ∈ (𝑦 ∪
(ℤ≥‘2))𝑚 < 𝑛) |
| 69 | 1, 11 | unex 4476 |
. . . . . . . . . . . 12
⊢ (𝑦 ∪
(ℤ≥‘2)) ∈ V |
| 70 | | sseq1 3206 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (𝑦 ∪ (ℤ≥‘2))
→ (𝑥 ⊆ ℕ
↔ (𝑦 ∪
(ℤ≥‘2)) ⊆ ℕ)) |
| 71 | | rexeq 2694 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (𝑦 ∪ (ℤ≥‘2))
→ (∃𝑛 ∈
𝑥 𝑚 < 𝑛 ↔ ∃𝑛 ∈ (𝑦 ∪ (ℤ≥‘2))𝑚 < 𝑛)) |
| 72 | 71 | ralbidv 2497 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (𝑦 ∪ (ℤ≥‘2))
→ (∀𝑚 ∈
ℕ ∃𝑛 ∈
𝑥 𝑚 < 𝑛 ↔ ∀𝑚 ∈ ℕ ∃𝑛 ∈ (𝑦 ∪ (ℤ≥‘2))𝑚 < 𝑛)) |
| 73 | 70, 72 | anbi12d 473 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝑦 ∪ (ℤ≥‘2))
→ ((𝑥 ⊆ ℕ
∧ ∀𝑚 ∈
ℕ ∃𝑛 ∈
𝑥 𝑚 < 𝑛) ↔ ((𝑦 ∪ (ℤ≥‘2))
⊆ ℕ ∧ ∀𝑚 ∈ ℕ ∃𝑛 ∈ (𝑦 ∪ (ℤ≥‘2))𝑚 < 𝑛))) |
| 74 | | breq1 4036 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝑦 ∪ (ℤ≥‘2))
→ (𝑥 ≈ ℕ
↔ (𝑦 ∪
(ℤ≥‘2)) ≈ ℕ)) |
| 75 | 73, 74 | imbi12d 234 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑦 ∪ (ℤ≥‘2))
→ (((𝑥 ⊆ ℕ
∧ ∀𝑚 ∈
ℕ ∃𝑛 ∈
𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ↔ (((𝑦 ∪
(ℤ≥‘2)) ⊆ ℕ ∧ ∀𝑚 ∈ ℕ ∃𝑛 ∈ (𝑦 ∪ (ℤ≥‘2))𝑚 < 𝑛) → (𝑦 ∪ (ℤ≥‘2))
≈ ℕ))) |
| 76 | 69, 75 | spcv 2858 |
. . . . . . . . . . 11
⊢
(∀𝑥((𝑥 ⊆ ℕ ∧
∀𝑚 ∈ ℕ
∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) → (((𝑦 ∪
(ℤ≥‘2)) ⊆ ℕ ∧ ∀𝑚 ∈ ℕ ∃𝑛 ∈ (𝑦 ∪ (ℤ≥‘2))𝑚 < 𝑛) → (𝑦 ∪ (ℤ≥‘2))
≈ ℕ)) |
| 77 | 76 | ad2antrr 488 |
. . . . . . . . . 10
⊢
(((∀𝑥((𝑥 ⊆ ℕ ∧
∀𝑚 ∈ ℕ
∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni)
∧ 𝑦 ⊆ {1}) →
(((𝑦 ∪
(ℤ≥‘2)) ⊆ ℕ ∧ ∀𝑚 ∈ ℕ ∃𝑛 ∈ (𝑦 ∪ (ℤ≥‘2))𝑚 < 𝑛) → (𝑦 ∪ (ℤ≥‘2))
≈ ℕ)) |
| 78 | 36, 68, 77 | mp2and 433 |
. . . . . . . . 9
⊢
(((∀𝑥((𝑥 ⊆ ℕ ∧
∀𝑚 ∈ ℕ
∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni)
∧ 𝑦 ⊆ {1}) →
(𝑦 ∪
(ℤ≥‘2)) ≈ ℕ) |
| 79 | | entr 6843 |
. . . . . . . . 9
⊢ (((𝑦 ⊔
(ℤ≥‘2)) ≈ (𝑦 ∪ (ℤ≥‘2))
∧ (𝑦 ∪
(ℤ≥‘2)) ≈ ℕ) → (𝑦 ⊔ (ℤ≥‘2))
≈ ℕ) |
| 80 | 27, 78, 79 | syl2anc 411 |
. . . . . . . 8
⊢
(((∀𝑥((𝑥 ⊆ ℕ ∧
∀𝑚 ∈ ℕ
∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni)
∧ 𝑦 ⊆ {1}) →
(𝑦 ⊔
(ℤ≥‘2)) ≈ ℕ) |
| 81 | | entr 6843 |
. . . . . . . 8
⊢ (((𝑦 ⊔ ℕ) ≈
(𝑦 ⊔
(ℤ≥‘2)) ∧ (𝑦 ⊔ (ℤ≥‘2))
≈ ℕ) → (𝑦
⊔ ℕ) ≈ ℕ) |
| 82 | 8, 80, 81 | sylancr 414 |
. . . . . . 7
⊢
(((∀𝑥((𝑥 ⊆ ℕ ∧
∀𝑚 ∈ ℕ
∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni)
∧ 𝑦 ⊆ {1}) →
(𝑦 ⊔ ℕ)
≈ ℕ) |
| 83 | 82 | ensymd 6842 |
. . . . . 6
⊢
(((∀𝑥((𝑥 ⊆ ℕ ∧
∀𝑚 ∈ ℕ
∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni)
∧ 𝑦 ⊆ {1}) →
ℕ ≈ (𝑦 ⊔
ℕ)) |
| 84 | | bren 6806 |
. . . . . 6
⊢ (ℕ
≈ (𝑦 ⊔
ℕ) ↔ ∃𝑓
𝑓:ℕ–1-1-onto→(𝑦 ⊔ ℕ)) |
| 85 | 83, 84 | sylib 122 |
. . . . 5
⊢
(((∀𝑥((𝑥 ⊆ ℕ ∧
∀𝑚 ∈ ℕ
∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni)
∧ 𝑦 ⊆ {1}) →
∃𝑓 𝑓:ℕ–1-1-onto→(𝑦 ⊔ ℕ)) |
| 86 | | simpllr 534 |
. . . . . . . . 9
⊢
((((∀𝑥((𝑥 ⊆ ℕ ∧
∀𝑚 ∈ ℕ
∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni)
∧ 𝑦 ⊆ {1}) ∧
𝑓:ℕ–1-1-onto→(𝑦 ⊔ ℕ)) → ω ∈
Omni) |
| 87 | | nnenom 10526 |
. . . . . . . . . 10
⊢ ℕ
≈ ω |
| 88 | | enomni 7205 |
. . . . . . . . . 10
⊢ (ℕ
≈ ω → (ℕ ∈ Omni ↔ ω ∈
Omni)) |
| 89 | 87, 88 | ax-mp 5 |
. . . . . . . . 9
⊢ (ℕ
∈ Omni ↔ ω ∈ Omni) |
| 90 | 86, 89 | sylibr 134 |
. . . . . . . 8
⊢
((((∀𝑥((𝑥 ⊆ ℕ ∧
∀𝑚 ∈ ℕ
∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni)
∧ 𝑦 ⊆ {1}) ∧
𝑓:ℕ–1-1-onto→(𝑦 ⊔ ℕ)) → ℕ ∈
Omni) |
| 91 | | f1ofo 5511 |
. . . . . . . . 9
⊢ (𝑓:ℕ–1-1-onto→(𝑦 ⊔ ℕ) → 𝑓:ℕ–onto→(𝑦 ⊔ ℕ)) |
| 92 | 91 | adantl 277 |
. . . . . . . 8
⊢
((((∀𝑥((𝑥 ⊆ ℕ ∧
∀𝑚 ∈ ℕ
∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni)
∧ 𝑦 ⊆ {1}) ∧
𝑓:ℕ–1-1-onto→(𝑦 ⊔ ℕ)) → 𝑓:ℕ–onto→(𝑦 ⊔ ℕ)) |
| 93 | 90, 92 | fodjuomni 7215 |
. . . . . . 7
⊢
((((∀𝑥((𝑥 ⊆ ℕ ∧
∀𝑚 ∈ ℕ
∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni)
∧ 𝑦 ⊆ {1}) ∧
𝑓:ℕ–1-1-onto→(𝑦 ⊔ ℕ)) → (∃𝑤 𝑤 ∈ 𝑦 ∨ 𝑦 = ∅)) |
| 94 | 93 | orcomd 730 |
. . . . . 6
⊢
((((∀𝑥((𝑥 ⊆ ℕ ∧
∀𝑚 ∈ ℕ
∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni)
∧ 𝑦 ⊆ {1}) ∧
𝑓:ℕ–1-1-onto→(𝑦 ⊔ ℕ)) → (𝑦 = ∅ ∨ ∃𝑤 𝑤 ∈ 𝑦)) |
| 95 | | simplr 528 |
. . . . . . . 8
⊢
((((∀𝑥((𝑥 ⊆ ℕ ∧
∀𝑚 ∈ ℕ
∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni)
∧ 𝑦 ⊆ {1}) ∧
𝑓:ℕ–1-1-onto→(𝑦 ⊔ ℕ)) → 𝑦 ⊆ {1}) |
| 96 | | sssnm 3784 |
. . . . . . . 8
⊢
(∃𝑤 𝑤 ∈ 𝑦 → (𝑦 ⊆ {1} ↔ 𝑦 = {1})) |
| 97 | 95, 96 | syl5ibcom 155 |
. . . . . . 7
⊢
((((∀𝑥((𝑥 ⊆ ℕ ∧
∀𝑚 ∈ ℕ
∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni)
∧ 𝑦 ⊆ {1}) ∧
𝑓:ℕ–1-1-onto→(𝑦 ⊔ ℕ)) → (∃𝑤 𝑤 ∈ 𝑦 → 𝑦 = {1})) |
| 98 | 97 | orim2d 789 |
. . . . . 6
⊢
((((∀𝑥((𝑥 ⊆ ℕ ∧
∀𝑚 ∈ ℕ
∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni)
∧ 𝑦 ⊆ {1}) ∧
𝑓:ℕ–1-1-onto→(𝑦 ⊔ ℕ)) → ((𝑦 = ∅ ∨ ∃𝑤 𝑤 ∈ 𝑦) → (𝑦 = ∅ ∨ 𝑦 = {1}))) |
| 99 | 94, 98 | mpd 13 |
. . . . 5
⊢
((((∀𝑥((𝑥 ⊆ ℕ ∧
∀𝑚 ∈ ℕ
∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni)
∧ 𝑦 ⊆ {1}) ∧
𝑓:ℕ–1-1-onto→(𝑦 ⊔ ℕ)) → (𝑦 = ∅ ∨ 𝑦 = {1})) |
| 100 | 85, 99 | exlimddv 1913 |
. . . 4
⊢
(((∀𝑥((𝑥 ⊆ ℕ ∧
∀𝑚 ∈ ℕ
∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni)
∧ 𝑦 ⊆ {1}) →
(𝑦 = ∅ ∨ 𝑦 = {1})) |
| 101 | 100 | ex 115 |
. . 3
⊢
((∀𝑥((𝑥 ⊆ ℕ ∧
∀𝑚 ∈ ℕ
∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni)
→ (𝑦 ⊆ {1}
→ (𝑦 = ∅ ∨
𝑦 = {1}))) |
| 102 | 101 | alrimiv 1888 |
. 2
⊢
((∀𝑥((𝑥 ⊆ ℕ ∧
∀𝑚 ∈ ℕ
∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni)
→ ∀𝑦(𝑦 ⊆ {1} → (𝑦 = ∅ ∨ 𝑦 = {1}))) |
| 103 | | exmidsssnc 4236 |
. . 3
⊢ (1 ∈
ℕ → (EXMID ↔ ∀𝑦(𝑦 ⊆ {1} → (𝑦 = ∅ ∨ 𝑦 = {1})))) |
| 104 | 29, 103 | ax-mp 5 |
. 2
⊢
(EXMID ↔ ∀𝑦(𝑦 ⊆ {1} → (𝑦 = ∅ ∨ 𝑦 = {1}))) |
| 105 | 102, 104 | sylibr 134 |
1
⊢
((∀𝑥((𝑥 ⊆ ℕ ∧
∀𝑚 ∈ ℕ
∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni)
→ EXMID) |