Metamath Proof Explorer

Theorem lhpexle3

Description: There exists atom under a co-atom different from any three other elements. (Contributed by NM, 24-Jul-2013)

Ref Expression
Hypotheses lhpex1.l 
|- .<_ = ( le ` K )
lhpex1.a 
|- A = ( Atoms ` K )
lhpex1.h 
|- H = ( LHyp ` K )
Assertion lhpexle3 
|- ( ( K e. HL /\ W e. H ) -> E. p e. A ( p .<_ W /\ ( p =/= X /\ p =/= Y /\ p =/= Z ) ) )

Proof

Step Hyp Ref Expression
1 lhpex1.l 
 |-  .<_ = ( le ` K )
2 lhpex1.a 
 |-  A = ( Atoms ` K )
3 lhpex1.h 
 |-  H = ( LHyp ` K )
4 1 2 3 lhpexle2 
 |-  ( ( K e. HL /\ W e. H ) -> E. p e. A ( p .<_ W /\ p =/= X /\ p =/= Y ) )
5 3anass 
 |-  ( ( p .<_ W /\ p =/= X /\ p =/= Y ) <-> ( p .<_ W /\ ( p =/= X /\ p =/= Y ) ) )
6 5 rexbii 
 |-  ( E. p e. A ( p .<_ W /\ p =/= X /\ p =/= Y ) <-> E. p e. A ( p .<_ W /\ ( p =/= X /\ p =/= Y ) ) )
7 4 6 sylib 
 |-  ( ( K e. HL /\ W e. H ) -> E. p e. A ( p .<_ W /\ ( p =/= X /\ p =/= Y ) ) )
8 1 2 3 lhpexle2 
 |-  ( ( K e. HL /\ W e. H ) -> E. p e. A ( p .<_ W /\ p =/= X /\ p =/= Z ) )
9 8 adantr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Z e. A /\ Z .<_ W ) ) -> E. p e. A ( p .<_ W /\ p =/= X /\ p =/= Z ) )
10 3anass 
 |-  ( ( p .<_ W /\ p =/= X /\ p =/= Z ) <-> ( p .<_ W /\ ( p =/= X /\ p =/= Z ) ) )
11 10 rexbii 
 |-  ( E. p e. A ( p .<_ W /\ p =/= X /\ p =/= Z ) <-> E. p e. A ( p .<_ W /\ ( p =/= X /\ p =/= Z ) ) )
12 9 11 sylib 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Z e. A /\ Z .<_ W ) ) -> E. p e. A ( p .<_ W /\ ( p =/= X /\ p =/= Z ) ) )
13 1 2 3 lhpexle2 
 |-  ( ( K e. HL /\ W e. H ) -> E. p e. A ( p .<_ W /\ p =/= Y /\ p =/= Z ) )
14 3anass 
 |-  ( ( p .<_ W /\ p =/= Y /\ p =/= Z ) <-> ( p .<_ W /\ ( p =/= Y /\ p =/= Z ) ) )
15 14 rexbii 
 |-  ( E. p e. A ( p .<_ W /\ p =/= Y /\ p =/= Z ) <-> E. p e. A ( p .<_ W /\ ( p =/= Y /\ p =/= Z ) ) )
16 13 15 sylib 
 |-  ( ( K e. HL /\ W e. H ) -> E. p e. A ( p .<_ W /\ ( p =/= Y /\ p =/= Z ) ) )
17 16 3ad2ant1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Z e. A /\ Z .<_ W ) /\ ( Y e. A /\ Y .<_ W ) ) -> E. p e. A ( p .<_ W /\ ( p =/= Y /\ p =/= Z ) ) )
18 simpl1 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( Z e. A /\ Z .<_ W ) /\ ( Y e. A /\ Y .<_ W ) ) /\ ( X e. A /\ X .<_ W ) ) -> ( K e. HL /\ W e. H ) )
19 simpl3l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( Z e. A /\ Z .<_ W ) /\ ( Y e. A /\ Y .<_ W ) ) /\ ( X e. A /\ X .<_ W ) ) -> Y e. A )
20 simpl2l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( Z e. A /\ Z .<_ W ) /\ ( Y e. A /\ Y .<_ W ) ) /\ ( X e. A /\ X .<_ W ) ) -> Z e. A )
21 simprl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( Z e. A /\ Z .<_ W ) /\ ( Y e. A /\ Y .<_ W ) ) /\ ( X e. A /\ X .<_ W ) ) -> X e. A )
22 simpl3r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( Z e. A /\ Z .<_ W ) /\ ( Y e. A /\ Y .<_ W ) ) /\ ( X e. A /\ X .<_ W ) ) -> Y .<_ W )
23 simpl2r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( Z e. A /\ Z .<_ W ) /\ ( Y e. A /\ Y .<_ W ) ) /\ ( X e. A /\ X .<_ W ) ) -> Z .<_ W )
24 simprr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( Z e. A /\ Z .<_ W ) /\ ( Y e. A /\ Y .<_ W ) ) /\ ( X e. A /\ X .<_ W ) ) -> X .<_ W )
25 1 2 3 lhpexle3lem 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Y e. A /\ Z e. A /\ X e. A ) /\ ( Y .<_ W /\ Z .<_ W /\ X .<_ W ) ) -> E. p e. A ( p .<_ W /\ ( p =/= Y /\ p =/= Z /\ p =/= X ) ) )
26 18 19 20 21 22 23 24 25 syl133anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( Z e. A /\ Z .<_ W ) /\ ( Y e. A /\ Y .<_ W ) ) /\ ( X e. A /\ X .<_ W ) ) -> E. p e. A ( p .<_ W /\ ( p =/= Y /\ p =/= Z /\ p =/= X ) ) )
27 df-3an 
 |-  ( ( p =/= Y /\ p =/= Z /\ p =/= X ) <-> ( ( p =/= Y /\ p =/= Z ) /\ p =/= X ) )
28 27 anbi2i 
 |-  ( ( p .<_ W /\ ( p =/= Y /\ p =/= Z /\ p =/= X ) ) <-> ( p .<_ W /\ ( ( p =/= Y /\ p =/= Z ) /\ p =/= X ) ) )
29 3anass 
 |-  ( ( p .<_ W /\ ( p =/= Y /\ p =/= Z ) /\ p =/= X ) <-> ( p .<_ W /\ ( ( p =/= Y /\ p =/= Z ) /\ p =/= X ) ) )
30 28 29 bitr4i 
 |-  ( ( p .<_ W /\ ( p =/= Y /\ p =/= Z /\ p =/= X ) ) <-> ( p .<_ W /\ ( p =/= Y /\ p =/= Z ) /\ p =/= X ) )
31 30 rexbii 
 |-  ( E. p e. A ( p .<_ W /\ ( p =/= Y /\ p =/= Z /\ p =/= X ) ) <-> E. p e. A ( p .<_ W /\ ( p =/= Y /\ p =/= Z ) /\ p =/= X ) )
32 26 31 sylib 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( Z e. A /\ Z .<_ W ) /\ ( Y e. A /\ Y .<_ W ) ) /\ ( X e. A /\ X .<_ W ) ) -> E. p e. A ( p .<_ W /\ ( p =/= Y /\ p =/= Z ) /\ p =/= X ) )
33 17 32 lhpexle1lem 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Z e. A /\ Z .<_ W ) /\ ( Y e. A /\ Y .<_ W ) ) -> E. p e. A ( p .<_ W /\ ( p =/= Y /\ p =/= Z ) /\ p =/= X ) )
34 an31 
 |-  ( ( ( p =/= Y /\ p =/= Z ) /\ p =/= X ) <-> ( ( p =/= X /\ p =/= Z ) /\ p =/= Y ) )
35 34 anbi2i 
 |-  ( ( p .<_ W /\ ( ( p =/= Y /\ p =/= Z ) /\ p =/= X ) ) <-> ( p .<_ W /\ ( ( p =/= X /\ p =/= Z ) /\ p =/= Y ) ) )
36 3anass 
 |-  ( ( p .<_ W /\ ( p =/= X /\ p =/= Z ) /\ p =/= Y ) <-> ( p .<_ W /\ ( ( p =/= X /\ p =/= Z ) /\ p =/= Y ) ) )
37 35 29 36 3bitr4i 
 |-  ( ( p .<_ W /\ ( p =/= Y /\ p =/= Z ) /\ p =/= X ) <-> ( p .<_ W /\ ( p =/= X /\ p =/= Z ) /\ p =/= Y ) )
38 37 rexbii 
 |-  ( E. p e. A ( p .<_ W /\ ( p =/= Y /\ p =/= Z ) /\ p =/= X ) <-> E. p e. A ( p .<_ W /\ ( p =/= X /\ p =/= Z ) /\ p =/= Y ) )
39 33 38 sylib 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Z e. A /\ Z .<_ W ) /\ ( Y e. A /\ Y .<_ W ) ) -> E. p e. A ( p .<_ W /\ ( p =/= X /\ p =/= Z ) /\ p =/= Y ) )
40 39 3expa 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( Z e. A /\ Z .<_ W ) ) /\ ( Y e. A /\ Y .<_ W ) ) -> E. p e. A ( p .<_ W /\ ( p =/= X /\ p =/= Z ) /\ p =/= Y ) )
41 12 40 lhpexle1lem 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Z e. A /\ Z .<_ W ) ) -> E. p e. A ( p .<_ W /\ ( p =/= X /\ p =/= Z ) /\ p =/= Y ) )
42 an32 
 |-  ( ( ( p =/= X /\ p =/= Z ) /\ p =/= Y ) <-> ( ( p =/= X /\ p =/= Y ) /\ p =/= Z ) )
43 42 anbi2i 
 |-  ( ( p .<_ W /\ ( ( p =/= X /\ p =/= Z ) /\ p =/= Y ) ) <-> ( p .<_ W /\ ( ( p =/= X /\ p =/= Y ) /\ p =/= Z ) ) )
44 3anass 
 |-  ( ( p .<_ W /\ ( p =/= X /\ p =/= Y ) /\ p =/= Z ) <-> ( p .<_ W /\ ( ( p =/= X /\ p =/= Y ) /\ p =/= Z ) ) )
45 43 36 44 3bitr4i 
 |-  ( ( p .<_ W /\ ( p =/= X /\ p =/= Z ) /\ p =/= Y ) <-> ( p .<_ W /\ ( p =/= X /\ p =/= Y ) /\ p =/= Z ) )
46 45 rexbii 
 |-  ( E. p e. A ( p .<_ W /\ ( p =/= X /\ p =/= Z ) /\ p =/= Y ) <-> E. p e. A ( p .<_ W /\ ( p =/= X /\ p =/= Y ) /\ p =/= Z ) )
47 41 46 sylib 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Z e. A /\ Z .<_ W ) ) -> E. p e. A ( p .<_ W /\ ( p =/= X /\ p =/= Y ) /\ p =/= Z ) )
48 7 47 lhpexle1lem 
 |-  ( ( K e. HL /\ W e. H ) -> E. p e. A ( p .<_ W /\ ( p =/= X /\ p =/= Y ) /\ p =/= Z ) )
49 df-3an 
 |-  ( ( p =/= X /\ p =/= Y /\ p =/= Z ) <-> ( ( p =/= X /\ p =/= Y ) /\ p =/= Z ) )
50 49 anbi2i 
 |-  ( ( p .<_ W /\ ( p =/= X /\ p =/= Y /\ p =/= Z ) ) <-> ( p .<_ W /\ ( ( p =/= X /\ p =/= Y ) /\ p =/= Z ) ) )
51 44 50 bitr4i 
 |-  ( ( p .<_ W /\ ( p =/= X /\ p =/= Y ) /\ p =/= Z ) <-> ( p .<_ W /\ ( p =/= X /\ p =/= Y /\ p =/= Z ) ) )
52 51 rexbii 
 |-  ( E. p e. A ( p .<_ W /\ ( p =/= X /\ p =/= Y ) /\ p =/= Z ) <-> E. p e. A ( p .<_ W /\ ( p =/= X /\ p =/= Y /\ p =/= Z ) ) )
53 48 52 sylib 
 |-  ( ( K e. HL /\ W e. H ) -> E. p e. A ( p .<_ W /\ ( p =/= X /\ p =/= Y /\ p =/= Z ) ) )