Theorem dalempjqeb 33212

Description: Lemma for dath 33303. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.)

Hypotheses

Ref	Expression
dalema.ph	|- ( ph <-> ( ( ( K e. HL /\ C e. ( Base ` K ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) /\ ( Y e. O /\ Z e. O ) /\ ( ( -. C .<_ ( P .\/ Q ) /\ -. C .<_ ( Q .\/ R ) /\ -. C .<_ ( R .\/ P ) ) /\ ( -. C .<_ ( S .\/ T ) /\ -. C .<_ ( T .\/ U ) /\ -. C .<_ ( U .\/ S ) ) /\ ( C .<_ ( P .\/ S ) /\ C .<_ ( Q .\/ T ) /\ C .<_ ( R .\/ U ) ) ) ) )
dalemb.j	|- .\/ = ( join ` K )
dalemb.a	|- A = ( Atoms ` K )

Assertion

Ref	Expression
dalempjqeb	|- ( ph -> ( P .\/ Q ) e. ( Base ` K ) )

Proof of Theorem dalempjqeb

Step	Hyp	Ref	Expression
1		dalema.ph	. . 3 |- ( ph <-> ( ( ( K e. HL /\ C e. ( Base ` K ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) /\ ( Y e. O /\ Z e. O ) /\ ( ( -. C .<_ ( P .\/ Q ) /\ -. C .<_ ( Q .\/ R ) /\ -. C .<_ ( R .\/ P ) ) /\ ( -. C .<_ ( S .\/ T ) /\ -. C .<_ ( T .\/ U ) /\ -. C .<_ ( U .\/ S ) ) /\ ( C .<_ ( P .\/ S ) /\ C .<_ ( Q .\/ T ) /\ C .<_ ( R .\/ U ) ) ) ) )
2	1	dalemkehl 33190	. 2 |- ( ph -> K e. HL )
3	1	dalempea 33193	. 2 |- ( ph -> P e. A )
4	1	dalemqea 33194	. 2 |- ( ph -> Q e. A )
5		eqid 2452	. . 3 |- ( Base ` K ) = ( Base ` K )
6		dalemb.j	. . 3 |- .\/ = ( join ` K )
7		dalemb.a	. . 3 |- A = ( Atoms ` K )
8	5, 6, 7	hlatjcl 32934	. 2 |- ( ( K e. HL /\ P e. A /\ Q e. A ) -> ( P .\/ Q ) e. ( Base ` K ) )
9	2, 3, 4, 8	syl3anc 1271	1 |- ( ph -> ( P .\/ Q ) e. ( Base ` K ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 189   /\ wa 375   /\ w3a 986   = wceq 1448   e. wcel 1891   class class class wbr 4374   ` cfv 5561  (class class class)co 6276   Basecbs 15132   joincjn 16200   Atomscatm 32831   HLchlt 32918

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1673  ax-4 1686  ax-5 1762  ax-6 1809  ax-7 1855  ax-8 1893  ax-9 1900  ax-10 1919  ax-11 1924  ax-12 1937  ax-13 2092  ax-ext 2432  ax-rep 4487  ax-sep 4497  ax-nul 4506  ax-pow 4554  ax-pr 4612  ax-un 6571

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 988  df-tru 1451  df-ex 1668  df-nf 1672  df-sb 1802  df-eu 2304  df-mo 2305  df-clab 2439  df-cleq 2445  df-clel 2448  df-nfc 2582  df-ne 2624  df-ral 2742  df-rex 2743  df-reu 2744  df-rab 2746  df-v 3015  df-sbc 3236  df-csb 3332  df-dif 3375  df-un 3377  df-in 3379  df-ss 3386  df-nul 3700  df-if 3850  df-pw 3921  df-sn 3937  df-pr 3939  df-op 3943  df-uni 4169  df-iun 4250  df-br 4375  df-opab 4434  df-mpt 4435  df-id 4727  df-xp 4818  df-rel 4819  df-cnv 4820  df-co 4821  df-dm 4822  df-rn 4823  df-res 4824  df-ima 4825  df-iota 5525  df-fun 5563  df-fn 5564  df-f 5565  df-f1 5566  df-fo 5567  df-f1o 5568  df-fv 5569  df-riota 6238  df-ov 6279  df-oprab 6280  df-lub 16231  df-glb 16232  df-join 16233  df-meet 16234  df-lat 16303  df-ats 32835  df-atl 32866  df-cvlat 32890  df-hlat 32919

This theorem is referenced by:  dalemcea  33227  dalem3  33231  dalem4  33232  dalem5  33234  dalem-cly  33238  dalem10  33240  dalem17  33247  dalem38  33277  dalem44  33283  dalem48  33287  dalem54  33293  dalem55  33294  dalem57  33296