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

Metamath Proof Explorer

Theorem lubsn

Description: The least upper bound of a singleton. ( chsupsn analog.) (Contributed by NM, 20-Oct-2011)

Ref Expression
Hypotheses lubsn.b ⊢ B = Base K
lubsn.u ⊢ U = lub ⁡ K
Assertion lubsn ⊢ K ∈ Lat ∧ X ∈ B → U ⁡ X = X

Proof

Step Hyp Ref Expression
1 lubsn.b ⊢ B = Base K
2 lubsn.u ⊢ U = lub ⁡ K
3 dfsn2 ⊢ X = X X
4 3 fveq2i ⊢ U ⁡ X = U ⁡ X X
5 eqid ⊢ join ⁡ K = join ⁡ K
6 simpl ⊢ K ∈ Lat ∧ X ∈ B → K ∈ Lat
7 simpr ⊢ K ∈ Lat ∧ X ∈ B → X ∈ B
8 2 5 6 7 7 joinval ⊢ K ∈ Lat ∧ X ∈ B → X join ⁡ K X = U ⁡ X X
9 4 8 eqtr4id ⊢ K ∈ Lat ∧ X ∈ B → U ⁡ X = X join ⁡ K X
10 1 5 latjidm ⊢ K ∈ Lat ∧ X ∈ B → X join ⁡ K X = X
11 9 10 eqtrd ⊢ K ∈ Lat ∧ X ∈ B → U ⁡ X = X