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 ‘ 𝐷 ) )