Theorem iswatN

Description: The predicate "is a W atom" (corresponding to fiducial atom D ). (Contributed by NM, 26-Jan-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	watomfval.a	|- A = ( Atoms ` K )
	watomfval.p	|- P = ( _|_P ` K )
	watomfval.w	|- W = ( WAtoms ` K )
Assertion	iswatN	|- ( ( K e. B /\ D e. A ) -> ( P e. ( W ` D ) <-> ( P e. A /\ -. P e. ( ( _|_P ` K ) ` { D } ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		watomfval.a	|- A = ( Atoms ` K )
2		watomfval.p	|- P = ( _|_P ` K )
3		watomfval.w	|- W = ( WAtoms ` K )
4	1 2 3	watvalN	|- ( ( K e. B /\ D e. A ) -> ( W ` D ) = ( A \ ( ( _|_P ` K ) ` { D } ) ) )
5	4	eleq2d	|- ( ( K e. B /\ D e. A ) -> ( P e. ( W ` D ) <-> P e. ( A \ ( ( _|_P ` K ) ` { D } ) ) ) )
6		eldif	|- ( P e. ( A \ ( ( _|_P ` K ) ` { D } ) ) <-> ( P e. A /\ -. P e. ( ( _|_P ` K ) ` { D } ) ) )
7	5 6	bitrdi	|- ( ( K e. B /\ D e. A ) -> ( P e. ( W ` D ) <-> ( P e. A /\ -. P e. ( ( _|_P ` K ) ` { D } ) ) ) )