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

Metamath Proof Explorer

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 ⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝐷 ∈ 𝐴 ) → ( 𝑊 ‘ 𝐷 ) = ( 𝐴 ∖ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ { 𝐷 } ) ) )