# Metamath Proof Explorer

## Theorem oduglb

Description: Greatest lower bounds in a dual order are least upper bounds in the original order. (Contributed by Stefan O'Rear, 29-Jan-2015)

Ref Expression
Hypotheses oduglb.d 𝐷 = ( ODual ‘ 𝑂 )
oduglb.l 𝑈 = ( lub ‘ 𝑂 )
Assertion oduglb ( 𝑂𝑉𝑈 = ( glb ‘ 𝐷 ) )

### Proof

Step Hyp Ref Expression
1 oduglb.d 𝐷 = ( ODual ‘ 𝑂 )
2 oduglb.l 𝑈 = ( lub ‘ 𝑂 )
3 vex 𝑏 ∈ V
4 vex 𝑐 ∈ V
5 3 4 brcnv ( 𝑏 ( le ‘ 𝑂 ) 𝑐𝑐 ( le ‘ 𝑂 ) 𝑏 )
6 5 ralbii ( ∀ 𝑐𝑎 𝑏 ( le ‘ 𝑂 ) 𝑐 ↔ ∀ 𝑐𝑎 𝑐 ( le ‘ 𝑂 ) 𝑏 )
7 vex 𝑑 ∈ V
8 7 4 brcnv ( 𝑑 ( le ‘ 𝑂 ) 𝑐𝑐 ( le ‘ 𝑂 ) 𝑑 )
9 8 ralbii ( ∀ 𝑐𝑎 𝑑 ( le ‘ 𝑂 ) 𝑐 ↔ ∀ 𝑐𝑎 𝑐 ( le ‘ 𝑂 ) 𝑑 )
10 7 3 brcnv ( 𝑑 ( le ‘ 𝑂 ) 𝑏𝑏 ( le ‘ 𝑂 ) 𝑑 )
11 9 10 imbi12i ( ( ∀ 𝑐𝑎 𝑑 ( le ‘ 𝑂 ) 𝑐𝑑 ( le ‘ 𝑂 ) 𝑏 ) ↔ ( ∀ 𝑐𝑎 𝑐 ( le ‘ 𝑂 ) 𝑑𝑏 ( le ‘ 𝑂 ) 𝑑 ) )
12 11 ralbii ( ∀ 𝑑 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐𝑎 𝑑 ( le ‘ 𝑂 ) 𝑐𝑑 ( le ‘ 𝑂 ) 𝑏 ) ↔ ∀ 𝑑 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐𝑎 𝑐 ( le ‘ 𝑂 ) 𝑑𝑏 ( le ‘ 𝑂 ) 𝑑 ) )
13 6 12 anbi12i ( ( ∀ 𝑐𝑎 𝑏 ( le ‘ 𝑂 ) 𝑐 ∧ ∀ 𝑑 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐𝑎 𝑑 ( le ‘ 𝑂 ) 𝑐𝑑 ( le ‘ 𝑂 ) 𝑏 ) ) ↔ ( ∀ 𝑐𝑎 𝑐 ( le ‘ 𝑂 ) 𝑏 ∧ ∀ 𝑑 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐𝑎 𝑐 ( le ‘ 𝑂 ) 𝑑𝑏 ( le ‘ 𝑂 ) 𝑑 ) ) )
14 13 a1i ( 𝑏 ∈ ( Base ‘ 𝑂 ) → ( ( ∀ 𝑐𝑎 𝑏 ( le ‘ 𝑂 ) 𝑐 ∧ ∀ 𝑑 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐𝑎 𝑑 ( le ‘ 𝑂 ) 𝑐𝑑 ( le ‘ 𝑂 ) 𝑏 ) ) ↔ ( ∀ 𝑐𝑎 𝑐 ( le ‘ 𝑂 ) 𝑏 ∧ ∀ 𝑑 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐𝑎 𝑐 ( le ‘ 𝑂 ) 𝑑𝑏 ( le ‘ 𝑂 ) 𝑑 ) ) ) )
15 14 riotabiia ( 𝑏 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐𝑎 𝑏 ( le ‘ 𝑂 ) 𝑐 ∧ ∀ 𝑑 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐𝑎 𝑑 ( le ‘ 𝑂 ) 𝑐𝑑 ( le ‘ 𝑂 ) 𝑏 ) ) ) = ( 𝑏 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐𝑎 𝑐 ( le ‘ 𝑂 ) 𝑏 ∧ ∀ 𝑑 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐𝑎 𝑐 ( le ‘ 𝑂 ) 𝑑𝑏 ( le ‘ 𝑂 ) 𝑑 ) ) )
16 15 mpteq2i ( 𝑎 ∈ 𝒫 ( Base ‘ 𝑂 ) ↦ ( 𝑏 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐𝑎 𝑏 ( le ‘ 𝑂 ) 𝑐 ∧ ∀ 𝑑 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐𝑎 𝑑 ( le ‘ 𝑂 ) 𝑐𝑑 ( le ‘ 𝑂 ) 𝑏 ) ) ) ) = ( 𝑎 ∈ 𝒫 ( Base ‘ 𝑂 ) ↦ ( 𝑏 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐𝑎 𝑐 ( le ‘ 𝑂 ) 𝑏 ∧ ∀ 𝑑 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐𝑎 𝑐 ( le ‘ 𝑂 ) 𝑑𝑏 ( le ‘ 𝑂 ) 𝑑 ) ) ) )
17 13 reubii ( ∃! 𝑏 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐𝑎 𝑏 ( le ‘ 𝑂 ) 𝑐 ∧ ∀ 𝑑 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐𝑎 𝑑 ( le ‘ 𝑂 ) 𝑐𝑑 ( le ‘ 𝑂 ) 𝑏 ) ) ↔ ∃! 𝑏 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐𝑎 𝑐 ( le ‘ 𝑂 ) 𝑏 ∧ ∀ 𝑑 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐𝑎 𝑐 ( le ‘ 𝑂 ) 𝑑𝑏 ( le ‘ 𝑂 ) 𝑑 ) ) )
18 17 abbii { 𝑎 ∣ ∃! 𝑏 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐𝑎 𝑏 ( le ‘ 𝑂 ) 𝑐 ∧ ∀ 𝑑 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐𝑎 𝑑 ( le ‘ 𝑂 ) 𝑐𝑑 ( le ‘ 𝑂 ) 𝑏 ) ) } = { 𝑎 ∣ ∃! 𝑏 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐𝑎 𝑐 ( le ‘ 𝑂 ) 𝑏 ∧ ∀ 𝑑 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐𝑎 𝑐 ( le ‘ 𝑂 ) 𝑑𝑏 ( le ‘ 𝑂 ) 𝑑 ) ) }
19 16 18 reseq12i ( ( 𝑎 ∈ 𝒫 ( Base ‘ 𝑂 ) ↦ ( 𝑏 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐𝑎 𝑏 ( le ‘ 𝑂 ) 𝑐 ∧ ∀ 𝑑 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐𝑎 𝑑 ( le ‘ 𝑂 ) 𝑐𝑑 ( le ‘ 𝑂 ) 𝑏 ) ) ) ) ↾ { 𝑎 ∣ ∃! 𝑏 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐𝑎 𝑏 ( le ‘ 𝑂 ) 𝑐 ∧ ∀ 𝑑 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐𝑎 𝑑 ( le ‘ 𝑂 ) 𝑐𝑑 ( le ‘ 𝑂 ) 𝑏 ) ) } ) = ( ( 𝑎 ∈ 𝒫 ( Base ‘ 𝑂 ) ↦ ( 𝑏 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐𝑎 𝑐 ( le ‘ 𝑂 ) 𝑏 ∧ ∀ 𝑑 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐𝑎 𝑐 ( le ‘ 𝑂 ) 𝑑𝑏 ( le ‘ 𝑂 ) 𝑑 ) ) ) ) ↾ { 𝑎 ∣ ∃! 𝑏 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐𝑎 𝑐 ( le ‘ 𝑂 ) 𝑏 ∧ ∀ 𝑑 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐𝑎 𝑐 ( le ‘ 𝑂 ) 𝑑𝑏 ( le ‘ 𝑂 ) 𝑑 ) ) } )
20 19 eqcomi ( ( 𝑎 ∈ 𝒫 ( Base ‘ 𝑂 ) ↦ ( 𝑏 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐𝑎 𝑐 ( le ‘ 𝑂 ) 𝑏 ∧ ∀ 𝑑 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐𝑎 𝑐 ( le ‘ 𝑂 ) 𝑑𝑏 ( le ‘ 𝑂 ) 𝑑 ) ) ) ) ↾ { 𝑎 ∣ ∃! 𝑏 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐𝑎 𝑐 ( le ‘ 𝑂 ) 𝑏 ∧ ∀ 𝑑 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐𝑎 𝑐 ( le ‘ 𝑂 ) 𝑑𝑏 ( le ‘ 𝑂 ) 𝑑 ) ) } ) = ( ( 𝑎 ∈ 𝒫 ( Base ‘ 𝑂 ) ↦ ( 𝑏 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐𝑎 𝑏 ( le ‘ 𝑂 ) 𝑐 ∧ ∀ 𝑑 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐𝑎 𝑑 ( le ‘ 𝑂 ) 𝑐𝑑 ( le ‘ 𝑂 ) 𝑏 ) ) ) ) ↾ { 𝑎 ∣ ∃! 𝑏 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐𝑎 𝑏 ( le ‘ 𝑂 ) 𝑐 ∧ ∀ 𝑑 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐𝑎 𝑑 ( le ‘ 𝑂 ) 𝑐𝑑 ( le ‘ 𝑂 ) 𝑏 ) ) } )
21 eqid ( Base ‘ 𝑂 ) = ( Base ‘ 𝑂 )
22 eqid ( le ‘ 𝑂 ) = ( le ‘ 𝑂 )
23 eqid ( lub ‘ 𝑂 ) = ( lub ‘ 𝑂 )
24 biid ( ( ∀ 𝑐𝑎 𝑐 ( le ‘ 𝑂 ) 𝑏 ∧ ∀ 𝑑 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐𝑎 𝑐 ( le ‘ 𝑂 ) 𝑑𝑏 ( le ‘ 𝑂 ) 𝑑 ) ) ↔ ( ∀ 𝑐𝑎 𝑐 ( le ‘ 𝑂 ) 𝑏 ∧ ∀ 𝑑 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐𝑎 𝑐 ( le ‘ 𝑂 ) 𝑑𝑏 ( le ‘ 𝑂 ) 𝑑 ) ) )
25 id ( 𝑂𝑉𝑂𝑉 )
26 21 22 23 24 25 lubfval ( 𝑂𝑉 → ( lub ‘ 𝑂 ) = ( ( 𝑎 ∈ 𝒫 ( Base ‘ 𝑂 ) ↦ ( 𝑏 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐𝑎 𝑐 ( le ‘ 𝑂 ) 𝑏 ∧ ∀ 𝑑 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐𝑎 𝑐 ( le ‘ 𝑂 ) 𝑑𝑏 ( le ‘ 𝑂 ) 𝑑 ) ) ) ) ↾ { 𝑎 ∣ ∃! 𝑏 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐𝑎 𝑐 ( le ‘ 𝑂 ) 𝑏 ∧ ∀ 𝑑 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐𝑎 𝑐 ( le ‘ 𝑂 ) 𝑑𝑏 ( le ‘ 𝑂 ) 𝑑 ) ) } ) )
27 1 fvexi 𝐷 ∈ V
28 1 21 odubas ( Base ‘ 𝑂 ) = ( Base ‘ 𝐷 )
29 1 22 oduleval ( le ‘ 𝑂 ) = ( le ‘ 𝐷 )
30 eqid ( glb ‘ 𝐷 ) = ( glb ‘ 𝐷 )
31 biid ( ( ∀ 𝑐𝑎 𝑏 ( le ‘ 𝑂 ) 𝑐 ∧ ∀ 𝑑 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐𝑎 𝑑 ( le ‘ 𝑂 ) 𝑐𝑑 ( le ‘ 𝑂 ) 𝑏 ) ) ↔ ( ∀ 𝑐𝑎 𝑏 ( le ‘ 𝑂 ) 𝑐 ∧ ∀ 𝑑 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐𝑎 𝑑 ( le ‘ 𝑂 ) 𝑐𝑑 ( le ‘ 𝑂 ) 𝑏 ) ) )
32 id ( 𝐷 ∈ V → 𝐷 ∈ V )
33 28 29 30 31 32 glbfval ( 𝐷 ∈ V → ( glb ‘ 𝐷 ) = ( ( 𝑎 ∈ 𝒫 ( Base ‘ 𝑂 ) ↦ ( 𝑏 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐𝑎 𝑏 ( le ‘ 𝑂 ) 𝑐 ∧ ∀ 𝑑 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐𝑎 𝑑 ( le ‘ 𝑂 ) 𝑐𝑑 ( le ‘ 𝑂 ) 𝑏 ) ) ) ) ↾ { 𝑎 ∣ ∃! 𝑏 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐𝑎 𝑏 ( le ‘ 𝑂 ) 𝑐 ∧ ∀ 𝑑 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐𝑎 𝑑 ( le ‘ 𝑂 ) 𝑐𝑑 ( le ‘ 𝑂 ) 𝑏 ) ) } ) )
34 27 33 mp1i ( 𝑂𝑉 → ( glb ‘ 𝐷 ) = ( ( 𝑎 ∈ 𝒫 ( Base ‘ 𝑂 ) ↦ ( 𝑏 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐𝑎 𝑏 ( le ‘ 𝑂 ) 𝑐 ∧ ∀ 𝑑 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐𝑎 𝑑 ( le ‘ 𝑂 ) 𝑐𝑑 ( le ‘ 𝑂 ) 𝑏 ) ) ) ) ↾ { 𝑎 ∣ ∃! 𝑏 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐𝑎 𝑏 ( le ‘ 𝑂 ) 𝑐 ∧ ∀ 𝑑 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐𝑎 𝑑 ( le ‘ 𝑂 ) 𝑐𝑑 ( le ‘ 𝑂 ) 𝑏 ) ) } ) )
35 20 26 34 3eqtr4a ( 𝑂𝑉 → ( lub ‘ 𝑂 ) = ( glb ‘ 𝐷 ) )
36 2 35 syl5eq ( 𝑂𝑉𝑈 = ( glb ‘ 𝐷 ) )