Theorem dalemcceb

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

	Ref	Expression
Hypotheses	da.ps0	|- ( ps <-> ( ( c e. A /\ d e. A ) /\ -. c .<_ Y /\ ( d =/= c /\ -. d .<_ Y /\ C .<_ ( c .\/ d ) ) ) )
	da.a1	|- A = ( Atoms ` K )
Assertion	dalemcceb	|- ( ps -> c e. ( Base ` K ) )

Proof

Step	Hyp	Ref	Expression
1		da.ps0	|- ( ps <-> ( ( c e. A /\ d e. A ) /\ -. c .<_ Y /\ ( d =/= c /\ -. d .<_ Y /\ C .<_ ( c .\/ d ) ) ) )
2		da.a1	|- A = ( Atoms ` K )
3	1	dalemccea	|- ( ps -> c e. A )
4		eqid	|- ( Base ` K ) = ( Base ` K )
5	4 2	atbase	|- ( c e. A -> c e. ( Base ` K ) )
6	3 5	syl	|- ( ps -> c e. ( Base ` K ) )