| Step | Hyp | Ref
| Expression |
| 1 | | funmpt 6604 |
. . . 4
⊢ Fun
(𝑠 ∈ 𝒫
(Base‘𝐾) ↦
(℩𝑥 ∈
(Base‘𝐾)(∀𝑦 ∈ 𝑠 𝑦(le‘𝐾)𝑥 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ 𝑠 𝑦(le‘𝐾)𝑧 → 𝑥(le‘𝐾)𝑧)))) |
| 2 | | funres 6608 |
. . . 4
⊢ (Fun
(𝑠 ∈ 𝒫
(Base‘𝐾) ↦
(℩𝑥 ∈
(Base‘𝐾)(∀𝑦 ∈ 𝑠 𝑦(le‘𝐾)𝑥 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ 𝑠 𝑦(le‘𝐾)𝑧 → 𝑥(le‘𝐾)𝑧)))) → Fun ((𝑠 ∈ 𝒫 (Base‘𝐾) ↦ (℩𝑥 ∈ (Base‘𝐾)(∀𝑦 ∈ 𝑠 𝑦(le‘𝐾)𝑥 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ 𝑠 𝑦(le‘𝐾)𝑧 → 𝑥(le‘𝐾)𝑧)))) ↾ {𝑠 ∣ ∃!𝑥 ∈ (Base‘𝐾)(∀𝑦 ∈ 𝑠 𝑦(le‘𝐾)𝑥 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ 𝑠 𝑦(le‘𝐾)𝑧 → 𝑥(le‘𝐾)𝑧))})) |
| 3 | 1, 2 | ax-mp 5 |
. . 3
⊢ Fun
((𝑠 ∈ 𝒫
(Base‘𝐾) ↦
(℩𝑥 ∈
(Base‘𝐾)(∀𝑦 ∈ 𝑠 𝑦(le‘𝐾)𝑥 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ 𝑠 𝑦(le‘𝐾)𝑧 → 𝑥(le‘𝐾)𝑧)))) ↾ {𝑠 ∣ ∃!𝑥 ∈ (Base‘𝐾)(∀𝑦 ∈ 𝑠 𝑦(le‘𝐾)𝑥 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ 𝑠 𝑦(le‘𝐾)𝑧 → 𝑥(le‘𝐾)𝑧))}) |
| 4 | | eqid 2737 |
. . . . 5
⊢
(Base‘𝐾) =
(Base‘𝐾) |
| 5 | | eqid 2737 |
. . . . 5
⊢
(le‘𝐾) =
(le‘𝐾) |
| 6 | | lubfun.u |
. . . . 5
⊢ 𝑈 = (lub‘𝐾) |
| 7 | | biid 261 |
. . . . 5
⊢
((∀𝑦 ∈
𝑠 𝑦(le‘𝐾)𝑥 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ 𝑠 𝑦(le‘𝐾)𝑧 → 𝑥(le‘𝐾)𝑧)) ↔ (∀𝑦 ∈ 𝑠 𝑦(le‘𝐾)𝑥 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ 𝑠 𝑦(le‘𝐾)𝑧 → 𝑥(le‘𝐾)𝑧))) |
| 8 | | id 22 |
. . . . 5
⊢ (𝐾 ∈ V → 𝐾 ∈ V) |
| 9 | 4, 5, 6, 7, 8 | lubfval 18395 |
. . . 4
⊢ (𝐾 ∈ V → 𝑈 = ((𝑠 ∈ 𝒫 (Base‘𝐾) ↦ (℩𝑥 ∈ (Base‘𝐾)(∀𝑦 ∈ 𝑠 𝑦(le‘𝐾)𝑥 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ 𝑠 𝑦(le‘𝐾)𝑧 → 𝑥(le‘𝐾)𝑧)))) ↾ {𝑠 ∣ ∃!𝑥 ∈ (Base‘𝐾)(∀𝑦 ∈ 𝑠 𝑦(le‘𝐾)𝑥 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ 𝑠 𝑦(le‘𝐾)𝑧 → 𝑥(le‘𝐾)𝑧))})) |
| 10 | 9 | funeqd 6588 |
. . 3
⊢ (𝐾 ∈ V → (Fun 𝑈 ↔ Fun ((𝑠 ∈ 𝒫 (Base‘𝐾) ↦ (℩𝑥 ∈ (Base‘𝐾)(∀𝑦 ∈ 𝑠 𝑦(le‘𝐾)𝑥 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ 𝑠 𝑦(le‘𝐾)𝑧 → 𝑥(le‘𝐾)𝑧)))) ↾ {𝑠 ∣ ∃!𝑥 ∈ (Base‘𝐾)(∀𝑦 ∈ 𝑠 𝑦(le‘𝐾)𝑥 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ 𝑠 𝑦(le‘𝐾)𝑧 → 𝑥(le‘𝐾)𝑧))}))) |
| 11 | 3, 10 | mpbiri 258 |
. 2
⊢ (𝐾 ∈ V → Fun 𝑈) |
| 12 | | fun0 6631 |
. . 3
⊢ Fun
∅ |
| 13 | | fvprc 6898 |
. . . . 5
⊢ (¬
𝐾 ∈ V →
(lub‘𝐾) =
∅) |
| 14 | 6, 13 | eqtrid 2789 |
. . . 4
⊢ (¬
𝐾 ∈ V → 𝑈 = ∅) |
| 15 | 14 | funeqd 6588 |
. . 3
⊢ (¬
𝐾 ∈ V → (Fun
𝑈 ↔ Fun
∅)) |
| 16 | 12, 15 | mpbiri 258 |
. 2
⊢ (¬
𝐾 ∈ V → Fun 𝑈) |
| 17 | 11, 16 | pm2.61i 182 |
1
⊢ Fun 𝑈 |