# Metamath Proof Explorer

## Theorem odulub

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

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

### Proof

Step Hyp Ref Expression
1 oduglb.d 𝐷 = ( ODual ‘ 𝑂 )
2 odulub.l 𝐿 = ( glb ‘ 𝑂 )
3 vex 𝑐 ∈ V
4 vex 𝑏 ∈ V
5 3 4 brcnv ( 𝑐 ( le ‘ 𝑂 ) 𝑏𝑏 ( le ‘ 𝑂 ) 𝑐 )
6 5 ralbii ( ∀ 𝑐𝑎 𝑐 ( le ‘ 𝑂 ) 𝑏 ↔ ∀ 𝑐𝑎 𝑏 ( le ‘ 𝑂 ) 𝑐 )
7 vex 𝑑 ∈ V
8 3 7 brcnv ( 𝑐 ( le ‘ 𝑂 ) 𝑑𝑑 ( le ‘ 𝑂 ) 𝑐 )
9 8 ralbii ( ∀ 𝑐𝑎 𝑐 ( le ‘ 𝑂 ) 𝑑 ↔ ∀ 𝑐𝑎 𝑑 ( le ‘ 𝑂 ) 𝑐 )
10 4 7 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 ( glb ‘ 𝑂 ) = ( glb ‘ 𝑂 )
24 biid ( ( ∀ 𝑐𝑎 𝑏 ( le ‘ 𝑂 ) 𝑐 ∧ ∀ 𝑑 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐𝑎 𝑑 ( le ‘ 𝑂 ) 𝑐𝑑 ( le ‘ 𝑂 ) 𝑏 ) ) ↔ ( ∀ 𝑐𝑎 𝑏 ( le ‘ 𝑂 ) 𝑐 ∧ ∀ 𝑑 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐𝑎 𝑑 ( le ‘ 𝑂 ) 𝑐𝑑 ( le ‘ 𝑂 ) 𝑏 ) ) )
25 id ( 𝑂𝑉𝑂𝑉 )
26 21 22 23 24 25 glbfval ( 𝑂𝑉 → ( glb ‘ 𝑂 ) = ( ( 𝑎 ∈ 𝒫 ( 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 ( lub ‘ 𝐷 ) = ( lub ‘ 𝐷 )
31 biid ( ( ∀ 𝑐𝑎 𝑐 ( le ‘ 𝑂 ) 𝑏 ∧ ∀ 𝑑 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐𝑎 𝑐 ( le ‘ 𝑂 ) 𝑑𝑏 ( le ‘ 𝑂 ) 𝑑 ) ) ↔ ( ∀ 𝑐𝑎 𝑐 ( le ‘ 𝑂 ) 𝑏 ∧ ∀ 𝑑 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐𝑎 𝑐 ( le ‘ 𝑂 ) 𝑑𝑏 ( le ‘ 𝑂 ) 𝑑 ) ) )
32 id ( 𝐷 ∈ V → 𝐷 ∈ V )
33 28 29 30 31 32 lubfval ( 𝐷 ∈ V → ( lub ‘ 𝐷 ) = ( ( 𝑎 ∈ 𝒫 ( Base ‘ 𝑂 ) ↦ ( 𝑏 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐𝑎 𝑐 ( le ‘ 𝑂 ) 𝑏 ∧ ∀ 𝑑 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐𝑎 𝑐 ( le ‘ 𝑂 ) 𝑑𝑏 ( le ‘ 𝑂 ) 𝑑 ) ) ) ) ↾ { 𝑎 ∣ ∃! 𝑏 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐𝑎 𝑐 ( le ‘ 𝑂 ) 𝑏 ∧ ∀ 𝑑 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐𝑎 𝑐 ( le ‘ 𝑂 ) 𝑑𝑏 ( le ‘ 𝑂 ) 𝑑 ) ) } ) )
34 27 33 mp1i ( 𝑂𝑉 → ( lub ‘ 𝐷 ) = ( ( 𝑎 ∈ 𝒫 ( Base ‘ 𝑂 ) ↦ ( 𝑏 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐𝑎 𝑐 ( le ‘ 𝑂 ) 𝑏 ∧ ∀ 𝑑 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐𝑎 𝑐 ( le ‘ 𝑂 ) 𝑑𝑏 ( le ‘ 𝑂 ) 𝑑 ) ) ) ) ↾ { 𝑎 ∣ ∃! 𝑏 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐𝑎 𝑐 ( le ‘ 𝑂 ) 𝑏 ∧ ∀ 𝑑 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐𝑎 𝑐 ( le ‘ 𝑂 ) 𝑑𝑏 ( le ‘ 𝑂 ) 𝑑 ) ) } ) )
35 20 26 34 3eqtr4a ( 𝑂𝑉 → ( glb ‘ 𝑂 ) = ( lub ‘ 𝐷 ) )
36 2 35 syl5eq ( 𝑂𝑉𝐿 = ( lub ‘ 𝐷 ) )