mblfinlem1 - Mathbox for Brendan Leahy

	Mathbox for Brendan Leahy		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > mblfinlem1		Structured version Visualization version GIF version

Theorem mblfinlem1 35811

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

**Assertion**
Ref	Expression
mblfinlem1	⊢ ((𝐴 ∈ (topGen‘ran (,)) ∧ 𝐴 ≠ ∅) → ∃𝑓 𝑓:ℕ–1-1-onto→{𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)})

Distinct variable group: 𝑎,𝑏,𝑐,𝑓,𝑥,𝑦,𝐴

Proof of Theorem mblfinlem1 Dummy variables 𝑛 𝑢 𝑣 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		peano2re 11146	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℝ → (𝑛 + 1) ∈ ℝ)
2		ltp1 11813	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℝ → 𝑛 < (𝑛 + 1))
3		breq2 5080	. . . . . . . . . . . . . 14 ⊢ (𝑧 = (𝑛 + 1) → (𝑛 < 𝑧 ↔ 𝑛 < (𝑛 + 1)))
4	3	rspcev 3561	. . . . . . . . . . . . 13 ⊢ (((𝑛 + 1) ∈ ℝ ∧ 𝑛 < (𝑛 + 1)) → ∃𝑧 ∈ ℝ 𝑛 < 𝑧)
5	1, 2, 4	syl2anc 584	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑛 < 𝑧)
6	5	rgen 3074	. . . . . . . . . . 11 ⊢ ∀𝑛 ∈ ℝ ∃𝑧 ∈ ℝ 𝑛 < 𝑧
7		ltnle 11052	. . . . . . . . . . . . . . 15 ⊢ ((𝑛 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑛 < 𝑧 ↔ ¬ 𝑧 ≤ 𝑛))
8	7	rexbidva 3224	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℝ → (∃𝑧 ∈ ℝ 𝑛 < 𝑧 ↔ ∃𝑧 ∈ ℝ ¬ 𝑧 ≤ 𝑛))
9		rexnal 3168	. . . . . . . . . . . . . 14 ⊢ (∃𝑧 ∈ ℝ ¬ 𝑧 ≤ 𝑛 ↔ ¬ ∀𝑧 ∈ ℝ 𝑧 ≤ 𝑛)
10	8, 9	bitrdi 287	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℝ → (∃𝑧 ∈ ℝ 𝑛 < 𝑧 ↔ ¬ ∀𝑧 ∈ ℝ 𝑧 ≤ 𝑛))
11	10	ralbiia 3091	. . . . . . . . . . . 12 ⊢ (∀𝑛 ∈ ℝ ∃𝑧 ∈ ℝ 𝑛 < 𝑧 ↔ ∀𝑛 ∈ ℝ ¬ ∀𝑧 ∈ ℝ 𝑧 ≤ 𝑛)
12		ralnex 3166	. . . . . . . . . . . 12 ⊢ (∀𝑛 ∈ ℝ ¬ ∀𝑧 ∈ ℝ 𝑧 ≤ 𝑛 ↔ ¬ ∃𝑛 ∈ ℝ ∀𝑧 ∈ ℝ 𝑧 ≤ 𝑛)
13	11, 12	bitri 274	. . . . . . . . . . 11 ⊢ (∀𝑛 ∈ ℝ ∃𝑧 ∈ ℝ 𝑛 < 𝑧 ↔ ¬ ∃𝑛 ∈ ℝ ∀𝑧 ∈ ℝ 𝑧 ≤ 𝑛)
14	6, 13	mpbi 229	. . . . . . . . . 10 ⊢ ¬ ∃𝑛 ∈ ℝ ∀𝑧 ∈ ℝ 𝑧 ≤ 𝑛
15		raleq 3341	. . . . . . . . . . 11 ⊢ (𝐴 = ℝ → (∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑛 ↔ ∀𝑧 ∈ ℝ 𝑧 ≤ 𝑛))
16	15	rexbidv 3225	. . . . . . . . . 10 ⊢ (𝐴 = ℝ → (∃𝑛 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑛 ↔ ∃𝑛 ∈ ℝ ∀𝑧 ∈ ℝ 𝑧 ≤ 𝑛))
17	14, 16	mtbiri 327	. . . . . . . . 9 ⊢ (𝐴 = ℝ → ¬ ∃𝑛 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑛)
18		ssrab2 4014	. . . . . . . . . . . . . 14 ⊢ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ⊆ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴}
19		ssrab2 4014	. . . . . . . . . . . . . . 15 ⊢ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ⊆ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩)
20		zre 12321	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℤ → 𝑥 ∈ ℝ)
21		2re 12045	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 2 ∈ ℝ
22		reexpcl 13797	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((2 ∈ ℝ ∧ 𝑦 ∈ ℕ₀) → (2↑𝑦) ∈ ℝ)
23	21, 22	mpan 687	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ ℕ₀ → (2↑𝑦) ∈ ℝ)
24		nn0z 12341	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ ℕ₀ → 𝑦 ∈ ℤ)
25		2cn 12046	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 2 ∈ ℂ
26		2ne0 12075	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 2 ≠ 0
27		expne0i 13813	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((2 ∈ ℂ ∧ 2 ≠ 0 ∧ 𝑦 ∈ ℤ) → (2↑𝑦) ≠ 0)
28	25, 26, 27	mp3an12 1450	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ ℤ → (2↑𝑦) ≠ 0)
29	24, 28	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ ℕ₀ → (2↑𝑦) ≠ 0)
30	23, 29	jca 512	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ ℕ₀ → ((2↑𝑦) ∈ ℝ ∧ (2↑𝑦) ≠ 0))
31		redivcl 11692	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ ℝ ∧ (2↑𝑦) ∈ ℝ ∧ (2↑𝑦) ≠ 0) → (𝑥 / (2↑𝑦)) ∈ ℝ)
32		peano2re 11146	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ ℝ → (𝑥 + 1) ∈ ℝ)
33		redivcl 11692	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑥 + 1) ∈ ℝ ∧ (2↑𝑦) ∈ ℝ ∧ (2↑𝑦) ≠ 0) → ((𝑥 + 1) / (2↑𝑦)) ∈ ℝ)
34	32, 33	syl3an1 1162	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ ℝ ∧ (2↑𝑦) ∈ ℝ ∧ (2↑𝑦) ≠ 0) → ((𝑥 + 1) / (2↑𝑦)) ∈ ℝ)
35		opelxpi 5628	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑥 / (2↑𝑦)) ∈ ℝ ∧ ((𝑥 + 1) / (2↑𝑦)) ∈ ℝ) → ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩ ∈ (ℝ × ℝ))
36	31, 34, 35	syl2anc 584	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ ℝ ∧ (2↑𝑦) ∈ ℝ ∧ (2↑𝑦) ≠ 0) → ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩ ∈ (ℝ × ℝ))
37	36	3expb 1119	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ ℝ ∧ ((2↑𝑦) ∈ ℝ ∧ (2↑𝑦) ≠ 0)) → ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩ ∈ (ℝ × ℝ))
38	20, 30, 37	syl2an 596	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ₀) → ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩ ∈ (ℝ × ℝ))
39	38	rgen2 3128	. . . . . . . . . . . . . . . . 17 ⊢ ∀𝑥 ∈ ℤ ∀𝑦 ∈ ℕ₀ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩ ∈ (ℝ × ℝ)
40		eqid 2738	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) = (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩)
41	40	fmpo 7908	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑥 ∈ ℤ ∀𝑦 ∈ ℕ₀ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩ ∈ (ℝ × ℝ) ↔ (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩):(ℤ × ℕ₀)⟶(ℝ × ℝ))
42	39, 41	mpbi 229	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩):(ℤ × ℕ₀)⟶(ℝ × ℝ)
43		frn 6609	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩):(ℤ × ℕ₀)⟶(ℝ × ℝ) → ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ⊆ (ℝ × ℝ))
44	42, 43	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ⊆ (ℝ × ℝ)
45	19, 44	sstri 3931	. . . . . . . . . . . . . 14 ⊢ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ⊆ (ℝ × ℝ)
46	18, 45	sstri 3931	. . . . . . . . . . . . 13 ⊢ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ⊆ (ℝ × ℝ)
47		rnss 5850	. . . . . . . . . . . . . 14 ⊢ ({𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ⊆ (ℝ × ℝ) → ran {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ⊆ ran (ℝ × ℝ))
48		rnxpid 6078	. . . . . . . . . . . . . 14 ⊢ ran (ℝ × ℝ) = ℝ
49	47, 48	sseqtrdi 3972	. . . . . . . . . . . . 13 ⊢ ({𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ⊆ (ℝ × ℝ) → ran {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ⊆ ℝ)
50	46, 49	ax-mp 5	. . . . . . . . . . . 12 ⊢ ran {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ⊆ ℝ
51		rnfi 9100	. . . . . . . . . . . 12 ⊢ ({𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ∈ Fin → ran {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ∈ Fin)
52		fimaxre2 11918	. . . . . . . . . . . 12 ⊢ ((ran {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ⊆ ℝ ∧ ran {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ∈ Fin) → ∃𝑛 ∈ ℝ ∀𝑢 ∈ ran {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}𝑢 ≤ 𝑛)
53	50, 51, 52	sylancr 587	. . . . . . . . . . 11 ⊢ ({𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ∈ Fin → ∃𝑛 ∈ ℝ ∀𝑢 ∈ ran {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}𝑢 ≤ 𝑛)
54	53	adantl 482	. . . . . . . . . 10 ⊢ ((∪ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}) = 𝐴 ∧ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ∈ Fin) → ∃𝑛 ∈ ℝ ∀𝑢 ∈ ran {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}𝑢 ≤ 𝑛)
55		eluni2 4845	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ ∪ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}) ↔ ∃𝑢 ∈ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)})𝑧 ∈ 𝑢)
56		iccf 13178	. . . . . . . . . . . . . . . . . . 19 ⊢ [,]:(ℝ^* × ℝ^)⟶𝒫 ℝ^
57		ffn 6602	. . . . . . . . . . . . . . . . . . 19 ⊢ ([,]:(ℝ^* × ℝ^)⟶𝒫 ℝ^ → [,] Fn (ℝ^* × ℝ^*))
58	56, 57	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ [,] Fn (ℝ^* × ℝ^*)
59		rexpssxrxp 11018	. . . . . . . . . . . . . . . . . . 19 ⊢ (ℝ × ℝ) ⊆ (ℝ^* × ℝ^*)
60	46, 59	sstri 3931	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ⊆ (ℝ^* × ℝ^*)
61		eleq2 2827	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 = ([,]‘𝑣) → (𝑧 ∈ 𝑢 ↔ 𝑧 ∈ ([,]‘𝑣)))
62	61	rexima 7115	. . . . . . . . . . . . . . . . . 18 ⊢ (([,] Fn (ℝ^* × ℝ^) ∧ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ⊆ (ℝ^ × ℝ^*)) → (∃𝑢 ∈ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)})𝑧 ∈ 𝑢 ↔ ∃𝑣 ∈ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}𝑧 ∈ ([,]‘𝑣)))
63	58, 60, 62	mp2an 689	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑢 ∈ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)})𝑧 ∈ 𝑢 ↔ ∃𝑣 ∈ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}𝑧 ∈ ([,]‘𝑣))
64	55, 63	bitri 274	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ ∪ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}) ↔ ∃𝑣 ∈ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}𝑧 ∈ ([,]‘𝑣))
65	46	sseli 3918	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 ∈ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} → 𝑣 ∈ (ℝ × ℝ))
66		1st2nd2 7870	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑣 ∈ (ℝ × ℝ) → 𝑣 = ⟨(1^st ‘𝑣), (2^nd ‘𝑣)⟩)
67	66	fveq2d 6780	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑣 ∈ (ℝ × ℝ) → ([,]‘𝑣) = ([,]‘⟨(1^st ‘𝑣), (2^nd ‘𝑣)⟩))
68		df-ov 7280	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((1^st ‘𝑣)[,](2^nd ‘𝑣)) = ([,]‘⟨(1^st ‘𝑣), (2^nd ‘𝑣)⟩)
69	67, 68	eqtr4di 2796	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 ∈ (ℝ × ℝ) → ([,]‘𝑣) = ((1^st ‘𝑣)[,](2^nd ‘𝑣)))
70	69	eleq2d 2824	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 ∈ (ℝ × ℝ) → (𝑧 ∈ ([,]‘𝑣) ↔ 𝑧 ∈ ((1^st ‘𝑣)[,](2^nd ‘𝑣))))
71	65, 70	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑣 ∈ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} → (𝑧 ∈ ([,]‘𝑣) ↔ 𝑧 ∈ ((1^st ‘𝑣)[,](2^nd ‘𝑣))))
72	71	biimpd 228	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑣 ∈ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} → (𝑧 ∈ ([,]‘𝑣) → 𝑧 ∈ ((1^st ‘𝑣)[,](2^nd ‘𝑣))))
73	72	imdistani 569	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑣 ∈ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ∧ 𝑧 ∈ ([,]‘𝑣)) → (𝑣 ∈ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ∧ 𝑧 ∈ ((1^st ‘𝑣)[,](2^nd ‘𝑣))))
74		eliccxr 13165	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ ((1^st ‘𝑣)[,](2^nd ‘𝑣)) → 𝑧 ∈ ℝ^*)
75	74	ad2antll 726	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((∪ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}) = 𝐴 ∧ 𝑛 ∈ ℝ) ∧ ∀𝑢 ∈ ran {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}𝑢 ≤ 𝑛) ∧ (𝑣 ∈ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ∧ 𝑧 ∈ ((1^st ‘𝑣)[,](2^nd ‘𝑣)))) → 𝑧 ∈ ℝ^*)
76		xp2nd 7864	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 ∈ (ℝ × ℝ) → (2^nd ‘𝑣) ∈ ℝ)
77	76	rexrd 11023	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 ∈ (ℝ × ℝ) → (2^nd ‘𝑣) ∈ ℝ^*)
78	65, 77	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑣 ∈ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} → (2^nd ‘𝑣) ∈ ℝ^*)
79	78	ad2antrl 725	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((∪ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}) = 𝐴 ∧ 𝑛 ∈ ℝ) ∧ ∀𝑢 ∈ ran {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}𝑢 ≤ 𝑛) ∧ (𝑣 ∈ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ∧ 𝑧 ∈ ((1^st ‘𝑣)[,](2^nd ‘𝑣)))) → (2^nd ‘𝑣) ∈ ℝ^*)
80		simpllr 773	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((∪ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}) = 𝐴 ∧ 𝑛 ∈ ℝ) ∧ ∀𝑢 ∈ ran {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}𝑢 ≤ 𝑛) ∧ (𝑣 ∈ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ∧ 𝑧 ∈ ((1^st ‘𝑣)[,](2^nd ‘𝑣)))) → 𝑛 ∈ ℝ)
81	80	rexrd 11023	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((∪ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}) = 𝐴 ∧ 𝑛 ∈ ℝ) ∧ ∀𝑢 ∈ ran {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}𝑢 ≤ 𝑛) ∧ (𝑣 ∈ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ∧ 𝑧 ∈ ((1^st ‘𝑣)[,](2^nd ‘𝑣)))) → 𝑛 ∈ ℝ^*)
82		xp1st 7863	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑣 ∈ (ℝ × ℝ) → (1^st ‘𝑣) ∈ ℝ)
83	82	rexrd 11023	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑣 ∈ (ℝ × ℝ) → (1^st ‘𝑣) ∈ ℝ^*)
84	83, 77	jca 512	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 ∈ (ℝ × ℝ) → ((1^st ‘𝑣) ∈ ℝ^* ∧ (2^nd ‘𝑣) ∈ ℝ^*))
85	65, 84	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 ∈ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} → ((1^st ‘𝑣) ∈ ℝ^* ∧ (2^nd ‘𝑣) ∈ ℝ^*))
86		iccleub 13132	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((1^st ‘𝑣) ∈ ℝ^* ∧ (2^nd ‘𝑣) ∈ ℝ^* ∧ 𝑧 ∈ ((1^st ‘𝑣)[,](2^nd ‘𝑣))) → 𝑧 ≤ (2^nd ‘𝑣))
87	86	3expa 1117	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((1^st ‘𝑣) ∈ ℝ^* ∧ (2^nd ‘𝑣) ∈ ℝ^*) ∧ 𝑧 ∈ ((1^st ‘𝑣)[,](2^nd ‘𝑣))) → 𝑧 ≤ (2^nd ‘𝑣))
88	85, 87	sylan 580	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑣 ∈ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ∧ 𝑧 ∈ ((1^st ‘𝑣)[,](2^nd ‘𝑣))) → 𝑧 ≤ (2^nd ‘𝑣))
89	88	adantl 482	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((∪ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}) = 𝐴 ∧ 𝑛 ∈ ℝ) ∧ ∀𝑢 ∈ ran {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}𝑢 ≤ 𝑛) ∧ (𝑣 ∈ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ∧ 𝑧 ∈ ((1^st ‘𝑣)[,](2^nd ‘𝑣)))) → 𝑧 ≤ (2^nd ‘𝑣))
90		xpss 5607	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (ℝ × ℝ) ⊆ (V × V)
91	46, 90	sstri 3931	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ⊆ (V × V)
92		df-rel 5598	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (Rel {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ↔ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ⊆ (V × V))
93	91, 92	mpbir 230	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Rel {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}
94		2ndrn 7882	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((Rel {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ∧ 𝑣 ∈ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}) → (2^nd ‘𝑣) ∈ ran {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)})
95	93, 94	mpan 687	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 ∈ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} → (2^nd ‘𝑣) ∈ ran {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)})
96		breq1 5079	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢 = (2^nd ‘𝑣) → (𝑢 ≤ 𝑛 ↔ (2^nd ‘𝑣) ≤ 𝑛))
97	96	rspccva 3560	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((∀𝑢 ∈ ran {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}𝑢 ≤ 𝑛 ∧ (2^nd ‘𝑣) ∈ ran {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}) → (2^nd ‘𝑣) ≤ 𝑛)
98	95, 97	sylan2 593	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((∀𝑢 ∈ ran {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}𝑢 ≤ 𝑛 ∧ 𝑣 ∈ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}) → (2^nd ‘𝑣) ≤ 𝑛)
99	98	ad2ant2lr 745	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((∪ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}) = 𝐴 ∧ 𝑛 ∈ ℝ) ∧ ∀𝑢 ∈ ran {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}𝑢 ≤ 𝑛) ∧ (𝑣 ∈ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ∧ 𝑧 ∈ ((1^st ‘𝑣)[,](2^nd ‘𝑣)))) → (2^nd ‘𝑣) ≤ 𝑛)
100	75, 79, 81, 89, 99	xrletrd 12894	. . . . . . . . . . . . . . . . . 18 ⊢ ((((∪ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}) = 𝐴 ∧ 𝑛 ∈ ℝ) ∧ ∀𝑢 ∈ ran {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}𝑢 ≤ 𝑛) ∧ (𝑣 ∈ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ∧ 𝑧 ∈ ((1^st ‘𝑣)[,](2^nd ‘𝑣)))) → 𝑧 ≤ 𝑛)
101	73, 100	sylan2 593	. . . . . . . . . . . . . . . . 17 ⊢ ((((∪ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}) = 𝐴 ∧ 𝑛 ∈ ℝ) ∧ ∀𝑢 ∈ ran {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}𝑢 ≤ 𝑛) ∧ (𝑣 ∈ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ∧ 𝑧 ∈ ([,]‘𝑣))) → 𝑧 ≤ 𝑛)
102	101	rexlimdvaa 3213	. . . . . . . . . . . . . . . 16 ⊢ (((∪ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}) = 𝐴 ∧ 𝑛 ∈ ℝ) ∧ ∀𝑢 ∈ ran {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}𝑢 ≤ 𝑛) → (∃𝑣 ∈ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}𝑧 ∈ ([,]‘𝑣) → 𝑧 ≤ 𝑛))
103	64, 102	syl5bi 241	. . . . . . . . . . . . . . 15 ⊢ (((∪ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}) = 𝐴 ∧ 𝑛 ∈ ℝ) ∧ ∀𝑢 ∈ ran {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}𝑢 ≤ 𝑛) → (𝑧 ∈ ∪ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}) → 𝑧 ≤ 𝑛))
104	103	ralrimiv 3102	. . . . . . . . . . . . . 14 ⊢ (((∪ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}) = 𝐴 ∧ 𝑛 ∈ ℝ) ∧ ∀𝑢 ∈ ran {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}𝑢 ≤ 𝑛) → ∀𝑧 ∈ ∪ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)})𝑧 ≤ 𝑛)
105		raleq 3341	. . . . . . . . . . . . . . 15 ⊢ (∪ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}) = 𝐴 → (∀𝑧 ∈ ∪ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)})𝑧 ≤ 𝑛 ↔ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑛))
106	105	ad2antrr 723	. . . . . . . . . . . . . 14 ⊢ (((∪ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}) = 𝐴 ∧ 𝑛 ∈ ℝ) ∧ ∀𝑢 ∈ ran {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}𝑢 ≤ 𝑛) → (∀𝑧 ∈ ∪ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)})𝑧 ≤ 𝑛 ↔ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑛))
107	104, 106	mpbid 231	. . . . . . . . . . . . 13 ⊢ (((∪ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}) = 𝐴 ∧ 𝑛 ∈ ℝ) ∧ ∀𝑢 ∈ ran {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}𝑢 ≤ 𝑛) → ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑛)
108	107	ex 413	. . . . . . . . . . . 12 ⊢ ((∪ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}) = 𝐴 ∧ 𝑛 ∈ ℝ) → (∀𝑢 ∈ ran {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}𝑢 ≤ 𝑛 → ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑛))
109	108	reximdva 3202	. . . . . . . . . . 11 ⊢ (∪ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}) = 𝐴 → (∃𝑛 ∈ ℝ ∀𝑢 ∈ ran {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}𝑢 ≤ 𝑛 → ∃𝑛 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑛))
110	109	adantr 481	. . . . . . . . . 10 ⊢ ((∪ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}) = 𝐴 ∧ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ∈ Fin) → (∃𝑛 ∈ ℝ ∀𝑢 ∈ ran {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}𝑢 ≤ 𝑛 → ∃𝑛 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑛))
111	54, 110	mpd 15	. . . . . . . . 9 ⊢ ((∪ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}) = 𝐴 ∧ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ∈ Fin) → ∃𝑛 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑛)
112	17, 111	nsyl 140	. . . . . . . 8 ⊢ (𝐴 = ℝ → ¬ (∪ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}) = 𝐴 ∧ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ∈ Fin))
113	112	adantl 482	. . . . . . 7 ⊢ (((𝐴 ∈ (topGen‘ran (,)) ∧ 𝐴 ≠ ∅) ∧ 𝐴 = ℝ) → ¬ (∪ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}) = 𝐴 ∧ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ∈ Fin))
114		uniretop 23924	. . . . . . . . . . 11 ⊢ ℝ = ∪ (topGen‘ran (,))
115		retopconn 23990	. . . . . . . . . . . 12 ⊢ (topGen‘ran (,)) ∈ Conn
116	115	a1i 11	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ (topGen‘ran (,)) ∧ 𝐴 ≠ ∅) ∧ (∪ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}) = 𝐴 ∧ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ∈ Fin)) → (topGen‘ran (,)) ∈ Conn)
117		simpll 764	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ (topGen‘ran (,)) ∧ 𝐴 ≠ ∅) ∧ (∪ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}) = 𝐴 ∧ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ∈ Fin)) → 𝐴 ∈ (topGen‘ran (,)))
118		simplr 766	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ (topGen‘ran (,)) ∧ 𝐴 ≠ ∅) ∧ (∪ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}) = 𝐴 ∧ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ∈ Fin)) → 𝐴 ≠ ∅)
119		simprl 768	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ (topGen‘ran (,)) ∧ 𝐴 ≠ ∅) ∧ (∪ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}) = 𝐴 ∧ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ∈ Fin)) → ∪ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}) = 𝐴)
120		ffun 6605	. . . . . . . . . . . . . . 15 ⊢ ([,]:(ℝ^* × ℝ^)⟶𝒫 ℝ^ → Fun [,])
121		funiunfv 7123	. . . . . . . . . . . . . . 15 ⊢ (Fun [,] → ∪ 𝑧 ∈ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ([,]‘𝑧) = ∪ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}))
122	56, 120, 121	mp2b 10	. . . . . . . . . . . . . 14 ⊢ ∪ 𝑧 ∈ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ([,]‘𝑧) = ∪ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)})
123		retop 23923	. . . . . . . . . . . . . . 15 ⊢ (topGen‘ran (,)) ∈ Top
124	46	sseli 3918	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} → 𝑧 ∈ (ℝ × ℝ))
125		1st2nd2 7870	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ (ℝ × ℝ) → 𝑧 = ⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩)
126	125	fveq2d 6780	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ (ℝ × ℝ) → ([,]‘𝑧) = ([,]‘⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩))
127		df-ov 7280	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1^st ‘𝑧)[,](2^nd ‘𝑧)) = ([,]‘⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩)
128	126, 127	eqtr4di 2796	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ (ℝ × ℝ) → ([,]‘𝑧) = ((1^st ‘𝑧)[,](2^nd ‘𝑧)))
129		xp1st 7863	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ (ℝ × ℝ) → (1^st ‘𝑧) ∈ ℝ)
130		xp2nd 7864	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ (ℝ × ℝ) → (2^nd ‘𝑧) ∈ ℝ)
131		icccld 23928	. . . . . . . . . . . . . . . . . . 19 ⊢ (((1^st ‘𝑧) ∈ ℝ ∧ (2^nd ‘𝑧) ∈ ℝ) → ((1^st ‘𝑧)[,](2^nd ‘𝑧)) ∈ (Clsd‘(topGen‘ran (,))))
132	129, 130, 131	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ (ℝ × ℝ) → ((1^st ‘𝑧)[,](2^nd ‘𝑧)) ∈ (Clsd‘(topGen‘ran (,))))
133	128, 132	eqeltrd 2839	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ (ℝ × ℝ) → ([,]‘𝑧) ∈ (Clsd‘(topGen‘ran (,))))
134	124, 133	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} → ([,]‘𝑧) ∈ (Clsd‘(topGen‘ran (,))))
135	134	rgen 3074	. . . . . . . . . . . . . . 15 ⊢ ∀𝑧 ∈ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ([,]‘𝑧) ∈ (Clsd‘(topGen‘ran (,)))
136	114	iuncld 22194	. . . . . . . . . . . . . . 15 ⊢ (((topGen‘ran (,)) ∈ Top ∧ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ∈ Fin ∧ ∀𝑧 ∈ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ([,]‘𝑧) ∈ (Clsd‘(topGen‘ran (,)))) → ∪ 𝑧 ∈ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ([,]‘𝑧) ∈ (Clsd‘(topGen‘ran (,))))
137	123, 135, 136	mp3an13 1451	. . . . . . . . . . . . . 14 ⊢ ({𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ∈ Fin → ∪ 𝑧 ∈ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ([,]‘𝑧) ∈ (Clsd‘(topGen‘ran (,))))
138	122, 137	eqeltrrid 2844	. . . . . . . . . . . . 13 ⊢ ({𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ∈ Fin → ∪ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}) ∈ (Clsd‘(topGen‘ran (,))))
139	138	ad2antll 726	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ (topGen‘ran (,)) ∧ 𝐴 ≠ ∅) ∧ (∪ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}) = 𝐴 ∧ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ∈ Fin)) → ∪ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}) ∈ (Clsd‘(topGen‘ran (,))))
140	119, 139	eqeltrrd 2840	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ (topGen‘ran (,)) ∧ 𝐴 ≠ ∅) ∧ (∪ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}) = 𝐴 ∧ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ∈ Fin)) → 𝐴 ∈ (Clsd‘(topGen‘ran (,))))
141	114, 116, 117, 118, 140	connclo 22564	. . . . . . . . . 10 ⊢ (((𝐴 ∈ (topGen‘ran (,)) ∧ 𝐴 ≠ ∅) ∧ (∪ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}) = 𝐴 ∧ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ∈ Fin)) → 𝐴 = ℝ)
142	141	ex 413	. . . . . . . . 9 ⊢ ((𝐴 ∈ (topGen‘ran (,)) ∧ 𝐴 ≠ ∅) → ((∪ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}) = 𝐴 ∧ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ∈ Fin) → 𝐴 = ℝ))
143	142	necon3ad 2956	. . . . . . . 8 ⊢ ((𝐴 ∈ (topGen‘ran (,)) ∧ 𝐴 ≠ ∅) → (𝐴 ≠ ℝ → ¬ (∪ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}) = 𝐴 ∧ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ∈ Fin)))
144	143	imp 407	. . . . . . 7 ⊢ (((𝐴 ∈ (topGen‘ran (,)) ∧ 𝐴 ≠ ∅) ∧ 𝐴 ≠ ℝ) → ¬ (∪ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}) = 𝐴 ∧ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ∈ Fin))
145	113, 144	pm2.61dane 3032	. . . . . 6 ⊢ ((𝐴 ∈ (topGen‘ran (,)) ∧ 𝐴 ≠ ∅) → ¬ (∪ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}) = 𝐴 ∧ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ∈ Fin))
146		oveq1 7284	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑢 → (𝑥 / (2↑𝑦)) = (𝑢 / (2↑𝑦)))
147		oveq1 7284	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑢 → (𝑥 + 1) = (𝑢 + 1))
148	147	oveq1d 7292	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑢 → ((𝑥 + 1) / (2↑𝑦)) = ((𝑢 + 1) / (2↑𝑦)))
149	146, 148	opeq12d 4814	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑢 → ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩ = ⟨(𝑢 / (2↑𝑦)), ((𝑢 + 1) / (2↑𝑦))⟩)
150		oveq2 7285	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑣 → (2↑𝑦) = (2↑𝑣))
151	150	oveq2d 7293	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑣 → (𝑢 / (2↑𝑦)) = (𝑢 / (2↑𝑣)))
152	150	oveq2d 7293	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑣 → ((𝑢 + 1) / (2↑𝑦)) = ((𝑢 + 1) / (2↑𝑣)))
153	151, 152	opeq12d 4814	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑣 → ⟨(𝑢 / (2↑𝑦)), ((𝑢 + 1) / (2↑𝑦))⟩ = ⟨(𝑢 / (2↑𝑣)), ((𝑢 + 1) / (2↑𝑣))⟩)
154	149, 153	cbvmpov 7370	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) = (𝑢 ∈ ℤ, 𝑣 ∈ ℕ₀ ↦ ⟨(𝑢 / (2↑𝑣)), ((𝑢 + 1) / (2↑𝑣))⟩)
155		fveq2 6776	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑧 → ([,]‘𝑎) = ([,]‘𝑧))
156	155	sseq1d 3953	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑧 → (([,]‘𝑎) ⊆ ([,]‘𝑐) ↔ ([,]‘𝑧) ⊆ ([,]‘𝑐)))
157		equequ1 2028	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑧 → (𝑎 = 𝑐 ↔ 𝑧 = 𝑐))
158	156, 157	imbi12d 345	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑧 → ((([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐) ↔ (([,]‘𝑧) ⊆ ([,]‘𝑐) → 𝑧 = 𝑐)))
159	158	ralbidv 3119	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑧 → (∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐) ↔ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑧) ⊆ ([,]‘𝑐) → 𝑧 = 𝑐)))
160	159	cbvrabv 3425	. . . . . . . . . 10 ⊢ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} = {𝑧 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑧) ⊆ ([,]‘𝑐) → 𝑧 = 𝑐)}
161	19	a1i 11	. . . . . . . . . 10 ⊢ (𝐴 ∈ (topGen‘ran (,)) → {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ⊆ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩))
162	154, 160, 161	dyadmbllem 24761	. . . . . . . . 9 ⊢ (𝐴 ∈ (topGen‘ran (,)) → ∪ ([,] “ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴}) = ∪ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}))
163		opnmbllem0 35810	. . . . . . . . 9 ⊢ (𝐴 ∈ (topGen‘ran (,)) → ∪ ([,] “ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴}) = 𝐴)
164	162, 163	eqtr3d 2780	. . . . . . . 8 ⊢ (𝐴 ∈ (topGen‘ran (,)) → ∪ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}) = 𝐴)
165	164	adantr 481	. . . . . . 7 ⊢ ((𝐴 ∈ (topGen‘ran (,)) ∧ 𝐴 ≠ ∅) → ∪ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}) = 𝐴)
166		nnenom 13698	. . . . . . . . 9 ⊢ ℕ ≈ ω
167		sdomentr 8896	. . . . . . . . 9 ⊢ (({𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ≺ ℕ ∧ ℕ ≈ ω) → {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ≺ ω)
168	166, 167	mpan2 688	. . . . . . . 8 ⊢ ({𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ≺ ℕ → {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ≺ ω)
169		isfinite 9408	. . . . . . . 8 ⊢ ({𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ∈ Fin ↔ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ≺ ω)
170	168, 169	sylibr 233	. . . . . . 7 ⊢ ({𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ≺ ℕ → {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ∈ Fin)
171	165, 170	anim12i 613	. . . . . 6 ⊢ (((𝐴 ∈ (topGen‘ran (,)) ∧ 𝐴 ≠ ∅) ∧ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ≺ ℕ) → (∪ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}) = 𝐴 ∧ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ∈ Fin))
172	145, 171	mtand 813	. . . . 5 ⊢ ((𝐴 ∈ (topGen‘ran (,)) ∧ 𝐴 ≠ ∅) → ¬ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ≺ ℕ)
173		qex 12699	. . . . . . . 8 ⊢ ℚ ∈ V
174	173, 173	xpex 7603	. . . . . . 7 ⊢ (ℚ × ℚ) ∈ V
175		zq 12692	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℤ → 𝑥 ∈ ℚ)
176		2nn 12044	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℕ
177		nnq 12700	. . . . . . . . . . . . . . . 16 ⊢ (2 ∈ ℕ → 2 ∈ ℚ)
178	176, 177	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℚ
179		qexpcl 13796	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ ℚ ∧ 𝑦 ∈ ℕ₀) → (2↑𝑦) ∈ ℚ)
180	178, 179	mpan 687	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ₀ → (2↑𝑦) ∈ ℚ)
181	180, 29	jca 512	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ₀ → ((2↑𝑦) ∈ ℚ ∧ (2↑𝑦) ≠ 0))
182		qdivcl 12708	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℚ ∧ (2↑𝑦) ∈ ℚ ∧ (2↑𝑦) ≠ 0) → (𝑥 / (2↑𝑦)) ∈ ℚ)
183		1z 12348	. . . . . . . . . . . . . . . . . 18 ⊢ 1 ∈ ℤ
184		zq 12692	. . . . . . . . . . . . . . . . . 18 ⊢ (1 ∈ ℤ → 1 ∈ ℚ)
185	183, 184	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℚ
186		qaddcl 12703	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℚ ∧ 1 ∈ ℚ) → (𝑥 + 1) ∈ ℚ)
187	185, 186	mpan2 688	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℚ → (𝑥 + 1) ∈ ℚ)
188		qdivcl 12708	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 + 1) ∈ ℚ ∧ (2↑𝑦) ∈ ℚ ∧ (2↑𝑦) ≠ 0) → ((𝑥 + 1) / (2↑𝑦)) ∈ ℚ)
189	187, 188	syl3an1 1162	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℚ ∧ (2↑𝑦) ∈ ℚ ∧ (2↑𝑦) ≠ 0) → ((𝑥 + 1) / (2↑𝑦)) ∈ ℚ)
190		opelxpi 5628	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 / (2↑𝑦)) ∈ ℚ ∧ ((𝑥 + 1) / (2↑𝑦)) ∈ ℚ) → ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩ ∈ (ℚ × ℚ))
191	182, 189, 190	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℚ ∧ (2↑𝑦) ∈ ℚ ∧ (2↑𝑦) ≠ 0) → ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩ ∈ (ℚ × ℚ))
192	191	3expb 1119	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℚ ∧ ((2↑𝑦) ∈ ℚ ∧ (2↑𝑦) ≠ 0)) → ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩ ∈ (ℚ × ℚ))
193	175, 181, 192	syl2an 596	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ₀) → ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩ ∈ (ℚ × ℚ))
194	193	rgen2 3128	. . . . . . . . . . 11 ⊢ ∀𝑥 ∈ ℤ ∀𝑦 ∈ ℕ₀ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩ ∈ (ℚ × ℚ)
195	40	fmpo 7908	. . . . . . . . . . 11 ⊢ (∀𝑥 ∈ ℤ ∀𝑦 ∈ ℕ₀ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩ ∈ (ℚ × ℚ) ↔ (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩):(ℤ × ℕ₀)⟶(ℚ × ℚ))
196	194, 195	mpbi 229	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩):(ℤ × ℕ₀)⟶(ℚ × ℚ)
197		frn 6609	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩):(ℤ × ℕ₀)⟶(ℚ × ℚ) → ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ⊆ (ℚ × ℚ))
198	196, 197	ax-mp 5	. . . . . . . . 9 ⊢ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ⊆ (ℚ × ℚ)
199	19, 198	sstri 3931	. . . . . . . 8 ⊢ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ⊆ (ℚ × ℚ)
200	18, 199	sstri 3931	. . . . . . 7 ⊢ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ⊆ (ℚ × ℚ)
201		ssdomg 8784	. . . . . . 7 ⊢ ((ℚ × ℚ) ∈ V → ({𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ⊆ (ℚ × ℚ) → {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ≼ (ℚ × ℚ)))
202	174, 200, 201	mp2 9	. . . . . 6 ⊢ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ≼ (ℚ × ℚ)
203		qnnen 15920	. . . . . . . 8 ⊢ ℚ ≈ ℕ
204		xpen 8925	. . . . . . . 8 ⊢ ((ℚ ≈ ℕ ∧ ℚ ≈ ℕ) → (ℚ × ℚ) ≈ (ℕ × ℕ))
205	203, 203, 204	mp2an 689	. . . . . . 7 ⊢ (ℚ × ℚ) ≈ (ℕ × ℕ)
206		xpnnen 15918	. . . . . . 7 ⊢ (ℕ × ℕ) ≈ ℕ
207	205, 206	entri 8792	. . . . . 6 ⊢ (ℚ × ℚ) ≈ ℕ
208		domentr 8797	. . . . . 6 ⊢ (({𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ≼ (ℚ × ℚ) ∧ (ℚ × ℚ) ≈ ℕ) → {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ≼ ℕ)
209	202, 207, 208	mp2an 689	. . . . 5 ⊢ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ≼ ℕ
210	172, 209	jctil 520	. . . 4 ⊢ ((𝐴 ∈ (topGen‘ran (,)) ∧ 𝐴 ≠ ∅) → ({𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ≼ ℕ ∧ ¬ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ≺ ℕ))
211		bren2 8769	. . . 4 ⊢ ({𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ≈ ℕ ↔ ({𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ≼ ℕ ∧ ¬ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ≺ ℕ))
212	210, 211	sylibr 233	. . 3 ⊢ ((𝐴 ∈ (topGen‘ran (,)) ∧ 𝐴 ≠ ∅) → {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ≈ ℕ)
213	212	ensymd 8789	. 2 ⊢ ((𝐴 ∈ (topGen‘ran (,)) ∧ 𝐴 ≠ ∅) → ℕ ≈ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)})
214		bren 8741	. 2 ⊢ (ℕ ≈ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ↔ ∃𝑓 𝑓:ℕ–1-1-onto→{𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)})
215	213, 214	sylib 217	1 ⊢ ((𝐴 ∈ (topGen‘ran (,)) ∧ 𝐴 ≠ ∅) → ∃𝑓 𝑓:ℕ–1-1-onto→{𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)})

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 ∧ w3a 1086 = wceq 1539 ∃wex 1782 ∈ wcel 2106 ≠ wne 2943 ∀wral 3064 ∃wrex 3065 {crab 3068 Vcvv 3431 ⊆ wss 3888 ∅c0 4258 𝒫 cpw 4535 ⟨cop 4569 ∪ cuni 4841 ∪ ciun 4926 class class class wbr 5076 × cxp 5589 ran crn 5592 “ cima 5594 Rel wrel 5596 Fun wfun 6429 Fn wfn 6430 ⟶wf 6431 –1-1-onto→wf1o 6434 ‘cfv 6435 (class class class)co 7277 ∈ cmpo 7279 ωcom 7712 1^st c1st 7829 2^nd c2nd 7830 ≈ cen 8728 ≼ cdom 8729 ≺ csdm 8730 Fincfn 8731 ℂcc 10867 ℝcr 10868 0cc0 10869 1c1 10870 + caddc 10872 ℝ^*cxr 11006 < clt 11007 ≤ cle 11008 / cdiv 11630 ℕcn 11971 2c2 12026 ℕ₀cn0 12231 ℤcz 12317 ℚcq 12686 (,)cioo 13077 [,]cicc 13080 ↑cexp 13780 topGenctg 17146 Topctop 22040 Clsdccld 22165 Conncconn 22560

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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2709 ax-rep 5211 ax-sep 5225 ax-nul 5232 ax-pow 5290 ax-pr 5354 ax-un 7588 ax-inf2 9397 ax-cnex 10925 ax-resscn 10926 ax-1cn 10927 ax-icn 10928 ax-addcl 10929 ax-addrcl 10930 ax-mulcl 10931 ax-mulrcl 10932 ax-mulcom 10933 ax-addass 10934 ax-mulass 10935 ax-distr 10936 ax-i2m1 10937 ax-1ne0 10938 ax-1rid 10939 ax-rnegex 10940 ax-rrecex 10941 ax-cnre 10942 ax-pre-lttri 10943 ax-pre-lttrn 10944 ax-pre-ltadd 10945 ax-pre-mulgt0 10946 ax-pre-sup 10947

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2068 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3069 df-rex 3070 df-rmo 3071 df-reu 3072 df-rab 3073 df-v 3433 df-sbc 3718 df-csb 3834 df-dif 3891 df-un 3893 df-in 3895 df-ss 3905 df-pss 3907 df-nul 4259 df-if 4462 df-pw 4537 df-sn 4564 df-pr 4566 df-op 4570 df-uni 4842 df-int 4882 df-iun 4928 df-iin 4929 df-br 5077 df-opab 5139 df-mpt 5160 df-tr 5194 df-id 5491 df-eprel 5497 df-po 5505 df-so 5506 df-fr 5546 df-se 5547 df-we 5548 df-xp 5597 df-rel 5598 df-cnv 5599 df-co 5600 df-dm 5601 df-rn 5602 df-res 5603 df-ima 5604 df-pred 6204 df-ord 6271 df-on 6272 df-lim 6273 df-suc 6274 df-iota 6393 df-fun 6437 df-fn 6438 df-f 6439 df-f1 6440 df-fo 6441 df-f1o 6442 df-fv 6443 df-isom 6444 df-riota 7234 df-ov 7280 df-oprab 7281 df-mpo 7282 df-om 7713 df-1st 7831 df-2nd 7832 df-frecs 8095 df-wrecs 8126 df-recs 8200 df-rdg 8239 df-1o 8295 df-oadd 8299 df-omul 8300 df-er 8496 df-map 8615 df-en 8732 df-dom 8733 df-sdom 8734 df-fin 8735 df-fi 9168 df-sup 9199 df-inf 9200 df-oi 9267 df-card 9695 df-acn 9698 df-pnf 11009 df-mnf 11010 df-xr 11011 df-ltxr 11012 df-le 11013 df-sub 11205 df-neg 11206 df-div 11631 df-nn 11972 df-2 12034 df-3 12035 df-n0 12232 df-z 12318 df-uz 12581 df-q 12687 df-rp 12729 df-xneg 12846 df-xadd 12847 df-xmul 12848 df-ioo 13081 df-ico 13083 df-icc 13084 df-fz 13238 df-fzo 13381 df-fl 13510 df-seq 13720 df-exp 13781 df-hash 14043 df-cj 14808 df-re 14809 df-im 14810 df-sqrt 14944 df-abs 14945 df-clim 15195 df-sum 15396 df-rest 17131 df-topgen 17152 df-psmet 20587 df-xmet 20588 df-met 20589 df-bl 20590 df-mopn 20591 df-top 22041 df-topon 22058 df-bases 22094 df-cld 22168 df-cmp 22536 df-conn 22561 df-ovol 24626

This theorem is referenced by: mblfinlem2 35812

W3C validator