Metamath Proof Explorer

Theorem atlatle

Description: The ordering of two Hilbert lattice elements is determined by the atoms under them. ( chrelat3 analog.) (Contributed by NM, 5-Nov-2012)

Ref Expression
Hypotheses atlatle.b 
|- B = ( Base ` K )
atlatle.l 
|- .<_ = ( le ` K )
atlatle.a 
|- A = ( Atoms ` K )
Assertion atlatle 
|- ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B /\ Y e. B ) -> ( X .<_ Y <-> A. p e. A ( p .<_ X -> p .<_ Y ) ) )

Proof

Step Hyp Ref Expression
1 atlatle.b 
 |-  B = ( Base ` K )
2 atlatle.l 
 |-  .<_ = ( le ` K )
3 atlatle.a 
 |-  A = ( Atoms ` K )
4 simpl13 
 |-  ( ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B /\ Y e. B ) /\ p e. A ) -> K e. AtLat )
5 atlpos 
 |-  ( K e. AtLat -> K e. Poset )
6 4 5 syl 
 |-  ( ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B /\ Y e. B ) /\ p e. A ) -> K e. Poset )
7 1 3 atbase 
 |-  ( p e. A -> p e. B )
8 7 adantl 
 |-  ( ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B /\ Y e. B ) /\ p e. A ) -> p e. B )
9 simpl2 
 |-  ( ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B /\ Y e. B ) /\ p e. A ) -> X e. B )
10 simpl3 
 |-  ( ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B /\ Y e. B ) /\ p e. A ) -> Y e. B )
11 1 2 postr 
 |-  ( ( K e. Poset /\ ( p e. B /\ X e. B /\ Y e. B ) ) -> ( ( p .<_ X /\ X .<_ Y ) -> p .<_ Y ) )
12 6 8 9 10 11 syl13anc 
 |-  ( ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B /\ Y e. B ) /\ p e. A ) -> ( ( p .<_ X /\ X .<_ Y ) -> p .<_ Y ) )
13 12 expcomd 
 |-  ( ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B /\ Y e. B ) /\ p e. A ) -> ( X .<_ Y -> ( p .<_ X -> p .<_ Y ) ) )
14 13 ralrimdva 
 |-  ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B /\ Y e. B ) -> ( X .<_ Y -> A. p e. A ( p .<_ X -> p .<_ Y ) ) )
15 ss2rab 
 |-  ( { p e. A | p .<_ X } C_ { p e. A | p .<_ Y } <-> A. p e. A ( p .<_ X -> p .<_ Y ) )
16 simpl12 
 |-  ( ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B /\ Y e. B ) /\ { p e. A | p .<_ X } C_ { p e. A | p .<_ Y } ) -> K e. CLat )
17 ssrab2 
 |-  { p e. A | p .<_ Y } C_ A
18 1 3 atssbase 
 |-  A C_ B
19 17 18 sstri 
 |-  { p e. A | p .<_ Y } C_ B
20 eqid 
 |-  ( lub ` K ) = ( lub ` K )
21 1 2 20 lubss 
 |-  ( ( K e. CLat /\ { p e. A | p .<_ Y } C_ B /\ { p e. A | p .<_ X } C_ { p e. A | p .<_ Y } ) -> ( ( lub ` K ) ` { p e. A | p .<_ X } ) .<_ ( ( lub ` K ) ` { p e. A | p .<_ Y } ) )
22 19 21 mp3an2 
 |-  ( ( K e. CLat /\ { p e. A | p .<_ X } C_ { p e. A | p .<_ Y } ) -> ( ( lub ` K ) ` { p e. A | p .<_ X } ) .<_ ( ( lub ` K ) ` { p e. A | p .<_ Y } ) )
23 16 22 sylancom 
 |-  ( ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B /\ Y e. B ) /\ { p e. A | p .<_ X } C_ { p e. A | p .<_ Y } ) -> ( ( lub ` K ) ` { p e. A | p .<_ X } ) .<_ ( ( lub ` K ) ` { p e. A | p .<_ Y } ) )
24 23 ex 
 |-  ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B /\ Y e. B ) -> ( { p e. A | p .<_ X } C_ { p e. A | p .<_ Y } -> ( ( lub ` K ) ` { p e. A | p .<_ X } ) .<_ ( ( lub ` K ) ` { p e. A | p .<_ Y } ) ) )
25 1 2 20 3 atlatmstc 
 |-  ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B ) -> ( ( lub ` K ) ` { p e. A | p .<_ X } ) = X )
26 25 3adant3 
 |-  ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B /\ Y e. B ) -> ( ( lub ` K ) ` { p e. A | p .<_ X } ) = X )
27 1 2 20 3 atlatmstc 
 |-  ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ Y e. B ) -> ( ( lub ` K ) ` { p e. A | p .<_ Y } ) = Y )
28 27 3adant2 
 |-  ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B /\ Y e. B ) -> ( ( lub ` K ) ` { p e. A | p .<_ Y } ) = Y )
29 26 28 breq12d 
 |-  ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B /\ Y e. B ) -> ( ( ( lub ` K ) ` { p e. A | p .<_ X } ) .<_ ( ( lub ` K ) ` { p e. A | p .<_ Y } ) <-> X .<_ Y ) )
30 24 29 sylibd 
 |-  ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B /\ Y e. B ) -> ( { p e. A | p .<_ X } C_ { p e. A | p .<_ Y } -> X .<_ Y ) )
31 15 30 syl5bir 
 |-  ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B /\ Y e. B ) -> ( A. p e. A ( p .<_ X -> p .<_ Y ) -> X .<_ Y ) )
32 14 31 impbid 
 |-  ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B /\ Y e. B ) -> ( X .<_ Y <-> A. p e. A ( p .<_ X -> p .<_ Y ) ) )