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