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 
|- D = ( ODual ` O )
oduglb.l 
|- U = ( lub ` O )
Assertion oduglb 
|- ( O e. V -> U = ( glb ` D ) )

Proof

Step Hyp Ref Expression
1 oduglb.d 
 |-  D = ( ODual ` O )
2 oduglb.l 
 |-  U = ( lub ` O )
3 vex 
 |-  b e. _V
4 vex 
 |-  c e. _V
5 3 4 brcnv 
 |-  ( b `' ( le ` O ) c <-> c ( le ` O ) b )
6 5 ralbii 
 |-  ( A. c e. a b `' ( le ` O ) c <-> A. c e. a c ( le ` O ) b )
7 vex 
 |-  d e. _V
8 7 4 brcnv 
 |-  ( d `' ( le ` O ) c <-> c ( le ` O ) d )
9 8 ralbii 
 |-  ( A. c e. a d `' ( le ` O ) c <-> A. c e. a c ( le ` O ) d )
10 7 3 brcnv 
 |-  ( d `' ( le ` O ) b <-> b ( le ` O ) d )
11 9 10 imbi12i 
 |-  ( ( A. c e. a d `' ( le ` O ) c -> d `' ( le ` O ) b ) <-> ( A. c e. a c ( le ` O ) d -> b ( le ` O ) d ) )
12 11 ralbii 
 |-  ( A. d e. ( Base ` O ) ( A. c e. a d `' ( le ` O ) c -> d `' ( le ` O ) b ) <-> A. d e. ( Base ` O ) ( A. c e. a c ( le ` O ) d -> b ( le ` O ) d ) )
13 6 12 anbi12i 
 |-  ( ( A. c e. a b `' ( le ` O ) c /\ A. d e. ( Base ` O ) ( A. c e. a d `' ( le ` O ) c -> d `' ( le ` O ) b ) ) <-> ( A. c e. a c ( le ` O ) b /\ A. d e. ( Base ` O ) ( A. c e. a c ( le ` O ) d -> b ( le ` O ) d ) ) )
14 13 a1i 
 |-  ( b e. ( Base ` O ) -> ( ( A. c e. a b `' ( le ` O ) c /\ A. d e. ( Base ` O ) ( A. c e. a d `' ( le ` O ) c -> d `' ( le ` O ) b ) ) <-> ( A. c e. a c ( le ` O ) b /\ A. d e. ( Base ` O ) ( A. c e. a c ( le ` O ) d -> b ( le ` O ) d ) ) ) )
15 14 riotabiia 
 |-  ( iota_ b e. ( Base ` O ) ( A. c e. a b `' ( le ` O ) c /\ A. d e. ( Base ` O ) ( A. c e. a d `' ( le ` O ) c -> d `' ( le ` O ) b ) ) ) = ( iota_ b e. ( Base ` O ) ( A. c e. a c ( le ` O ) b /\ A. d e. ( Base ` O ) ( A. c e. a c ( le ` O ) d -> b ( le ` O ) d ) ) )
16 15 mpteq2i 
 |-  ( a e. ~P ( Base ` O ) |-> ( iota_ b e. ( Base ` O ) ( A. c e. a b `' ( le ` O ) c /\ A. d e. ( Base ` O ) ( A. c e. a d `' ( le ` O ) c -> d `' ( le ` O ) b ) ) ) ) = ( a e. ~P ( Base ` O ) |-> ( iota_ b e. ( Base ` O ) ( A. c e. a c ( le ` O ) b /\ A. d e. ( Base ` O ) ( A. c e. a c ( le ` O ) d -> b ( le ` O ) d ) ) ) )
17 13 reubii 
 |-  ( E! b e. ( Base ` O ) ( A. c e. a b `' ( le ` O ) c /\ A. d e. ( Base ` O ) ( A. c e. a d `' ( le ` O ) c -> d `' ( le ` O ) b ) ) <-> E! b e. ( Base ` O ) ( A. c e. a c ( le ` O ) b /\ A. d e. ( Base ` O ) ( A. c e. a c ( le ` O ) d -> b ( le ` O ) d ) ) )
18 17 abbii 
 |-  { a | E! b e. ( Base ` O ) ( A. c e. a b `' ( le ` O ) c /\ A. d e. ( Base ` O ) ( A. c e. a d `' ( le ` O ) c -> d `' ( le ` O ) b ) ) } = { a | E! b e. ( Base ` O ) ( A. c e. a c ( le ` O ) b /\ A. d e. ( Base ` O ) ( A. c e. a c ( le ` O ) d -> b ( le ` O ) d ) ) }
19 16 18 reseq12i 
 |-  ( ( a e. ~P ( Base ` O ) |-> ( iota_ b e. ( Base ` O ) ( A. c e. a b `' ( le ` O ) c /\ A. d e. ( Base ` O ) ( A. c e. a d `' ( le ` O ) c -> d `' ( le ` O ) b ) ) ) ) |` { a | E! b e. ( Base ` O ) ( A. c e. a b `' ( le ` O ) c /\ A. d e. ( Base ` O ) ( A. c e. a d `' ( le ` O ) c -> d `' ( le ` O ) b ) ) } ) = ( ( a e. ~P ( Base ` O ) |-> ( iota_ b e. ( Base ` O ) ( A. c e. a c ( le ` O ) b /\ A. d e. ( Base ` O ) ( A. c e. a c ( le ` O ) d -> b ( le ` O ) d ) ) ) ) |` { a | E! b e. ( Base ` O ) ( A. c e. a c ( le ` O ) b /\ A. d e. ( Base ` O ) ( A. c e. a c ( le ` O ) d -> b ( le ` O ) d ) ) } )
20 19 eqcomi 
 |-  ( ( a e. ~P ( Base ` O ) |-> ( iota_ b e. ( Base ` O ) ( A. c e. a c ( le ` O ) b /\ A. d e. ( Base ` O ) ( A. c e. a c ( le ` O ) d -> b ( le ` O ) d ) ) ) ) |` { a | E! b e. ( Base ` O ) ( A. c e. a c ( le ` O ) b /\ A. d e. ( Base ` O ) ( A. c e. a c ( le ` O ) d -> b ( le ` O ) d ) ) } ) = ( ( a e. ~P ( Base ` O ) |-> ( iota_ b e. ( Base ` O ) ( A. c e. a b `' ( le ` O ) c /\ A. d e. ( Base ` O ) ( A. c e. a d `' ( le ` O ) c -> d `' ( le ` O ) b ) ) ) ) |` { a | E! b e. ( Base ` O ) ( A. c e. a b `' ( le ` O ) c /\ A. d e. ( Base ` O ) ( A. c e. a d `' ( le ` O ) c -> d `' ( le ` O ) b ) ) } )
21 eqid 
 |-  ( Base ` O ) = ( Base ` O )
22 eqid 
 |-  ( le ` O ) = ( le ` O )
23 eqid 
 |-  ( lub ` O ) = ( lub ` O )
24 biid 
 |-  ( ( A. c e. a c ( le ` O ) b /\ A. d e. ( Base ` O ) ( A. c e. a c ( le ` O ) d -> b ( le ` O ) d ) ) <-> ( A. c e. a c ( le ` O ) b /\ A. d e. ( Base ` O ) ( A. c e. a c ( le ` O ) d -> b ( le ` O ) d ) ) )
25 id 
 |-  ( O e. V -> O e. V )
26 21 22 23 24 25 lubfval 
 |-  ( O e. V -> ( lub ` O ) = ( ( a e. ~P ( Base ` O ) |-> ( iota_ b e. ( Base ` O ) ( A. c e. a c ( le ` O ) b /\ A. d e. ( Base ` O ) ( A. c e. a c ( le ` O ) d -> b ( le ` O ) d ) ) ) ) |` { a | E! b e. ( Base ` O ) ( A. c e. a c ( le ` O ) b /\ A. d e. ( Base ` O ) ( A. c e. a c ( le ` O ) d -> b ( le ` O ) d ) ) } ) )
27 1 fvexi 
 |-  D e. _V
28 1 21 odubas 
 |-  ( Base ` O ) = ( Base ` D )
29 1 22 oduleval 
 |-  `' ( le ` O ) = ( le ` D )
30 eqid 
 |-  ( glb ` D ) = ( glb ` D )
31 biid 
 |-  ( ( A. c e. a b `' ( le ` O ) c /\ A. d e. ( Base ` O ) ( A. c e. a d `' ( le ` O ) c -> d `' ( le ` O ) b ) ) <-> ( A. c e. a b `' ( le ` O ) c /\ A. d e. ( Base ` O ) ( A. c e. a d `' ( le ` O ) c -> d `' ( le ` O ) b ) ) )
32 id 
 |-  ( D e. _V -> D e. _V )
33 28 29 30 31 32 glbfval 
 |-  ( D e. _V -> ( glb ` D ) = ( ( a e. ~P ( Base ` O ) |-> ( iota_ b e. ( Base ` O ) ( A. c e. a b `' ( le ` O ) c /\ A. d e. ( Base ` O ) ( A. c e. a d `' ( le ` O ) c -> d `' ( le ` O ) b ) ) ) ) |` { a | E! b e. ( Base ` O ) ( A. c e. a b `' ( le ` O ) c /\ A. d e. ( Base ` O ) ( A. c e. a d `' ( le ` O ) c -> d `' ( le ` O ) b ) ) } ) )
34 27 33 mp1i 
 |-  ( O e. V -> ( glb ` D ) = ( ( a e. ~P ( Base ` O ) |-> ( iota_ b e. ( Base ` O ) ( A. c e. a b `' ( le ` O ) c /\ A. d e. ( Base ` O ) ( A. c e. a d `' ( le ` O ) c -> d `' ( le ` O ) b ) ) ) ) |` { a | E! b e. ( Base ` O ) ( A. c e. a b `' ( le ` O ) c /\ A. d e. ( Base ` O ) ( A. c e. a d `' ( le ` O ) c -> d `' ( le ` O ) b ) ) } ) )
35 20 26 34 3eqtr4a 
 |-  ( O e. V -> ( lub ` O ) = ( glb ` D ) )
36 2 35 syl5eq 
 |-  ( O e. V -> U = ( glb ` D ) )