Metamath Proof Explorer

Theorem atlrelat1

Description: An atomistic lattice with 0 is relatively atomic. Part of Lemma 7.2 of MaedaMaeda p. 30. ( chpssati , with /\ swapped, analog.) (Contributed by NM, 4-Dec-2011)

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

Proof

Step Hyp Ref Expression
1 atlrelat1.b 
 |-  B = ( Base ` K )
2 atlrelat1.l 
 |-  .<_ = ( le ` K )
3 atlrelat1.s 
 |-  .< = ( lt ` K )
4 atlrelat1.a 
 |-  A = ( Atoms ` K )
5 simp13 
 |-  ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B /\ Y e. B ) -> K e. AtLat )
6 atlpos 
 |-  ( K e. AtLat -> K e. Poset )
7 5 6 syl 
 |-  ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B /\ Y e. B ) -> K e. Poset )
8 1 2 3 pltnle 
 |-  ( ( ( K e. Poset /\ X e. B /\ Y e. B ) /\ X .< Y ) -> -. Y .<_ X )
9 8 ex 
 |-  ( ( K e. Poset /\ X e. B /\ Y e. B ) -> ( X .< Y -> -. Y .<_ X ) )
10 7 9 syld3an1 
 |-  ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B /\ Y e. B ) -> ( X .< Y -> -. Y .<_ X ) )
11 iman 
 |-  ( ( p .<_ Y -> p .<_ X ) <-> -. ( p .<_ Y /\ -. p .<_ X ) )
12 ancom 
 |-  ( ( p .<_ Y /\ -. p .<_ X ) <-> ( -. p .<_ X /\ p .<_ Y ) )
13 11 12 xchbinx 
 |-  ( ( p .<_ Y -> p .<_ X ) <-> -. ( -. p .<_ X /\ p .<_ Y ) )
14 13 ralbii 
 |-  ( A. p e. A ( p .<_ Y -> p .<_ X ) <-> A. p e. A -. ( -. p .<_ X /\ p .<_ Y ) )
15 1 2 4 atlatle 
 |-  ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ Y e. B /\ X e. B ) -> ( Y .<_ X <-> A. p e. A ( p .<_ Y -> p .<_ X ) ) )
16 15 3com23 
 |-  ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B /\ Y e. B ) -> ( Y .<_ X <-> A. p e. A ( p .<_ Y -> p .<_ X ) ) )
17 16 biimprd 
 |-  ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B /\ Y e. B ) -> ( A. p e. A ( p .<_ Y -> p .<_ X ) -> Y .<_ X ) )
18 14 17 biimtrrid 
 |-  ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B /\ Y e. B ) -> ( A. p e. A -. ( -. p .<_ X /\ p .<_ Y ) -> Y .<_ X ) )
19 18 con3d 
 |-  ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B /\ Y e. B ) -> ( -. Y .<_ X -> -. A. p e. A -. ( -. p .<_ X /\ p .<_ Y ) ) )
20 dfrex2 
 |-  ( E. p e. A ( -. p .<_ X /\ p .<_ Y ) <-> -. A. p e. A -. ( -. p .<_ X /\ p .<_ Y ) )
21 19 20 imbitrrdi 
 |-  ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B /\ Y e. B ) -> ( -. Y .<_ X -> E. p e. A ( -. p .<_ X /\ p .<_ Y ) ) )
22 10 21 syld 
 |-  ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B /\ Y e. B ) -> ( X .< Y -> E. p e. A ( -. p .<_ X /\ p .<_ Y ) ) )