Theorem leatb

Description: A poset element less than or equal to an atom equals either zero or the atom. ( atss analog.) (Contributed by NM, 17-Nov-2011)

	Ref	Expression
Hypotheses	leatom.b	|- B = ( Base ` K )
	leatom.l	|- .<_ = ( le ` K )
	leatom.z	|- .0. = ( 0. ` K )
	leatom.a	|- A = ( Atoms ` K )
Assertion	leatb	|- ( ( K e. OP /\ X e. B /\ P e. A ) -> ( X .<_ P <-> ( X = P \/ X = .0. ) ) )

Proof

Step	Hyp	Ref	Expression
1		leatom.b	|- B = ( Base ` K )
2		leatom.l	|- .<_ = ( le ` K )
3		leatom.z	|- .0. = ( 0. ` K )
4		leatom.a	|- A = ( Atoms ` K )
5	1 2 3	op0le	|- ( ( K e. OP /\ X e. B ) -> .0. .<_ X )
6	5	3adant3	|- ( ( K e. OP /\ X e. B /\ P e. A ) -> .0. .<_ X )
7	6	biantrurd	|- ( ( K e. OP /\ X e. B /\ P e. A ) -> ( X .<_ P <-> ( .0. .<_ X /\ X .<_ P ) ) )
8		opposet	|- ( K e. OP -> K e. Poset )
9	8	3ad2ant1	|- ( ( K e. OP /\ X e. B /\ P e. A ) -> K e. Poset )
10	1 3	op0cl	|- ( K e. OP -> .0. e. B )
11	1 4	atbase	|- ( P e. A -> P e. B )
12		id	|- ( X e. B -> X e. B )
13	10 11 12	3anim123i	|- ( ( K e. OP /\ P e. A /\ X e. B ) -> ( .0. e. B /\ P e. B /\ X e. B ) )
14	13	3com23	|- ( ( K e. OP /\ X e. B /\ P e. A ) -> ( .0. e. B /\ P e. B /\ X e. B ) )
15		eqid	|- (
16	3 15 4	atcvr0	|- ( ( K e. OP /\ P e. A ) -> .0. (
17	16	3adant2	|- ( ( K e. OP /\ X e. B /\ P e. A ) -> .0. (
18	1 2 15	cvrnbtwn4	|- ( ( K e. Poset /\ ( .0. e. B /\ P e. B /\ X e. B ) /\ .0. ( ( ( .0. .<_ X /\ X .<_ P ) <-> ( .0. = X \/ X = P ) ) )
19	9 14 17 18	syl3anc	|- ( ( K e. OP /\ X e. B /\ P e. A ) -> ( ( .0. .<_ X /\ X .<_ P ) <-> ( .0. = X \/ X = P ) ) )
20		eqcom	|- ( .0. = X <-> X = .0. )
21	20	orbi1i	|- ( ( .0. = X \/ X = P ) <-> ( X = .0. \/ X = P ) )
22	19 21	bitrdi	|- ( ( K e. OP /\ X e. B /\ P e. A ) -> ( ( .0. .<_ X /\ X .<_ P ) <-> ( X = .0. \/ X = P ) ) )
23	7 22	bitrd	|- ( ( K e. OP /\ X e. B /\ P e. A ) -> ( X .<_ P <-> ( X = .0. \/ X = P ) ) )
24		orcom	|- ( ( X = .0. \/ X = P ) <-> ( X = P \/ X = .0. ) )
25	23 24	bitrdi	|- ( ( K e. OP /\ X e. B /\ P e. A ) -> ( X .<_ P <-> ( X = P \/ X = .0. ) ) )