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 \in 𝒫 {Base}_{K} ⟼ (ι x \in {Base}_{K} \| (\forall y \in s x \leq_{K} y \land \forall z \in {Base}_{K} (\forall y \in s z \leq_{K} y \to z \leq_{K} x))))$
3		funres	$⊢ Fun (s \in 𝒫 {Base}_{K} ⟼ (ι x \in {Base}_{K} \| (\forall y \in s x \leq_{K} y \land \forall z \in {Base}_{K} (\forall y \in s z \leq_{K} y \to z \leq_{K} x)))) \to Fun ({(s \in 𝒫 {Base}_{K} ⟼ (ι x \in {Base}_{K} \| (\forall y \in s x \leq_{K} y \land \forall z \in {Base}_{K} (\forall y \in s z \leq_{K} y \to z \leq_{K} x)))) ↾}_{\{s \| \exists! x \in {Base}_{K} (\forall y \in s x \leq_{K} y \land \forall z \in {Base}_{K} (\forall y \in s z \leq_{K} y \to z \leq_{K} x))\}})$
4	2 3	ax-mp	$⊢ Fun ({(s \in 𝒫 {Base}_{K} ⟼ (ι x \in {Base}_{K} \| (\forall y \in s x \leq_{K} y \land \forall z \in {Base}_{K} (\forall y \in s z \leq_{K} y \to z \leq_{K} x)))) ↾}_{\{s \| \exists! x \in {Base}_{K} (\forall y \in s x \leq_{K} y \land \forall z \in {Base}_{K} (\forall y \in s z \leq_{K} y \to z \leq_{K} x))\}})$
5		eqid	$⊢ {Base}_{K} = {Base}_{K}$
6		eqid	$⊢ \leq_{K} = \leq_{K}$
7		biid	$⊢ (\forall y \in s x \leq_{K} y \land \forall z \in {Base}_{K} (\forall y \in s z \leq_{K} y \to z \leq_{K} x)) \leftrightarrow (\forall y \in s x \leq_{K} y \land \forall z \in {Base}_{K} (\forall y \in s z \leq_{K} y \to z \leq_{K} x))$
8		id	$⊢ K \in V \to K \in V$
9	5 6 1 7 8	glbfval	$⊢ K \in V \to G = {(s \in 𝒫 {Base}_{K} ⟼ (ι x \in {Base}_{K} \| (\forall y \in s x \leq_{K} y \land \forall z \in {Base}_{K} (\forall y \in s z \leq_{K} y \to z \leq_{K} x)))) ↾}_{\{s \| \exists! x \in {Base}_{K} (\forall y \in s x \leq_{K} y \land \forall z \in {Base}_{K} (\forall y \in s z \leq_{K} y \to z \leq_{K} x))\}}$
10	9	funeqd	$⊢ K \in V \to (Fun G \leftrightarrow Fun ({(s \in 𝒫 {Base}_{K} ⟼ (ι x \in {Base}_{K} \| (\forall y \in s x \leq_{K} y \land \forall z \in {Base}_{K} (\forall y \in s z \leq_{K} y \to z \leq_{K} x)))) ↾}_{\{s \| \exists! x \in {Base}_{K} (\forall y \in s x \leq_{K} y \land \forall z \in {Base}_{K} (\forall y \in s z \leq_{K} y \to z \leq_{K} x))\}}))$
11	4 10	mpbiri	$⊢ K \in V \to Fun G$
12		fun0	$⊢ Fun \emptyset$
13		fvprc	$⊢ \neg K \in V \to glb (K) = \emptyset$
14	1 13	eqtrid	$⊢ \neg K \in V \to G = \emptyset$
15	14	funeqd	$⊢ \neg K \in V \to (Fun G \leftrightarrow Fun \emptyset)$
16	12 15	mpbiri	$⊢ \neg K \in V \to Fun G$
17	11 16	pm2.61i	$⊢ Fun G$