Description: Preimage of a singleton. (Contributed by Mario Carneiro, 26-Jun-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | i1fima2sn | ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐴 ∈ ( 𝐵 ∖ { 0 } ) ) → ( vol ‘ ( ◡ 𝐹 “ { 𝐴 } ) ) ∈ ℝ ) |
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 ‘ ( ◡ 𝐹 “ { 𝐴 } ) ) ∈ ℝ ) |