Theorem iccioo01 35006

Description: The closed unit interval is equinumerous to the open unit interval. Based on a Mastodon post by Michael Kinyon. (Contributed by Jim Kingdon, 4-Jun-2024.)

Assertion

Ref	Expression
iccioo01	⊢ (0[,]1) ≈ (0(,)1)

Proof of Theorem iccioo01

Step	Hyp	Ref	Expression
1		4nn 11742	. . . . 5 ⊢ 4 ∈ ℕ
2		nnrecre 11701	. . . . 5 ⊢ (4 ∈ ℕ → (1 / 4) ∈ ℝ)
3	1, 2	ax-mp 5	. . . 4 ⊢ (1 / 4) ∈ ℝ
4		halfre 11873	. . . 4 ⊢ (1 / 2) ∈ ℝ
5		2lt4 11834	. . . . 5 ⊢ 2 < 4
6		2re 11733	. . . . . 6 ⊢ 2 ∈ ℝ
7		4re 11743	. . . . . 6 ⊢ 4 ∈ ℝ
8		2pos 11762	. . . . . 6 ⊢ 0 < 2
9		4pos 11766	. . . . . 6 ⊢ 0 < 4
10	6, 7, 8, 9	ltrecii 11579	. . . . 5 ⊢ (2 < 4 ↔ (1 / 4) < (1 / 2))
11	5, 10	mpbi 233	. . . 4 ⊢ (1 / 4) < (1 / 2)
12		iccen 12914	. . . 4 ⊢ (((1 / 4) ∈ ℝ ∧ (1 / 2) ∈ ℝ ∧ (1 / 4) < (1 / 2)) → (0[,]1) ≈ ((1 / 4)[,](1 / 2)))
13	3, 4, 11, 12	mp3an 1459	. . 3 ⊢ (0[,]1) ≈ ((1 / 4)[,](1 / 2))
14		ovex 7176	. . . 4 ⊢ (0(,)1) ∈ V
15		0xr 10711	. . . . 5 ⊢ 0 ∈ ℝ*
16		1xr 10723	. . . . 5 ⊢ 1 ∈ ℝ*
17	7, 9	recgt0ii 11569	. . . . 5 ⊢ 0 < (1 / 4)
18		halflt1 11877	. . . . 5 ⊢ (1 / 2) < 1
19		iccssioo 12833	. . . . 5 ⊢ (((0 ∈ ℝ* ∧ 1 ∈ ℝ*) ∧ (0 < (1 / 4) ∧ (1 / 2) < 1)) → ((1 / 4)[,](1 / 2)) ⊆ (0(,)1))
20	15, 16, 17, 18, 19	mp4an 693	. . . 4 ⊢ ((1 / 4)[,](1 / 2)) ⊆ (0(,)1)
21		ssdomg 8566	. . . 4 ⊢ ((0(,)1) ∈ V → (((1 / 4)[,](1 / 2)) ⊆ (0(,)1) → ((1 / 4)[,](1 / 2)) ≼ (0(,)1)))
22	14, 20, 21	mp2 9	. . 3 ⊢ ((1 / 4)[,](1 / 2)) ≼ (0(,)1)
23		endomtr 8578	. . 3 ⊢ (((0[,]1) ≈ ((1 / 4)[,](1 / 2)) ∧ ((1 / 4)[,](1 / 2)) ≼ (0(,)1)) → (0[,]1) ≼ (0(,)1))
24	13, 22, 23	mp2an 692	. 2 ⊢ (0[,]1) ≼ (0(,)1)
25		ovex 7176	. . 3 ⊢ (0[,]1) ∈ V
26		ioossicc 12850	. . 3 ⊢ (0(,)1) ⊆ (0[,]1)
27		ssdomg 8566	. . 3 ⊢ ((0[,]1) ∈ V → ((0(,)1) ⊆ (0[,]1) → (0(,)1) ≼ (0[,]1)))
28	25, 26, 27	mp2 9	. 2 ⊢ (0(,)1) ≼ (0[,]1)
29		sbth 8651	. 2 ⊢ (((0[,]1) ≼ (0(,)1) ∧ (0(,)1) ≼ (0[,]1)) → (0[,]1) ≈ (0(,)1))
30	24, 28, 29	mp2an 692	1 ⊢ (0[,]1) ≈ (0(,)1)

Syntax hints:   ∈ wcel 2112  Vcvv 3407   ⊆ wss 3854   class class class wbr 5025  (class class class)co 7143   ≈ cen 8517   ≼ cdom 8518  ℝcr 10559  0cc0 10560  1c1 10561  ℝ^*cxr 10697   < clt 10698   / cdiv 11320  ℕcn 11659  2c2 11714  4c4 11716  (,)cioo 12764  [,]cicc 12767

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-sep 5162  ax-nul 5169  ax-pow 5227  ax-pr 5291  ax-un 7452  ax-cnex 10616  ax-resscn 10617  ax-1cn 10618  ax-icn 10619  ax-addcl 10620  ax-addrcl 10621  ax-mulcl 10622  ax-mulrcl 10623  ax-mulcom 10624  ax-addass 10625  ax-mulass 10626  ax-distr 10627  ax-i2m1 10628  ax-1ne0 10629  ax-1rid 10630  ax-rnegex 10631  ax-rrecex 10632  ax-cnre 10633  ax-pre-lttri 10634  ax-pre-lttrn 10635  ax-pre-ltadd 10636  ax-pre-mulgt0 10637

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2899  df-ne 2950  df-nel 3054  df-ral 3073  df-rex 3074  df-reu 3075  df-rmo 3076  df-rab 3077  df-v 3409  df-sbc 3694  df-csb 3802  df-dif 3857  df-un 3859  df-in 3861  df-ss 3871  df-pss 3873  df-nul 4222  df-if 4414  df-pw 4489  df-sn 4516  df-pr 4518  df-tp 4520  df-op 4522  df-uni 4792  df-iun 4878  df-br 5026  df-opab 5088  df-mpt 5106  df-tr 5132  df-id 5423  df-eprel 5428  df-po 5436  df-so 5437  df-fr 5476  df-we 5478  df-xp 5523  df-rel 5524  df-cnv 5525  df-co 5526  df-dm 5527  df-rn 5528  df-res 5529  df-ima 5530  df-pred 6119  df-ord 6165  df-on 6166  df-lim 6167  df-suc 6168  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-riota 7101  df-ov 7146  df-oprab 7147  df-mpo 7148  df-om 7573  df-1st 7686  df-2nd 7687  df-wrecs 7950  df-recs 8011  df-rdg 8049  df-er 8292  df-en 8521  df-dom 8522  df-sdom 8523  df-pnf 10700  df-mnf 10701  df-xr 10702  df-ltxr 10703  df-le 10704  df-sub 10895  df-neg 10896  df-div 11321  df-nn 11660  df-2 11722  df-3 11723  df-4 11724  df-rp 12416  df-ioo 12768  df-icc 12771

This theorem is referenced by: (None)