Metamath Proof Explorer

Theorem lubfun

Description: The LUB is a function. (Contributed by NM, 9-Sep-2018)

Ref Expression
Hypothesis lubfun.u ⊢ U = lub ⁡ K
Assertion lubfun ⊢ Fun ⁡ U

Proof

Step Hyp Ref Expression
1 lubfun.u ⊢ U = lub ⁡ K
2 funmpt ⊢ Fun ⁡ s ∈ 𝒫 Base K ⟼ ι x ∈ Base K | ∀ y ∈ s y ≤ K x ∧ ∀ z ∈ Base K ∀ y ∈ s y ≤ K z → x ≤ K z
3 funres ⊢ Fun ⁡ s ∈ 𝒫 Base K ⟼ ι x ∈ Base K | ∀ y ∈ s y ≤ K x ∧ ∀ z ∈ Base K ∀ y ∈ s y ≤ K z → x ≤ K z → Fun ⁡ s ∈ 𝒫 Base K ⟼ ι x ∈ Base K | ∀ y ∈ s y ≤ K x ∧ ∀ z ∈ Base K ∀ y ∈ s y ≤ K z → x ≤ K z ↾ s | ∃! x ∈ Base K ∀ y ∈ s y ≤ K x ∧ ∀ z ∈ Base K ∀ y ∈ s y ≤ K z → x ≤ K z
4 2 3 ax-mp ⊢ Fun ⁡ s ∈ 𝒫 Base K ⟼ ι x ∈ Base K | ∀ y ∈ s y ≤ K x ∧ ∀ z ∈ Base K ∀ y ∈ s y ≤ K z → x ≤ K z ↾ s | ∃! x ∈ Base K ∀ y ∈ s y ≤ K x ∧ ∀ z ∈ Base K ∀ y ∈ s y ≤ K z → x ≤ K z
5 eqid ⊢ Base K = Base K
6 eqid ⊢ ≤ K = ≤ K
7 biid ⊢ ∀ y ∈ s y ≤ K x ∧ ∀ z ∈ Base K ∀ y ∈ s y ≤ K z → x ≤ K z ↔ ∀ y ∈ s y ≤ K x ∧ ∀ z ∈ Base K ∀ y ∈ s y ≤ K z → x ≤ K z
8 id ⊢ K ∈ V → K ∈ V
9 5 6 1 7 8 lubfval ⊢ K ∈ V → U = s ∈ 𝒫 Base K ⟼ ι x ∈ Base K | ∀ y ∈ s y ≤ K x ∧ ∀ z ∈ Base K ∀ y ∈ s y ≤ K z → x ≤ K z ↾ s | ∃! x ∈ Base K ∀ y ∈ s y ≤ K x ∧ ∀ z ∈ Base K ∀ y ∈ s y ≤ K z → x ≤ K z
10 9 funeqd ⊢ K ∈ V → Fun ⁡ U ↔ Fun ⁡ s ∈ 𝒫 Base K ⟼ ι x ∈ Base K | ∀ y ∈ s y ≤ K x ∧ ∀ z ∈ Base K ∀ y ∈ s y ≤ K z → x ≤ K z ↾ s | ∃! x ∈ Base K ∀ y ∈ s y ≤ K x ∧ ∀ z ∈ Base K ∀ y ∈ s y ≤ K z → x ≤ K z
11 4 10 mpbiri ⊢ K ∈ V → Fun ⁡ U
12 fun0 ⊢ Fun ⁡ ∅
13 fvprc ⊢ ¬ K ∈ V → lub ⁡ K = ∅
14 1 13 syl5eq ⊢ ¬ K ∈ V → U = ∅
15 14 funeqd ⊢ ¬ K ∈ V → Fun ⁡ U ↔ Fun ⁡ ∅
16 12 15 mpbiri ⊢ ¬ K ∈ V → Fun ⁡ U
17 11 16 pm2.61i ⊢ Fun ⁡ U