This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 eqtrid ⊢ ( 𝐾 ∈ V → 𝑊 = ( 𝑑 ∈ 𝐴 ↦ ( 𝐴 ∖ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ { 𝑑 } ) ) ) )
14 4 13 syl ⊢ ( 𝐾 ∈ 𝐵 → 𝑊 = ( 𝑑 ∈ 𝐴 ↦ ( 𝐴 ∖ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ { 𝑑 } ) ) ) )