Metamath Proof Explorer

Theorem 4atexlemp

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	4atexlemp	\|- ( ph -> P e. A )

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

4atexlemp

|- ( ph -> P 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	1	4atexlempw	\|- ( ph -> ( P e. A /\ -. P .<_ W ) )
3	2	simpld	\|- ( ph -> P e. A )

Step

Hyp

Ref

Expression

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

4atexlempw

 |-  ( ph -> ( P e. A /\ -. P .<_ W ) )

simpld

 |-  ( ph -> P e. A )