Metamath Proof Explorer

Theorem glbfun

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

Ref Expression
Hypothesis glbfun.g ⊢ G = glb ⁡ K
Assertion glbfun ⊢ Fun ⁡ G

Proof

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