Theorem icoreunrn

Description: The union of all closed-below, open-above intervals of reals is the set of reals. (Contributed by ML, 27-Jul-2020)

	Ref	Expression
Hypothesis	icoreunrn.1	⊢ 𝐼 = ( [,) “ ( ℝ × ℝ ) )
Assertion	icoreunrn	⊢ ℝ = ∪ 𝐼

Proof

Step	Hyp	Ref	Expression
1		icoreunrn.1	⊢ 𝐼 = ( [,) “ ( ℝ × ℝ ) )
2		rexr	⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℝ* )
3		peano2re	⊢ ( 𝑥 ∈ ℝ → ( 𝑥 + 1 ) ∈ ℝ )
4		rexr	⊢ ( ( 𝑥 + 1 ) ∈ ℝ → ( 𝑥 + 1 ) ∈ ℝ* )
5	3 4	syl	⊢ ( 𝑥 ∈ ℝ → ( 𝑥 + 1 ) ∈ ℝ* )
6		ltp1	⊢ ( 𝑥 ∈ ℝ → 𝑥 < ( 𝑥 + 1 ) )
7		lbico1	⊢ ( ( 𝑥 ∈ ℝ* ∧ ( 𝑥 + 1 ) ∈ ℝ* ∧ 𝑥 < ( 𝑥 + 1 ) ) → 𝑥 ∈ ( 𝑥 [,) ( 𝑥 + 1 ) ) )
8	2 5 6 7	syl3anc	⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ( 𝑥 [,) ( 𝑥 + 1 ) ) )
9		df-ov	⊢ ( 𝑥 [,) ( 𝑥 + 1 ) ) = ( [,) ‘ ⟨ 𝑥 , ( 𝑥 + 1 ) ⟩ )
10	8 9	eleqtrdi	⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ( [,) ‘ ⟨ 𝑥 , ( 𝑥 + 1 ) ⟩ ) )
11		opelxpi	⊢ ( ( 𝑥 ∈ ℝ ∧ ( 𝑥 + 1 ) ∈ ℝ ) → ⟨ 𝑥 , ( 𝑥 + 1 ) ⟩ ∈ ( ℝ × ℝ ) )
12	3 11	mpdan	⊢ ( 𝑥 ∈ ℝ → ⟨ 𝑥 , ( 𝑥 + 1 ) ⟩ ∈ ( ℝ × ℝ ) )
13		fvres	⊢ ( ⟨ 𝑥 , ( 𝑥 + 1 ) ⟩ ∈ ( ℝ × ℝ ) → ( ( [,) ↾ ( ℝ × ℝ ) ) ‘ ⟨ 𝑥 , ( 𝑥 + 1 ) ⟩ ) = ( [,) ‘ ⟨ 𝑥 , ( 𝑥 + 1 ) ⟩ ) )
14	12 13	syl	⊢ ( 𝑥 ∈ ℝ → ( ( [,) ↾ ( ℝ × ℝ ) ) ‘ ⟨ 𝑥 , ( 𝑥 + 1 ) ⟩ ) = ( [,) ‘ ⟨ 𝑥 , ( 𝑥 + 1 ) ⟩ ) )
15	10 14	eleqtrrd	⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ( ( [,) ↾ ( ℝ × ℝ ) ) ‘ ⟨ 𝑥 , ( 𝑥 + 1 ) ⟩ ) )
16		icoreresf	⊢ ( [,) ↾ ( ℝ × ℝ ) ) : ( ℝ × ℝ ) ⟶ 𝒫 ℝ
17	16	fdmi	⊢ dom ( [,) ↾ ( ℝ × ℝ ) ) = ( ℝ × ℝ )
18	11 17	eleqtrrdi	⊢ ( ( 𝑥 ∈ ℝ ∧ ( 𝑥 + 1 ) ∈ ℝ ) → ⟨ 𝑥 , ( 𝑥 + 1 ) ⟩ ∈ dom ( [,) ↾ ( ℝ × ℝ ) ) )
19	3 18	mpdan	⊢ ( 𝑥 ∈ ℝ → ⟨ 𝑥 , ( 𝑥 + 1 ) ⟩ ∈ dom ( [,) ↾ ( ℝ × ℝ ) ) )
20		ffun	⊢ ( ( [,) ↾ ( ℝ × ℝ ) ) : ( ℝ × ℝ ) ⟶ 𝒫 ℝ → Fun ( [,) ↾ ( ℝ × ℝ ) ) )
21	16 20	ax-mp	⊢ Fun ( [,) ↾ ( ℝ × ℝ ) )
22		fvelrn	⊢ ( ( Fun ( [,) ↾ ( ℝ × ℝ ) ) ∧ ⟨ 𝑥 , ( 𝑥 + 1 ) ⟩ ∈ dom ( [,) ↾ ( ℝ × ℝ ) ) ) → ( ( [,) ↾ ( ℝ × ℝ ) ) ‘ ⟨ 𝑥 , ( 𝑥 + 1 ) ⟩ ) ∈ ran ( [,) ↾ ( ℝ × ℝ ) ) )
23	21 22	mpan	⊢ ( ⟨ 𝑥 , ( 𝑥 + 1 ) ⟩ ∈ dom ( [,) ↾ ( ℝ × ℝ ) ) → ( ( [,) ↾ ( ℝ × ℝ ) ) ‘ ⟨ 𝑥 , ( 𝑥 + 1 ) ⟩ ) ∈ ran ( [,) ↾ ( ℝ × ℝ ) ) )
24		df-ima	⊢ ( [,) “ ( ℝ × ℝ ) ) = ran ( [,) ↾ ( ℝ × ℝ ) )
25	1 24	eqtri	⊢ 𝐼 = ran ( [,) ↾ ( ℝ × ℝ ) )
26	23 25	eleqtrrdi	⊢ ( ⟨ 𝑥 , ( 𝑥 + 1 ) ⟩ ∈ dom ( [,) ↾ ( ℝ × ℝ ) ) → ( ( [,) ↾ ( ℝ × ℝ ) ) ‘ ⟨ 𝑥 , ( 𝑥 + 1 ) ⟩ ) ∈ 𝐼 )
27	19 26	syl	⊢ ( 𝑥 ∈ ℝ → ( ( [,) ↾ ( ℝ × ℝ ) ) ‘ ⟨ 𝑥 , ( 𝑥 + 1 ) ⟩ ) ∈ 𝐼 )
28		elunii	⊢ ( ( 𝑥 ∈ ( ( [,) ↾ ( ℝ × ℝ ) ) ‘ ⟨ 𝑥 , ( 𝑥 + 1 ) ⟩ ) ∧ ( ( [,) ↾ ( ℝ × ℝ ) ) ‘ ⟨ 𝑥 , ( 𝑥 + 1 ) ⟩ ) ∈ 𝐼 ) → 𝑥 ∈ ∪ 𝐼 )
29	15 27 28	syl2anc	⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ∪ 𝐼 )
30	29	ssriv	⊢ ℝ ⊆ ∪ 𝐼
31		frn	⊢ ( ( [,) ↾ ( ℝ × ℝ ) ) : ( ℝ × ℝ ) ⟶ 𝒫 ℝ → ran ( [,) ↾ ( ℝ × ℝ ) ) ⊆ 𝒫 ℝ )
32	16 31	ax-mp	⊢ ran ( [,) ↾ ( ℝ × ℝ ) ) ⊆ 𝒫 ℝ
33	25 32	eqsstri	⊢ 𝐼 ⊆ 𝒫 ℝ
34		uniss	⊢ ( 𝐼 ⊆ 𝒫 ℝ → ∪ 𝐼 ⊆ ∪ 𝒫 ℝ )
35		unipw	⊢ ∪ 𝒫 ℝ = ℝ
36	34 35	sseqtrdi	⊢ ( 𝐼 ⊆ 𝒫 ℝ → ∪ 𝐼 ⊆ ℝ )
37	33 36	ax-mp	⊢ ∪ 𝐼 ⊆ ℝ
38	30 37	eqssi	⊢ ℝ = ∪ 𝐼