This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 eqtrid ⊢ ( ¬ 𝐾 ∈ V → 𝐺 = ∅ )
15 14 funeqd ⊢ ( ¬ 𝐾 ∈ V → ( Fun 𝐺 ↔ Fun ∅ ) )
16 12 15 mpbiri ⊢ ( ¬ 𝐾 ∈ V → Fun 𝐺 )
17 11 16 pm2.61i ⊢ Fun 𝐺