Metamath Proof Explorer


Theorem i1fima2sn

Description: Preimage of a singleton. (Contributed by Mario Carneiro, 26-Jun-2014)

Ref Expression
Assertion i1fima2sn ( ( 𝐹 ∈ dom ∫1𝐴 ∈ ( 𝐵 ∖ { 0 } ) ) → ( vol ‘ ( 𝐹 “ { 𝐴 } ) ) ∈ ℝ )

Proof

Step Hyp Ref Expression
1 eldifn ( 𝐴 ∈ ( 𝐵 ∖ { 0 } ) → ¬ 𝐴 ∈ { 0 } )
2 elsni ( 0 ∈ { 𝐴 } → 0 = 𝐴 )
3 snidg ( 0 ∈ { 𝐴 } → 0 ∈ { 0 } )
4 2 3 eqeltrrd ( 0 ∈ { 𝐴 } → 𝐴 ∈ { 0 } )
5 1 4 nsyl ( 𝐴 ∈ ( 𝐵 ∖ { 0 } ) → ¬ 0 ∈ { 𝐴 } )
6 i1fima2 ( ( 𝐹 ∈ dom ∫1 ∧ ¬ 0 ∈ { 𝐴 } ) → ( vol ‘ ( 𝐹 “ { 𝐴 } ) ) ∈ ℝ )
7 5 6 sylan2 ( ( 𝐹 ∈ dom ∫1𝐴 ∈ ( 𝐵 ∖ { 0 } ) ) → ( vol ‘ ( 𝐹 “ { 𝐴 } ) ) ∈ ℝ )