Theorem glbfun

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

	Ref	Expression
Hypothesis	glbfun.g	⊢ 𝐺 = ( glb ‘ 𝐾 )
Assertion	glbfun	⊢ Fun 𝐺

Proof

Step	Hyp	Ref	Expression
1		glbfun.g	⊢ 𝐺 = ( glb ‘ 𝐾 )
2		funmpt	⊢ Fun ( 𝑠 ∈ 𝒫 ( Base ‘ 𝐾 ) ↦ ( ℩ 𝑥 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑠 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑠 𝑧 ( le ‘ 𝐾 ) 𝑦 → 𝑧 ( le ‘ 𝐾 ) 𝑥 ) ) ) )
3		funres	⊢ ( Fun ( 𝑠 ∈ 𝒫 ( Base ‘ 𝐾 ) ↦ ( ℩ 𝑥 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑠 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑠 𝑧 ( le ‘ 𝐾 ) 𝑦 → 𝑧 ( le ‘ 𝐾 ) 𝑥 ) ) ) ) → Fun ( ( 𝑠 ∈ 𝒫 ( Base ‘ 𝐾 ) ↦ ( ℩ 𝑥 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑠 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑠 𝑧 ( le ‘ 𝐾 ) 𝑦 → 𝑧 ( le ‘ 𝐾 ) 𝑥 ) ) ) ) ↾ { 𝑠 ∣ ∃! 𝑥 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑠 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑠 𝑧 ( le ‘ 𝐾 ) 𝑦 → 𝑧 ( le ‘ 𝐾 ) 𝑥 ) ) } ) )
4	2 3	ax-mp	⊢ Fun ( ( 𝑠 ∈ 𝒫 ( Base ‘ 𝐾 ) ↦ ( ℩ 𝑥 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑠 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑠 𝑧 ( le ‘ 𝐾 ) 𝑦 → 𝑧 ( le ‘ 𝐾 ) 𝑥 ) ) ) ) ↾ { 𝑠 ∣ ∃! 𝑥 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑠 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑠 𝑧 ( le ‘ 𝐾 ) 𝑦 → 𝑧 ( le ‘ 𝐾 ) 𝑥 ) ) } )
5		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
6		eqid	⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
7		biid	⊢ ( ( ∀ 𝑦 ∈ 𝑠 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑠 𝑧 ( le ‘ 𝐾 ) 𝑦 → 𝑧 ( le ‘ 𝐾 ) 𝑥 ) ) ↔ ( ∀ 𝑦 ∈ 𝑠 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑠 𝑧 ( le ‘ 𝐾 ) 𝑦 → 𝑧 ( le ‘ 𝐾 ) 𝑥 ) ) )
8		id	⊢ ( 𝐾 ∈ V → 𝐾 ∈ V )
9	5 6 1 7 8	glbfval	⊢ ( 𝐾 ∈ V → 𝐺 = ( ( 𝑠 ∈ 𝒫 ( Base ‘ 𝐾 ) ↦ ( ℩ 𝑥 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑠 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑠 𝑧 ( le ‘ 𝐾 ) 𝑦 → 𝑧 ( le ‘ 𝐾 ) 𝑥 ) ) ) ) ↾ { 𝑠 ∣ ∃! 𝑥 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑠 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑠 𝑧 ( le ‘ 𝐾 ) 𝑦 → 𝑧 ( le ‘ 𝐾 ) 𝑥 ) ) } ) )
10	9	funeqd	⊢ ( 𝐾 ∈ V → ( Fun 𝐺 ↔ Fun ( ( 𝑠 ∈ 𝒫 ( Base ‘ 𝐾 ) ↦ ( ℩ 𝑥 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑠 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑠 𝑧 ( le ‘ 𝐾 ) 𝑦 → 𝑧 ( le ‘ 𝐾 ) 𝑥 ) ) ) ) ↾ { 𝑠 ∣ ∃! 𝑥 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑠 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑠 𝑧 ( le ‘ 𝐾 ) 𝑦 → 𝑧 ( le ‘ 𝐾 ) 𝑥 ) ) } ) ) )
11	4 10	mpbiri	⊢ ( 𝐾 ∈ V → Fun 𝐺 )
12		fun0	⊢ Fun ∅
13		fvprc	⊢ ( ¬ 𝐾 ∈ V → ( glb ‘ 𝐾 ) = ∅ )
14	1 13	syl5eq	⊢ ( ¬ 𝐾 ∈ V → 𝐺 = ∅ )
15	14	funeqd	⊢ ( ¬ 𝐾 ∈ V → ( Fun 𝐺 ↔ Fun ∅ ) )
16	12 15	mpbiri	⊢ ( ¬ 𝐾 ∈ V → Fun 𝐺 )
17	11 16	pm2.61i	⊢ Fun 𝐺