Metamath Proof Explorer

Theorem 4atexlemkc

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

		Ref	Expression
	Hypothesis	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 ) ) ) )
	Assertion	4atexlemkc	\|- ( ph -> K e. CvLat )

Ref

Expression

Hypothesis

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 ) ) ) )

Assertion

4atexlemkc

|- ( ph -> K e. CvLat )

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	1	4atexlemk	\|- ( ph -> K e. HL )
3		hlcvl	\|- ( K e. HL -> K e. CvLat )
4	2 3	syl	\|- ( ph -> K e. CvLat )