Theorem watfvalN

Description: 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	watfvalN	⊢ ( 𝐾 ∈ 𝐵 → 𝑊 = ( 𝑑 ∈ 𝐴 ↦ ( 𝐴 ∖ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ { 𝑑 } ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		watomfval.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
2		watomfval.p	⊢ 𝑃 = ( ⊥𝑃 ‘ 𝐾 )
3		watomfval.w	⊢ 𝑊 = ( WAtoms ‘ 𝐾 )
4		elex	⊢ ( 𝐾 ∈ 𝐵 → 𝐾 ∈ V )
5		fveq2	⊢ ( 𝑘 = 𝐾 → ( Atoms ‘ 𝑘 ) = ( Atoms ‘ 𝐾 ) )
6	5 1	eqtr4di	⊢ ( 𝑘 = 𝐾 → ( Atoms ‘ 𝑘 ) = 𝐴 )
7		fveq2	⊢ ( 𝑘 = 𝐾 → ( ⊥𝑃 ‘ 𝑘 ) = ( ⊥𝑃 ‘ 𝐾 ) )
8	7	fveq1d	⊢ ( 𝑘 = 𝐾 → ( ( ⊥𝑃 ‘ 𝑘 ) ‘ { 𝑑 } ) = ( ( ⊥𝑃 ‘ 𝐾 ) ‘ { 𝑑 } ) )
9	6 8	difeq12d	⊢ ( 𝑘 = 𝐾 → ( ( Atoms ‘ 𝑘 ) ∖ ( ( ⊥𝑃 ‘ 𝑘 ) ‘ { 𝑑 } ) ) = ( 𝐴 ∖ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ { 𝑑 } ) ) )
10	6 9	mpteq12dv	⊢ ( 𝑘 = 𝐾 → ( 𝑑 ∈ ( Atoms ‘ 𝑘 ) ↦ ( ( Atoms ‘ 𝑘 ) ∖ ( ( ⊥𝑃 ‘ 𝑘 ) ‘ { 𝑑 } ) ) ) = ( 𝑑 ∈ 𝐴 ↦ ( 𝐴 ∖ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ { 𝑑 } ) ) ) )
11		df-watsN	⊢ WAtoms = ( 𝑘 ∈ V ↦ ( 𝑑 ∈ ( Atoms ‘ 𝑘 ) ↦ ( ( Atoms ‘ 𝑘 ) ∖ ( ( ⊥𝑃 ‘ 𝑘 ) ‘ { 𝑑 } ) ) ) )
12	10 11 1	mptfvmpt	⊢ ( 𝐾 ∈ V → ( WAtoms ‘ 𝐾 ) = ( 𝑑 ∈ 𝐴 ↦ ( 𝐴 ∖ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ { 𝑑 } ) ) ) )
13	3 12	syl5eq	⊢ ( 𝐾 ∈ V → 𝑊 = ( 𝑑 ∈ 𝐴 ↦ ( 𝐴 ∖ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ { 𝑑 } ) ) ) )
14	4 13	syl	⊢ ( 𝐾 ∈ 𝐵 → 𝑊 = ( 𝑑 ∈ 𝐴 ↦ ( 𝐴 ∖ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ { 𝑑 } ) ) ) )