mblfinlem1

Description: Lemma for ismblfin , ordering the sets of dyadic intervals that are antichains under subset and whose unions are contained entirely in A . (Contributed by Brendan Leahy, 13-Jul-2018)

		Ref	Expression
	Assertion	mblfinlem1	$⊢ (A \in topGen (ran (.)) \land A \neq \emptyset) \to \exists f f : ℕ \underset{1-1 onto}{⟶} \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}$

Proof

Step	Hyp	Ref	Expression
1		peano2re	$⊢ n \in ℝ \to n + 1 \in ℝ$
2		ltp1	$⊢ n \in ℝ \to n < n + 1$
3		breq2	$⊢ z = n + 1 \to (n < z \leftrightarrow n < n + 1)$
4	3	rspcev	$⊢ (n + 1 \in ℝ \land n < n + 1) \to \exists z \in ℝ n < z$
5	1 2 4	syl2anc	$⊢ n \in ℝ \to \exists z \in ℝ n < z$
6	5	rgen	$⊢ \forall n \in ℝ \exists z \in ℝ n < z$
7		ltnle	$⊢ (n \in ℝ \land z \in ℝ) \to (n < z \leftrightarrow \neg z \leq n)$
8	7	rexbidva	$⊢ n \in ℝ \to (\exists z \in ℝ n < z \leftrightarrow \exists z \in ℝ \neg z \leq n)$
9		rexnal	$⊢ \exists z \in ℝ \neg z \leq n \leftrightarrow \neg \forall z \in ℝ z \leq n$
10	8 9	bitrdi	$⊢ n \in ℝ \to (\exists z \in ℝ n < z \leftrightarrow \neg \forall z \in ℝ z \leq n)$
11	10	ralbiia	$⊢ \forall n \in ℝ \exists z \in ℝ n < z \leftrightarrow \forall n \in ℝ \neg \forall z \in ℝ z \leq n$
12		ralnex	$⊢ \forall n \in ℝ \neg \forall z \in ℝ z \leq n \leftrightarrow \neg \exists n \in ℝ \forall z \in ℝ z \leq n$
13	11 12	bitri	$⊢ \forall n \in ℝ \exists z \in ℝ n < z \leftrightarrow \neg \exists n \in ℝ \forall z \in ℝ z \leq n$
14	6 13	mpbi	$⊢ \neg \exists n \in ℝ \forall z \in ℝ z \leq n$
15		raleq	$⊢ A = ℝ \to (\forall z \in A z \leq n \leftrightarrow \forall z \in ℝ z \leq n)$
16	15	rexbidv	$⊢ A = ℝ \to (\exists n \in ℝ \forall z \in A z \leq n \leftrightarrow \exists n \in ℝ \forall z \in ℝ z \leq n)$
17	14 16	mtbiri	$⊢ A = ℝ \to \neg \exists n \in ℝ \forall z \in A z \leq n$
18		ssrab2	$⊢ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \subseteq \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\}$
19		ssrab2	$⊢ \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \subseteq ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩)$
20		zre	$⊢ x \in ℤ \to x \in ℝ$
21		2re	$⊢ 2 \in ℝ$
22		reexpcl	$⊢ (2 \in ℝ \land y \in ℕ_{0}) \to 2^{y} \in ℝ$
23	21 22	mpan	$⊢ y \in ℕ_{0} \to 2^{y} \in ℝ$
24		nn0z	$⊢ y \in ℕ_{0} \to y \in ℤ$
25		2cn	$⊢ 2 \in ℂ$
26		2ne0	$⊢ 2 \neq 0$
27		expne0i	$⊢ (2 \in ℂ \land 2 \neq 0 \land y \in ℤ) \to 2^{y} \neq 0$
28	25 26 27	mp3an12	$⊢ y \in ℤ \to 2^{y} \neq 0$
29	24 28	syl	$⊢ y \in ℕ_{0} \to 2^{y} \neq 0$
30	23 29	jca	$⊢ y \in ℕ_{0} \to (2^{y} \in ℝ \land 2^{y} \neq 0)$
31		redivcl	$⊢ (x \in ℝ \land 2^{y} \in ℝ \land 2^{y} \neq 0) \to \frac{x}{2^{y}} \in ℝ$
32		peano2re	$⊢ x \in ℝ \to x + 1 \in ℝ$
33		redivcl	$⊢ (x + 1 \in ℝ \land 2^{y} \in ℝ \land 2^{y} \neq 0) \to \frac{x + 1}{2^{y}} \in ℝ$
34	32 33	syl3an1	$⊢ (x \in ℝ \land 2^{y} \in ℝ \land 2^{y} \neq 0) \to \frac{x + 1}{2^{y}} \in ℝ$
35		opelxpi	$⊢ (\frac{x}{2^{y}} \in ℝ \land \frac{x + 1}{2^{y}} \in ℝ) \to ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩ \in ℝ^{2}$
36	31 34 35	syl2anc	$⊢ (x \in ℝ \land 2^{y} \in ℝ \land 2^{y} \neq 0) \to ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩ \in ℝ^{2}$
37	36	3expb	$⊢ (x \in ℝ \land (2^{y} \in ℝ \land 2^{y} \neq 0)) \to ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩ \in ℝ^{2}$
38	20 30 37	syl2an	$⊢ (x \in ℤ \land y \in ℕ_{0}) \to ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩ \in ℝ^{2}$
39	38	rgen2	$⊢ \forall x \in ℤ \forall y \in ℕ_{0} ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩ \in ℝ^{2}$
40		eqid	$⊢ (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) = (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩)$
41	40	fmpo	$⊢ \forall x \in ℤ \forall y \in ℕ_{0} ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩ \in ℝ^{2} \leftrightarrow (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) : ℤ \times ℕ_{0} ⟶ ℝ^{2}$
42	39 41	mpbi	$⊢ (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) : ℤ \times ℕ_{0} ⟶ ℝ^{2}$
43		frn	$⊢ (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) : ℤ \times ℕ_{0} ⟶ ℝ^{2} \to ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \subseteq ℝ^{2}$
44	42 43	ax-mp	$⊢ ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \subseteq ℝ^{2}$
45	19 44	sstri	$⊢ \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \subseteq ℝ^{2}$
46	18 45	sstri	$⊢ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \subseteq ℝ^{2}$
47		rnss	$⊢ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \subseteq ℝ^{2} \to ran \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \subseteq ran ℝ^{2}$
48		rnxpid	$⊢ ran ℝ^{2} = ℝ$
49	47 48	sseqtrdi	$⊢ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \subseteq ℝ^{2} \to ran \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \subseteq ℝ$
50	46 49	ax-mp	$⊢ ran \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \subseteq ℝ$
51		rnfi	$⊢ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \in Fin \to ran \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \in Fin$
52		fimaxre2	$⊢ (ran \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \subseteq ℝ \land ran \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \in Fin) \to \exists n \in ℝ \forall u \in ran \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} u \leq n$
53	50 51 52	sylancr	$⊢ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \in Fin \to \exists n \in ℝ \forall u \in ran \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} u \leq n$
54	53	adantl	$⊢ (⋃ [.] [\{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}] = A \land \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \in Fin) \to \exists n \in ℝ \forall u \in ran \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} u \leq n$
55		eluni2	$⊢ z \in ⋃ [.] [\{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}] \leftrightarrow \exists u \in [.] [\{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}] z \in u$
56		iccf	$⊢ [.] : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ^{*}$
57		ffn	$⊢ [.] : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ^{} \to [.] Fn (ℝ^{} \times ℝ^{*})$
58	56 57	ax-mp	$⊢ [.] Fn (ℝ^{} \times ℝ^{})$
59		rexpssxrxp	$⊢ ℝ^{2} \subseteq ℝ^{} \times ℝ^{}$
60	46 59	sstri	$⊢ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \subseteq ℝ^{} \times ℝ^{}$
61		eleq2	$⊢ u = [.] (v) \to (z \in u \leftrightarrow z \in [.] (v))$
62	61	rexima	$⊢ ([.] Fn (ℝ^{} \times ℝ^{}) \land \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \subseteq ℝ^{} \times ℝ^{}) \to (\exists u \in [.] [\{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}] z \in u \leftrightarrow \exists v \in \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} z \in [.] (v))$
63	58 60 62	mp2an	$⊢ \exists u \in [.] [\{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}] z \in u \leftrightarrow \exists v \in \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} z \in [.] (v)$
64	55 63	bitri	$⊢ z \in ⋃ [.] [\{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}] \leftrightarrow \exists v \in \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} z \in [.] (v)$
65	46	sseli	$⊢ v \in \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \to v \in ℝ^{2}$
66		1st2nd2	$⊢ v \in ℝ^{2} \to v = ⟨1^{st} (v), 2^{nd} (v)⟩$
67	66	fveq2d	$⊢ v \in ℝ^{2} \to [.] (v) = [.] (⟨1^{st} (v), 2^{nd} (v)⟩)$
68		df-ov	$⊢ [1^{st} (v), 2^{nd} (v)] = [.] (⟨1^{st} (v), 2^{nd} (v)⟩)$
69	67 68	eqtr4di	$⊢ v \in ℝ^{2} \to [.] (v) = [1^{st} (v), 2^{nd} (v)]$
70	69	eleq2d	$⊢ v \in ℝ^{2} \to (z \in [.] (v) \leftrightarrow z \in [1^{st} (v), 2^{nd} (v)])$
71	65 70	syl	$⊢ v \in \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \to (z \in [.] (v) \leftrightarrow z \in [1^{st} (v), 2^{nd} (v)])$
72	71	biimpd	$⊢ v \in \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \to (z \in [.] (v) \to z \in [1^{st} (v), 2^{nd} (v)])$
73	72	imdistani	$⊢ (v \in \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land z \in [.] (v)) \to (v \in \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land z \in [1^{st} (v), 2^{nd} (v)])$
74		eliccxr	$⊢ z \in [1^{st} (v), 2^{nd} (v)] \to z \in ℝ^{*}$
75	74	ad2antll	$⊢ (((⋃ [.] [\{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}] = A \land n \in ℝ) \land \forall u \in ran \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} u \leq n) \land (v \in \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land z \in [1^{st} (v), 2^{nd} (v)])) \to z \in ℝ^{*}$
76		xp2nd	$⊢ v \in ℝ^{2} \to 2^{nd} (v) \in ℝ$
77	76	rexrd	$⊢ v \in ℝ^{2} \to 2^{nd} (v) \in ℝ^{*}$
78	65 77	syl	$⊢ v \in \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \to 2^{nd} (v) \in ℝ^{*}$
79	78	ad2antrl	$⊢ (((⋃ [.] [\{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}] = A \land n \in ℝ) \land \forall u \in ran \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} u \leq n) \land (v \in \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land z \in [1^{st} (v), 2^{nd} (v)])) \to 2^{nd} (v) \in ℝ^{*}$
80		simpllr	$⊢ (((⋃ [.] [\{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}] = A \land n \in ℝ) \land \forall u \in ran \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} u \leq n) \land (v \in \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land z \in [1^{st} (v), 2^{nd} (v)])) \to n \in ℝ$
81	80	rexrd	$⊢ (((⋃ [.] [\{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}] = A \land n \in ℝ) \land \forall u \in ran \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} u \leq n) \land (v \in \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land z \in [1^{st} (v), 2^{nd} (v)])) \to n \in ℝ^{*}$
82		xp1st	$⊢ v \in ℝ^{2} \to 1^{st} (v) \in ℝ$
83	82	rexrd	$⊢ v \in ℝ^{2} \to 1^{st} (v) \in ℝ^{*}$
84	83 77	jca	$⊢ v \in ℝ^{2} \to (1^{st} (v) \in ℝ^{} \land 2^{nd} (v) \in ℝ^{})$
85	65 84	syl	$⊢ v \in \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \to (1^{st} (v) \in ℝ^{} \land 2^{nd} (v) \in ℝ^{})$
86		iccleub	$⊢ (1^{st} (v) \in ℝ^{} \land 2^{nd} (v) \in ℝ^{} \land z \in [1^{st} (v), 2^{nd} (v)]) \to z \leq 2^{nd} (v)$
87	86	3expa	$⊢ ((1^{st} (v) \in ℝ^{} \land 2^{nd} (v) \in ℝ^{}) \land z \in [1^{st} (v), 2^{nd} (v)]) \to z \leq 2^{nd} (v)$
88	85 87	sylan	$⊢ (v \in \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land z \in [1^{st} (v), 2^{nd} (v)]) \to z \leq 2^{nd} (v)$
89	88	adantl	$⊢ (((⋃ [.] [\{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}] = A \land n \in ℝ) \land \forall u \in ran \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} u \leq n) \land (v \in \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land z \in [1^{st} (v), 2^{nd} (v)])) \to z \leq 2^{nd} (v)$
90		xpss	$⊢ ℝ^{2} \subseteq V \times V$
91	46 90	sstri	$⊢ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \subseteq V \times V$
92		df-rel	$⊢ Rel \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \leftrightarrow \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \subseteq V \times V$
93	91 92	mpbir	$⊢ Rel \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}$
94		2ndrn	$⊢ (Rel \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land v \in \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}) \to 2^{nd} (v) \in ran \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}$
95	93 94	mpan	$⊢ v \in \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \to 2^{nd} (v) \in ran \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}$
96		breq1	$⊢ u = 2^{nd} (v) \to (u \leq n \leftrightarrow 2^{nd} (v) \leq n)$
97	96	rspccva	$⊢ (\forall u \in ran \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} u \leq n \land 2^{nd} (v) \in ran \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}) \to 2^{nd} (v) \leq n$
98	95 97	sylan2	$⊢ (\forall u \in ran \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} u \leq n \land v \in \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}) \to 2^{nd} (v) \leq n$
99	98	ad2ant2lr	$⊢ (((⋃ [.] [\{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}] = A \land n \in ℝ) \land \forall u \in ran \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} u \leq n) \land (v \in \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land z \in [1^{st} (v), 2^{nd} (v)])) \to 2^{nd} (v) \leq n$
100	75 79 81 89 99	xrletrd	$⊢ (((⋃ [.] [\{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}] = A \land n \in ℝ) \land \forall u \in ran \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} u \leq n) \land (v \in \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land z \in [1^{st} (v), 2^{nd} (v)])) \to z \leq n$
101	73 100	sylan2	$⊢ (((⋃ [.] [\{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}] = A \land n \in ℝ) \land \forall u \in ran \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} u \leq n) \land (v \in \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land z \in [.] (v))) \to z \leq n$
102	101	rexlimdvaa	$⊢ ((⋃ [.] [\{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}] = A \land n \in ℝ) \land \forall u \in ran \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} u \leq n) \to (\exists v \in \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} z \in [.] (v) \to z \leq n)$
103	64 102	syl5bi	$⊢ ((⋃ [.] [\{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}] = A \land n \in ℝ) \land \forall u \in ran \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} u \leq n) \to (z \in ⋃ [.] [\{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}] \to z \leq n)$
104	103	ralrimiv	$⊢ ((⋃ [.] [\{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}] = A \land n \in ℝ) \land \forall u \in ran \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} u \leq n) \to \forall z \in ⋃ [.] [\{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}] z \leq n$
105		raleq	$⊢ ⋃ [.] [\{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}] = A \to (\forall z \in ⋃ [.] [\{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}] z \leq n \leftrightarrow \forall z \in A z \leq n)$
106	105	ad2antrr	$⊢ ((⋃ [.] [\{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}] = A \land n \in ℝ) \land \forall u \in ran \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} u \leq n) \to (\forall z \in ⋃ [.] [\{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}] z \leq n \leftrightarrow \forall z \in A z \leq n)$
107	104 106	mpbid	$⊢ ((⋃ [.] [\{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}] = A \land n \in ℝ) \land \forall u \in ran \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} u \leq n) \to \forall z \in A z \leq n$
108	107	ex	$⊢ (⋃ [.] [\{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}] = A \land n \in ℝ) \to (\forall u \in ran \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} u \leq n \to \forall z \in A z \leq n)$
109	108	reximdva	$⊢ ⋃ [.] [\{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}] = A \to (\exists n \in ℝ \forall u \in ran \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} u \leq n \to \exists n \in ℝ \forall z \in A z \leq n)$
110	109	adantr	$⊢ (⋃ [.] [\{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}] = A \land \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \in Fin) \to (\exists n \in ℝ \forall u \in ran \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} u \leq n \to \exists n \in ℝ \forall z \in A z \leq n)$
111	54 110	mpd	$⊢ (⋃ [.] [\{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}] = A \land \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \in Fin) \to \exists n \in ℝ \forall z \in A z \leq n$
112	17 111	nsyl	$⊢ A = ℝ \to \neg (⋃ [.] [\{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}] = A \land \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \in Fin)$
113	112	adantl	$⊢ ((A \in topGen (ran (.)) \land A \neq \emptyset) \land A = ℝ) \to \neg (⋃ [.] [\{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}] = A \land \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \in Fin)$
114		uniretop	$⊢ ℝ = ⋃ topGen (ran (.))$
115		retopconn	$⊢ topGen (ran (.)) \in Conn$
116	115	a1i	$⊢ ((A \in topGen (ran (.)) \land A \neq \emptyset) \land (⋃ [.] [\{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}] = A \land \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \in Fin)) \to topGen (ran (.)) \in Conn$
117		simpll	$⊢ ((A \in topGen (ran (.)) \land A \neq \emptyset) \land (⋃ [.] [\{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}] = A \land \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \in Fin)) \to A \in topGen (ran (.))$
118		simplr	$⊢ ((A \in topGen (ran (.)) \land A \neq \emptyset) \land (⋃ [.] [\{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}] = A \land \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \in Fin)) \to A \neq \emptyset$
119		simprl	$⊢ ((A \in topGen (ran (.)) \land A \neq \emptyset) \land (⋃ [.] [\{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}] = A \land \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \in Fin)) \to ⋃ [.] [\{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}] = A$
120		ffun	$⊢ [.] : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ^{*} \to Fun [.]$
121		funiunfv	$⊢ Fun [.] \to ⋃_{z \in \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}} [.] (z) = ⋃ [.] [\{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}]$
122	56 120 121	mp2b	$⊢ ⋃_{z \in \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}} [.] (z) = ⋃ [.] [\{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}]$
123		retop	$⊢ topGen (ran (.)) \in Top$
124	46	sseli	$⊢ z \in \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \to z \in ℝ^{2}$
125		1st2nd2	$⊢ z \in ℝ^{2} \to z = ⟨1^{st} (z), 2^{nd} (z)⟩$
126	125	fveq2d	$⊢ z \in ℝ^{2} \to [.] (z) = [.] (⟨1^{st} (z), 2^{nd} (z)⟩)$
127		df-ov	$⊢ [1^{st} (z), 2^{nd} (z)] = [.] (⟨1^{st} (z), 2^{nd} (z)⟩)$
128	126 127	eqtr4di	$⊢ z \in ℝ^{2} \to [.] (z) = [1^{st} (z), 2^{nd} (z)]$
129		xp1st	$⊢ z \in ℝ^{2} \to 1^{st} (z) \in ℝ$
130		xp2nd	$⊢ z \in ℝ^{2} \to 2^{nd} (z) \in ℝ$
131		icccld	$⊢ (1^{st} (z) \in ℝ \land 2^{nd} (z) \in ℝ) \to [1^{st} (z), 2^{nd} (z)] \in Clsd (topGen (ran (.)))$
132	129 130 131	syl2anc	$⊢ z \in ℝ^{2} \to [1^{st} (z), 2^{nd} (z)] \in Clsd (topGen (ran (.)))$
133	128 132	eqeltrd	$⊢ z \in ℝ^{2} \to [.] (z) \in Clsd (topGen (ran (.)))$
134	124 133	syl	$⊢ z \in \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \to [.] (z) \in Clsd (topGen (ran (.)))$
135	134	rgen	$⊢ \forall z \in \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} [.] (z) \in Clsd (topGen (ran (.)))$
136	114	iuncld	$⊢ (topGen (ran (.)) \in Top \land \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \in Fin \land \forall z \in \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} [.] (z) \in Clsd (topGen (ran (.)))) \to ⋃_{z \in \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}} [.] (z) \in Clsd (topGen (ran (.)))$
137	123 135 136	mp3an13	$⊢ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \in Fin \to ⋃_{z \in \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}} [.] (z) \in Clsd (topGen (ran (.)))$
138	122 137	eqeltrrid	$⊢ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \in Fin \to ⋃ [.] [\{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}] \in Clsd (topGen (ran (.)))$
139	138	ad2antll	$⊢ ((A \in topGen (ran (.)) \land A \neq \emptyset) \land (⋃ [.] [\{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}] = A \land \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \in Fin)) \to ⋃ [.] [\{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}] \in Clsd (topGen (ran (.)))$
140	119 139	eqeltrrd	$⊢ ((A \in topGen (ran (.)) \land A \neq \emptyset) \land (⋃ [.] [\{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}] = A \land \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \in Fin)) \to A \in Clsd (topGen (ran (.)))$
141	114 116 117 118 140	connclo	$⊢ ((A \in topGen (ran (.)) \land A \neq \emptyset) \land (⋃ [.] [\{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}] = A \land \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \in Fin)) \to A = ℝ$
142	141	ex	$⊢ (A \in topGen (ran (.)) \land A \neq \emptyset) \to ((⋃ [.] [\{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}] = A \land \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \in Fin) \to A = ℝ)$
143	142	necon3ad	$⊢ (A \in topGen (ran (.)) \land A \neq \emptyset) \to (A \neq ℝ \to \neg (⋃ [.] [\{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}] = A \land \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \in Fin))$
144	143	imp	$⊢ ((A \in topGen (ran (.)) \land A \neq \emptyset) \land A \neq ℝ) \to \neg (⋃ [.] [\{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}] = A \land \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \in Fin)$
145	113 144	pm2.61dane	$⊢ (A \in topGen (ran (.)) \land A \neq \emptyset) \to \neg (⋃ [.] [\{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}] = A \land \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \in Fin)$
146		oveq1	$⊢ x = u \to \frac{x}{2^{y}} = \frac{u}{2^{y}}$
147		oveq1	$⊢ x = u \to x + 1 = u + 1$
148	147	oveq1d	$⊢ x = u \to \frac{x + 1}{2^{y}} = \frac{u + 1}{2^{y}}$
149	146 148	opeq12d	$⊢ x = u \to ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩ = ⟨\frac{u}{2^{y}}, \frac{u + 1}{2^{y}}⟩$
150		oveq2	$⊢ y = v \to 2^{y} = 2^{v}$
151	150	oveq2d	$⊢ y = v \to \frac{u}{2^{y}} = \frac{u}{2^{v}}$
152	150	oveq2d	$⊢ y = v \to \frac{u + 1}{2^{y}} = \frac{u + 1}{2^{v}}$
153	151 152	opeq12d	$⊢ y = v \to ⟨\frac{u}{2^{y}}, \frac{u + 1}{2^{y}}⟩ = ⟨\frac{u}{2^{v}}, \frac{u + 1}{2^{v}}⟩$
154	149 153	cbvmpov	$⊢ (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) = (u \in ℤ, v \in ℕ_{0} ⟼ ⟨\frac{u}{2^{v}}, \frac{u + 1}{2^{v}}⟩)$
155		fveq2	$⊢ a = z \to [.] (a) = [.] (z)$
156	155	sseq1d	$⊢ a = z \to ([.] (a) \subseteq [.] (c) \leftrightarrow [.] (z) \subseteq [.] (c))$
157		equequ1	$⊢ a = z \to (a = c \leftrightarrow z = c)$
158	156 157	imbi12d	$⊢ a = z \to (([.] (a) \subseteq [.] (c) \to a = c) \leftrightarrow ([.] (z) \subseteq [.] (c) \to z = c))$
159	158	ralbidv	$⊢ a = z \to (\forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c) \leftrightarrow \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (z) \subseteq [.] (c) \to z = c))$
160	159	cbvrabv	$⊢ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} = \{z \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (z) \subseteq [.] (c) \to z = c)\}$
161	19	a1i	$⊢ A \in topGen (ran (.)) \to \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \subseteq ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩)$
162	154 160 161	dyadmbllem	$⊢ A \in topGen (ran (.)) \to ⋃ [.] [\{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\}] = ⋃ [.] [\{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}]$
163		opnmbllem0	$⊢ A \in topGen (ran (.)) \to ⋃ [.] [\{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\}] = A$
164	162 163	eqtr3d	$⊢ A \in topGen (ran (.)) \to ⋃ [.] [\{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}] = A$
165	164	adantr	$⊢ (A \in topGen (ran (.)) \land A \neq \emptyset) \to ⋃ [.] [\{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}] = A$
166		nnenom	$⊢ ℕ \approx ω$
167		sdomentr	$⊢ (\{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} ≺ ℕ \land ℕ \approx ω) \to \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} ≺ ω$
168	166 167	mpan2	$⊢ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} ≺ ℕ \to \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} ≺ ω$
169		isfinite	$⊢ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \in Fin \leftrightarrow \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} ≺ ω$
170	168 169	sylibr	$⊢ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} ≺ ℕ \to \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \in Fin$
171	165 170	anim12i	$⊢ ((A \in topGen (ran (.)) \land A \neq \emptyset) \land \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} ≺ ℕ) \to (⋃ [.] [\{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}] = A \land \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \in Fin)$
172	145 171	mtand	$⊢ (A \in topGen (ran (.)) \land A \neq \emptyset) \to \neg \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} ≺ ℕ$
173		qex	$⊢ ℚ \in V$
174	173 173	xpex	$⊢ ℚ \times ℚ \in V$
175		zq	$⊢ x \in ℤ \to x \in ℚ$
176		2nn	$⊢ 2 \in ℕ$
177		nnq	$⊢ 2 \in ℕ \to 2 \in ℚ$
178	176 177	ax-mp	$⊢ 2 \in ℚ$
179		qexpcl	$⊢ (2 \in ℚ \land y \in ℕ_{0}) \to 2^{y} \in ℚ$
180	178 179	mpan	$⊢ y \in ℕ_{0} \to 2^{y} \in ℚ$
181	180 29	jca	$⊢ y \in ℕ_{0} \to (2^{y} \in ℚ \land 2^{y} \neq 0)$
182		qdivcl	$⊢ (x \in ℚ \land 2^{y} \in ℚ \land 2^{y} \neq 0) \to \frac{x}{2^{y}} \in ℚ$
183		1z	$⊢ 1 \in ℤ$
184		zq	$⊢ 1 \in ℤ \to 1 \in ℚ$
185	183 184	ax-mp	$⊢ 1 \in ℚ$
186		qaddcl	$⊢ (x \in ℚ \land 1 \in ℚ) \to x + 1 \in ℚ$
187	185 186	mpan2	$⊢ x \in ℚ \to x + 1 \in ℚ$
188		qdivcl	$⊢ (x + 1 \in ℚ \land 2^{y} \in ℚ \land 2^{y} \neq 0) \to \frac{x + 1}{2^{y}} \in ℚ$
189	187 188	syl3an1	$⊢ (x \in ℚ \land 2^{y} \in ℚ \land 2^{y} \neq 0) \to \frac{x + 1}{2^{y}} \in ℚ$
190		opelxpi	$⊢ (\frac{x}{2^{y}} \in ℚ \land \frac{x + 1}{2^{y}} \in ℚ) \to ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩ \in (ℚ \times ℚ)$
191	182 189 190	syl2anc	$⊢ (x \in ℚ \land 2^{y} \in ℚ \land 2^{y} \neq 0) \to ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩ \in (ℚ \times ℚ)$
192	191	3expb	$⊢ (x \in ℚ \land (2^{y} \in ℚ \land 2^{y} \neq 0)) \to ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩ \in (ℚ \times ℚ)$
193	175 181 192	syl2an	$⊢ (x \in ℤ \land y \in ℕ_{0}) \to ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩ \in (ℚ \times ℚ)$
194	193	rgen2	$⊢ \forall x \in ℤ \forall y \in ℕ_{0} ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩ \in (ℚ \times ℚ)$
195	40	fmpo	$⊢ \forall x \in ℤ \forall y \in ℕ_{0} ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩ \in (ℚ \times ℚ) \leftrightarrow (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) : ℤ \times ℕ_{0} ⟶ ℚ \times ℚ$
196	194 195	mpbi	$⊢ (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) : ℤ \times ℕ_{0} ⟶ ℚ \times ℚ$
197		frn	$⊢ (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) : ℤ \times ℕ_{0} ⟶ ℚ \times ℚ \to ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \subseteq ℚ \times ℚ$
198	196 197	ax-mp	$⊢ ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \subseteq ℚ \times ℚ$
199	19 198	sstri	$⊢ \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \subseteq ℚ \times ℚ$
200	18 199	sstri	$⊢ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \subseteq ℚ \times ℚ$
201		ssdomg	$⊢ ℚ \times ℚ \in V \to (\{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \subseteq ℚ \times ℚ \to \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} ≼ (ℚ \times ℚ))$
202	174 200 201	mp2	$⊢ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} ≼ (ℚ \times ℚ)$
203		qnnen	$⊢ ℚ \approx ℕ$
204		xpen	$⊢ (ℚ \approx ℕ \land ℚ \approx ℕ) \to (ℚ \times ℚ) \approx (ℕ \times ℕ)$
205	203 203 204	mp2an	$⊢ (ℚ \times ℚ) \approx (ℕ \times ℕ)$
206		xpnnen	$⊢ (ℕ \times ℕ) \approx ℕ$
207	205 206	entri	$⊢ (ℚ \times ℚ) \approx ℕ$
208		domentr	$⊢ (\{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} ≼ (ℚ \times ℚ) \land (ℚ \times ℚ) \approx ℕ) \to \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} ≼ ℕ$
209	202 207 208	mp2an	$⊢ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} ≼ ℕ$
210	172 209	jctil	$⊢ (A \in topGen (ran (.)) \land A \neq \emptyset) \to (\{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} ≼ ℕ \land \neg \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} ≺ ℕ)$
211		bren2	$⊢ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \approx ℕ \leftrightarrow (\{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} ≼ ℕ \land \neg \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} ≺ ℕ)$
212	210 211	sylibr	$⊢ (A \in topGen (ran (.)) \land A \neq \emptyset) \to \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \approx ℕ$
213	212	ensymd	$⊢ (A \in topGen (ran (.)) \land A \neq \emptyset) \to ℕ \approx \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}$
214		bren	$⊢ ℕ \approx \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \leftrightarrow \exists f f : ℕ \underset{1-1 onto}{⟶} \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}$
215	213 214	sylib	$⊢ (A \in topGen (ran (.)) \land A \neq \emptyset) \to \exists f f : ℕ \underset{1-1 onto}{⟶} \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}$

Metamath Proof Explorer

Theorem mblfinlem1

Proof