Metamath Proof Explorer

Theorem tosglb

Description: Same theorem as toslub , for infinimum. (Contributed by Thierry Arnoux, 17-Feb-2018) (Revised by AV, 28-Sep-2020)

Ref Expression
Hypotheses tosglb.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
tosglb.l ⊢ < = ( lt ‘ 𝐾 )
tosglb.1 ⊢ ( 𝜑 → 𝐾 ∈ Toset )
tosglb.2 ⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
Assertion tosglb ( 𝜑 → ( ( glb ‘ 𝐾 ) ‘ 𝐴 ) = inf ( 𝐴 , 𝐵 , < ) )

Proof

Step Hyp Ref Expression
1 tosglb.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 tosglb.l ⊢ < = ( lt ‘ 𝐾 )
3 tosglb.1 ⊢ ( 𝜑 → 𝐾 ∈ Toset )
4 tosglb.2 ⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
5 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
6 1 2 3 4 5 tosglblem ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( ( ∀ 𝑏 ∈ 𝐴 𝑎 ( le ‘ 𝐾 ) 𝑏 ∧ ∀ 𝑐 ∈ 𝐵 ( ∀ 𝑏 ∈ 𝐴 𝑐 ( le ‘ 𝐾 ) 𝑏 → 𝑐 ( le ‘ 𝐾 ) 𝑎 ) ) ↔ ( ∀ 𝑏 ∈ 𝐴 ¬ 𝑎 ◡ < 𝑏 ∧ ∀ 𝑏 ∈ 𝐵 ( 𝑏 ◡ < 𝑎 → ∃ 𝑑 ∈ 𝐴 𝑏 ◡ < 𝑑 ) ) ) )
7 6 riotabidva ⊢ ( 𝜑 → ( ℩ 𝑎 ∈ 𝐵 ( ∀ 𝑏 ∈ 𝐴 𝑎 ( le ‘ 𝐾 ) 𝑏 ∧ ∀ 𝑐 ∈ 𝐵 ( ∀ 𝑏 ∈ 𝐴 𝑐 ( le ‘ 𝐾 ) 𝑏 → 𝑐 ( le ‘ 𝐾 ) 𝑎 ) ) ) = ( ℩ 𝑎 ∈ 𝐵 ( ∀ 𝑏 ∈ 𝐴 ¬ 𝑎 ◡ < 𝑏 ∧ ∀ 𝑏 ∈ 𝐵 ( 𝑏 ◡ < 𝑎 → ∃ 𝑑 ∈ 𝐴 𝑏 ◡ < 𝑑 ) ) ) )
8 eqid ⊢ ( glb ‘ 𝐾 ) = ( glb ‘ 𝐾 )
9 biid ⊢ ( ( ∀ 𝑏 ∈ 𝐴 𝑎 ( le ‘ 𝐾 ) 𝑏 ∧ ∀ 𝑐 ∈ 𝐵 ( ∀ 𝑏 ∈ 𝐴 𝑐 ( le ‘ 𝐾 ) 𝑏 → 𝑐 ( le ‘ 𝐾 ) 𝑎 ) ) ↔ ( ∀ 𝑏 ∈ 𝐴 𝑎 ( le ‘ 𝐾 ) 𝑏 ∧ ∀ 𝑐 ∈ 𝐵 ( ∀ 𝑏 ∈ 𝐴 𝑐 ( le ‘ 𝐾 ) 𝑏 → 𝑐 ( le ‘ 𝐾 ) 𝑎 ) ) )
10 1 5 8 9 3 4 glbval ⊢ ( 𝜑 → ( ( glb ‘ 𝐾 ) ‘ 𝐴 ) = ( ℩ 𝑎 ∈ 𝐵 ( ∀ 𝑏 ∈ 𝐴 𝑎 ( 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 cnvso ⊢ ( < Or 𝐵 ↔ ◡ < Or 𝐵 )
15 13 14 sylib ⊢ ( 𝐾 ∈ Toset → ◡ < Or 𝐵 )
16 id ⊢ ( ◡ < Or 𝐵 → ◡ < Or 𝐵 )
17 16 supval2 ⊢ ( ◡ < Or 𝐵 → sup ( 𝐴 , 𝐵 , ◡ < ) = ( ℩ 𝑎 ∈ 𝐵 ( ∀ 𝑏 ∈ 𝐴 ¬ 𝑎 ◡ < 𝑏 ∧ ∀ 𝑏 ∈ 𝐵 ( 𝑏 ◡ < 𝑎 → ∃ 𝑑 ∈ 𝐴 𝑏 ◡ < 𝑑 ) ) ) )
18 3 15 17 3syl ⊢ ( 𝜑 → sup ( 𝐴 , 𝐵 , ◡ < ) = ( ℩ 𝑎 ∈ 𝐵 ( ∀ 𝑏 ∈ 𝐴 ¬ 𝑎 ◡ < 𝑏 ∧ ∀ 𝑏 ∈ 𝐵 ( 𝑏 ◡ < 𝑎 → ∃ 𝑑 ∈ 𝐴 𝑏 ◡ < 𝑑 ) ) ) )
19 7 10 18 3eqtr4d ⊢ ( 𝜑 → ( ( glb ‘ 𝐾 ) ‘ 𝐴 ) = sup ( 𝐴 , 𝐵 , ◡ < ) )
20 df-inf ⊢ inf ( 𝐴 , 𝐵 , < ) = sup ( 𝐴 , 𝐵 , ◡ < )
21 20 eqcomi ⊢ sup ( 𝐴 , 𝐵 , ◡ < ) = inf ( 𝐴 , 𝐵 , < )
22 21 a1i ⊢ ( 𝜑 → sup ( 𝐴 , 𝐵 , ◡ < ) = inf ( 𝐴 , 𝐵 , < ) )
23 19 22 eqtrd ⊢ ( 𝜑 → ( ( glb ‘ 𝐾 ) ‘ 𝐴 ) = inf ( 𝐴 , 𝐵 , < ) )