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

Metamath Proof Explorer

Theorem i1f0

Description: The zero function is simple. (Contributed by Mario Carneiro, 18-Jun-2014)

Ref Expression
Assertion i1f0 ( ℝ × { 0 } ) ∈ dom ∫1

Proof

Step Hyp Ref Expression
1 0re ⊢ 0 ∈ ℝ
2 1 fconst6 ⊢ ( ℝ × { 0 } ) : ℝ ⟶ ℝ
3 2 a1i ⊢ ( ⊤ → ( ℝ × { 0 } ) : ℝ ⟶ ℝ )
4 snfi ⊢ { 0 } ∈ Fin
5 rnxpss ⊢ ran ( ℝ × { 0 } ) ⊆ { 0 }
6 ssfi ⊢ ( ( { 0 } ∈ Fin ∧ ran ( ℝ × { 0 } ) ⊆ { 0 } ) → ran ( ℝ × { 0 } ) ∈ Fin )
7 4 5 6 mp2an ⊢ ran ( ℝ × { 0 } ) ∈ Fin
8 7 a1i ⊢ ( ⊤ → ran ( ℝ × { 0 } ) ∈ Fin )
9 difss ⊢ ( ran ( ℝ × { 0 } ) ∖ { 0 } ) ⊆ ran ( ℝ × { 0 } )
10 9 5 sstri ⊢ ( ran ( ℝ × { 0 } ) ∖ { 0 } ) ⊆ { 0 }
11 10 sseli ⊢ ( 𝑥 ∈ ( ran ( ℝ × { 0 } ) ∖ { 0 } ) → 𝑥 ∈ { 0 } )
12 11 adantl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( ran ( ℝ × { 0 } ) ∖ { 0 } ) ) → 𝑥 ∈ { 0 } )
13 eldifn ⊢ ( 𝑥 ∈ ( ran ( ℝ × { 0 } ) ∖ { 0 } ) → ¬ 𝑥 ∈ { 0 } )
14 13 adantl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( ran ( ℝ × { 0 } ) ∖ { 0 } ) ) → ¬ 𝑥 ∈ { 0 } )
15 12 14 pm2.21dd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( ran ( ℝ × { 0 } ) ∖ { 0 } ) ) → ( ◡ ( ℝ × { 0 } ) “ { 𝑥 } ) ∈ dom vol )
16 12 14 pm2.21dd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( ran ( ℝ × { 0 } ) ∖ { 0 } ) ) → ( vol ‘ ( ◡ ( ℝ × { 0 } ) “ { 𝑥 } ) ) ∈ ℝ )
17 3 8 15 16 i1fd ⊢ ( ⊤ → ( ℝ × { 0 } ) ∈ dom ∫1 )
18 17 mptru ⊢ ( ℝ × { 0 } ) ∈ dom ∫1