Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  athgt Structured version   Unicode version

Theorem athgt 32990
 Description: A Hilbert lattice, whose height is at least 4, has a chain of 4 successively covering atom joins. (Contributed by NM, 3-May-2012.)
Hypotheses
Ref Expression
athgt.j
athgt.c
athgt.a
Assertion
Ref Expression
athgt
Distinct variable groups:   ,,,,   ,,   ,,,,
Allowed substitution hints:   (,,,)   (,)

Proof of Theorem athgt
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2422 . . 3
2 eqid 2422 . . 3
3 eqid 2422 . . 3
4 eqid 2422 . . 3
51, 2, 3, 4hlhgt4 32922 . 2
6 simpl1 1008 . . . . . . . . 9
7 hlop 32897 . . . . . . . . . 10
81, 3op0cl 32719 . . . . . . . . . 10
96, 7, 83syl 18 . . . . . . . . 9
10 simpl2l 1058 . . . . . . . . 9
11 simprll 770 . . . . . . . . 9
12 eqid 2422 . . . . . . . . . 10
13 athgt.j . . . . . . . . . 10
14 athgt.c . . . . . . . . . 10
15 athgt.a . . . . . . . . . 10
161, 12, 2, 13, 14, 15hlrelat3 32946 . . . . . . . . 9
176, 9, 10, 11, 16syl31anc 1267 . . . . . . . 8
18 simp11 1035 . . . . . . . . . . . . . 14
19 simp3 1007 . . . . . . . . . . . . . 14
203, 14, 15atcvr0 32823 . . . . . . . . . . . . . 14
2118, 19, 20syl2anc 665 . . . . . . . . . . . . 13
22 hlol 32896 . . . . . . . . . . . . . . 15
2318, 22syl 17 . . . . . . . . . . . . . 14
241, 15atbase 32824 . . . . . . . . . . . . . . 15
25243ad2ant3 1028 . . . . . . . . . . . . . 14
261, 13, 3olj02 32761 . . . . . . . . . . . . . 14
2723, 25, 26syl2anc 665 . . . . . . . . . . . . 13
2821, 27breqtrrd 4450 . . . . . . . . . . . 12
2928biantrurd 510 . . . . . . . . . . 11
3027breq1d 4433 . . . . . . . . . . 11
3129, 30bitr3d 258 . . . . . . . . . 10
32313expa 1205 . . . . . . . . 9
3332rexbidva 2933 . . . . . . . 8
3417, 33mpbid 213 . . . . . . 7
35 simp11 1035 . . . . . . . . . . . 12
36253adant3r 1261 . . . . . . . . . . . 12
37 simp12r 1119 . . . . . . . . . . . 12
38 simp3r 1034 . . . . . . . . . . . . 13
39 simp2lr 1073 . . . . . . . . . . . . 13
40 hlpos 32900 . . . . . . . . . . . . . . 15
4135, 40syl 17 . . . . . . . . . . . . . 14
42 simp12l 1118 . . . . . . . . . . . . . 14
431, 12, 2plelttr 16217 . . . . . . . . . . . . . 14
4441, 36, 42, 37, 43syl13anc 1266 . . . . . . . . . . . . 13
4538, 39, 44mp2and 683 . . . . . . . . . . . 12
461, 12, 2, 13, 14, 15hlrelat3 32946 . . . . . . . . . . . 12
4735, 36, 37, 45, 46syl31anc 1267 . . . . . . . . . . 11
48 simp11 1035 . . . . . . . . . . . . . . . . . . . . . 22
49 hllat 32898 . . . . . . . . . . . . . . . . . . . . . . . 24
5048, 49syl 17 . . . . . . . . . . . . . . . . . . . . . . 23
51 simp3ll 1076 . . . . . . . . . . . . . . . . . . . . . . . 24
5251, 24syl 17 . . . . . . . . . . . . . . . . . . . . . . 23
53 simp3lr 1077 . . . . . . . . . . . . . . . . . . . . . . . 24
541, 15atbase 32824 . . . . . . . . . . . . . . . . . . . . . . . 24
5553, 54syl 17 . . . . . . . . . . . . . . . . . . . . . . 23
561, 13latjcl 16296 . . . . . . . . . . . . . . . . . . . . . . 23
5750, 52, 55, 56syl3anc 1264 . . . . . . . . . . . . . . . . . . . . . 22
58 simp13 1037 . . . . . . . . . . . . . . . . . . . . . 22
59 simp3r 1034 . . . . . . . . . . . . . . . . . . . . . . 23
60 simp2l 1031 . . . . . . . . . . . . . . . . . . . . . . 23
6148, 40syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24
62 simp12 1036 . . . . . . . . . . . . . . . . . . . . . . . 24
631, 12, 2plelttr 16217 . . . . . . . . . . . . . . . . . . . . . . . 24
6461, 57, 62, 58, 63syl13anc 1266 . . . . . . . . . . . . . . . . . . . . . . 23
6559, 60, 64mp2and 683 . . . . . . . . . . . . . . . . . . . . . 22
661, 12, 2, 13, 14, 15hlrelat3 32946 . . . . . . . . . . . . . . . . . . . . . 22
6748, 57, 58, 65, 66syl31anc 1267 . . . . . . . . . . . . . . . . . . . . 21
68 simp1ll 1068 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
6968, 49syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
70 simp2ll 1072 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
7170, 24syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
72 simp2lr 1073 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
7372, 54syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
7469, 71, 73, 56syl3anc 1264 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
75 simp3l 1033 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
761, 15atbase 32824 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
7775, 76syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
781, 13latjcl 16296 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
7969, 74, 77, 78syl3anc 1264 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
801, 4op1cl 32720 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
8168, 7, 803syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
82 simp3r 1034 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
83 simp1r 1030 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
8468, 40syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
85 simp1lr 1069 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
861, 12, 2plelttr 16217 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
8784, 79, 85, 81, 86syl13anc 1266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
8882, 83, 87mp2and 683 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
891, 12, 2, 13, 14, 15hlrelat3 32946 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
9068, 79, 81, 88, 89syl31anc 1267 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
91 simpl 458 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
9291reximi 2890 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
9390, 92syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
94933exp 1204 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
9594exp4a 609 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
9695ex 435 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
97963adant2 1024 . . . . . . . . . . . . . . . . . . . . . . . . . 26
98973imp 1199 . . . . . . . . . . . . . . . . . . . . . . . . 25
99983adant2l 1258 . . . . . . . . . . . . . . . . . . . . . . . 24
10099imp 430 . . . . . . . . . . . . . . . . . . . . . . 23
101100anim2d 567 . . . . . . . . . . . . . . . . . . . . . 22
102101reximdva 2897 . . . . . . . . . . . . . . . . . . . . 21
10367, 102mpd 15 . . . . . . . . . . . . . . . . . . . 20
1041033exp 1204 . . . . . . . . . . . . . . . . . . 19
105104exp4a 609 . . . . . . . . . . . . . . . . . 18
106105exp4a 609 . . . . . . . . . . . . . . . . 17
1071063adant2l 1258 . . . . . . . . . . . . . . . 16
1081073imp1 1218 . . . . . . . . . . . . . . 15
109108anim2d 567 . . . . . . . . . . . . . 14
110109reximdva 2897 . . . . . . . . . . . . 13
1111103adant2l 1258 . . . . . . . . . . . 12
1121113adant3r 1261 . . . . . . . . . . 11
11347, 112mpd 15 . . . . . . . . . 10
1141133expia 1207 . . . . . . . . 9
115114expd 437 . . . . . . . 8
116115reximdvai 2894 . . . . . . 7
11734, 116mpd 15 . . . . . 6
1181173exp1 1221 . . . . 5
119118imp 430 . . . 4
120119rexlimdv 2912 . . 3
121120rexlimdvva 2921 . 2
1225, 121mpd 15 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 187   wa 370   w3a 982   wceq 1437   wcel 1872  wrex 2772   class class class wbr 4423  cfv 5601  (class class class)co 6305  cbs 15120  cple 15196  cpo 16184  cplt 16185  cjn 16188  cp0 16282  cp1 16283  clat 16290  cops 32707  col 32709   ccvr 32797  catm 32798  chlt 32885 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-rep 4536  ax-sep 4546  ax-nul 4555  ax-pow 4602  ax-pr 4660  ax-un 6597 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-ral 2776  df-rex 2777  df-reu 2778  df-rab 2780  df-v 3082  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3912  df-pw 3983  df-sn 3999  df-pr 4001  df-op 4005  df-uni 4220  df-iun 4301  df-br 4424  df-opab 4483  df-mpt 4484  df-id 4768  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-riota 6267  df-ov 6308  df-oprab 6309  df-preset 16172  df-poset 16190  df-plt 16203  df-lub 16219  df-glb 16220  df-join 16221  df-meet 16222  df-p0 16284  df-p1 16285  df-lat 16291  df-clat 16353  df-oposet 32711  df-ol 32713  df-oml 32714  df-covers 32801  df-ats 32802  df-atl 32833  df-cvlat 32857  df-hlat 32886 This theorem is referenced by:  3dim0  32991
 Copyright terms: Public domain W3C validator