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 ‘ ( ◡ 𝐹 “ { 𝐴 } ) ) ∈ ℝ )