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 37995

Description: Lemma for ismblfin 37999, 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 11313	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℝ → (𝑛 + 1) ∈ ℝ)
2		ltp1 11989	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℝ → 𝑛 < (𝑛 + 1))
3		breq2 5090	. . . . . . . . . . . . . 14 ⊢ (𝑧 = (𝑛 + 1) → (𝑛 < 𝑧 ↔ 𝑛 < (𝑛 + 1)))
4	3	rspcev 3565	. . . . . . . . . . . . 13 ⊢ (((𝑛 + 1) ∈ ℝ ∧ 𝑛 < (𝑛 + 1)) → ∃𝑧 ∈ ℝ 𝑛 < 𝑧)
5	1, 2, 4	syl2anc 585	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑛 < 𝑧)
6	5	rgen 3054	. . . . . . . . . . 11 ⊢ ∀𝑛 ∈ ℝ ∃𝑧 ∈ ℝ 𝑛 < 𝑧
7		ltnle 11219	. . . . . . . . . . . . . . 15 ⊢ ((𝑛 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑛 < 𝑧 ↔ ¬ 𝑧 ≤ 𝑛))
8	7	rexbidva 3160	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℝ → (∃𝑧 ∈ ℝ 𝑛 < 𝑧 ↔ ∃𝑧 ∈ ℝ ¬ 𝑧 ≤ 𝑛))
9		rexnal 3090	. . . . . . . . . . . . . 14 ⊢ (∃𝑧 ∈ ℝ ¬ 𝑧 ≤ 𝑛 ↔ ¬ ∀𝑧 ∈ ℝ 𝑧 ≤ 𝑛)
10	8, 9	bitrdi 287	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℝ → (∃𝑧 ∈ ℝ 𝑛 < 𝑧 ↔ ¬ ∀𝑧 ∈ ℝ 𝑧 ≤ 𝑛))
11	10	ralbiia 3082	. . . . . . . . . . . 12 ⊢ (∀𝑛 ∈ ℝ ∃𝑧 ∈ ℝ 𝑛 < 𝑧 ↔ ∀𝑛 ∈ ℝ ¬ ∀𝑧 ∈ ℝ 𝑧 ≤ 𝑛)
12		ralnex 3064	. . . . . . . . . . . 12 ⊢ (∀𝑛 ∈ ℝ ¬ ∀𝑧 ∈ ℝ 𝑧 ≤ 𝑛 ↔ ¬ ∃𝑛 ∈ ℝ ∀𝑧 ∈ ℝ 𝑧 ≤ 𝑛)
13	11, 12	bitri 275	. . . . . . . . . . 11 ⊢ (∀𝑛 ∈ ℝ ∃𝑧 ∈ ℝ 𝑛 < 𝑧 ↔ ¬ ∃𝑛 ∈ ℝ ∀𝑧 ∈ ℝ 𝑧 ≤ 𝑛)
14	6, 13	mpbi 230	. . . . . . . . . 10 ⊢ ¬ ∃𝑛 ∈ ℝ ∀𝑧 ∈ ℝ 𝑧 ≤ 𝑛
15		raleq 3293	. . . . . . . . . . 11 ⊢ (𝐴 = ℝ → (∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑛 ↔ ∀𝑧 ∈ ℝ 𝑧 ≤ 𝑛))
16	15	rexbidv 3162	. . . . . . . . . 10 ⊢ (𝐴 = ℝ → (∃𝑛 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑛 ↔ ∃𝑛 ∈ ℝ ∀𝑧 ∈ ℝ 𝑧 ≤ 𝑛))
17	14, 16	mtbiri 327	. . . . . . . . 9 ⊢ (𝐴 = ℝ → ¬ ∃𝑛 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑛)
18		ssrab2 4021	. . . . . . . . . . . . . 14 ⊢ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ⊆ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴}
19		ssrab2 4021	. . . . . . . . . . . . . . 15 ⊢ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ⊆ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩)
20		zre 12522	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℤ → 𝑥 ∈ ℝ)
21		2re 12249	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 2 ∈ ℝ
22		reexpcl 14034	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((2 ∈ ℝ ∧ 𝑦 ∈ ℕ₀) → (2↑𝑦) ∈ ℝ)
23	21, 22	mpan 691	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ ℕ₀ → (2↑𝑦) ∈ ℝ)
24		nn0z 12542	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ ℕ₀ → 𝑦 ∈ ℤ)
25		2cn 12250	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 2 ∈ ℂ
26		2ne0 12279	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 2 ≠ 0
27		expne0i 14050	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((2 ∈ ℂ ∧ 2 ≠ 0 ∧ 𝑦 ∈ ℤ) → (2↑𝑦) ≠ 0)
28	25, 26, 27	mp3an12 1454	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ ℤ → (2↑𝑦) ≠ 0)
29	24, 28	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ ℕ₀ → (2↑𝑦) ≠ 0)
30	23, 29	jca 511	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ ℕ₀ → ((2↑𝑦) ∈ ℝ ∧ (2↑𝑦) ≠ 0))
31		redivcl 11868	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ ℝ ∧ (2↑𝑦) ∈ ℝ ∧ (2↑𝑦) ≠ 0) → (𝑥 / (2↑𝑦)) ∈ ℝ)
32		peano2re 11313	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ ℝ → (𝑥 + 1) ∈ ℝ)
33		redivcl 11868	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑥 + 1) ∈ ℝ ∧ (2↑𝑦) ∈ ℝ ∧ (2↑𝑦) ≠ 0) → ((𝑥 + 1) / (2↑𝑦)) ∈ ℝ)
34	32, 33	syl3an1 1164	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ ℝ ∧ (2↑𝑦) ∈ ℝ ∧ (2↑𝑦) ≠ 0) → ((𝑥 + 1) / (2↑𝑦)) ∈ ℝ)
35		opelxpi 5662	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑥 / (2↑𝑦)) ∈ ℝ ∧ ((𝑥 + 1) / (2↑𝑦)) ∈ ℝ) → ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩ ∈ (ℝ × ℝ))
36	31, 34, 35	syl2anc 585	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ ℝ ∧ (2↑𝑦) ∈ ℝ ∧ (2↑𝑦) ≠ 0) → ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩ ∈ (ℝ × ℝ))
37	36	3expb 1121	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ ℝ ∧ ((2↑𝑦) ∈ ℝ ∧ (2↑𝑦) ≠ 0)) → ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩ ∈ (ℝ × ℝ))
38	20, 30, 37	syl2an 597	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ₀) → ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩ ∈ (ℝ × ℝ))
39	38	rgen2 3178	. . . . . . . . . . . . . . . . 17 ⊢ ∀𝑥 ∈ ℤ ∀𝑦 ∈ ℕ₀ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩ ∈ (ℝ × ℝ)
40		eqid 2737	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) = (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩)
41	40	fmpo 8015	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑥 ∈ ℤ ∀𝑦 ∈ ℕ₀ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩ ∈ (ℝ × ℝ) ↔ (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩):(ℤ × ℕ₀)⟶(ℝ × ℝ))
42	39, 41	mpbi 230	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩):(ℤ × ℕ₀)⟶(ℝ × ℝ)
43		frn 6670	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩):(ℤ × ℕ₀)⟶(ℝ × ℝ) → ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ⊆ (ℝ × ℝ))
44	42, 43	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ⊆ (ℝ × ℝ)
45	19, 44	sstri 3932	. . . . . . . . . . . . . 14 ⊢ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ⊆ (ℝ × ℝ)
46	18, 45	sstri 3932	. . . . . . . . . . . . 13 ⊢ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ⊆ (ℝ × ℝ)
47		rnss 5889	. . . . . . . . . . . . . 14 ⊢ ({𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ⊆ (ℝ × ℝ) → ran {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ⊆ ran (ℝ × ℝ))
48		rnxpid 6132	. . . . . . . . . . . . . 14 ⊢ ran (ℝ × ℝ) = ℝ
49	47, 48	sseqtrdi 3963	. . . . . . . . . . . . 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 9244	. . . . . . . . . . . 12 ⊢ ({𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ∈ Fin → ran {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ∈ Fin)
52		fimaxre2 12095	. . . . . . . . . . . 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 588	. . . . . . . . . . 11 ⊢ ({𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ∈ Fin → ∃𝑛 ∈ ℝ ∀𝑢 ∈ ran {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}𝑢 ≤ 𝑛)
54	53	adantl 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↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}𝑢 ≤ 𝑛)
55		eluni2 4855	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ ∪ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}) ↔ ∃𝑢 ∈ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)})𝑧 ∈ 𝑢)
56		iccf 13395	. . . . . . . . . . . . . . . . . . 19 ⊢ [,]:(ℝ^* × ℝ^)⟶𝒫 ℝ^
57		ffn 6663	. . . . . . . . . . . . . . . . . . 19 ⊢ ([,]:(ℝ^* × ℝ^)⟶𝒫 ℝ^ → [,] Fn (ℝ^* × ℝ^*))
58	56, 57	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ [,] Fn (ℝ^* × ℝ^*)
59		rexpssxrxp 11184	. . . . . . . . . . . . . . . . . . 19 ⊢ (ℝ × ℝ) ⊆ (ℝ^* × ℝ^*)
60	46, 59	sstri 3932	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ⊆ (ℝ^* × ℝ^*)
61		eleq2 2826	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 = ([,]‘𝑣) → (𝑧 ∈ 𝑢 ↔ 𝑧 ∈ ([,]‘𝑣)))
62	61	rexima 7187	. . . . . . . . . . . . . . . . . 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 693	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑢 ∈ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)})𝑧 ∈ 𝑢 ↔ ∃𝑣 ∈ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}𝑧 ∈ ([,]‘𝑣))
64	55, 63	bitri 275	. . . . . . . . . . . . . . . 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 7975	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑣 ∈ (ℝ × ℝ) → 𝑣 = ⟨(1^st ‘𝑣), (2^nd ‘𝑣)⟩)
67	66	fveq2d 6839	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑣 ∈ (ℝ × ℝ) → ([,]‘𝑣) = ([,]‘⟨(1^st ‘𝑣), (2^nd ‘𝑣)⟩))
68		df-ov 7364	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((1^st ‘𝑣)[,](2^nd ‘𝑣)) = ([,]‘⟨(1^st ‘𝑣), (2^nd ‘𝑣)⟩)
69	67, 68	eqtr4di 2790	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 ∈ (ℝ × ℝ) → ([,]‘𝑣) = ((1^st ‘𝑣)[,](2^nd ‘𝑣)))
70	69	eleq2d 2823	. . . . . . . . . . . . . . . . . . . . 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 229	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑣 ∈ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} → (𝑧 ∈ ([,]‘𝑣) → 𝑧 ∈ ((1^st ‘𝑣)[,](2^nd ‘𝑣))))
73	72	imdistani 568	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑣 ∈ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ∧ 𝑧 ∈ ([,]‘𝑣)) → (𝑣 ∈ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ∧ 𝑧 ∈ ((1^st ‘𝑣)[,](2^nd ‘𝑣))))
74		eliccxr 13382	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ ((1^st ‘𝑣)[,](2^nd ‘𝑣)) → 𝑧 ∈ ℝ^*)
75	74	ad2antll 730	. . . . . . . . . . . . . . . . . . 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 7969	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 ∈ (ℝ × ℝ) → (2^nd ‘𝑣) ∈ ℝ)
77	76	rexrd 11189	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 ∈ (ℝ × ℝ) → (2^nd ‘𝑣) ∈ ℝ^*)
78	65, 77	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑣 ∈ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} → (2^nd ‘𝑣) ∈ ℝ^*)
79	78	ad2antrl 729	. . . . . . . . . . . . . . . . . . 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 776	. . . . . . . . . . . . . . . . . . . 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 11189	. . . . . . . . . . . . . . . . . . 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 7968	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑣 ∈ (ℝ × ℝ) → (1^st ‘𝑣) ∈ ℝ)
83	82	rexrd 11189	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑣 ∈ (ℝ × ℝ) → (1^st ‘𝑣) ∈ ℝ^*)
84	83, 77	jca 511	. . . . . . . . . . . . . . . . . . . . . 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 13348	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((1^st ‘𝑣) ∈ ℝ^* ∧ (2^nd ‘𝑣) ∈ ℝ^* ∧ 𝑧 ∈ ((1^st ‘𝑣)[,](2^nd ‘𝑣))) → 𝑧 ≤ (2^nd ‘𝑣))
87	86	3expa 1119	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((1^st ‘𝑣) ∈ ℝ^* ∧ (2^nd ‘𝑣) ∈ ℝ^*) ∧ 𝑧 ∈ ((1^st ‘𝑣)[,](2^nd ‘𝑣))) → 𝑧 ≤ (2^nd ‘𝑣))
88	85, 87	sylan 581	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑣 ∈ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ∧ 𝑧 ∈ ((1^st ‘𝑣)[,](2^nd ‘𝑣))) → 𝑧 ≤ (2^nd ‘𝑣))
89	88	adantl 481	. . . . . . . . . . . . . . . . . . 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 5641	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (ℝ × ℝ) ⊆ (V × V)
91	46, 90	sstri 3932	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ⊆ (V × V)
92		df-rel 5632	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (Rel {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ↔ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ⊆ (V × V))
93	91, 92	mpbir 231	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Rel {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}
94		2ndrn 7988	. . . . . . . . . . . . . . . . . . . . . 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 691	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 ∈ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} → (2^nd ‘𝑣) ∈ ran {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)})
96		breq1 5089	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢 = (2^nd ‘𝑣) → (𝑢 ≤ 𝑛 ↔ (2^nd ‘𝑣) ≤ 𝑛))
97	96	rspccva 3564	. . . . . . . . . . . . . . . . . . . . 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 594	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((∀𝑢 ∈ ran {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}𝑢 ≤ 𝑛 ∧ 𝑣 ∈ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}) → (2^nd ‘𝑣) ≤ 𝑛)
99	98	ad2ant2lr 749	. . . . . . . . . . . . . . . . . . 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 13107	. . . . . . . . . . . . . . . . . 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 594	. . . . . . . . . . . . . . . . 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 3140	. . . . . . . . . . . . . . . 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 242	. . . . . . . . . . . . . . 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 3129	. . . . . . . . . . . . . 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 3293	. . . . . . . . . . . . . . 15 ⊢ (∪ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}) = 𝐴 → (∀𝑧 ∈ ∪ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)})𝑧 ≤ 𝑛 ↔ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑛))
106	105	ad2antrr 727	. . . . . . . . . . . . . 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 232	. . . . . . . . . . . . 13 ⊢ (((∪ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}) = 𝐴 ∧ 𝑛 ∈ ℝ) ∧ ∀𝑢 ∈ ran {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}𝑢 ≤ 𝑛) → ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑛)
108	107	ex 412	. . . . . . . . . . . 12 ⊢ ((∪ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}) = 𝐴 ∧ 𝑛 ∈ ℝ) → (∀𝑢 ∈ ran {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}𝑢 ≤ 𝑛 → ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑛))
109	108	reximdva 3151	. . . . . . . . . . 11 ⊢ (∪ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}) = 𝐴 → (∃𝑛 ∈ ℝ ∀𝑢 ∈ ran {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}𝑢 ≤ 𝑛 → ∃𝑛 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑛))
110	109	adantr 480	. . . . . . . . . 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 481	. . . . . . 7 ⊢ (((𝐴 ∈ (topGen‘ran (,)) ∧ 𝐴 ≠ ∅) ∧ 𝐴 = ℝ) → ¬ (∪ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}) = 𝐴 ∧ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ∈ Fin))
114		uniretop 24740	. . . . . . . . . . 11 ⊢ ℝ = ∪ (topGen‘ran (,))
115		retopconn 24808	. . . . . . . . . . . 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 767	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ (topGen‘ran (,)) ∧ 𝐴 ≠ ∅) ∧ (∪ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}) = 𝐴 ∧ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ∈ Fin)) → 𝐴 ∈ (topGen‘ran (,)))
118		simplr 769	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ (topGen‘ran (,)) ∧ 𝐴 ≠ ∅) ∧ (∪ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}) = 𝐴 ∧ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ∈ Fin)) → 𝐴 ≠ ∅)
119		simprl 771	. . . . . . . . . . . 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 6666	. . . . . . . . . . . . . . 15 ⊢ ([,]:(ℝ^* × ℝ^)⟶𝒫 ℝ^ → Fun [,])
121		funiunfv 7197	. . . . . . . . . . . . . . 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 24739	. . . . . . . . . . . . . . 15 ⊢ (topGen‘ran (,)) ∈ Top
124	46	sseli 3918	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} → 𝑧 ∈ (ℝ × ℝ))
125		1st2nd2 7975	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ (ℝ × ℝ) → 𝑧 = ⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩)
126	125	fveq2d 6839	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ (ℝ × ℝ) → ([,]‘𝑧) = ([,]‘⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩))
127		df-ov 7364	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1^st ‘𝑧)[,](2^nd ‘𝑧)) = ([,]‘⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩)
128	126, 127	eqtr4di 2790	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ (ℝ × ℝ) → ([,]‘𝑧) = ((1^st ‘𝑧)[,](2^nd ‘𝑧)))
129		xp1st 7968	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ (ℝ × ℝ) → (1^st ‘𝑧) ∈ ℝ)
130		xp2nd 7969	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ (ℝ × ℝ) → (2^nd ‘𝑧) ∈ ℝ)
131		icccld 24744	. . . . . . . . . . . . . . . . . . 19 ⊢ (((1^st ‘𝑧) ∈ ℝ ∧ (2^nd ‘𝑧) ∈ ℝ) → ((1^st ‘𝑧)[,](2^nd ‘𝑧)) ∈ (Clsd‘(topGen‘ran (,))))
132	129, 130, 131	syl2anc 585	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ (ℝ × ℝ) → ((1^st ‘𝑧)[,](2^nd ‘𝑧)) ∈ (Clsd‘(topGen‘ran (,))))
133	128, 132	eqeltrd 2837	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ (ℝ × ℝ) → ([,]‘𝑧) ∈ (Clsd‘(topGen‘ran (,))))
134	124, 133	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} → ([,]‘𝑧) ∈ (Clsd‘(topGen‘ran (,))))
135	134	rgen 3054	. . . . . . . . . . . . . . 15 ⊢ ∀𝑧 ∈ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ([,]‘𝑧) ∈ (Clsd‘(topGen‘ran (,)))
136	114	iuncld 23023	. . . . . . . . . . . . . . 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 1455	. . . . . . . . . . . . . 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 2842	. . . . . . . . . . . . 13 ⊢ ({𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ∈ Fin → ∪ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}) ∈ (Clsd‘(topGen‘ran (,))))
139	138	ad2antll 730	. . . . . . . . . . . 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 2838	. . . . . . . . . . 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 23393	. . . . . . . . . 10 ⊢ (((𝐴 ∈ (topGen‘ran (,)) ∧ 𝐴 ≠ ∅) ∧ (∪ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}) = 𝐴 ∧ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ∈ Fin)) → 𝐴 = ℝ)
142	141	ex 412	. . . . . . . . 9 ⊢ ((𝐴 ∈ (topGen‘ran (,)) ∧ 𝐴 ≠ ∅) → ((∪ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}) = 𝐴 ∧ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ∈ Fin) → 𝐴 = ℝ))
143	142	necon3ad 2946	. . . . . . . 8 ⊢ ((𝐴 ∈ (topGen‘ran (,)) ∧ 𝐴 ≠ ∅) → (𝐴 ≠ ℝ → ¬ (∪ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}) = 𝐴 ∧ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ∈ Fin)))
144	143	imp 406	. . . . . . 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 3020	. . . . . 6 ⊢ ((𝐴 ∈ (topGen‘ran (,)) ∧ 𝐴 ≠ ∅) → ¬ (∪ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}) = 𝐴 ∧ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ∈ Fin))
146		oveq1 7368	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑢 → (𝑥 / (2↑𝑦)) = (𝑢 / (2↑𝑦)))
147		oveq1 7368	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑢 → (𝑥 + 1) = (𝑢 + 1))
148	147	oveq1d 7376	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑢 → ((𝑥 + 1) / (2↑𝑦)) = ((𝑢 + 1) / (2↑𝑦)))
149	146, 148	opeq12d 4825	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑢 → ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩ = ⟨(𝑢 / (2↑𝑦)), ((𝑢 + 1) / (2↑𝑦))⟩)
150		oveq2 7369	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑣 → (2↑𝑦) = (2↑𝑣))
151	150	oveq2d 7377	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑣 → (𝑢 / (2↑𝑦)) = (𝑢 / (2↑𝑣)))
152	150	oveq2d 7377	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑣 → ((𝑢 + 1) / (2↑𝑦)) = ((𝑢 + 1) / (2↑𝑣)))
153	151, 152	opeq12d 4825	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑣 → ⟨(𝑢 / (2↑𝑦)), ((𝑢 + 1) / (2↑𝑦))⟩ = ⟨(𝑢 / (2↑𝑣)), ((𝑢 + 1) / (2↑𝑣))⟩)
154	149, 153	cbvmpov 7456	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) = (𝑢 ∈ ℤ, 𝑣 ∈ ℕ₀ ↦ ⟨(𝑢 / (2↑𝑣)), ((𝑢 + 1) / (2↑𝑣))⟩)
155		fveq2 6835	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑧 → ([,]‘𝑎) = ([,]‘𝑧))
156	155	sseq1d 3954	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑧 → (([,]‘𝑎) ⊆ ([,]‘𝑐) ↔ ([,]‘𝑧) ⊆ ([,]‘𝑐)))
157		equequ1 2027	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑧 → (𝑎 = 𝑐 ↔ 𝑧 = 𝑐))
158	156, 157	imbi12d 344	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑧 → ((([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐) ↔ (([,]‘𝑧) ⊆ ([,]‘𝑐) → 𝑧 = 𝑐)))
159	158	ralbidv 3161	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑧 → (∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐) ↔ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑧) ⊆ ([,]‘𝑐) → 𝑧 = 𝑐)))
160	159	cbvrabv 3400	. . . . . . . . . 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 25579	. . . . . . . . 9 ⊢ (𝐴 ∈ (topGen‘ran (,)) → ∪ ([,] “ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴}) = ∪ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}))
163		opnmbllem0 37994	. . . . . . . . 9 ⊢ (𝐴 ∈ (topGen‘ran (,)) → ∪ ([,] “ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴}) = 𝐴)
164	162, 163	eqtr3d 2774	. . . . . . . 8 ⊢ (𝐴 ∈ (topGen‘ran (,)) → ∪ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}) = 𝐴)
165	164	adantr 480	. . . . . . 7 ⊢ ((𝐴 ∈ (topGen‘ran (,)) ∧ 𝐴 ≠ ∅) → ∪ ([,] “ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)}) = 𝐴)
166		nnenom 13936	. . . . . . . . 9 ⊢ ℕ ≈ ω
167		sdomentr 9043	. . . . . . . . 9 ⊢ (({𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ≺ ℕ ∧ ℕ ≈ ω) → {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ≺ ω)
168	166, 167	mpan2 692	. . . . . . . 8 ⊢ ({𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ≺ ℕ → {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ≺ ω)
169		isfinite 9567	. . . . . . . 8 ⊢ ({𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ∈ Fin ↔ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ≺ ω)
170	168, 169	sylibr 234	. . . . . . 7 ⊢ ({𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ≺ ℕ → {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ∈ Fin)
171	165, 170	anim12i 614	. . . . . 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 816	. . . . 5 ⊢ ((𝐴 ∈ (topGen‘ran (,)) ∧ 𝐴 ≠ ∅) → ¬ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ≺ ℕ)
173		qex 12905	. . . . . . . 8 ⊢ ℚ ∈ V
174	173, 173	xpex 7701	. . . . . . 7 ⊢ (ℚ × ℚ) ∈ V
175		zq 12898	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℤ → 𝑥 ∈ ℚ)
176		2nn 12248	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℕ
177		nnq 12906	. . . . . . . . . . . . . . . 16 ⊢ (2 ∈ ℕ → 2 ∈ ℚ)
178	176, 177	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℚ
179		qexpcl 14033	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ ℚ ∧ 𝑦 ∈ ℕ₀) → (2↑𝑦) ∈ ℚ)
180	178, 179	mpan 691	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ₀ → (2↑𝑦) ∈ ℚ)
181	180, 29	jca 511	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ₀ → ((2↑𝑦) ∈ ℚ ∧ (2↑𝑦) ≠ 0))
182		qdivcl 12914	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℚ ∧ (2↑𝑦) ∈ ℚ ∧ (2↑𝑦) ≠ 0) → (𝑥 / (2↑𝑦)) ∈ ℚ)
183		1z 12551	. . . . . . . . . . . . . . . . . 18 ⊢ 1 ∈ ℤ
184		zq 12898	. . . . . . . . . . . . . . . . . 18 ⊢ (1 ∈ ℤ → 1 ∈ ℚ)
185	183, 184	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℚ
186		qaddcl 12909	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℚ ∧ 1 ∈ ℚ) → (𝑥 + 1) ∈ ℚ)
187	185, 186	mpan2 692	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℚ → (𝑥 + 1) ∈ ℚ)
188		qdivcl 12914	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 + 1) ∈ ℚ ∧ (2↑𝑦) ∈ ℚ ∧ (2↑𝑦) ≠ 0) → ((𝑥 + 1) / (2↑𝑦)) ∈ ℚ)
189	187, 188	syl3an1 1164	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℚ ∧ (2↑𝑦) ∈ ℚ ∧ (2↑𝑦) ≠ 0) → ((𝑥 + 1) / (2↑𝑦)) ∈ ℚ)
190		opelxpi 5662	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 / (2↑𝑦)) ∈ ℚ ∧ ((𝑥 + 1) / (2↑𝑦)) ∈ ℚ) → ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩ ∈ (ℚ × ℚ))
191	182, 189, 190	syl2anc 585	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℚ ∧ (2↑𝑦) ∈ ℚ ∧ (2↑𝑦) ≠ 0) → ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩ ∈ (ℚ × ℚ))
192	191	3expb 1121	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℚ ∧ ((2↑𝑦) ∈ ℚ ∧ (2↑𝑦) ≠ 0)) → ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩ ∈ (ℚ × ℚ))
193	175, 181, 192	syl2an 597	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ₀) → ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩ ∈ (ℚ × ℚ))
194	193	rgen2 3178	. . . . . . . . . . 11 ⊢ ∀𝑥 ∈ ℤ ∀𝑦 ∈ ℕ₀ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩ ∈ (ℚ × ℚ)
195	40	fmpo 8015	. . . . . . . . . . 11 ⊢ (∀𝑥 ∈ ℤ ∀𝑦 ∈ ℕ₀ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩ ∈ (ℚ × ℚ) ↔ (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩):(ℤ × ℕ₀)⟶(ℚ × ℚ))
196	194, 195	mpbi 230	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩):(ℤ × ℕ₀)⟶(ℚ × ℚ)
197		frn 6670	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩):(ℤ × ℕ₀)⟶(ℚ × ℚ) → ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ⊆ (ℚ × ℚ))
198	196, 197	ax-mp 5	. . . . . . . . 9 ⊢ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ⊆ (ℚ × ℚ)
199	19, 198	sstri 3932	. . . . . . . 8 ⊢ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ⊆ (ℚ × ℚ)
200	18, 199	sstri 3932	. . . . . . 7 ⊢ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ⊆ (ℚ × ℚ)
201		ssdomg 8941	. . . . . . 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 16174	. . . . . . . 8 ⊢ ℚ ≈ ℕ
204		xpen 9072	. . . . . . . 8 ⊢ ((ℚ ≈ ℕ ∧ ℚ ≈ ℕ) → (ℚ × ℚ) ≈ (ℕ × ℕ))
205	203, 203, 204	mp2an 693	. . . . . . 7 ⊢ (ℚ × ℚ) ≈ (ℕ × ℕ)
206		xpnnen 16172	. . . . . . 7 ⊢ (ℕ × ℕ) ≈ ℕ
207	205, 206	entri 8949	. . . . . 6 ⊢ (ℚ × ℚ) ≈ ℕ
208		domentr 8954	. . . . . 6 ⊢ (({𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ≼ (ℚ × ℚ) ∧ (ℚ × ℚ) ≈ ℕ) → {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ≼ ℕ)
209	202, 207, 208	mp2an 693	. . . . 5 ⊢ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ≼ ℕ
210	172, 209	jctil 519	. . . 4 ⊢ ((𝐴 ∈ (topGen‘ran (,)) ∧ 𝐴 ≠ ∅) → ({𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ≼ ℕ ∧ ¬ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ≺ ℕ))
211		bren2 8924	. . . 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 234	. . 3 ⊢ ((𝐴 ∈ (topGen‘ran (,)) ∧ 𝐴 ≠ ∅) → {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ≈ ℕ)
213	212	ensymd 8946	. 2 ⊢ ((𝐴 ∈ (topGen‘ran (,)) ∧ 𝐴 ≠ ∅) → ℕ ≈ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)})
214		bren 8897	. 2 ⊢ (ℕ ≈ {𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)} ↔ ∃𝑓 𝑓:ℕ–1-1-onto→{𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)})
215	213, 214	sylib 218	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 206 ∧ wa 395 ∧ w3a 1087 = wceq 1542 ∃wex 1781 ∈ wcel 2114 ≠ wne 2933 ∀wral 3052 ∃wrex 3062 {crab 3390 Vcvv 3430 ⊆ wss 3890 ∅c0 4274 𝒫 cpw 4542 ⟨cop 4574 ∪ cuni 4851 ∪ ciun 4934 class class class wbr 5086 × cxp 5623 ran crn 5626 “ cima 5628 Rel wrel 5630 Fun wfun 6487 Fn wfn 6488 ⟶wf 6489 –1-1-onto→wf1o 6492 ‘cfv 6493 (class class class)co 7361 ∈ cmpo 7363 ωcom 7811 1^st c1st 7934 2^nd c2nd 7935 ≈ cen 8884 ≼ cdom 8885 ≺ csdm 8886 Fincfn 8887 ℂcc 11030 ℝcr 11031 0cc0 11032 1c1 11033 + caddc 11035 ℝ^*cxr 11172 < clt 11173 ≤ cle 11174 / cdiv 11801 ℕcn 12168 2c2 12230 ℕ₀cn0 12431 ℤcz 12518 ℚcq 12892 (,)cioo 13292 [,]cicc 13295 ↑cexp 14017 topGenctg 17394 Topctop 22871 Clsdccld 22994 Conncconn 23389

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5213 ax-sep 5232 ax-nul 5242 ax-pow 5303 ax-pr 5371 ax-un 7683 ax-inf2 9556 ax-cnex 11088 ax-resscn 11089 ax-1cn 11090 ax-icn 11091 ax-addcl 11092 ax-addrcl 11093 ax-mulcl 11094 ax-mulrcl 11095 ax-mulcom 11096 ax-addass 11097 ax-mulass 11098 ax-distr 11099 ax-i2m1 11100 ax-1ne0 11101 ax-1rid 11102 ax-rnegex 11103 ax-rrecex 11104 ax-cnre 11105 ax-pre-lttri 11106 ax-pre-lttrn 11107 ax-pre-ltadd 11108 ax-pre-mulgt0 11109 ax-pre-sup 11110

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rmo 3343 df-reu 3344 df-rab 3391 df-v 3432 df-sbc 3730 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-pss 3910 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-op 4575 df-uni 4852 df-int 4891 df-iun 4936 df-iin 4937 df-br 5087 df-opab 5149 df-mpt 5168 df-tr 5194 df-id 5520 df-eprel 5525 df-po 5533 df-so 5534 df-fr 5578 df-se 5579 df-we 5580 df-xp 5631 df-rel 5632 df-cnv 5633 df-co 5634 df-dm 5635 df-rn 5636 df-res 5637 df-ima 5638 df-pred 6260 df-ord 6321 df-on 6322 df-lim 6323 df-suc 6324 df-iota 6449 df-fun 6495 df-fn 6496 df-f 6497 df-f1 6498 df-fo 6499 df-f1o 6500 df-fv 6501 df-isom 6502 df-riota 7318 df-ov 7364 df-oprab 7365 df-mpo 7366 df-om 7812 df-1st 7936 df-2nd 7937 df-frecs 8225 df-wrecs 8256 df-recs 8305 df-rdg 8343 df-1o 8399 df-2o 8400 df-oadd 8403 df-omul 8404 df-er 8637 df-map 8769 df-en 8888 df-dom 8889 df-sdom 8890 df-fin 8891 df-fi 9318 df-sup 9349 df-inf 9350 df-oi 9419 df-card 9857 df-acn 9860 df-pnf 11175 df-mnf 11176 df-xr 11177 df-ltxr 11178 df-le 11179 df-sub 11373 df-neg 11374 df-div 11802 df-nn 12169 df-2 12238 df-3 12239 df-n0 12432 df-z 12519 df-uz 12783 df-q 12893 df-rp 12937 df-xneg 13057 df-xadd 13058 df-xmul 13059 df-ioo 13296 df-ico 13298 df-icc 13299 df-fz 13456 df-fzo 13603 df-fl 13745 df-seq 13958 df-exp 14018 df-hash 14287 df-cj 15055 df-re 15056 df-im 15057 df-sqrt 15191 df-abs 15192 df-clim 15444 df-sum 15643 df-rest 17379 df-topgen 17400 df-psmet 21339 df-xmet 21340 df-met 21341 df-bl 21342 df-mopn 21343 df-top 22872 df-topon 22889 df-bases 22924 df-cld 22997 df-cmp 23365 df-conn 23390 df-ovol 25444

This theorem is referenced by: mblfinlem2 37996

W3C validator