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 38409

Description: Lemma for ismblfin 38413, 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 11410	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℝ → (𝑛 + 1) ∈ ℝ)
2		ltp1 12082	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℝ → 𝑛 < (𝑛 + 1))
3		breq2 5107	. . . . . . . . . . . . . 14 ⊢ (𝑧 = (𝑛 + 1) → (𝑛 < 𝑧 ↔ 𝑛 < (𝑛 + 1)))
4	3	rspcev 3576	. . . . . . . . . . . . 13 ⊢ (((𝑛 + 1) ∈ ℝ ∧ 𝑛 < (𝑛 + 1)) → ∃𝑧 ∈ ℝ 𝑛 < 𝑧)
5	1, 2, 4	syl2anc 596	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑛 < 𝑧)
6	5	rgen 3078	. . . . . . . . . . 11 ⊢ ∀𝑛 ∈ ℝ ∃𝑧 ∈ ℝ 𝑛 < 𝑧
7		ltnle 11316	. . . . . . . . . . . . . . 15 ⊢ ((𝑛 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑛 < 𝑧 ↔ ¬ 𝑧 ≤ 𝑛))
8	7	rexbidva 3184	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℝ → (∃𝑧 ∈ ℝ 𝑛 < 𝑧 ↔ ∃𝑧 ∈ ℝ ¬ 𝑧 ≤ 𝑛))
9		rexnal 3114	. . . . . . . . . . . . . 14 ⊢ (∃𝑧 ∈ ℝ ¬ 𝑧 ≤ 𝑛 ↔ ¬ ∀𝑧 ∈ ℝ 𝑧 ≤ 𝑛)
10	8, 9	bitrdi 290	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℝ → (∃𝑧 ∈ ℝ 𝑛 < 𝑧 ↔ ¬ ∀𝑧 ∈ ℝ 𝑧 ≤ 𝑛))
11	10	ralbiia 3106	. . . . . . . . . . . 12 ⊢ (∀𝑛 ∈ ℝ ∃𝑧 ∈ ℝ 𝑛 < 𝑧 ↔ ∀𝑛 ∈ ℝ ¬ ∀𝑧 ∈ ℝ 𝑧 ≤ 𝑛)
12		ralnex 3088	. . . . . . . . . . . 12 ⊢ (∀𝑛 ∈ ℝ ¬ ∀𝑧 ∈ ℝ 𝑧 ≤ 𝑛 ↔ ¬ ∃𝑛 ∈ ℝ ∀𝑧 ∈ ℝ 𝑧 ≤ 𝑛)
13	11, 12	bitri 278	. . . . . . . . . . 11 ⊢ (∀𝑛 ∈ ℝ ∃𝑧 ∈ ℝ 𝑛 < 𝑧 ↔ ¬ ∃𝑛 ∈ ℝ ∀𝑧 ∈ ℝ 𝑧 ≤ 𝑛)
14	6, 13	mpbi 233	. . . . . . . . . 10 ⊢ ¬ ∃𝑛 ∈ ℝ ∀𝑧 ∈ ℝ 𝑧 ≤ 𝑛
15		raleq 3316	. . . . . . . . . . 11 ⊢ (𝐴 = ℝ → (∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑛 ↔ ∀𝑧 ∈ ℝ 𝑧 ≤ 𝑛))
16	15	rexbidv 3186	. . . . . . . . . 10 ⊢ (𝐴 = ℝ → (∃𝑛 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑛 ↔ ∃𝑛 ∈ ℝ ∀𝑧 ∈ ℝ 𝑧 ≤ 𝑛))
17	14, 16	mtbiri 330	. . . . . . . . 9 ⊢ (𝐴 = ℝ → ¬ ∃𝑛 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑛)
18		ssrab2 4028	. . . . . . . . . . . . . 14 ⊢ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ⊆ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴}
19		ssrab2 4028	. . . . . . . . . . . . . . 15 ⊢ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ⊆ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩)
20		zre 12622	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℤ → 𝑥 ∈ ℝ)
21		2re 12342	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 2 ∈ ℝ
22		reexpcl 14145	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((2 ∈ ℝ ∧ 𝑦 ∈ ℕ₀) → (2↑𝑦) ∈ ℝ)
23	21, 22	mpan 703	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ ℕ₀ → (2↑𝑦) ∈ ℝ)
24		nn0z 12642	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ ℕ₀ → 𝑦 ∈ ℤ)
25		2cn 12343	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 2 ∈ ℂ
26		2ne0 12374	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 2 ≠ 0
27		expne0i 14161	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((2 ∈ ℂ ∧ 2 ≠ 0 ∧ 𝑦 ∈ ℤ) → (2↑𝑦) ≠ 0)
28	25, 26, 27	mp3an12 1480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ ℤ → (2↑𝑦) ≠ 0)
29	24, 28	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ ℕ₀ → (2↑𝑦) ≠ 0)
30	23, 29	jca 521	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ ℕ₀ → ((2↑𝑦) ∈ ℝ ∧ (2↑𝑦) ≠ 0))
31		redivcl 11961	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ ℝ ∧ (2↑𝑦) ∈ ℝ ∧ (2↑𝑦) ≠ 0) → (𝑥 / (2↑𝑦)) ∈ ℝ)
32		peano2re 11410	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ ℝ → (𝑥 + 1) ∈ ℝ)
33		redivcl 11961	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑥 + 1) ∈ ℝ ∧ (2↑𝑦) ∈ ℝ ∧ (2↑𝑦) ≠ 0) → ((𝑥 + 1) / (2↑𝑦)) ∈ ℝ)
34	32, 33	syl3an1 1181	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ ℝ ∧ (2↑𝑦) ∈ ℝ ∧ (2↑𝑦) ≠ 0) → ((𝑥 + 1) / (2↑𝑦)) ∈ ℝ)
35		opelxpi 5692	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑥 / (2↑𝑦)) ∈ ℝ ∧ ((𝑥 + 1) / (2↑𝑦)) ∈ ℝ) → ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩ ∈ (ℝ × ℝ))
36	31, 34, 35	syl2anc 596	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ ℝ ∧ (2↑𝑦) ∈ ℝ ∧ (2↑𝑦) ≠ 0) → ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩ ∈ (ℝ × ℝ))
37	36	3expb 1138	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ ℝ ∧ ((2↑𝑦) ∈ ℝ ∧ (2↑𝑦) ≠ 0)) → ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩ ∈ (ℝ × ℝ))
38	20, 30, 37	syl2an 608	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ₀) → ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩ ∈ (ℝ × ℝ))
39	38	rgen2 3202	. . . . . . . . . . . . . . . . 17 ⊢ ∀𝑥 ∈ ℤ ∀𝑦 ∈ ℕ₀ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩ ∈ (ℝ × ℝ)
40		eqid 2760	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) = (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩)
41	40	fmpo 8066	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑥 ∈ ℤ ∀𝑦 ∈ ℕ₀ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩ ∈ (ℝ × ℝ) ↔ (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩):(ℤ × ℕ₀)⟶(ℝ × ℝ))
42	39, 41	mpbi 233	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩):(ℤ × ℕ₀)⟶(ℝ × ℝ)
43		frn 6711	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩):(ℤ × ℕ₀)⟶(ℝ × ℝ) → ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ⊆ (ℝ × ℝ))
44	42, 43	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ⊆ (ℝ × ℝ)
45	19, 44	sstri 3940	. . . . . . . . . . . . . 14 ⊢ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ⊆ (ℝ × ℝ)
46	18, 45	sstri 3940	. . . . . . . . . . . . 13 ⊢ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ⊆ (ℝ × ℝ)
47		rnss 5923	. . . . . . . . . . . . . 14 ⊢ ({𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ⊆ (ℝ × ℝ) → ran {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ⊆ ran (ℝ × ℝ))
48		rnxpid 6166	. . . . . . . . . . . . . 14 ⊢ ran (ℝ × ℝ) = ℝ
49	47, 48	sseqtrdi 3971	. . . . . . . . . . . . 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 9310	. . . . . . . . . . . 12 ⊢ ({𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ∈ Fin → ran {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ∈ Fin)
52		fimaxre2 12187	. . . . . . . . . . . 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 599	. . . . . . . . . . 11 ⊢ ({𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ∈ Fin → ∃𝑛 ∈ ℝ ∀𝑢 ∈ ran {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}𝑢 ≤ 𝑛)
54	53	adantl 487	. . . . . . . . . 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 4871	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ ∪ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}) ↔ ∃𝑢 ∈ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)})𝑧 ∈ 𝑢)
56		iccf 13504	. . . . . . . . . . . . . . . . . . 19 ⊢ [,]:(ℝ^* × ℝ^)⟶𝒫 ℝ^
57		ffn 6703	. . . . . . . . . . . . . . . . . . 19 ⊢ ([,]:(ℝ^* × ℝ^)⟶𝒫 ℝ^ → [,] Fn (ℝ^* × ℝ^*))
58	56, 57	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ [,] Fn (ℝ^* × ℝ^*)
59		rexpssxrxp 11281	. . . . . . . . . . . . . . . . . . 19 ⊢ (ℝ × ℝ) ⊆ (ℝ^* × ℝ^*)
60	46, 59	sstri 3940	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ⊆ (ℝ^* × ℝ^*)
61		eleq2 2849	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 = ([,]‘𝑣) → (𝑧 ∈ 𝑢 ↔ 𝑧 ∈ ([,]‘𝑣)))
62	61	rexima 7238	. . . . . . . . . . . . . . . . . 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 705	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑢 ∈ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)})𝑧 ∈ 𝑢 ↔ ∃𝑣 ∈ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}𝑧 ∈ ([,]‘𝑣))
64	55, 63	bitri 278	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ ∪ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}) ↔ ∃𝑣 ∈ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}𝑧 ∈ ([,]‘𝑣))
65	46	sseli 3927	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 ∈ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} → 𝑣 ∈ (ℝ × ℝ))
66		1st2nd2 8026	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑣 ∈ (ℝ × ℝ) → 𝑣 = ⟨(1^st ‘𝑣), (2^nd ‘𝑣)⟩)
67	66	fveq2d 6883	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑣 ∈ (ℝ × ℝ) → ([,]‘𝑣) = ([,]‘⟨(1^st ‘𝑣), (2^nd ‘𝑣)⟩))
68		df-ov 7417	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((1^st ‘𝑣)[,](2^nd ‘𝑣)) = ([,]‘⟨(1^st ‘𝑣), (2^nd ‘𝑣)⟩)
69	67, 68	eqtr4di 2813	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 ∈ (ℝ × ℝ) → ([,]‘𝑣) = ((1^st ‘𝑣)[,](2^nd ‘𝑣)))
70	69	eleq2d 2846	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 ∈ (ℝ × ℝ) → (𝑧 ∈ ([,]‘𝑣) ↔ 𝑧 ∈ ((1^st ‘𝑣)[,](2^nd ‘𝑣))))
71	65, 70	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑣 ∈ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} → (𝑧 ∈ ([,]‘𝑣) ↔ 𝑧 ∈ ((1^st ‘𝑣)[,](2^nd ‘𝑣))))
72	71	biimpd 232	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑣 ∈ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} → (𝑧 ∈ ([,]‘𝑣) → 𝑧 ∈ ((1^st ‘𝑣)[,](2^nd ‘𝑣))))
73	72	imdistani 579	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑣 ∈ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ∧ 𝑧 ∈ ([,]‘𝑣)) → (𝑣 ∈ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ∧ 𝑧 ∈ ((1^st ‘𝑣)[,](2^nd ‘𝑣))))
74		eliccxr 13491	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ ((1^st ‘𝑣)[,](2^nd ‘𝑣)) → 𝑧 ∈ ℝ^*)
75	74	ad2antll 742	. . . . . . . . . . . . . . . . . . 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 8020	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 ∈ (ℝ × ℝ) → (2^nd ‘𝑣) ∈ ℝ)
77	76	rexrd 11286	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 ∈ (ℝ × ℝ) → (2^nd ‘𝑣) ∈ ℝ^*)
78	65, 77	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑣 ∈ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} → (2^nd ‘𝑣) ∈ ℝ^*)
79	78	ad2antrl 741	. . . . . . . . . . . . . . . . . . 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 788	. . . . . . . . . . . . . . . . . . . 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 11286	. . . . . . . . . . . . . . . . . . 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 8019	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑣 ∈ (ℝ × ℝ) → (1^st ‘𝑣) ∈ ℝ)
83	82	rexrd 11286	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑣 ∈ (ℝ × ℝ) → (1^st ‘𝑣) ∈ ℝ^*)
84	83, 77	jca 521	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 ∈ (ℝ × ℝ) → ((1^st ‘𝑣) ∈ ℝ^* ∧ (2^nd ‘𝑣) ∈ ℝ^*))
85	65, 84	syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 ∈ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} → ((1^st ‘𝑣) ∈ ℝ^* ∧ (2^nd ‘𝑣) ∈ ℝ^*))
86		iccleub 13457	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((1^st ‘𝑣) ∈ ℝ^* ∧ (2^nd ‘𝑣) ∈ ℝ^* ∧ 𝑧 ∈ ((1^st ‘𝑣)[,](2^nd ‘𝑣))) → 𝑧 ≤ (2^nd ‘𝑣))
87	86	3expa 1136	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((1^st ‘𝑣) ∈ ℝ^* ∧ (2^nd ‘𝑣) ∈ ℝ^*) ∧ 𝑧 ∈ ((1^st ‘𝑣)[,](2^nd ‘𝑣))) → 𝑧 ≤ (2^nd ‘𝑣))
88	85, 87	sylan 592	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑣 ∈ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ∧ 𝑧 ∈ ((1^st ‘𝑣)[,](2^nd ‘𝑣))) → 𝑧 ≤ (2^nd ‘𝑣))
89	88	adantl 487	. . . . . . . . . . . . . . . . . . 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 5671	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (ℝ × ℝ) ⊆ (V × V)
91	46, 90	sstri 3940	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ⊆ (V × V)
92		df-rel 5662	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (Rel {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ↔ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ⊆ (V × V))
93	91, 92	mpbir 234	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Rel {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}
94		2ndrn 8039	. . . . . . . . . . . . . . . . . . . . . 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 703	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 ∈ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} → (2^nd ‘𝑣) ∈ ran {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)})
96		breq1 5106	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢 = (2^nd ‘𝑣) → (𝑢 ≤ 𝑛 ↔ (2^nd ‘𝑣) ≤ 𝑛))
97	96	rspccva 3575	. . . . . . . . . . . . . . . . . . . . 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 605	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((∀𝑢 ∈ ran {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}𝑢 ≤ 𝑛 ∧ 𝑣 ∈ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}) → (2^nd ‘𝑣) ≤ 𝑛)
99	98	ad2ant2lr 761	. . . . . . . . . . . . . . . . . . 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 13216	. . . . . . . . . . . . . . . . . 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 605	. . . . . . . . . . . . . . . . 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 3164	. . . . . . . . . . . . . . . 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	biimtrid 245	. . . . . . . . . . . . . . 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 3153	. . . . . . . . . . . . . 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 3316	. . . . . . . . . . . . . . 15 ⊢ (∪ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}) = 𝐴 → (∀𝑧 ∈ ∪ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)})𝑧 ≤ 𝑛 ↔ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑛))
106	105	ad2antrr 739	. . . . . . . . . . . . . 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 235	. . . . . . . . . . . . 13 ⊢ (((∪ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}) = 𝐴 ∧ 𝑛 ∈ ℝ) ∧ ∀𝑢 ∈ ran {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}𝑢 ≤ 𝑛) → ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑛)
108	107	ex 418	. . . . . . . . . . . 12 ⊢ ((∪ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}) = 𝐴 ∧ 𝑛 ∈ ℝ) → (∀𝑢 ∈ ran {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}𝑢 ≤ 𝑛 → ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑛))
109	108	reximdva 3175	. . . . . . . . . . 11 ⊢ (∪ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}) = 𝐴 → (∃𝑛 ∈ ℝ ∀𝑢 ∈ ran {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}𝑢 ≤ 𝑛 → ∃𝑛 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑛))
110	109	adantr 486	. . . . . . . . . 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 16	. . . . . . . . 9 ⊢ ((∪ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}) = 𝐴 ∧ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ∈ Fin) → ∃𝑛 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑛)
112	17, 111	nsyl 141	. . . . . . . 8 ⊢ (𝐴 = ℝ → ¬ (∪ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}) = 𝐴 ∧ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ∈ Fin))
113	112	adantl 487	. . . . . . 7 ⊢ (((𝐴 ∈ (topGen‘ran (,)) ∧ 𝐴 ≠ ∅) ∧ 𝐴 = ℝ) → ¬ (∪ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}) = 𝐴 ∧ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ∈ Fin))
114		uniretop 24991	. . . . . . . . . . 11 ⊢ ℝ = ∪ (topGen‘ran (,))
115		retopconn 25059	. . . . . . . . . . . 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 779	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ (topGen‘ran (,)) ∧ 𝐴 ≠ ∅) ∧ (∪ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}) = 𝐴 ∧ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ∈ Fin)) → 𝐴 ∈ (topGen‘ran (,)))
118		simplr 781	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ (topGen‘ran (,)) ∧ 𝐴 ≠ ∅) ∧ (∪ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}) = 𝐴 ∧ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ∈ Fin)) → 𝐴 ≠ ∅)
119		simprl 783	. . . . . . . . . . . 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 6706	. . . . . . . . . . . . . . 15 ⊢ ([,]:(ℝ^* × ℝ^)⟶𝒫 ℝ^ → Fun [,])
121		funiunfv 7246	. . . . . . . . . . . . . . 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 24990	. . . . . . . . . . . . . . 15 ⊢ (topGen‘ran (,)) ∈ Top
124	46	sseli 3927	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} → 𝑧 ∈ (ℝ × ℝ))
125		1st2nd2 8026	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ (ℝ × ℝ) → 𝑧 = ⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩)
126	125	fveq2d 6883	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ (ℝ × ℝ) → ([,]‘𝑧) = ([,]‘⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩))
127		df-ov 7417	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1^st ‘𝑧)[,](2^nd ‘𝑧)) = ([,]‘⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩)
128	126, 127	eqtr4di 2813	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ (ℝ × ℝ) → ([,]‘𝑧) = ((1^st ‘𝑧)[,](2^nd ‘𝑧)))
129		xp1st 8019	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ (ℝ × ℝ) → (1^st ‘𝑧) ∈ ℝ)
130		xp2nd 8020	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ (ℝ × ℝ) → (2^nd ‘𝑧) ∈ ℝ)
131		icccld 24995	. . . . . . . . . . . . . . . . . . 19 ⊢ (((1^st ‘𝑧) ∈ ℝ ∧ (2^nd ‘𝑧) ∈ ℝ) → ((1^st ‘𝑧)[,](2^nd ‘𝑧)) ∈ (Clsd‘(topGen‘ran (,))))
132	129, 130, 131	syl2anc 596	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ (ℝ × ℝ) → ((1^st ‘𝑧)[,](2^nd ‘𝑧)) ∈ (Clsd‘(topGen‘ran (,))))
133	128, 132	eqeltrd 2860	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ (ℝ × ℝ) → ([,]‘𝑧) ∈ (Clsd‘(topGen‘ran (,))))
134	124, 133	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} → ([,]‘𝑧) ∈ (Clsd‘(topGen‘ran (,))))
135	134	rgen 3078	. . . . . . . . . . . . . . 15 ⊢ ∀𝑧 ∈ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ([,]‘𝑧) ∈ (Clsd‘(topGen‘ran (,)))
136	114	iuncld 23273	. . . . . . . . . . . . . . 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 1481	. . . . . . . . . . . . . 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 2865	. . . . . . . . . . . . 13 ⊢ ({𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ∈ Fin → ∪ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}) ∈ (Clsd‘(topGen‘ran (,))))
139	138	ad2antll 742	. . . . . . . . . . . 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 2861	. . . . . . . . . . 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 23643	. . . . . . . . . 10 ⊢ (((𝐴 ∈ (topGen‘ran (,)) ∧ 𝐴 ≠ ∅) ∧ (∪ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}) = 𝐴 ∧ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ∈ Fin)) → 𝐴 = ℝ)
142	141	ex 418	. . . . . . . . 9 ⊢ ((𝐴 ∈ (topGen‘ran (,)) ∧ 𝐴 ≠ ∅) → ((∪ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}) = 𝐴 ∧ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ∈ Fin) → 𝐴 = ℝ))
143	142	necon3ad 2968	. . . . . . . 8 ⊢ ((𝐴 ∈ (topGen‘ran (,)) ∧ 𝐴 ≠ ∅) → (𝐴 ≠ ℝ → ¬ (∪ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}) = 𝐴 ∧ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ∈ Fin)))
144	143	imp 412	. . . . . . 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 3042	. . . . . 6 ⊢ ((𝐴 ∈ (topGen‘ran (,)) ∧ 𝐴 ≠ ∅) → ¬ (∪ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}) = 𝐴 ∧ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ∈ Fin))
146		oveq1 7421	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑢 → (𝑥 / (2↑𝑦)) = (𝑢 / (2↑𝑦)))
147		oveq1 7421	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑢 → (𝑥 + 1) = (𝑢 + 1))
148	147	oveq1d 7429	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑢 → ((𝑥 + 1) / (2↑𝑦)) = ((𝑢 + 1) / (2↑𝑦)))
149	146, 148	opeq12d 4841	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑢 → ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩ = ⟨(𝑢 / (2↑𝑦)), ((𝑢 + 1) / (2↑𝑦))⟩)
150		oveq2 7422	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑣 → (2↑𝑦) = (2↑𝑣))
151	150	oveq2d 7430	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑣 → (𝑢 / (2↑𝑦)) = (𝑢 / (2↑𝑣)))
152	150	oveq2d 7430	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑣 → ((𝑢 + 1) / (2↑𝑦)) = ((𝑢 + 1) / (2↑𝑣)))
153	151, 152	opeq12d 4841	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑣 → ⟨(𝑢 / (2↑𝑦)), ((𝑢 + 1) / (2↑𝑦))⟩ = ⟨(𝑢 / (2↑𝑣)), ((𝑢 + 1) / (2↑𝑣))⟩)
154	149, 153	cbvmpov 7509	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) = (𝑢 ∈ ℤ, 𝑣 ∈ ℕ₀ ↦ ⟨(𝑢 / (2↑𝑣)), ((𝑢 + 1) / (2↑𝑣))⟩)
155		fveq2 6879	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑧 → ([,]‘𝑎) = ([,]‘𝑧))
156	155	sseq1d 3962	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑧 → (([,]‘𝑎) ⊆ ([,]‘𝑐) ↔ ([,]‘𝑧) ⊆ ([,]‘𝑐)))
157		equequ1 2058	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑧 → (𝑎 = 𝑐 ↔ 𝑧 = 𝑐))
158	156, 157	imbi12d 347	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑧 → ((([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐) ↔ (([,]‘𝑧) ⊆ ([,]‘𝑐) → 𝑧 = 𝑐)))
159	158	ralbidv 3185	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑧 → (∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐) ↔ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑧) ⊆ ([,]‘𝑐) → 𝑧 = 𝑐)))
160	159	cbvrabv 3422	. . . . . . . . . 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 25830	. . . . . . . . 9 ⊢ (𝐴 ∈ (topGen‘ran (,)) → ∪ ([,] “ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴}) = ∪ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}))
163		opnmbllem0 38408	. . . . . . . . 9 ⊢ (𝐴 ∈ (topGen‘ran (,)) → ∪ ([,] “ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴}) = 𝐴)
164	162, 163	eqtr3d 2797	. . . . . . . 8 ⊢ (𝐴 ∈ (topGen‘ran (,)) → ∪ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}) = 𝐴)
165	164	adantr 486	. . . . . . 7 ⊢ ((𝐴 ∈ (topGen‘ran (,)) ∧ 𝐴 ≠ ∅) → ∪ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}) = 𝐴)
166		nnenom 14047	. . . . . . . . 9 ⊢ ℕ ≈ ω
167		sdomentr 9112	. . . . . . . . 9 ⊢ (({𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ≺ ℕ ∧ ℕ ≈ ω) → {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ≺ ω)
168	166, 167	mpan2 704	. . . . . . . 8 ⊢ ({𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ≺ ℕ → {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ≺ ω)
169		isfinite 9634	. . . . . . . 8 ⊢ ({𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ∈ Fin ↔ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ≺ ω)
170	168, 169	sylibr 237	. . . . . . 7 ⊢ ({𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ≺ ℕ → {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ∈ Fin)
171	165, 170	anim12i 625	. . . . . 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 828	. . . . 5 ⊢ ((𝐴 ∈ (topGen‘ran (,)) ∧ 𝐴 ≠ ∅) → ¬ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ≺ ℕ)
173		qex 13013	. . . . . . . 8 ⊢ ℚ ∈ V
174	173, 173	xpex 7753	. . . . . . 7 ⊢ (ℚ × ℚ) ∈ V
175		zq 13006	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℤ → 𝑥 ∈ ℚ)
176		2nn 12341	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℕ
177		nnq 13014	. . . . . . . . . . . . . . . 16 ⊢ (2 ∈ ℕ → 2 ∈ ℚ)
178	176, 177	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℚ
179		qexpcl 14144	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ ℚ ∧ 𝑦 ∈ ℕ₀) → (2↑𝑦) ∈ ℚ)
180	178, 179	mpan 703	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ₀ → (2↑𝑦) ∈ ℚ)
181	180, 29	jca 521	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ₀ → ((2↑𝑦) ∈ ℚ ∧ (2↑𝑦) ≠ 0))
182		qdivcl 13023	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℚ ∧ (2↑𝑦) ∈ ℚ ∧ (2↑𝑦) ≠ 0) → (𝑥 / (2↑𝑦)) ∈ ℚ)
183		1z 12651	. . . . . . . . . . . . . . . . . 18 ⊢ 1 ∈ ℤ
184		zq 13006	. . . . . . . . . . . . . . . . . 18 ⊢ (1 ∈ ℤ → 1 ∈ ℚ)
185	183, 184	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℚ
186		qaddcl 13018	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℚ ∧ 1 ∈ ℚ) → (𝑥 + 1) ∈ ℚ)
187	185, 186	mpan2 704	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℚ → (𝑥 + 1) ∈ ℚ)
188		qdivcl 13023	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 + 1) ∈ ℚ ∧ (2↑𝑦) ∈ ℚ ∧ (2↑𝑦) ≠ 0) → ((𝑥 + 1) / (2↑𝑦)) ∈ ℚ)
189	187, 188	syl3an1 1181	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℚ ∧ (2↑𝑦) ∈ ℚ ∧ (2↑𝑦) ≠ 0) → ((𝑥 + 1) / (2↑𝑦)) ∈ ℚ)
190		opelxpi 5692	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 / (2↑𝑦)) ∈ ℚ ∧ ((𝑥 + 1) / (2↑𝑦)) ∈ ℚ) → ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩ ∈ (ℚ × ℚ))
191	182, 189, 190	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℚ ∧ (2↑𝑦) ∈ ℚ ∧ (2↑𝑦) ≠ 0) → ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩ ∈ (ℚ × ℚ))
192	191	3expb 1138	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℚ ∧ ((2↑𝑦) ∈ ℚ ∧ (2↑𝑦) ≠ 0)) → ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩ ∈ (ℚ × ℚ))
193	175, 181, 192	syl2an 608	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ₀) → ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩ ∈ (ℚ × ℚ))
194	193	rgen2 3202	. . . . . . . . . . 11 ⊢ ∀𝑥 ∈ ℤ ∀𝑦 ∈ ℕ₀ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩ ∈ (ℚ × ℚ)
195	40	fmpo 8066	. . . . . . . . . . 11 ⊢ (∀𝑥 ∈ ℤ ∀𝑦 ∈ ℕ₀ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩ ∈ (ℚ × ℚ) ↔ (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩):(ℤ × ℕ₀)⟶(ℚ × ℚ))
196	194, 195	mpbi 233	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩):(ℤ × ℕ₀)⟶(ℚ × ℚ)
197		frn 6711	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩):(ℤ × ℕ₀)⟶(ℚ × ℚ) → ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ⊆ (ℚ × ℚ))
198	196, 197	ax-mp 5	. . . . . . . . 9 ⊢ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ⊆ (ℚ × ℚ)
199	19, 198	sstri 3940	. . . . . . . 8 ⊢ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ⊆ (ℚ × ℚ)
200	18, 199	sstri 3940	. . . . . . 7 ⊢ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ⊆ (ℚ × ℚ)
201		ssdomg 9009	. . . . . . 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 16304	. . . . . . . 8 ⊢ ℚ ≈ ℕ
204		xpen 9141	. . . . . . . 8 ⊢ ((ℚ ≈ ℕ ∧ ℚ ≈ ℕ) → (ℚ × ℚ) ≈ (ℕ × ℕ))
205	203, 203, 204	mp2an 705	. . . . . . 7 ⊢ (ℚ × ℚ) ≈ (ℕ × ℕ)
206		xpnnen 16302	. . . . . . 7 ⊢ (ℕ × ℕ) ≈ ℕ
207	205, 206	entri 9017	. . . . . 6 ⊢ (ℚ × ℚ) ≈ ℕ
208		domentr 9022	. . . . . 6 ⊢ (({𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ≼ (ℚ × ℚ) ∧ (ℚ × ℚ) ≈ ℕ) → {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ≼ ℕ)
209	202, 207, 208	mp2an 705	. . . . 5 ⊢ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ≼ ℕ
210	172, 209	jctil 529	. . . 4 ⊢ ((𝐴 ∈ (topGen‘ran (,)) ∧ 𝐴 ≠ ∅) → ({𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ≼ ℕ ∧ ¬ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ≺ ℕ))
211		bren2 8992	. . . 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 237	. . 3 ⊢ ((𝐴 ∈ (topGen‘ran (,)) ∧ 𝐴 ≠ ∅) → {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ≈ ℕ)
213	212	ensymd 9014	. 2 ⊢ ((𝐴 ∈ (topGen‘ran (,)) ∧ 𝐴 ≠ ∅) → ℕ ≈ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)})
214		bren 8965	. 2 ⊢ (ℕ ≈ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ↔ ∃𝑓 𝑓:ℕ–1-1-onto→{𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)})
215	213, 214	sylib 221	1 ⊢ ((𝐴 ∈ (topGen‘ran (,)) ∧ 𝐴 ≠ ∅) → ∃𝑓 𝑓:ℕ–1-1-onto→{𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)})

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∃wex 1812 ∈ wcel 2145 ≠ wne 2955 ∀wral 3076 ∃wrex 3086 {crab 3412 Vcvv 3450 ⊆ wss 3899 ∅c0 4279 𝒫 cpw 4557 ⟨cop 4590 ∪ cuni 4867 ∪ ciun 4951 class class class wbr 5103 × cxp 5653 ran crn 5656 “ cima 5658 Rel wrel 5660 Fun wfun 6527 Fn wfn 6528 ⟶wf 6529 –1-1-onto→wf1o 6532 ‘cfv 6533 (class class class)co 7414 ∈ cmpo 7416 ωcom 7863 1^st c1st 7985 2^nd c2nd 7986 ≈ cen 8952 ≼ cdom 8953 ≺ csdm 8954 Fincfn 8955 ℂcc 11125 ℝcr 11126 0cc0 11127 1c1 11128 + caddc 11130 ℝ^*cxr 11269 < clt 11270 ≤ cle 11271 / cdiv 11898 ℕcn 12260 2c2 12322 ℕ₀cn0 12531 ℤcz 12618 ℚcq 13000 (,)cioo 13401 [,]cicc 13404 ↑cexp 14128 topGenctg 17525 Topctop 23121 Clsdccld 23244 Conncconn 23639

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2732 ax-rep 5232 ax-sep 5251 ax-nul 5263 ax-pow 5330 ax-pr 5398 ax-un 7737 ax-inf2 9623 ax-cnex 11183 ax-resscn 11184 ax-1cn 11185 ax-icn 11186 ax-addcl 11187 ax-addrcl 11188 ax-mulcl 11189 ax-mulrcl 11190 ax-mulcom 11191 ax-addass 11192 ax-mulass 11193 ax-distr 11194 ax-i2m1 11195 ax-1ne0 11196 ax-1rid 11197 ax-rnegex 11198 ax-rrecex 11199 ax-cnre 11200 ax-pre-lttri 11201 ax-pre-lttrn 11202 ax-pre-ltadd 11203 ax-pre-mulgt0 11204 ax-pre-sup 11205

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-int 4908 df-iun 4953 df-iin 4954 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5550 df-eprel 5555 df-po 5563 df-so 5564 df-fr 5608 df-se 5609 df-we 5610 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-rn 5666 df-res 5667 df-ima 5668 df-pred 6299 df-ord 6360 df-on 6361 df-lim 6362 df-suc 6363 df-iota 6489 df-fun 6535 df-fn 6536 df-f 6537 df-f1 6538 df-fo 6539 df-f1o 6540 df-fv 6541 df-isom 6542 df-riota 7371 df-ov 7417 df-oprab 7418 df-mpo 7419 df-om 7864 df-1st 7987 df-2nd 7988 df-frecs 8281 df-wrecs 8312 df-recs 8361 df-rdg 8400 df-1o 8458 df-2o 8459 df-oadd 8462 df-omul 8463 df-er 8699 df-map 8831 df-en 8956 df-dom 8957 df-sdom 8958 df-fin 8959 df-fi 9384 df-sup 9415 df-inf 9416 df-oi 9485 df-card 9947 df-acn 9950 df-pnf 11272 df-mnf 11273 df-xr 11274 df-ltxr 11275 df-le 11276 df-sub 11470 df-neg 11471 df-div 11899 df-nn 12261 df-2 12330 df-3 12331 df-n0 12532 df-z 12619 df-uz 12891 df-q 13001 df-rp 13046 df-xneg 13166 df-xadd 13167 df-xmul 13168 df-ioo 13405 df-ico 13407 df-icc 13408 df-fz 13565 df-fzo 13713 df-fl 13856 df-seq 14069 df-exp 14129 df-hash 14398 df-cj 15189 df-re 15190 df-im 15191 df-sqrt 15325 df-abs 15326 df-clim 15578 df-sum 15777 df-rest 17510 df-topgen 17531 df-psmet 21580 df-xmet 21581 df-met 21582 df-bl 21583 df-mopn 21584 df-top 23122 df-topon 23139 df-bases 23174 df-cld 23247 df-cmp 23615 df-conn 23640 df-ovol 25695

This theorem is used by: mblfinlem2 38410

W3C validator