Theorem pats

Description: The set of atoms in a poset. (Contributed by NM, 18-Sep-2011)

	Ref	Expression
Hypotheses	patoms.b	|- B = ( Base ` K )
	patoms.z	|- .0. = ( 0. ` K )
	patoms.c	|- C = (
	patoms.a	|- A = ( Atoms ` K )
Assertion	pats	|- ( K e. D -> A = { x e. B | .0. C x } )

Proof

Step	Hyp	Ref	Expression
1		patoms.b	|- B = ( Base ` K )
2		patoms.z	|- .0. = ( 0. ` K )
3		patoms.c	|- C = (
4		patoms.a	|- A = ( Atoms ` K )
5		elex	|- ( K e. D -> K e. _V )
6		fveq2	|- ( p = K -> ( Base ` p ) = ( Base ` K ) )
7	6 1	eqtr4di	|- ( p = K -> ( Base ` p ) = B )
8		fveq2	|- ( p = K -> (
9	8 3	eqtr4di	|- ( p = K -> (
10	9	breqd	|- ( p = K -> ( ( 0. ` p ) ( ( 0. ` p ) C x ) )
11		fveq2	|- ( p = K -> ( 0. ` p ) = ( 0. ` K ) )
12	11 2	eqtr4di	|- ( p = K -> ( 0. ` p ) = .0. )
13	12	breq1d	|- ( p = K -> ( ( 0. ` p ) C x <-> .0. C x ) )
14	10 13	bitrd	|- ( p = K -> ( ( 0. ` p ) ( .0. C x ) )
15	7 14	rabeqbidv	|- ( p = K -> { x e. ( Base ` p ) | ( 0. ` p ) (
16		df-ats	|- Atoms = ( p e. _V |-> { x e. ( Base ` p ) | ( 0. ` p ) (
17	1	fvexi	|- B e. _V
18	17	rabex	|- { x e. B | .0. C x } e. _V
19	15 16 18	fvmpt	|- ( K e. _V -> ( Atoms ` K ) = { x e. B | .0. C x } )
20	4 19	syl5eq	|- ( K e. _V -> A = { x e. B | .0. C x } )
21	5 20	syl	|- ( K e. D -> A = { x e. B | .0. C x } )