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

Metamath Proof Explorer

Theorem lublecl

Description: The set of all elements less than a given element has an LUB. (Contributed by NM, 8-Sep-2018)

Ref Expression
Hypotheses lublecl.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
lublecl.l ⊢ ≤ = ( le ‘ 𝐾 )
lublecl.u ⊢ 𝑈 = ( lub ‘ 𝐾 )
lublecl.k ⊢ ( 𝜑 → 𝐾 ∈ Poset )
lublecl.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
Assertion lublecl ( 𝜑 → { 𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑋 } ∈ dom 𝑈 )

Proof

Step Hyp Ref Expression
1 lublecl.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 lublecl.l ⊢ ≤ = ( le ‘ 𝐾 )
3 lublecl.u ⊢ 𝑈 = ( lub ‘ 𝐾 )
4 lublecl.k ⊢ ( 𝜑 → 𝐾 ∈ Poset )
5 lublecl.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6 ssrab2 ⊢ { 𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑋 } ⊆ 𝐵
7 6 a1i ⊢ ( 𝜑 → { 𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑋 } ⊆ 𝐵 )
8 1 2 3 4 5 lublecllem ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( ∀ 𝑧 ∈ { 𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑋 } 𝑧 ≤ 𝑥 ∧ ∀ 𝑤 ∈ 𝐵 ( ∀ 𝑧 ∈ { 𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑋 } 𝑧 ≤ 𝑤 → 𝑥 ≤ 𝑤 ) ) ↔ 𝑥 = 𝑋 ) )
9 8 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ( ( ∀ 𝑧 ∈ { 𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑋 } 𝑧 ≤ 𝑥 ∧ ∀ 𝑤 ∈ 𝐵 ( ∀ 𝑧 ∈ { 𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑋 } 𝑧 ≤ 𝑤 → 𝑥 ≤ 𝑤 ) ) ↔ 𝑥 = 𝑋 ) )
10 reu6i ⊢ ( ( 𝑋 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( ∀ 𝑧 ∈ { 𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑋 } 𝑧 ≤ 𝑥 ∧ ∀ 𝑤 ∈ 𝐵 ( ∀ 𝑧 ∈ { 𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑋 } 𝑧 ≤ 𝑤 → 𝑥 ≤ 𝑤 ) ) ↔ 𝑥 = 𝑋 ) ) → ∃! 𝑥 ∈ 𝐵 ( ∀ 𝑧 ∈ { 𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑋 } 𝑧 ≤ 𝑥 ∧ ∀ 𝑤 ∈ 𝐵 ( ∀ 𝑧 ∈ { 𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑋 } 𝑧 ≤ 𝑤 → 𝑥 ≤ 𝑤 ) ) )
11 5 9 10 syl2anc ⊢ ( 𝜑 → ∃! 𝑥 ∈ 𝐵 ( ∀ 𝑧 ∈ { 𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑋 } 𝑧 ≤ 𝑥 ∧ ∀ 𝑤 ∈ 𝐵 ( ∀ 𝑧 ∈ { 𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑋 } 𝑧 ≤ 𝑤 → 𝑥 ≤ 𝑤 ) ) )
12 biid ⊢ ( ( ∀ 𝑧 ∈ { 𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑋 } 𝑧 ≤ 𝑥 ∧ ∀ 𝑤 ∈ 𝐵 ( ∀ 𝑧 ∈ { 𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑋 } 𝑧 ≤ 𝑤 → 𝑥 ≤ 𝑤 ) ) ↔ ( ∀ 𝑧 ∈ { 𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑋 } 𝑧 ≤ 𝑥 ∧ ∀ 𝑤 ∈ 𝐵 ( ∀ 𝑧 ∈ { 𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑋 } 𝑧 ≤ 𝑤 → 𝑥 ≤ 𝑤 ) ) )
13 1 2 3 12 4 lubeldm ⊢ ( 𝜑 → ( { 𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑋 } ∈ dom 𝑈 ↔ ( { 𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑋 } ⊆ 𝐵 ∧ ∃! 𝑥 ∈ 𝐵 ( ∀ 𝑧 ∈ { 𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑋 } 𝑧 ≤ 𝑥 ∧ ∀ 𝑤 ∈ 𝐵 ( ∀ 𝑧 ∈ { 𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑋 } 𝑧 ≤ 𝑤 → 𝑥 ≤ 𝑤 ) ) ) ) )
14 7 11 13 mpbir2and ⊢ ( 𝜑 → { 𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑋 } ∈ dom 𝑈 )