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	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	watomfval.p	⊢ 𝑃 = ( ⊥𝑃 ‘ 𝐾 )
	watomfval.w	⊢ 𝑊 = ( WAtoms ‘ 𝐾 )
Assertion	iswatN	⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝐷 ∈ 𝐴 ) → ( 𝑃 ∈ ( 𝑊 ‘ 𝐷 ) ↔ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ∈ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ { 𝐷 } ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		watomfval.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
2		watomfval.p	⊢ 𝑃 = ( ⊥𝑃 ‘ 𝐾 )
3		watomfval.w	⊢ 𝑊 = ( WAtoms ‘ 𝐾 )
4	1 2 3	watvalN	⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝐷 ∈ 𝐴 ) → ( 𝑊 ‘ 𝐷 ) = ( 𝐴 ∖ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ { 𝐷 } ) ) )
5	4	eleq2d	⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝐷 ∈ 𝐴 ) → ( 𝑃 ∈ ( 𝑊 ‘ 𝐷 ) ↔ 𝑃 ∈ ( 𝐴 ∖ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ { 𝐷 } ) ) ) )
6		eldif	⊢ ( 𝑃 ∈ ( 𝐴 ∖ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ { 𝐷 } ) ) ↔ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ∈ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ { 𝐷 } ) ) )
7	5 6	bitrdi	⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝐷 ∈ 𝐴 ) → ( 𝑃 ∈ ( 𝑊 ‘ 𝐷 ) ↔ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ∈ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ { 𝐷 } ) ) ) )