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 ⊢ 𝐵 = ( Base ‘ 𝐾 )
toslub.l ⊢ < = ( lt ‘ 𝐾 )
toslub.1 ⊢ ( 𝜑 → 𝐾 ∈ Toset )
toslub.2 ⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
Assertion toslub ( 𝜑 → ( ( lub ‘ 𝐾 ) ‘ 𝐴 ) = sup ( 𝐴 , 𝐵 , < ) )

Proof

Step Hyp Ref Expression
1 toslub.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 toslub.l ⊢ < = ( lt ‘ 𝐾 )
3 toslub.1 ⊢ ( 𝜑 → 𝐾 ∈ Toset )
4 toslub.2 ⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
5 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
6 1 2 3 4 5 toslublem ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( ( ∀ 𝑏 ∈ 𝐴 𝑏 ( le ‘ 𝐾 ) 𝑎 ∧ ∀ 𝑐 ∈ 𝐵 ( ∀ 𝑏 ∈ 𝐴 𝑏 ( le ‘ 𝐾 ) 𝑐 → 𝑎 ( le ‘ 𝐾 ) 𝑐 ) ) ↔ ( ∀ 𝑏 ∈ 𝐴 ¬ 𝑎 < 𝑏 ∧ ∀ 𝑏 ∈ 𝐵 ( 𝑏 < 𝑎 → ∃ 𝑑 ∈ 𝐴 𝑏 < 𝑑 ) ) ) )
7 6 riotabidva ⊢ ( 𝜑 → ( ℩ 𝑎 ∈ 𝐵 ( ∀ 𝑏 ∈ 𝐴 𝑏 ( le ‘ 𝐾 ) 𝑎 ∧ ∀ 𝑐 ∈ 𝐵 ( ∀ 𝑏 ∈ 𝐴 𝑏 ( le ‘ 𝐾 ) 𝑐 → 𝑎 ( le ‘ 𝐾 ) 𝑐 ) ) ) = ( ℩ 𝑎 ∈ 𝐵 ( ∀ 𝑏 ∈ 𝐴 ¬ 𝑎 < 𝑏 ∧ ∀ 𝑏 ∈ 𝐵 ( 𝑏 < 𝑎 → ∃ 𝑑 ∈ 𝐴 𝑏 < 𝑑 ) ) ) )
8 eqid ⊢ ( lub ‘ 𝐾 ) = ( lub ‘ 𝐾 )
9 biid ⊢ ( ( ∀ 𝑏 ∈ 𝐴 𝑏 ( le ‘ 𝐾 ) 𝑎 ∧ ∀ 𝑐 ∈ 𝐵 ( ∀ 𝑏 ∈ 𝐴 𝑏 ( le ‘ 𝐾 ) 𝑐 → 𝑎 ( le ‘ 𝐾 ) 𝑐 ) ) ↔ ( ∀ 𝑏 ∈ 𝐴 𝑏 ( le ‘ 𝐾 ) 𝑎 ∧ ∀ 𝑐 ∈ 𝐵 ( ∀ 𝑏 ∈ 𝐴 𝑏 ( le ‘ 𝐾 ) 𝑐 → 𝑎 ( le ‘ 𝐾 ) 𝑐 ) ) )
10 1 5 8 9 3 4 lubval ⊢ ( 𝜑 → ( ( lub ‘ 𝐾 ) ‘ 𝐴 ) = ( ℩ 𝑎 ∈ 𝐵 ( ∀ 𝑏 ∈ 𝐴 𝑏 ( le ‘ 𝐾 ) 𝑎 ∧ ∀ 𝑐 ∈ 𝐵 ( ∀ 𝑏 ∈ 𝐴 𝑏 ( le ‘ 𝐾 ) 𝑐 → 𝑎 ( le ‘ 𝐾 ) 𝑐 ) ) ) )
11 1 5 2 tosso ⊢ ( 𝐾 ∈ Toset → ( 𝐾 ∈ Toset ↔ ( < Or 𝐵 ∧ ( I ↾ 𝐵 ) ⊆ ( le ‘ 𝐾 ) ) ) )
12 11 ibi ⊢ ( 𝐾 ∈ Toset → ( < Or 𝐵 ∧ ( I ↾ 𝐵 ) ⊆ ( le ‘ 𝐾 ) ) )
13 12 simpld ⊢ ( 𝐾 ∈ Toset → < Or 𝐵 )
14 id ⊢ ( < Or 𝐵 → < Or 𝐵 )
15 14 supval2 ⊢ ( < Or 𝐵 → sup ( 𝐴 , 𝐵 , < ) = ( ℩ 𝑎 ∈ 𝐵 ( ∀ 𝑏 ∈ 𝐴 ¬ 𝑎 < 𝑏 ∧ ∀ 𝑏 ∈ 𝐵 ( 𝑏 < 𝑎 → ∃ 𝑑 ∈ 𝐴 𝑏 < 𝑑 ) ) ) )
16 3 13 15 3syl ⊢ ( 𝜑 → sup ( 𝐴 , 𝐵 , < ) = ( ℩ 𝑎 ∈ 𝐵 ( ∀ 𝑏 ∈ 𝐴 ¬ 𝑎 < 𝑏 ∧ ∀ 𝑏 ∈ 𝐵 ( 𝑏 < 𝑎 → ∃ 𝑑 ∈ 𝐴 𝑏 < 𝑑 ) ) ) )
17 7 10 16 3eqtr4d ⊢ ( 𝜑 → ( ( lub ‘ 𝐾 ) ‘ 𝐴 ) = sup ( 𝐴 , 𝐵 , < ) )