Metamath Proof Explorer

Theorem glbeldm2

Description: Member of the domain of the greatest lower bound function of a poset. (Contributed by Zhi Wang, 26-Sep-2024)

Ref Expression
Hypotheses lubeldm2.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
lubeldm2.l ⊢ ≤ = ( le ‘ 𝐾 )
glbeldm2.g ⊢ 𝐺 = ( glb ‘ 𝐾 )
glbeldm2.p ⊢ ( 𝜓 ↔ ( ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) )
glbeldm2.k ⊢ ( 𝜑 → 𝐾 ∈ Poset )
Assertion glbeldm2 ( 𝜑 → ( 𝑆 ∈ dom 𝐺 ↔ ( 𝑆 ⊆ 𝐵 ∧ ∃ 𝑥 ∈ 𝐵 𝜓 ) ) )

Proof

Step Hyp Ref Expression
1 lubeldm2.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 lubeldm2.l ⊢ ≤ = ( le ‘ 𝐾 )
3 glbeldm2.g ⊢ 𝐺 = ( glb ‘ 𝐾 )
4 glbeldm2.p ⊢ ( 𝜓 ↔ ( ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) )
5 glbeldm2.k ⊢ ( 𝜑 → 𝐾 ∈ Poset )
6 1 2 3 4 5 glbeldm ⊢ ( 𝜑 → ( 𝑆 ∈ dom 𝐺 ↔ ( 𝑆 ⊆ 𝐵 ∧ ∃! 𝑥 ∈ 𝐵 𝜓 ) ) )
7 6 biimpa ⊢ ( ( 𝜑 ∧ 𝑆 ∈ dom 𝐺 ) → ( 𝑆 ⊆ 𝐵 ∧ ∃! 𝑥 ∈ 𝐵 𝜓 ) )
8 reurex ⊢ ( ∃! 𝑥 ∈ 𝐵 𝜓 → ∃ 𝑥 ∈ 𝐵 𝜓 )
9 8 anim2i ⊢ ( ( 𝑆 ⊆ 𝐵 ∧ ∃! 𝑥 ∈ 𝐵 𝜓 ) → ( 𝑆 ⊆ 𝐵 ∧ ∃ 𝑥 ∈ 𝐵 𝜓 ) )
10 7 9 syl ⊢ ( ( 𝜑 ∧ 𝑆 ∈ dom 𝐺 ) → ( 𝑆 ⊆ 𝐵 ∧ ∃ 𝑥 ∈ 𝐵 𝜓 ) )
11 simpl ⊢ ( ( 𝜑 ∧ ( 𝑆 ⊆ 𝐵 ∧ ∃ 𝑥 ∈ 𝐵 𝜓 ) ) → 𝜑 )
12 simprl ⊢ ( ( 𝜑 ∧ ( 𝑆 ⊆ 𝐵 ∧ ∃ 𝑥 ∈ 𝐵 𝜓 ) ) → 𝑆 ⊆ 𝐵 )
13 2 1 posglbmo ⊢ ( ( 𝐾 ∈ Poset ∧ 𝑆 ⊆ 𝐵 ) → ∃* 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) )
14 5 13 sylan ⊢ ( ( 𝜑 ∧ 𝑆 ⊆ 𝐵 ) → ∃* 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) )
15 4 rmobii ⊢ ( ∃* 𝑥 ∈ 𝐵 𝜓 ↔ ∃* 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) )
16 14 15 sylibr ⊢ ( ( 𝜑 ∧ 𝑆 ⊆ 𝐵 ) → ∃* 𝑥 ∈ 𝐵 𝜓 )
17 16 anim1ci ⊢ ( ( ( 𝜑 ∧ 𝑆 ⊆ 𝐵 ) ∧ ∃ 𝑥 ∈ 𝐵 𝜓 ) → ( ∃ 𝑥 ∈ 𝐵 𝜓 ∧ ∃* 𝑥 ∈ 𝐵 𝜓 ) )
18 reu5 ⊢ ( ∃! 𝑥 ∈ 𝐵 𝜓 ↔ ( ∃ 𝑥 ∈ 𝐵 𝜓 ∧ ∃* 𝑥 ∈ 𝐵 𝜓 ) )
19 17 18 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑆 ⊆ 𝐵 ) ∧ ∃ 𝑥 ∈ 𝐵 𝜓 ) → ∃! 𝑥 ∈ 𝐵 𝜓 )
20 19 anasss ⊢ ( ( 𝜑 ∧ ( 𝑆 ⊆ 𝐵 ∧ ∃ 𝑥 ∈ 𝐵 𝜓 ) ) → ∃! 𝑥 ∈ 𝐵 𝜓 )
21 6 biimpar ⊢ ( ( 𝜑 ∧ ( 𝑆 ⊆ 𝐵 ∧ ∃! 𝑥 ∈ 𝐵 𝜓 ) ) → 𝑆 ∈ dom 𝐺 )
22 11 12 20 21 syl12anc ⊢ ( ( 𝜑 ∧ ( 𝑆 ⊆ 𝐵 ∧ ∃ 𝑥 ∈ 𝐵 𝜓 ) ) → 𝑆 ∈ dom 𝐺 )
23 10 22 impbida ⊢ ( 𝜑 → ( 𝑆 ∈ dom 𝐺 ↔ ( 𝑆 ⊆ 𝐵 ∧ ∃ 𝑥 ∈ 𝐵 𝜓 ) ) )