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