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 𝑈 )