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

Theorem cdlemd4 33685
 Description: Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 30-May-2012.)
Hypotheses
Ref Expression
cdlemd4.l
cdlemd4.j
cdlemd4.a
cdlemd4.h
cdlemd4.t
Assertion
Ref Expression
cdlemd4

Proof of Theorem cdlemd4
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 simp11l 1116 . . 3
2 simp11r 1117 . . 3
3 simp21 1038 . . 3
4 simp22 1039 . . 3
5 simp231 1149 . . 3
6 cdlemd4.l . . . 4
7 cdlemd4.j . . . 4
8 cdlemd4.a . . . 4
9 cdlemd4.h . . . 4
106, 7, 8, 9cdlemb2 33524 . . 3
111, 2, 3, 4, 5, 10syl221anc 1275 . 2
12 simpl11 1080 . . 3
13 simpl12 1081 . . 3
14 simpl13 1082 . . 3
15 simpl21 1083 . . 3
16 simprl 762 . . . 4
17 simprrl 772 . . . 4
1816, 17jca 534 . . 3
19 hllat 32847 . . . . . . 7
201, 19syl 17 . . . . . 6
2120adantr 466 . . . . 5
22 eqid 2422 . . . . . . 7
2322, 8atbase 32773 . . . . . 6
2423ad2antrl 732 . . . . 5
25 simp21l 1122 . . . . . . 7
2622, 8atbase 32773 . . . . . . 7
2725, 26syl 17 . . . . . 6
2827adantr 466 . . . . 5
29 simp22l 1124 . . . . . . 7
3022, 8atbase 32773 . . . . . . 7
3129, 30syl 17 . . . . . 6
3231adantr 466 . . . . 5
33 simprrr 773 . . . . 5
3422, 6, 7latnlej1l 16302 . . . . . 6
3534necomd 2695 . . . . 5
3621, 24, 28, 32, 33, 35syl131anc 1277 . . . 4
37 simpl22 1084 . . . . 5
38 simpl23 1085 . . . . 5
396, 7, 8, 9cdlemd3 33684 . . . . 5
4012, 15, 37, 38, 14, 16, 33, 39syl133anc 1287 . . . 4
4136, 40jca 534 . . 3
42 simpl3l 1060 . . 3
435adantr 466 . . . . 5
4443, 33jca 534 . . . 4
45 simpl3 1010 . . . 4
46 cdlemd4.t . . . . 5
476, 7, 8, 9, 46cdlemd2 33683 . . . 4
4812, 13, 16, 15, 37, 44, 45, 47syl331anc 1289 . . 3
496, 7, 8, 9, 46cdlemd2 33683 . . 3
5012, 13, 14, 15, 18, 41, 42, 48, 49syl332anc 1295 . 2
5111, 50rexlimddv 2921 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wa 370   w3a 982   wceq 1437   wcel 1868   wne 2618  wrex 2776   class class class wbr 4420  cfv 5597  (class class class)co 6301  cbs 15108  cple 15184  cjn 16176  clat 16278  catm 32747  chlt 32834  clh 33467  cltrn 33584 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-rep 4533  ax-sep 4543  ax-nul 4551  ax-pow 4598  ax-pr 4656  ax-un 6593 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-reu 2782  df-rab 2784  df-v 3083  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3910  df-pw 3981  df-sn 3997  df-pr 3999  df-op 4003  df-uni 4217  df-iun 4298  df-iin 4299  df-br 4421  df-opab 4480  df-mpt 4481  df-id 4764  df-xp 4855  df-rel 4856  df-cnv 4857  df-co 4858  df-dm 4859  df-rn 4860  df-res 4861  df-ima 4862  df-iota 5561  df-fun 5599  df-fn 5600  df-f 5601  df-f1 5602  df-fo 5603  df-f1o 5604  df-fv 5605  df-riota 6263  df-ov 6304  df-oprab 6305  df-mpt2 6306  df-1st 6803  df-2nd 6804  df-map 7478  df-preset 16160  df-poset 16178  df-plt 16191  df-lub 16207  df-glb 16208  df-join 16209  df-meet 16210  df-p0 16272  df-p1 16273  df-lat 16279  df-clat 16341  df-oposet 32660  df-ol 32662  df-oml 32663  df-covers 32750  df-ats 32751  df-atl 32782  df-cvlat 32806  df-hlat 32835  df-psubsp 32986  df-pmap 32987  df-padd 33279  df-lhyp 33471  df-laut 33472  df-ldil 33587  df-ltrn 33588 This theorem is referenced by:  cdlemd5  33686
 Copyright terms: Public domain W3C validator