Metamath Proof Explorer

Theorem lubeldm2

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

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

Proof

Step Hyp Ref Expression
1 lubeldm2.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 lubeldm2.l ⊢ ≤ = ( le ‘ 𝐾 )
3 lubeldm2.u ⊢ 𝑈 = ( lub ‘ 𝐾 )
4 lubeldm2.p ⊢ ( 𝜓 ↔ ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) )
5 lubeldm2.k ⊢ ( 𝜑 → 𝐾 ∈ Poset )
6 1 2 3 4 5 lubeldm ⊢ ( 𝜑 → ( 𝑆 ∈ dom 𝑈 ↔ ( 𝑆 ⊆ 𝐵 ∧ ∃! 𝑥 ∈ 𝐵 𝜓 ) ) )
7 6 biimpa ⊢ ( ( 𝜑 ∧ 𝑆 ∈ dom 𝑈 ) → ( 𝑆 ⊆ 𝐵 ∧ ∃! 𝑥 ∈ 𝐵 𝜓 ) )
8 reurex ⊢ ( ∃! 𝑥 ∈ 𝐵 𝜓 → ∃ 𝑥 ∈ 𝐵 𝜓 )
9 8 anim2i ⊢ ( ( 𝑆 ⊆ 𝐵 ∧ ∃! 𝑥 ∈ 𝐵 𝜓 ) → ( 𝑆 ⊆ 𝐵 ∧ ∃ 𝑥 ∈ 𝐵 𝜓 ) )
10 7 9 syl ⊢ ( ( 𝜑 ∧ 𝑆 ∈ dom 𝑈 ) → ( 𝑆 ⊆ 𝐵 ∧ ∃ 𝑥 ∈ 𝐵 𝜓 ) )
11 simpl ⊢ ( ( 𝜑 ∧ ( 𝑆 ⊆ 𝐵 ∧ ∃ 𝑥 ∈ 𝐵 𝜓 ) ) → 𝜑 )
12 simprl ⊢ ( ( 𝜑 ∧ ( 𝑆 ⊆ 𝐵 ∧ ∃ 𝑥 ∈ 𝐵 𝜓 ) ) → 𝑆 ⊆ 𝐵 )
13 2 1 poslubmo ⊢ ( ( 𝐾 ∈ 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 𝑈 ↔ ( 𝑆 ⊆ 𝐵 ∧ ∃ 𝑥 ∈ 𝐵 𝜓 ) ) )