Metamath Proof Explorer


Theorem hlrelat2

Description: A consequence of relative atomicity. ( chrelat2i analog.) (Contributed by NM, 5-Feb-2012)

Ref Expression
Hypotheses hlrelat2.b B=BaseK
hlrelat2.l ˙=K
hlrelat2.a A=AtomsK
Assertion hlrelat2 KHLXBYB¬X˙YpAp˙X¬p˙Y

Proof

Step Hyp Ref Expression
1 hlrelat2.b B=BaseK
2 hlrelat2.l ˙=K
3 hlrelat2.a A=AtomsK
4 hllat KHLKLat
5 eqid <K=<K
6 eqid meetK=meetK
7 1 2 5 6 latnlemlt KLatXBYB¬X˙YXmeetKY<KX
8 4 7 syl3an1 KHLXBYB¬X˙YXmeetKY<KX
9 simp1 KHLXBYBKHL
10 1 6 latmcl KLatXBYBXmeetKYB
11 4 10 syl3an1 KHLXBYBXmeetKYB
12 simp2 KHLXBYBXB
13 eqid joinK=joinK
14 1 2 5 13 3 hlrelat KHLXmeetKYBXBXmeetKY<KXpAXmeetKY<KXmeetKYjoinKpXmeetKYjoinKp˙X
15 14 ex KHLXmeetKYBXBXmeetKY<KXpAXmeetKY<KXmeetKYjoinKpXmeetKYjoinKp˙X
16 9 11 12 15 syl3anc KHLXBYBXmeetKY<KXpAXmeetKY<KXmeetKYjoinKpXmeetKYjoinKp˙X
17 simpl1 KHLXBYBpAKHL
18 17 hllatd KHLXBYBpAKLat
19 11 adantr KHLXBYBpAXmeetKYB
20 1 3 atbase pApB
21 20 adantl KHLXBYBpApB
22 simpl2 KHLXBYBpAXB
23 1 2 13 latjle12 KLatXmeetKYBpBXBXmeetKY˙Xp˙XXmeetKYjoinKp˙X
24 18 19 21 22 23 syl13anc KHLXBYBpAXmeetKY˙Xp˙XXmeetKYjoinKp˙X
25 simpr XmeetKY˙Xp˙Xp˙X
26 24 25 syl6bir KHLXBYBpAXmeetKYjoinKp˙Xp˙X
27 26 adantld KHLXBYBpAXmeetKY<KXmeetKYjoinKpXmeetKYjoinKp˙Xp˙X
28 simpl3 KHLXBYBpAYB
29 1 2 6 latlem12 KLatpBXBYBp˙Xp˙Yp˙XmeetKY
30 18 21 22 28 29 syl13anc KHLXBYBpAp˙Xp˙Yp˙XmeetKY
31 30 notbid KHLXBYBpA¬p˙Xp˙Y¬p˙XmeetKY
32 1 2 5 13 latnle KLatXmeetKYBpB¬p˙XmeetKYXmeetKY<KXmeetKYjoinKp
33 18 19 21 32 syl3anc KHLXBYBpA¬p˙XmeetKYXmeetKY<KXmeetKYjoinKp
34 31 33 bitrd KHLXBYBpA¬p˙Xp˙YXmeetKY<KXmeetKYjoinKp
35 34 24 anbi12d KHLXBYBpA¬p˙Xp˙YXmeetKY˙Xp˙XXmeetKY<KXmeetKYjoinKpXmeetKYjoinKp˙X
36 pm3.21 p˙Yp˙Xp˙Xp˙Y
37 orcom p˙Xp˙Y¬p˙X¬p˙Xp˙Xp˙Y
38 pm4.55 ¬¬p˙Xp˙Yp˙Xp˙Xp˙Y¬p˙X
39 imor p˙Xp˙Xp˙Y¬p˙Xp˙Xp˙Y
40 37 38 39 3bitr4ri p˙Xp˙Xp˙Y¬¬p˙Xp˙Yp˙X
41 36 40 sylib p˙Y¬¬p˙Xp˙Yp˙X
42 41 con2i ¬p˙Xp˙Yp˙X¬p˙Y
43 42 adantrl ¬p˙Xp˙YXmeetKY˙Xp˙X¬p˙Y
44 35 43 syl6bir KHLXBYBpAXmeetKY<KXmeetKYjoinKpXmeetKYjoinKp˙X¬p˙Y
45 27 44 jcad KHLXBYBpAXmeetKY<KXmeetKYjoinKpXmeetKYjoinKp˙Xp˙X¬p˙Y
46 45 reximdva KHLXBYBpAXmeetKY<KXmeetKYjoinKpXmeetKYjoinKp˙XpAp˙X¬p˙Y
47 16 46 syld KHLXBYBXmeetKY<KXpAp˙X¬p˙Y
48 8 47 sylbid KHLXBYB¬X˙YpAp˙X¬p˙Y
49 1 2 lattr KLatpBXBYBp˙XX˙Yp˙Y
50 18 21 22 28 49 syl13anc KHLXBYBpAp˙XX˙Yp˙Y
51 50 exp4b KHLXBYBpAp˙XX˙Yp˙Y
52 51 com34 KHLXBYBpAX˙Yp˙Xp˙Y
53 52 com23 KHLXBYBX˙YpAp˙Xp˙Y
54 53 ralrimdv KHLXBYBX˙YpAp˙Xp˙Y
55 iman p˙Xp˙Y¬p˙X¬p˙Y
56 55 ralbii pAp˙Xp˙YpA¬p˙X¬p˙Y
57 ralnex pA¬p˙X¬p˙Y¬pAp˙X¬p˙Y
58 56 57 bitri pAp˙Xp˙Y¬pAp˙X¬p˙Y
59 54 58 syl6ib KHLXBYBX˙Y¬pAp˙X¬p˙Y
60 59 con2d KHLXBYBpAp˙X¬p˙Y¬X˙Y
61 48 60 impbid KHLXBYB¬X˙YpAp˙X¬p˙Y