Theorem 4atexlemv

Description: Lemma for 4atexlem7 . (Contributed by NM, 23-Nov-2012)

	Ref	Expression
Hypotheses	4thatlem.ph	|- ( ph <-> ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( S e. A /\ ( R e. A /\ -. R .<_ W /\ ( P .\/ R ) = ( Q .\/ R ) ) /\ ( T e. A /\ ( U .\/ T ) = ( V .\/ T ) ) ) /\ ( P =/= Q /\ -. S .<_ ( P .\/ Q ) ) ) )
	4thatlem0.l	|- .<_ = ( le ` K )
	4thatlem0.j	|- .\/ = ( join ` K )
	4thatlem0.m	|- ./\ = ( meet ` K )
	4thatlem0.a	|- A = ( Atoms ` K )
	4thatlem0.h	|- H = ( LHyp ` K )
	4thatlem0.u	|- U = ( ( P .\/ Q ) ./\ W )
	4thatlem0.v	|- V = ( ( P .\/ S ) ./\ W )
Assertion	4atexlemv	|- ( ph -> V e. A )

Proof

Step	Hyp	Ref	Expression
1		4thatlem.ph	|- ( ph <-> ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( S e. A /\ ( R e. A /\ -. R .<_ W /\ ( P .\/ R ) = ( Q .\/ R ) ) /\ ( T e. A /\ ( U .\/ T ) = ( V .\/ T ) ) ) /\ ( P =/= Q /\ -. S .<_ ( P .\/ Q ) ) ) )
2		4thatlem0.l	|- .<_ = ( le ` K )
3		4thatlem0.j	|- .\/ = ( join ` K )
4		4thatlem0.m	|- ./\ = ( meet ` K )
5		4thatlem0.a	|- A = ( Atoms ` K )
6		4thatlem0.h	|- H = ( LHyp ` K )
7		4thatlem0.u	|- U = ( ( P .\/ Q ) ./\ W )
8		4thatlem0.v	|- V = ( ( P .\/ S ) ./\ W )
9	1	4atexlemk	|- ( ph -> K e. HL )
10	1	4atexlemw	|- ( ph -> W e. H )
11	1	4atexlempw	|- ( ph -> ( P e. A /\ -. P .<_ W ) )
12	1	4atexlems	|- ( ph -> S e. A )
13	1 2 3 5	4atexlempns	|- ( ph -> P =/= S )
14	2 3 4 5 6 8	lhpat2	|- ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( S e. A /\ P =/= S ) ) -> V e. A )
15	9 10 11 12 13 14	syl212anc	|- ( ph -> V e. A )