opnreen

Description: Every nonempty open set is uncountable. (Contributed by Mario Carneiro, 26-Jul-2014) (Revised by Mario Carneiro, 20-Feb-2015)

		Ref	Expression
	Assertion	opnreen	$⊢ (A \in topGen (ran (.)) \land A \neq \emptyset) \to A \approx 𝒫 ℕ$

Proof

Step	Hyp	Ref	Expression
1		reex	$⊢ ℝ \in V$
2		elssuni	$⊢ A \in topGen (ran (.)) \to A \subseteq ⋃ topGen (ran (.))$
3		uniretop	$⊢ ℝ = ⋃ topGen (ran (.))$
4	2 3	sseqtrrdi	$⊢ A \in topGen (ran (.)) \to A \subseteq ℝ$
5		ssdomg	$⊢ ℝ \in V \to (A \subseteq ℝ \to A ≼ ℝ)$
6	1 4 5	mpsyl	$⊢ A \in topGen (ran (.)) \to A ≼ ℝ$
7		rpnnen	$⊢ ℝ \approx 𝒫 ℕ$
8		domentr	$⊢ (A ≼ ℝ \land ℝ \approx 𝒫 ℕ) \to A ≼ 𝒫 ℕ$
9	6 7 8	sylancl	$⊢ A \in topGen (ran (.)) \to A ≼ 𝒫 ℕ$
10		n0	$⊢ A \neq \emptyset \leftrightarrow \exists x x \in A$
11	4	sselda	$⊢ (A \in topGen (ran (.)) \land x \in A) \to x \in ℝ$
12		rpnnen2	$⊢ 𝒫 ℕ ≼ [0, 1]$
13		rphalfcl	$⊢ y \in ℝ^{+} \to \frac{y}{2} \in ℝ^{+}$
14	13	rpred	$⊢ y \in ℝ^{+} \to \frac{y}{2} \in ℝ$
15		resubcl	$⊢ (x \in ℝ \land \frac{y}{2} \in ℝ) \to x - (\frac{y}{2}) \in ℝ$
16	14 15	sylan2	$⊢ (x \in ℝ \land y \in ℝ^{+}) \to x - (\frac{y}{2}) \in ℝ$
17		readdcl	$⊢ (x \in ℝ \land \frac{y}{2} \in ℝ) \to x + (\frac{y}{2}) \in ℝ$
18	14 17	sylan2	$⊢ (x \in ℝ \land y \in ℝ^{+}) \to x + (\frac{y}{2}) \in ℝ$
19		simpl	$⊢ (x \in ℝ \land y \in ℝ^{+}) \to x \in ℝ$
20		ltsubrp	$⊢ (x \in ℝ \land \frac{y}{2} \in ℝ^{+}) \to x - (\frac{y}{2}) < x$
21	13 20	sylan2	$⊢ (x \in ℝ \land y \in ℝ^{+}) \to x - (\frac{y}{2}) < x$
22		ltaddrp	$⊢ (x \in ℝ \land \frac{y}{2} \in ℝ^{+}) \to x < x + (\frac{y}{2})$
23	13 22	sylan2	$⊢ (x \in ℝ \land y \in ℝ^{+}) \to x < x + (\frac{y}{2})$
24	16 19 18 21 23	lttrd	$⊢ (x \in ℝ \land y \in ℝ^{+}) \to x - (\frac{y}{2}) < x + (\frac{y}{2})$
25		iccen	$⊢ (x - (\frac{y}{2}) \in ℝ \land x + (\frac{y}{2}) \in ℝ \land x - (\frac{y}{2}) < x + (\frac{y}{2})) \to [0, 1] \approx [x - (\frac{y}{2}), x + (\frac{y}{2})]$
26	16 18 24 25	syl3anc	$⊢ (x \in ℝ \land y \in ℝ^{+}) \to [0, 1] \approx [x - (\frac{y}{2}), x + (\frac{y}{2})]$
27		domentr	$⊢ (𝒫 ℕ ≼ [0, 1] \land [0, 1] \approx [x - (\frac{y}{2}), x + (\frac{y}{2})]) \to 𝒫 ℕ ≼ [x - (\frac{y}{2}), x + (\frac{y}{2})]$
28	12 26 27	sylancr	$⊢ (x \in ℝ \land y \in ℝ^{+}) \to 𝒫 ℕ ≼ [x - (\frac{y}{2}), x + (\frac{y}{2})]$
29		ovex	$⊢ (x - y, x + y) \in V$
30		rpre	$⊢ y \in ℝ^{+} \to y \in ℝ$
31		resubcl	$⊢ (x \in ℝ \land y \in ℝ) \to x - y \in ℝ$
32	30 31	sylan2	$⊢ (x \in ℝ \land y \in ℝ^{+}) \to x - y \in ℝ$
33	32	rexrd	$⊢ (x \in ℝ \land y \in ℝ^{+}) \to x - y \in ℝ^{*}$
34		readdcl	$⊢ (x \in ℝ \land y \in ℝ) \to x + y \in ℝ$
35	30 34	sylan2	$⊢ (x \in ℝ \land y \in ℝ^{+}) \to x + y \in ℝ$
36	35	rexrd	$⊢ (x \in ℝ \land y \in ℝ^{+}) \to x + y \in ℝ^{*}$
37	19	recnd	$⊢ (x \in ℝ \land y \in ℝ^{+}) \to x \in ℂ$
38	14	adantl	$⊢ (x \in ℝ \land y \in ℝ^{+}) \to \frac{y}{2} \in ℝ$
39	38	recnd	$⊢ (x \in ℝ \land y \in ℝ^{+}) \to \frac{y}{2} \in ℂ$
40	37 39 39	subsub4d	$⊢ (x \in ℝ \land y \in ℝ^{+}) \to x - (\frac{y}{2}) - (\frac{y}{2}) = x - ((\frac{y}{2}) + (\frac{y}{2}))$
41	30	adantl	$⊢ (x \in ℝ \land y \in ℝ^{+}) \to y \in ℝ$
42	41	recnd	$⊢ (x \in ℝ \land y \in ℝ^{+}) \to y \in ℂ$
43	42	2halvesd	$⊢ (x \in ℝ \land y \in ℝ^{+}) \to (\frac{y}{2}) + (\frac{y}{2}) = y$
44	43	oveq2d	$⊢ (x \in ℝ \land y \in ℝ^{+}) \to x - ((\frac{y}{2}) + (\frac{y}{2})) = x - y$
45	40 44	eqtrd	$⊢ (x \in ℝ \land y \in ℝ^{+}) \to x - (\frac{y}{2}) - (\frac{y}{2}) = x - y$
46	13	adantl	$⊢ (x \in ℝ \land y \in ℝ^{+}) \to \frac{y}{2} \in ℝ^{+}$
47	16 46	ltsubrpd	$⊢ (x \in ℝ \land y \in ℝ^{+}) \to x - (\frac{y}{2}) - (\frac{y}{2}) < x - (\frac{y}{2})$
48	45 47	eqbrtrrd	$⊢ (x \in ℝ \land y \in ℝ^{+}) \to x - y < x - (\frac{y}{2})$
49	18 46	ltaddrpd	$⊢ (x \in ℝ \land y \in ℝ^{+}) \to x + (\frac{y}{2}) < x + (\frac{y}{2}) + (\frac{y}{2})$
50	37 39 39	addassd	$⊢ (x \in ℝ \land y \in ℝ^{+}) \to x + (\frac{y}{2}) + (\frac{y}{2}) = x + (\frac{y}{2}) + (\frac{y}{2})$
51	43	oveq2d	$⊢ (x \in ℝ \land y \in ℝ^{+}) \to x + (\frac{y}{2}) + (\frac{y}{2}) = x + y$
52	50 51	eqtrd	$⊢ (x \in ℝ \land y \in ℝ^{+}) \to x + (\frac{y}{2}) + (\frac{y}{2}) = x + y$
53	49 52	breqtrd	$⊢ (x \in ℝ \land y \in ℝ^{+}) \to x + (\frac{y}{2}) < x + y$
54		iccssioo	$⊢ ((x - y \in ℝ^{} \land x + y \in ℝ^{}) \land (x - y < x - (\frac{y}{2}) \land x + (\frac{y}{2}) < x + y)) \to [x - (\frac{y}{2}), x + (\frac{y}{2})] \subseteq (x - y, x + y)$
55	33 36 48 53 54	syl22anc	$⊢ (x \in ℝ \land y \in ℝ^{+}) \to [x - (\frac{y}{2}), x + (\frac{y}{2})] \subseteq (x - y, x + y)$
56		ssdomg	$⊢ (x - y, x + y) \in V \to ([x - (\frac{y}{2}), x + (\frac{y}{2})] \subseteq (x - y, x + y) \to [x - (\frac{y}{2}), x + (\frac{y}{2})] ≼ (x - y, x + y))$
57	29 55 56	mpsyl	$⊢ (x \in ℝ \land y \in ℝ^{+}) \to [x - (\frac{y}{2}), x + (\frac{y}{2})] ≼ (x - y, x + y)$
58		domtr	$⊢ (𝒫 ℕ ≼ [x - (\frac{y}{2}), x + (\frac{y}{2})] \land [x - (\frac{y}{2}), x + (\frac{y}{2})] ≼ (x - y, x + y)) \to 𝒫 ℕ ≼ (x - y, x + y)$
59	28 57 58	syl2anc	$⊢ (x \in ℝ \land y \in ℝ^{+}) \to 𝒫 ℕ ≼ (x - y, x + y)$
60		eqid	$⊢ {(abs \circ -) ↾}_{ℝ^{2}} = {(abs \circ -) ↾}_{ℝ^{2}}$
61	60	bl2ioo	$⊢ (x \in ℝ \land y \in ℝ) \to x ball ({(abs \circ -) ↾}_{ℝ^{2}}) y = (x - y, x + y)$
62	30 61	sylan2	$⊢ (x \in ℝ \land y \in ℝ^{+}) \to x ball ({(abs \circ -) ↾}_{ℝ^{2}}) y = (x - y, x + y)$
63	59 62	breqtrrd	$⊢ (x \in ℝ \land y \in ℝ^{+}) \to 𝒫 ℕ ≼ (x ball ({(abs \circ -) ↾}_{ℝ^{2}}) y)$
64	11 63	sylan	$⊢ ((A \in topGen (ran (.)) \land x \in A) \land y \in ℝ^{+}) \to 𝒫 ℕ ≼ (x ball ({(abs \circ -) ↾}_{ℝ^{2}}) y)$
65		simplll	$⊢ (((A \in topGen (ran (.)) \land x \in A) \land y \in ℝ^{+}) \land x ball ({(abs \circ -) ↾}_{ℝ^{2}}) y \subseteq A) \to A \in topGen (ran (.))$
66		simpr	$⊢ (((A \in topGen (ran (.)) \land x \in A) \land y \in ℝ^{+}) \land x ball ({(abs \circ -) ↾}_{ℝ^{2}}) y \subseteq A) \to x ball ({(abs \circ -) ↾}_{ℝ^{2}}) y \subseteq A$
67		ssdomg	$⊢ A \in topGen (ran (.)) \to (x ball ({(abs \circ -) ↾}_{ℝ^{2}}) y \subseteq A \to (x ball ({(abs \circ -) ↾}_{ℝ^{2}}) y) ≼ A)$
68	65 66 67	sylc	$⊢ (((A \in topGen (ran (.)) \land x \in A) \land y \in ℝ^{+}) \land x ball ({(abs \circ -) ↾}_{ℝ^{2}}) y \subseteq A) \to (x ball ({(abs \circ -) ↾}_{ℝ^{2}}) y) ≼ A$
69		domtr	$⊢ (𝒫 ℕ ≼ (x ball ({(abs \circ -) ↾}_{ℝ^{2}}) y) \land (x ball ({(abs \circ -) ↾}_{ℝ^{2}}) y) ≼ A) \to 𝒫 ℕ ≼ A$
70	64 68 69	syl2an2r	$⊢ (((A \in topGen (ran (.)) \land x \in A) \land y \in ℝ^{+}) \land x ball ({(abs \circ -) ↾}_{ℝ^{2}}) y \subseteq A) \to 𝒫 ℕ ≼ A$
71		eqid	$⊢ MetOpen ({(abs \circ -) ↾}_{ℝ^{2}}) = MetOpen ({(abs \circ -) ↾}_{ℝ^{2}})$
72	60 71	tgioo	$⊢ topGen (ran (.)) = MetOpen ({(abs \circ -) ↾}_{ℝ^{2}})$
73	72	eleq2i	$⊢ A \in topGen (ran (.)) \leftrightarrow A \in MetOpen ({(abs \circ -) ↾}_{ℝ^{2}})$
74	60	rexmet	$⊢ {(abs \circ -) ↾}_{ℝ^{2}} \in ∞Met (ℝ)$
75	71	mopni2	$⊢ ({(abs \circ -) ↾}_{ℝ^{2}} \in ∞Met (ℝ) \land A \in MetOpen ({(abs \circ -) ↾}_{ℝ^{2}}) \land x \in A) \to \exists y \in ℝ^{+} x ball ({(abs \circ -) ↾}_{ℝ^{2}}) y \subseteq A$
76	74 75	mp3an1	$⊢ (A \in MetOpen ({(abs \circ -) ↾}_{ℝ^{2}}) \land x \in A) \to \exists y \in ℝ^{+} x ball ({(abs \circ -) ↾}_{ℝ^{2}}) y \subseteq A$
77	73 76	sylanb	$⊢ (A \in topGen (ran (.)) \land x \in A) \to \exists y \in ℝ^{+} x ball ({(abs \circ -) ↾}_{ℝ^{2}}) y \subseteq A$
78	70 77	r19.29a	$⊢ (A \in topGen (ran (.)) \land x \in A) \to 𝒫 ℕ ≼ A$
79	78	ex	$⊢ A \in topGen (ran (.)) \to (x \in A \to 𝒫 ℕ ≼ A)$
80	79	exlimdv	$⊢ A \in topGen (ran (.)) \to (\exists x x \in A \to 𝒫 ℕ ≼ A)$
81	10 80	syl5bi	$⊢ A \in topGen (ran (.)) \to (A \neq \emptyset \to 𝒫 ℕ ≼ A)$
82	81	imp	$⊢ (A \in topGen (ran (.)) \land A \neq \emptyset) \to 𝒫 ℕ ≼ A$
83		sbth	$⊢ (A ≼ 𝒫 ℕ \land 𝒫 ℕ ≼ A) \to A \approx 𝒫 ℕ$
84	9 82 83	syl2an2r	$⊢ (A \in topGen (ran (.)) \land A \neq \emptyset) \to A \approx 𝒫 ℕ$

Metamath Proof Explorer

Theorem opnreen

Proof