Metamath Proof Explorer

Theorem toslub

Description: In a toset, the lowest upper bound lub , defined for partial orders is the supremum, sup ( A , B , .< ) , defined for total orders. (these are the set.mm definitions: lowest upper bound and supremum are normally synonymous). Note that those two values are also equal if such a supremum does not exist: in that case, both are equal to the empty set. (Contributed by Thierry Arnoux, 15-Feb-2018) (Revised by Thierry Arnoux, 24-Sep-2018)

Ref Expression
Hypotheses toslub.b ⊢B=BaseK
toslub.l ⊢<˙=<K
toslub.1 ⊢φ→K∈Toset
toslub.2 ⊢φ→A⊆B
Assertion toslub ⊢φ→lub⁡K⁡A=supAB<˙

Proof

Step Hyp Ref Expression
1 toslub.b ⊢B=BaseK
2 toslub.l ⊢<˙=<K
3 toslub.1 ⊢φ→K∈Toset
4 toslub.2 ⊢φ→A⊆B
5 eqid ⊢≤K=≤K
6 1 2 3 4 5 toslublem ⊢φ∧a∈B→∀b∈Ab≤Ka∧∀c∈B∀b∈Ab≤Kc→a≤Kc↔∀b∈A¬a<˙b∧∀b∈Bb<˙a→∃d∈Ab<˙d
7 6 riotabidva ⊢φ→ιa∈B|∀b∈Ab≤Ka∧∀c∈B∀b∈Ab≤Kc→a≤Kc=ιa∈B|∀b∈A¬a<˙b∧∀b∈Bb<˙a→∃d∈Ab<˙d
8 eqid ⊢lub⁡K=lub⁡K
9 biid ⊢∀b∈Ab≤Ka∧∀c∈B∀b∈Ab≤Kc→a≤Kc↔∀b∈Ab≤Ka∧∀c∈B∀b∈Ab≤Kc→a≤Kc
10 1 5 8 9 3 4 lubval ⊢φ→lub⁡K⁡A=ιa∈B|∀b∈Ab≤Ka∧∀c∈B∀b∈Ab≤Kc→a≤Kc
11 1 5 2 tosso ⊢K∈Toset→K∈Toset↔<˙OrB∧I↾B⊆≤K
12 11 ibi ⊢K∈Toset→<˙OrB∧I↾B⊆≤K
13 12 simpld ⊢K∈Toset→<˙OrB
14 id ⊢<˙OrB→<˙OrB
15 14 supval2 ⊢<˙OrB→supAB<˙=ιa∈B|∀b∈A¬a<˙b∧∀b∈Bb<˙a→∃d∈Ab<˙d
16 3 13 15 3syl ⊢φ→supAB<˙=ιa∈B|∀b∈A¬a<˙b∧∀b∈Bb<˙a→∃d∈Ab<˙d
17 7 10 16 3eqtr4d ⊢φ→lub⁡K⁡A=supAB<˙