Theorem watvalN

Description: Value of the W atoms function. (Contributed by NM, 26-Jan-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	watomfval.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	watomfval.p	⊢ 𝑃 = ( ⊥𝑃 ‘ 𝐾 )
	watomfval.w	⊢ 𝑊 = ( WAtoms ‘ 𝐾 )
Assertion	watvalN	⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝐷 ∈ 𝐴 ) → ( 𝑊 ‘ 𝐷 ) = ( 𝐴 ∖ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ { 𝐷 } ) ) )

Proof

Step	Hyp	Ref	Expression
1		watomfval.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
2		watomfval.p	⊢ 𝑃 = ( ⊥𝑃 ‘ 𝐾 )
3		watomfval.w	⊢ 𝑊 = ( WAtoms ‘ 𝐾 )
4	1 2 3	watfvalN	⊢ ( 𝐾 ∈ 𝐵 → 𝑊 = ( 𝑑 ∈ 𝐴 ↦ ( 𝐴 ∖ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ { 𝑑 } ) ) ) )
5	4	fveq1d	⊢ ( 𝐾 ∈ 𝐵 → ( 𝑊 ‘ 𝐷 ) = ( ( 𝑑 ∈ 𝐴 ↦ ( 𝐴 ∖ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ { 𝑑 } ) ) ) ‘ 𝐷 ) )
6		sneq	⊢ ( 𝑑 = 𝐷 → { 𝑑 } = { 𝐷 } )
7	6	fveq2d	⊢ ( 𝑑 = 𝐷 → ( ( ⊥𝑃 ‘ 𝐾 ) ‘ { 𝑑 } ) = ( ( ⊥𝑃 ‘ 𝐾 ) ‘ { 𝐷 } ) )
8	7	difeq2d	⊢ ( 𝑑 = 𝐷 → ( 𝐴 ∖ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ { 𝑑 } ) ) = ( 𝐴 ∖ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ { 𝐷 } ) ) )
9		eqid	⊢ ( 𝑑 ∈ 𝐴 ↦ ( 𝐴 ∖ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ { 𝑑 } ) ) ) = ( 𝑑 ∈ 𝐴 ↦ ( 𝐴 ∖ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ { 𝑑 } ) ) )
10	1	fvexi	⊢ 𝐴 ∈ V
11	10	difexi	⊢ ( 𝐴 ∖ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ { 𝐷 } ) ) ∈ V
12	8 9 11	fvmpt	⊢ ( 𝐷 ∈ 𝐴 → ( ( 𝑑 ∈ 𝐴 ↦ ( 𝐴 ∖ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ { 𝑑 } ) ) ) ‘ 𝐷 ) = ( 𝐴 ∖ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ { 𝐷 } ) ) )
13	5 12	sylan9eq	⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝐷 ∈ 𝐴 ) → ( 𝑊 ‘ 𝐷 ) = ( 𝐴 ∖ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ { 𝐷 } ) ) )