Users' Mathboxes Mathbox for Brendan Leahy < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  mblfinlem1 Structured version   Visualization version   GIF version
Theorem mblfinlem1 36514
Description: Lemma for ismblfin 36518, 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 (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)})
Distinct variable group:   π‘Ž,𝑏,𝑐,𝑓,π‘₯,𝑦,𝐴
Proof of Theorem mblfinlem1
Dummy variables 𝑛 𝑒 𝑣 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 peano2re 11384 . . . . . . . . . . . . 13 (𝑛 ∈ ℝ β†’ (𝑛 + 1) ∈ ℝ)
2 ltp1 12051 . . . . . . . . . . . . 13 (𝑛 ∈ ℝ β†’ 𝑛 < (𝑛 + 1))
3 breq2 5152 . . . . . . . . . . . . . 14 (𝑧 = (𝑛 + 1) β†’ (𝑛 < 𝑧 ↔ 𝑛 < (𝑛 + 1)))
43rspcev 3613 . . . . . . . . . . . . 13 (((𝑛 + 1) ∈ ℝ ∧ 𝑛 < (𝑛 + 1)) β†’ βˆƒπ‘§ ∈ ℝ 𝑛 < 𝑧)
51, 2, 4syl2anc 585 . . . . . . . . . . . 12 (𝑛 ∈ ℝ β†’ βˆƒπ‘§ ∈ ℝ 𝑛 < 𝑧)
65rgen 3064 . . . . . . . . . . 11 βˆ€π‘› ∈ ℝ βˆƒπ‘§ ∈ ℝ 𝑛 < 𝑧
7 ltnle 11290 . . . . . . . . . . . . . . 15 ((𝑛 ∈ ℝ ∧ 𝑧 ∈ ℝ) β†’ (𝑛 < 𝑧 ↔ Β¬ 𝑧 ≀ 𝑛))
87rexbidva 3177 . . . . . . . . . . . . . 14 (𝑛 ∈ ℝ β†’ (βˆƒπ‘§ ∈ ℝ 𝑛 < 𝑧 ↔ βˆƒπ‘§ ∈ ℝ Β¬ 𝑧 ≀ 𝑛))
9 rexnal 3101 . . . . . . . . . . . . . 14 (βˆƒπ‘§ ∈ ℝ Β¬ 𝑧 ≀ 𝑛 ↔ Β¬ βˆ€π‘§ ∈ ℝ 𝑧 ≀ 𝑛)
108, 9bitrdi 287 . . . . . . . . . . . . 13 (𝑛 ∈ ℝ β†’ (βˆƒπ‘§ ∈ ℝ 𝑛 < 𝑧 ↔ Β¬ βˆ€π‘§ ∈ ℝ 𝑧 ≀ 𝑛))
1110ralbiia 3092 . . . . . . . . . . . 12 (βˆ€π‘› ∈ ℝ βˆƒπ‘§ ∈ ℝ 𝑛 < 𝑧 ↔ βˆ€π‘› ∈ ℝ Β¬ βˆ€π‘§ ∈ ℝ 𝑧 ≀ 𝑛)
12 ralnex 3073 . . . . . . . . . . . 12 (βˆ€π‘› ∈ ℝ Β¬ βˆ€π‘§ ∈ ℝ 𝑧 ≀ 𝑛 ↔ Β¬ βˆƒπ‘› ∈ ℝ βˆ€π‘§ ∈ ℝ 𝑧 ≀ 𝑛)
1311, 12bitri 275 . . . . . . . . . . 11 (βˆ€π‘› ∈ ℝ βˆƒπ‘§ ∈ ℝ 𝑛 < 𝑧 ↔ Β¬ βˆƒπ‘› ∈ ℝ βˆ€π‘§ ∈ ℝ 𝑧 ≀ 𝑛)
146, 13mpbi 229 . . . . . . . . . 10 Β¬ βˆƒπ‘› ∈ ℝ βˆ€π‘§ ∈ ℝ 𝑧 ≀ 𝑛
15 raleq 3323 . . . . . . . . . . 11 (𝐴 = ℝ β†’ (βˆ€π‘§ ∈ 𝐴 𝑧 ≀ 𝑛 ↔ βˆ€π‘§ ∈ ℝ 𝑧 ≀ 𝑛))
1615rexbidv 3179 . . . . . . . . . 10 (𝐴 = ℝ β†’ (βˆƒπ‘› ∈ ℝ βˆ€π‘§ ∈ 𝐴 𝑧 ≀ 𝑛 ↔ βˆƒπ‘› ∈ ℝ βˆ€π‘§ ∈ ℝ 𝑧 ≀ 𝑛))
1714, 16mtbiri 327 . . . . . . . . 9 (𝐴 = ℝ β†’ Β¬ βˆƒπ‘› ∈ ℝ βˆ€π‘§ ∈ 𝐴 𝑧 ≀ 𝑛)
18 ssrab2 4077 . . . . . . . . . . . . . 14 {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} βŠ† {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴}
19 ssrab2 4077 . . . . . . . . . . . . . . 15 {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} βŠ† ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩)
20 zre 12559 . . . . . . . . . . . . . . . . . . 19 (π‘₯ ∈ β„€ β†’ π‘₯ ∈ ℝ)
21 2re 12283 . . . . . . . . . . . . . . . . . . . . 21 2 ∈ ℝ
22 reexpcl 14041 . . . . . . . . . . . . . . . . . . . . 21 ((2 ∈ ℝ ∧ 𝑦 ∈ β„•0) β†’ (2↑𝑦) ∈ ℝ)
2321, 22mpan 689 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ β„•0 β†’ (2↑𝑦) ∈ ℝ)
24 nn0z 12580 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ β„•0 β†’ 𝑦 ∈ β„€)
25 2cn 12284 . . . . . . . . . . . . . . . . . . . . . 22 2 ∈ β„‚
26 2ne0 12313 . . . . . . . . . . . . . . . . . . . . . 22 2 β‰  0
27 expne0i 14057 . . . . . . . . . . . . . . . . . . . . . 22 ((2 ∈ β„‚ ∧ 2 β‰  0 ∧ 𝑦 ∈ β„€) β†’ (2↑𝑦) β‰  0)
2825, 26, 27mp3an12 1452 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ β„€ β†’ (2↑𝑦) β‰  0)
2924, 28syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ β„•0 β†’ (2↑𝑦) β‰  0)
3023, 29jca 513 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ β„•0 β†’ ((2↑𝑦) ∈ ℝ ∧ (2↑𝑦) β‰  0))
31 redivcl 11930 . . . . . . . . . . . . . . . . . . . . 21 ((π‘₯ ∈ ℝ ∧ (2↑𝑦) ∈ ℝ ∧ (2↑𝑦) β‰  0) β†’ (π‘₯ / (2↑𝑦)) ∈ ℝ)
32 peano2re 11384 . . . . . . . . . . . . . . . . . . . . . 22 (π‘₯ ∈ ℝ β†’ (π‘₯ + 1) ∈ ℝ)
33 redivcl 11930 . . . . . . . . . . . . . . . . . . . . . 22 (((π‘₯ + 1) ∈ ℝ ∧ (2↑𝑦) ∈ ℝ ∧ (2↑𝑦) β‰  0) β†’ ((π‘₯ + 1) / (2↑𝑦)) ∈ ℝ)
3432, 33syl3an1 1164 . . . . . . . . . . . . . . . . . . . . 21 ((π‘₯ ∈ ℝ ∧ (2↑𝑦) ∈ ℝ ∧ (2↑𝑦) β‰  0) β†’ ((π‘₯ + 1) / (2↑𝑦)) ∈ ℝ)
35 opelxpi 5713 . . . . . . . . . . . . . . . . . . . . 21 (((π‘₯ / (2↑𝑦)) ∈ ℝ ∧ ((π‘₯ + 1) / (2↑𝑦)) ∈ ℝ) β†’ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩ ∈ (ℝ Γ— ℝ))
3631, 34, 35syl2anc 585 . . . . . . . . . . . . . . . . . . . 20 ((π‘₯ ∈ ℝ ∧ (2↑𝑦) ∈ ℝ ∧ (2↑𝑦) β‰  0) β†’ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩ ∈ (ℝ Γ— ℝ))
37363expb 1121 . . . . . . . . . . . . . . . . . . 19 ((π‘₯ ∈ ℝ ∧ ((2↑𝑦) ∈ ℝ ∧ (2↑𝑦) β‰  0)) β†’ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩ ∈ (ℝ Γ— ℝ))
3820, 30, 37syl2an 597 . . . . . . . . . . . . . . . . . 18 ((π‘₯ ∈ β„€ ∧ 𝑦 ∈ β„•0) β†’ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩ ∈ (ℝ Γ— ℝ))
3938rgen2 3198 . . . . . . . . . . . . . . . . 17 βˆ€π‘₯ ∈ β„€ βˆ€π‘¦ ∈ β„•0 ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩ ∈ (ℝ Γ— ℝ)
40 eqid 2733 . . . . . . . . . . . . . . . . . 18 (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) = (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩)
4140fmpo 8051 . . . . . . . . . . . . . . . . 17 (βˆ€π‘₯ ∈ β„€ βˆ€π‘¦ ∈ β„•0 ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩ ∈ (ℝ Γ— ℝ) ↔ (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩):(β„€ Γ— β„•0)⟢(ℝ Γ— ℝ))
4239, 41mpbi 229 . . . . . . . . . . . . . . . 16 (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩):(β„€ Γ— β„•0)⟢(ℝ Γ— ℝ)
43 frn 6722 . . . . . . . . . . . . . . . 16 ((π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩):(β„€ Γ— β„•0)⟢(ℝ Γ— ℝ) β†’ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) βŠ† (ℝ Γ— ℝ))
4442, 43ax-mp 5 . . . . . . . . . . . . . . 15 ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) βŠ† (ℝ Γ— ℝ)
4519, 44sstri 3991 . . . . . . . . . . . . . 14 {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} βŠ† (ℝ Γ— ℝ)
4618, 45sstri 3991 . . . . . . . . . . . . 13 {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} βŠ† (ℝ Γ— ℝ)
47 rnss 5937 . . . . . . . . . . . . . 14 ({π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} βŠ† (ℝ Γ— ℝ) β†’ ran {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} βŠ† ran (ℝ Γ— ℝ))
48 rnxpid 6170 . . . . . . . . . . . . . 14 ran (ℝ Γ— ℝ) = ℝ
4947, 48sseqtrdi 4032 . . . . . . . . . . . . 13 ({π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} βŠ† (ℝ Γ— ℝ) β†’ ran {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} βŠ† ℝ)
5046, 49ax-mp 5 . . . . . . . . . . . 12 ran {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} βŠ† ℝ
51 rnfi 9332 . . . . . . . . . . . 12 ({π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} ∈ Fin β†’ ran {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} ∈ Fin)
52 fimaxre2 12156 . . . . . . . . . . . 12 ((ran {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} βŠ† ℝ ∧ ran {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} ∈ Fin) β†’ βˆƒπ‘› ∈ ℝ βˆ€π‘’ ∈ ran {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)}𝑒 ≀ 𝑛)
5350, 51, 52sylancr 588 . . . . . . . . . . 11 ({π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} ∈ Fin β†’ βˆƒπ‘› ∈ ℝ βˆ€π‘’ ∈ ran {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)}𝑒 ≀ 𝑛)
5453adantl 483 . . . . . . . . . 10 ((βˆͺ ([,] β€œ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)}) = 𝐴 ∧ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} ∈ Fin) β†’ βˆƒπ‘› ∈ ℝ βˆ€π‘’ ∈ ran {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)}𝑒 ≀ 𝑛)
55 eluni2 4912 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ βˆͺ ([,] β€œ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)}) ↔ βˆƒπ‘’ ∈ ([,] β€œ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)})𝑧 ∈ 𝑒)
56 iccf 13422 . . . . . . . . . . . . . . . . . . 19 [,]:(ℝ* Γ— ℝ*)βŸΆπ’« ℝ*
57 ffn 6715 . . . . . . . . . . . . . . . . . . 19 ([,]:(ℝ* Γ— ℝ*)βŸΆπ’« ℝ* β†’ [,] Fn (ℝ* Γ— ℝ*))
5856, 57ax-mp 5 . . . . . . . . . . . . . . . . . 18 [,] Fn (ℝ* Γ— ℝ*)
59 rexpssxrxp 11256 . . . . . . . . . . . . . . . . . . 19 (ℝ Γ— ℝ) βŠ† (ℝ* Γ— ℝ*)
6046, 59sstri 3991 . . . . . . . . . . . . . . . . . 18 {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} βŠ† (ℝ* Γ— ℝ*)
61 eleq2 2823 . . . . . . . . . . . . . . . . . . 19 (𝑒 = ([,]β€˜π‘£) β†’ (𝑧 ∈ 𝑒 ↔ 𝑧 ∈ ([,]β€˜π‘£)))
6261rexima 7236 . . . . . . . . . . . . . . . . . 18 (([,] Fn (ℝ* Γ— ℝ*) ∧ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} βŠ† (ℝ* Γ— ℝ*)) β†’ (βˆƒπ‘’ ∈ ([,] β€œ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)})𝑧 ∈ 𝑒 ↔ βˆƒπ‘£ ∈ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)}𝑧 ∈ ([,]β€˜π‘£)))
6358, 60, 62mp2an 691 . . . . . . . . . . . . . . . . 17 (βˆƒπ‘’ ∈ ([,] β€œ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)})𝑧 ∈ 𝑒 ↔ βˆƒπ‘£ ∈ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)}𝑧 ∈ ([,]β€˜π‘£))
6455, 63bitri 275 . . . . . . . . . . . . . . . 16 (𝑧 ∈ βˆͺ ([,] β€œ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)}) ↔ βˆƒπ‘£ ∈ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)}𝑧 ∈ ([,]β€˜π‘£))
6546sseli 3978 . . . . . . . . . . . . . . . . . . . . 21 (𝑣 ∈ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} β†’ 𝑣 ∈ (ℝ Γ— ℝ))
66 1st2nd2 8011 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑣 ∈ (ℝ Γ— ℝ) β†’ 𝑣 = ⟨(1st β€˜π‘£), (2nd β€˜π‘£)⟩)
6766fveq2d 6893 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑣 ∈ (ℝ Γ— ℝ) β†’ ([,]β€˜π‘£) = ([,]β€˜βŸ¨(1st β€˜π‘£), (2nd β€˜π‘£)⟩))
68 df-ov 7409 . . . . . . . . . . . . . . . . . . . . . . 23 ((1st β€˜π‘£)[,](2nd β€˜π‘£)) = ([,]β€˜βŸ¨(1st β€˜π‘£), (2nd β€˜π‘£)⟩)
6967, 68eqtr4di 2791 . . . . . . . . . . . . . . . . . . . . . 22 (𝑣 ∈ (ℝ Γ— ℝ) β†’ ([,]β€˜π‘£) = ((1st β€˜π‘£)[,](2nd β€˜π‘£)))
7069eleq2d 2820 . . . . . . . . . . . . . . . . . . . . 21 (𝑣 ∈ (ℝ Γ— ℝ) β†’ (𝑧 ∈ ([,]β€˜π‘£) ↔ 𝑧 ∈ ((1st β€˜π‘£)[,](2nd β€˜π‘£))))
7165, 70syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝑣 ∈ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} β†’ (𝑧 ∈ ([,]β€˜π‘£) ↔ 𝑧 ∈ ((1st β€˜π‘£)[,](2nd β€˜π‘£))))
7271biimpd 228 . . . . . . . . . . . . . . . . . . 19 (𝑣 ∈ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} β†’ (𝑧 ∈ ([,]β€˜π‘£) β†’ 𝑧 ∈ ((1st β€˜π‘£)[,](2nd β€˜π‘£))))
7372imdistani 570 . . . . . . . . . . . . . . . . . 18 ((𝑣 ∈ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} ∧ 𝑧 ∈ ([,]β€˜π‘£)) β†’ (𝑣 ∈ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} ∧ 𝑧 ∈ ((1st β€˜π‘£)[,](2nd β€˜π‘£))))
74 eliccxr 13409 . . . . . . . . . . . . . . . . . . . 20 (𝑧 ∈ ((1st β€˜π‘£)[,](2nd β€˜π‘£)) β†’ 𝑧 ∈ ℝ*)
7574ad2antll 728 . . . . . . . . . . . . . . . . . . 19 ((((βˆͺ ([,] β€œ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)}) = 𝐴 ∧ 𝑛 ∈ ℝ) ∧ βˆ€π‘’ ∈ ran {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)}𝑒 ≀ 𝑛) ∧ (𝑣 ∈ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} ∧ 𝑧 ∈ ((1st β€˜π‘£)[,](2nd β€˜π‘£)))) β†’ 𝑧 ∈ ℝ*)
76 xp2nd 8005 . . . . . . . . . . . . . . . . . . . . . 22 (𝑣 ∈ (ℝ Γ— ℝ) β†’ (2nd β€˜π‘£) ∈ ℝ)
7776rexrd 11261 . . . . . . . . . . . . . . . . . . . . 21 (𝑣 ∈ (ℝ Γ— ℝ) β†’ (2nd β€˜π‘£) ∈ ℝ*)
7865, 77syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝑣 ∈ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} β†’ (2nd β€˜π‘£) ∈ ℝ*)
7978ad2antrl 727 . . . . . . . . . . . . . . . . . . 19 ((((βˆͺ ([,] β€œ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)}) = 𝐴 ∧ 𝑛 ∈ ℝ) ∧ βˆ€π‘’ ∈ ran {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)}𝑒 ≀ 𝑛) ∧ (𝑣 ∈ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} ∧ 𝑧 ∈ ((1st β€˜π‘£)[,](2nd β€˜π‘£)))) β†’ (2nd β€˜π‘£) ∈ ℝ*)
80 simpllr 775 . . . . . . . . . . . . . . . . . . . 20 ((((βˆͺ ([,] β€œ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)}) = 𝐴 ∧ 𝑛 ∈ ℝ) ∧ βˆ€π‘’ ∈ ran {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)}𝑒 ≀ 𝑛) ∧ (𝑣 ∈ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} ∧ 𝑧 ∈ ((1st β€˜π‘£)[,](2nd β€˜π‘£)))) β†’ 𝑛 ∈ ℝ)
8180rexrd 11261 . . . . . . . . . . . . . . . . . . 19 ((((βˆͺ ([,] β€œ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)}) = 𝐴 ∧ 𝑛 ∈ ℝ) ∧ βˆ€π‘’ ∈ ran {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)}𝑒 ≀ 𝑛) ∧ (𝑣 ∈ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} ∧ 𝑧 ∈ ((1st β€˜π‘£)[,](2nd β€˜π‘£)))) β†’ 𝑛 ∈ ℝ*)
82 xp1st 8004 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑣 ∈ (ℝ Γ— ℝ) β†’ (1st β€˜π‘£) ∈ ℝ)
8382rexrd 11261 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑣 ∈ (ℝ Γ— ℝ) β†’ (1st β€˜π‘£) ∈ ℝ*)
8483, 77jca 513 . . . . . . . . . . . . . . . . . . . . . 22 (𝑣 ∈ (ℝ Γ— ℝ) β†’ ((1st β€˜π‘£) ∈ ℝ* ∧ (2nd β€˜π‘£) ∈ ℝ*))
8565, 84syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝑣 ∈ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} β†’ ((1st β€˜π‘£) ∈ ℝ* ∧ (2nd β€˜π‘£) ∈ ℝ*))
86 iccleub 13376 . . . . . . . . . . . . . . . . . . . . . 22 (((1st β€˜π‘£) ∈ ℝ* ∧ (2nd β€˜π‘£) ∈ ℝ* ∧ 𝑧 ∈ ((1st β€˜π‘£)[,](2nd β€˜π‘£))) β†’ 𝑧 ≀ (2nd β€˜π‘£))
87863expa 1119 . . . . . . . . . . . . . . . . . . . . 21 ((((1st β€˜π‘£) ∈ ℝ* ∧ (2nd β€˜π‘£) ∈ ℝ*) ∧ 𝑧 ∈ ((1st β€˜π‘£)[,](2nd β€˜π‘£))) β†’ 𝑧 ≀ (2nd β€˜π‘£))
8885, 87sylan 581 . . . . . . . . . . . . . . . . . . . 20 ((𝑣 ∈ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} ∧ 𝑧 ∈ ((1st β€˜π‘£)[,](2nd β€˜π‘£))) β†’ 𝑧 ≀ (2nd β€˜π‘£))
8988adantl 483 . . . . . . . . . . . . . . . . . . 19 ((((βˆͺ ([,] β€œ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)}) = 𝐴 ∧ 𝑛 ∈ ℝ) ∧ βˆ€π‘’ ∈ ran {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)}𝑒 ≀ 𝑛) ∧ (𝑣 ∈ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} ∧ 𝑧 ∈ ((1st β€˜π‘£)[,](2nd β€˜π‘£)))) β†’ 𝑧 ≀ (2nd β€˜π‘£))
90 xpss 5692 . . . . . . . . . . . . . . . . . . . . . . . 24 (ℝ Γ— ℝ) βŠ† (V Γ— V)
9146, 90sstri 3991 . . . . . . . . . . . . . . . . . . . . . . 23 {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} βŠ† (V Γ— V)
92 df-rel 5683 . . . . . . . . . . . . . . . . . . . . . . 23 (Rel {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} ↔ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} βŠ† (V Γ— V))
9391, 92mpbir 230 . . . . . . . . . . . . . . . . . . . . . 22 Rel {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)}
94 2ndrn 8024 . . . . . . . . . . . . . . . . . . . . . 22 ((Rel {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} ∧ 𝑣 ∈ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)}) β†’ (2nd β€˜π‘£) ∈ ran {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)})
9593, 94mpan 689 . . . . . . . . . . . . . . . . . . . . 21 (𝑣 ∈ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} β†’ (2nd β€˜π‘£) ∈ ran {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)})
96 breq1 5151 . . . . . . . . . . . . . . . . . . . . . 22 (𝑒 = (2nd β€˜π‘£) β†’ (𝑒 ≀ 𝑛 ↔ (2nd β€˜π‘£) ≀ 𝑛))
9796rspccva 3612 . . . . . . . . . . . . . . . . . . . . 21 ((βˆ€π‘’ ∈ ran {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)}𝑒 ≀ 𝑛 ∧ (2nd β€˜π‘£) ∈ ran {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)}) β†’ (2nd β€˜π‘£) ≀ 𝑛)
9895, 97sylan2 594 . . . . . . . . . . . . . . . . . . . 20 ((βˆ€π‘’ ∈ ran {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)}𝑒 ≀ 𝑛 ∧ 𝑣 ∈ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)}) β†’ (2nd β€˜π‘£) ≀ 𝑛)
9998ad2ant2lr 747 . . . . . . . . . . . . . . . . . . 19 ((((βˆͺ ([,] β€œ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)}) = 𝐴 ∧ 𝑛 ∈ ℝ) ∧ βˆ€π‘’ ∈ ran {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)}𝑒 ≀ 𝑛) ∧ (𝑣 ∈ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} ∧ 𝑧 ∈ ((1st β€˜π‘£)[,](2nd β€˜π‘£)))) β†’ (2nd β€˜π‘£) ≀ 𝑛)
10075, 79, 81, 89, 99xrletrd 13138 . . . . . . . . . . . . . . . . . 18 ((((βˆͺ ([,] β€œ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)}) = 𝐴 ∧ 𝑛 ∈ ℝ) ∧ βˆ€π‘’ ∈ ran {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)}𝑒 ≀ 𝑛) ∧ (𝑣 ∈ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} ∧ 𝑧 ∈ ((1st β€˜π‘£)[,](2nd β€˜π‘£)))) β†’ 𝑧 ≀ 𝑛)
10173, 100sylan2 594 . . . . . . . . . . . . . . . . 17 ((((βˆͺ ([,] β€œ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)}) = 𝐴 ∧ 𝑛 ∈ ℝ) ∧ βˆ€π‘’ ∈ ran {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)}𝑒 ≀ 𝑛) ∧ (𝑣 ∈ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} ∧ 𝑧 ∈ ([,]β€˜π‘£))) β†’ 𝑧 ≀ 𝑛)
102101rexlimdvaa 3157 . . . . . . . . . . . . . . . 16 (((βˆͺ ([,] β€œ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)}) = 𝐴 ∧ 𝑛 ∈ ℝ) ∧ βˆ€π‘’ ∈ ran {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)}𝑒 ≀ 𝑛) β†’ (βˆƒπ‘£ ∈ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)}𝑧 ∈ ([,]β€˜π‘£) β†’ 𝑧 ≀ 𝑛))
10364, 102biimtrid 241 . . . . . . . . . . . . . . 15 (((βˆͺ ([,] β€œ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)}) = 𝐴 ∧ 𝑛 ∈ ℝ) ∧ βˆ€π‘’ ∈ ran {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)}𝑒 ≀ 𝑛) β†’ (𝑧 ∈ βˆͺ ([,] β€œ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)}) β†’ 𝑧 ≀ 𝑛))
104103ralrimiv 3146 . . . . . . . . . . . . . 14 (((βˆͺ ([,] β€œ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)}) = 𝐴 ∧ 𝑛 ∈ ℝ) ∧ βˆ€π‘’ ∈ ran {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)}𝑒 ≀ 𝑛) β†’ βˆ€π‘§ ∈ βˆͺ ([,] β€œ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)})𝑧 ≀ 𝑛)
105 raleq 3323 . . . . . . . . . . . . . . 15 (βˆͺ ([,] β€œ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)}) = 𝐴 β†’ (βˆ€π‘§ ∈ βˆͺ ([,] β€œ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)})𝑧 ≀ 𝑛 ↔ βˆ€π‘§ ∈ 𝐴 𝑧 ≀ 𝑛))
106105ad2antrr 725 . . . . . . . . . . . . . 14 (((βˆͺ ([,] β€œ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)}) = 𝐴 ∧ 𝑛 ∈ ℝ) ∧ βˆ€π‘’ ∈ ran {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)}𝑒 ≀ 𝑛) β†’ (βˆ€π‘§ ∈ βˆͺ ([,] β€œ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)})𝑧 ≀ 𝑛 ↔ βˆ€π‘§ ∈ 𝐴 𝑧 ≀ 𝑛))
107104, 106mpbid 231 . . . . . . . . . . . . 13 (((βˆͺ ([,] β€œ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)}) = 𝐴 ∧ 𝑛 ∈ ℝ) ∧ βˆ€π‘’ ∈ ran {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)}𝑒 ≀ 𝑛) β†’ βˆ€π‘§ ∈ 𝐴 𝑧 ≀ 𝑛)
108107ex 414 . . . . . . . . . . . 12 ((βˆͺ ([,] β€œ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)}) = 𝐴 ∧ 𝑛 ∈ ℝ) β†’ (βˆ€π‘’ ∈ ran {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)}𝑒 ≀ 𝑛 β†’ βˆ€π‘§ ∈ 𝐴 𝑧 ≀ 𝑛))
109108reximdva 3169 . . . . . . . . . . 11 (βˆͺ ([,] β€œ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)}) = 𝐴 β†’ (βˆƒπ‘› ∈ ℝ βˆ€π‘’ ∈ ran {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)}𝑒 ≀ 𝑛 β†’ βˆƒπ‘› ∈ ℝ βˆ€π‘§ ∈ 𝐴 𝑧 ≀ 𝑛))
110109adantr 482 . . . . . . . . . 10 ((βˆͺ ([,] β€œ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)}) = 𝐴 ∧ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} ∈ Fin) β†’ (βˆƒπ‘› ∈ ℝ βˆ€π‘’ ∈ ran {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)}𝑒 ≀ 𝑛 β†’ βˆƒπ‘› ∈ ℝ βˆ€π‘§ ∈ 𝐴 𝑧 ≀ 𝑛))
11154, 110mpd 15 . . . . . . . . 9 ((βˆͺ ([,] β€œ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)}) = 𝐴 ∧ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} ∈ Fin) β†’ βˆƒπ‘› ∈ ℝ βˆ€π‘§ ∈ 𝐴 𝑧 ≀ 𝑛)
11217, 111nsyl 140 . . . . . . . 8 (𝐴 = ℝ β†’ Β¬ (βˆͺ ([,] β€œ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)}) = 𝐴 ∧ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} ∈ Fin))
113112adantl 483 . . . . . . 7 (((𝐴 ∈ (topGenβ€˜ran (,)) ∧ 𝐴 β‰  βˆ…) ∧ 𝐴 = ℝ) β†’ Β¬ (βˆͺ ([,] β€œ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)}) = 𝐴 ∧ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} ∈ Fin))
114 uniretop 24271 . . . . . . . . . . 11 ℝ = βˆͺ (topGenβ€˜ran (,))
115 retopconn 24337 . . . . . . . . . . . 12 (topGenβ€˜ran (,)) ∈ Conn
116115a1i 11 . . . . . . . . . . 11 (((𝐴 ∈ (topGenβ€˜ran (,)) ∧ 𝐴 β‰  βˆ…) ∧ (βˆͺ ([,] β€œ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)}) = 𝐴 ∧ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} ∈ Fin)) β†’ (topGenβ€˜ran (,)) ∈ Conn)
117 simpll 766 . . . . . . . . . . 11 (((𝐴 ∈ (topGenβ€˜ran (,)) ∧ 𝐴 β‰  βˆ…) ∧ (βˆͺ ([,] β€œ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)}) = 𝐴 ∧ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} ∈ Fin)) β†’ 𝐴 ∈ (topGenβ€˜ran (,)))
118 simplr 768 . . . . . . . . . . 11 (((𝐴 ∈ (topGenβ€˜ran (,)) ∧ 𝐴 β‰  βˆ…) ∧ (βˆͺ ([,] β€œ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)}) = 𝐴 ∧ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} ∈ Fin)) β†’ 𝐴 β‰  βˆ…)
119 simprl 770 . . . . . . . . . . . 12 (((𝐴 ∈ (topGenβ€˜ran (,)) ∧ 𝐴 β‰  βˆ…) ∧ (βˆͺ ([,] β€œ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)}) = 𝐴 ∧ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} ∈ Fin)) β†’ βˆͺ ([,] β€œ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)}) = 𝐴)
120 ffun 6718 . . . . . . . . . . . . . . 15 ([,]:(ℝ* Γ— ℝ*)βŸΆπ’« ℝ* β†’ Fun [,])
121 funiunfv 7244 . . . . . . . . . . . . . . 15 (Fun [,] β†’ βˆͺ 𝑧 ∈ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} ([,]β€˜π‘§) = βˆͺ ([,] β€œ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)}))
12256, 120, 121mp2b 10 . . . . . . . . . . . . . 14 βˆͺ 𝑧 ∈ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} ([,]β€˜π‘§) = βˆͺ ([,] β€œ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)})
123 retop 24270 . . . . . . . . . . . . . . 15 (topGenβ€˜ran (,)) ∈ Top
12446sseli 3978 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} β†’ 𝑧 ∈ (ℝ Γ— ℝ))
125 1st2nd2 8011 . . . . . . . . . . . . . . . . . . . 20 (𝑧 ∈ (ℝ Γ— ℝ) β†’ 𝑧 = ⟨(1st β€˜π‘§), (2nd β€˜π‘§)⟩)
126125fveq2d 6893 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ (ℝ Γ— ℝ) β†’ ([,]β€˜π‘§) = ([,]β€˜βŸ¨(1st β€˜π‘§), (2nd β€˜π‘§)⟩))
127 df-ov 7409 . . . . . . . . . . . . . . . . . . 19 ((1st β€˜π‘§)[,](2nd β€˜π‘§)) = ([,]β€˜βŸ¨(1st β€˜π‘§), (2nd β€˜π‘§)⟩)
128126, 127eqtr4di 2791 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ (ℝ Γ— ℝ) β†’ ([,]β€˜π‘§) = ((1st β€˜π‘§)[,](2nd β€˜π‘§)))
129 xp1st 8004 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ (ℝ Γ— ℝ) β†’ (1st β€˜π‘§) ∈ ℝ)
130 xp2nd 8005 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ (ℝ Γ— ℝ) β†’ (2nd β€˜π‘§) ∈ ℝ)
131 icccld 24275 . . . . . . . . . . . . . . . . . . 19 (((1st β€˜π‘§) ∈ ℝ ∧ (2nd β€˜π‘§) ∈ ℝ) β†’ ((1st β€˜π‘§)[,](2nd β€˜π‘§)) ∈ (Clsdβ€˜(topGenβ€˜ran (,))))
132129, 130, 131syl2anc 585 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ (ℝ Γ— ℝ) β†’ ((1st β€˜π‘§)[,](2nd β€˜π‘§)) ∈ (Clsdβ€˜(topGenβ€˜ran (,))))
133128, 132eqeltrd 2834 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ (ℝ Γ— ℝ) β†’ ([,]β€˜π‘§) ∈ (Clsdβ€˜(topGenβ€˜ran (,))))
134124, 133syl 17 . . . . . . . . . . . . . . . 16 (𝑧 ∈ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} β†’ ([,]β€˜π‘§) ∈ (Clsdβ€˜(topGenβ€˜ran (,))))
135134rgen 3064 . . . . . . . . . . . . . . 15 βˆ€π‘§ ∈ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} ([,]β€˜π‘§) ∈ (Clsdβ€˜(topGenβ€˜ran (,)))
136114iuncld 22541 . . . . . . . . . . . . . . 15 (((topGenβ€˜ran (,)) ∈ Top ∧ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} ∈ Fin ∧ βˆ€π‘§ ∈ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} ([,]β€˜π‘§) ∈ (Clsdβ€˜(topGenβ€˜ran (,)))) β†’ βˆͺ 𝑧 ∈ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} ([,]β€˜π‘§) ∈ (Clsdβ€˜(topGenβ€˜ran (,))))
137123, 135, 136mp3an13 1453 . . . . . . . . . . . . . 14 ({π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} ∈ Fin β†’ βˆͺ 𝑧 ∈ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} ([,]β€˜π‘§) ∈ (Clsdβ€˜(topGenβ€˜ran (,))))
138122, 137eqeltrrid 2839 . . . . . . . . . . . . 13 ({π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} ∈ Fin β†’ βˆͺ ([,] β€œ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)}) ∈ (Clsdβ€˜(topGenβ€˜ran (,))))
139138ad2antll 728 . . . . . . . . . . . 12 (((𝐴 ∈ (topGenβ€˜ran (,)) ∧ 𝐴 β‰  βˆ…) ∧ (βˆͺ ([,] β€œ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)}) = 𝐴 ∧ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} ∈ Fin)) β†’ βˆͺ ([,] β€œ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)}) ∈ (Clsdβ€˜(topGenβ€˜ran (,))))
140119, 139eqeltrrd 2835 . . . . . . . . . . 11 (((𝐴 ∈ (topGenβ€˜ran (,)) ∧ 𝐴 β‰  βˆ…) ∧ (βˆͺ ([,] β€œ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)}) = 𝐴 ∧ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} ∈ Fin)) β†’ 𝐴 ∈ (Clsdβ€˜(topGenβ€˜ran (,))))
141114, 116, 117, 118, 140connclo 22911 . . . . . . . . . 10 (((𝐴 ∈ (topGenβ€˜ran (,)) ∧ 𝐴 β‰  βˆ…) ∧ (βˆͺ ([,] β€œ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)}) = 𝐴 ∧ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} ∈ Fin)) β†’ 𝐴 = ℝ)
142141ex 414 . . . . . . . . 9 ((𝐴 ∈ (topGenβ€˜ran (,)) ∧ 𝐴 β‰  βˆ…) β†’ ((βˆͺ ([,] β€œ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)}) = 𝐴 ∧ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} ∈ Fin) β†’ 𝐴 = ℝ))
143142necon3ad 2954 . . . . . . . 8 ((𝐴 ∈ (topGenβ€˜ran (,)) ∧ 𝐴 β‰  βˆ…) β†’ (𝐴 β‰  ℝ β†’ Β¬ (βˆͺ ([,] β€œ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)}) = 𝐴 ∧ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} ∈ Fin)))
144143imp 408 . . . . . . 7 (((𝐴 ∈ (topGenβ€˜ran (,)) ∧ 𝐴 β‰  βˆ…) ∧ 𝐴 β‰  ℝ) β†’ Β¬ (βˆͺ ([,] β€œ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)}) = 𝐴 ∧ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} ∈ Fin))
145113, 144pm2.61dane 3030 . . . . . 6 ((𝐴 ∈ (topGenβ€˜ran (,)) ∧ 𝐴 β‰  βˆ…) β†’ Β¬ (βˆͺ ([,] β€œ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)}) = 𝐴 ∧ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} ∈ Fin))
146 oveq1 7413 . . . . . . . . . . . 12 (π‘₯ = 𝑒 β†’ (π‘₯ / (2↑𝑦)) = (𝑒 / (2↑𝑦)))
147 oveq1 7413 . . . . . . . . . . . . 13 (π‘₯ = 𝑒 β†’ (π‘₯ + 1) = (𝑒 + 1))
148147oveq1d 7421 . . . . . . . . . . . 12 (π‘₯ = 𝑒 β†’ ((π‘₯ + 1) / (2↑𝑦)) = ((𝑒 + 1) / (2↑𝑦)))
149146, 148opeq12d 4881 . . . . . . . . . . 11 (π‘₯ = 𝑒 β†’ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩ = ⟨(𝑒 / (2↑𝑦)), ((𝑒 + 1) / (2↑𝑦))⟩)
150 oveq2 7414 . . . . . . . . . . . . 13 (𝑦 = 𝑣 β†’ (2↑𝑦) = (2↑𝑣))
151150oveq2d 7422 . . . . . . . . . . . 12 (𝑦 = 𝑣 β†’ (𝑒 / (2↑𝑦)) = (𝑒 / (2↑𝑣)))
152150oveq2d 7422 . . . . . . . . . . . 12 (𝑦 = 𝑣 β†’ ((𝑒 + 1) / (2↑𝑦)) = ((𝑒 + 1) / (2↑𝑣)))
153151, 152opeq12d 4881 . . . . . . . . . . 11 (𝑦 = 𝑣 β†’ ⟨(𝑒 / (2↑𝑦)), ((𝑒 + 1) / (2↑𝑦))⟩ = ⟨(𝑒 / (2↑𝑣)), ((𝑒 + 1) / (2↑𝑣))⟩)
154149, 153cbvmpov 7501 . . . . . . . . . 10 (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) = (𝑒 ∈ β„€, 𝑣 ∈ β„•0 ↦ ⟨(𝑒 / (2↑𝑣)), ((𝑒 + 1) / (2↑𝑣))⟩)
155 fveq2 6889 . . . . . . . . . . . . . 14 (π‘Ž = 𝑧 β†’ ([,]β€˜π‘Ž) = ([,]β€˜π‘§))
156155sseq1d 4013 . . . . . . . . . . . . 13 (π‘Ž = 𝑧 β†’ (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) ↔ ([,]β€˜π‘§) βŠ† ([,]β€˜π‘)))
157 equequ1 2029 . . . . . . . . . . . . 13 (π‘Ž = 𝑧 β†’ (π‘Ž = 𝑐 ↔ 𝑧 = 𝑐))
158156, 157imbi12d 345 . . . . . . . . . . . 12 (π‘Ž = 𝑧 β†’ ((([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐) ↔ (([,]β€˜π‘§) βŠ† ([,]β€˜π‘) β†’ 𝑧 = 𝑐)))
159158ralbidv 3178 . . . . . . . . . . 11 (π‘Ž = 𝑧 β†’ (βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐) ↔ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘§) βŠ† ([,]β€˜π‘) β†’ 𝑧 = 𝑐)))
160159cbvrabv 3443 . . . . . . . . . 10 {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} = {𝑧 ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘§) βŠ† ([,]β€˜π‘) β†’ 𝑧 = 𝑐)}
16119a1i 11 . . . . . . . . . 10 (𝐴 ∈ (topGenβ€˜ran (,)) β†’ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} βŠ† ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩))
162154, 160, 161dyadmbllem 25108 . . . . . . . . 9 (𝐴 ∈ (topGenβ€˜ran (,)) β†’ βˆͺ ([,] β€œ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴}) = βˆͺ ([,] β€œ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)}))
163 opnmbllem0 36513 . . . . . . . . 9 (𝐴 ∈ (topGenβ€˜ran (,)) β†’ βˆͺ ([,] β€œ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴}) = 𝐴)
164162, 163eqtr3d 2775 . . . . . . . 8 (𝐴 ∈ (topGenβ€˜ran (,)) β†’ βˆͺ ([,] β€œ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)}) = 𝐴)
165164adantr 482 . . . . . . 7 ((𝐴 ∈ (topGenβ€˜ran (,)) ∧ 𝐴 β‰  βˆ…) β†’ βˆͺ ([,] β€œ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)}) = 𝐴)
166 nnenom 13942 . . . . . . . . 9 β„• β‰ˆ Ο‰
167 sdomentr 9108 . . . . . . . . 9 (({π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} β‰Ί β„• ∧ β„• β‰ˆ Ο‰) β†’ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} β‰Ί Ο‰)
168166, 167mpan2 690 . . . . . . . 8 ({π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} β‰Ί β„• β†’ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} β‰Ί Ο‰)
169 isfinite 9644 . . . . . . . 8 ({π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} ∈ Fin ↔ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} β‰Ί Ο‰)
170168, 169sylibr 233 . . . . . . 7 ({π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} β‰Ί β„• β†’ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} ∈ Fin)
171165, 170anim12i 614 . . . . . 6 (((𝐴 ∈ (topGenβ€˜ran (,)) ∧ 𝐴 β‰  βˆ…) ∧ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} β‰Ί β„•) β†’ (βˆͺ ([,] β€œ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)}) = 𝐴 ∧ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} ∈ Fin))
172145, 171mtand 815 . . . . 5 ((𝐴 ∈ (topGenβ€˜ran (,)) ∧ 𝐴 β‰  βˆ…) β†’ Β¬ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} β‰Ί β„•)
173 qex 12942 . . . . . . . 8 β„š ∈ V
174173, 173xpex 7737 . . . . . . 7 (β„š Γ— β„š) ∈ V
175 zq 12935 . . . . . . . . . . . . 13 (π‘₯ ∈ β„€ β†’ π‘₯ ∈ β„š)
176 2nn 12282 . . . . . . . . . . . . . . . 16 2 ∈ β„•
177 nnq 12943 . . . . . . . . . . . . . . . 16 (2 ∈ β„• β†’ 2 ∈ β„š)
178176, 177ax-mp 5 . . . . . . . . . . . . . . 15 2 ∈ β„š
179 qexpcl 14040 . . . . . . . . . . . . . . 15 ((2 ∈ β„š ∧ 𝑦 ∈ β„•0) β†’ (2↑𝑦) ∈ β„š)
180178, 179mpan 689 . . . . . . . . . . . . . 14 (𝑦 ∈ β„•0 β†’ (2↑𝑦) ∈ β„š)
181180, 29jca 513 . . . . . . . . . . . . 13 (𝑦 ∈ β„•0 β†’ ((2↑𝑦) ∈ β„š ∧ (2↑𝑦) β‰  0))
182 qdivcl 12951 . . . . . . . . . . . . . . 15 ((π‘₯ ∈ β„š ∧ (2↑𝑦) ∈ β„š ∧ (2↑𝑦) β‰  0) β†’ (π‘₯ / (2↑𝑦)) ∈ β„š)
183 1z 12589 . . . . . . . . . . . . . . . . . 18 1 ∈ β„€
184 zq 12935 . . . . . . . . . . . . . . . . . 18 (1 ∈ β„€ β†’ 1 ∈ β„š)
185183, 184ax-mp 5 . . . . . . . . . . . . . . . . 17 1 ∈ β„š
186 qaddcl 12946 . . . . . . . . . . . . . . . . 17 ((π‘₯ ∈ β„š ∧ 1 ∈ β„š) β†’ (π‘₯ + 1) ∈ β„š)
187185, 186mpan2 690 . . . . . . . . . . . . . . . 16 (π‘₯ ∈ β„š β†’ (π‘₯ + 1) ∈ β„š)
188 qdivcl 12951 . . . . . . . . . . . . . . . 16 (((π‘₯ + 1) ∈ β„š ∧ (2↑𝑦) ∈ β„š ∧ (2↑𝑦) β‰  0) β†’ ((π‘₯ + 1) / (2↑𝑦)) ∈ β„š)
189187, 188syl3an1 1164 . . . . . . . . . . . . . . 15 ((π‘₯ ∈ β„š ∧ (2↑𝑦) ∈ β„š ∧ (2↑𝑦) β‰  0) β†’ ((π‘₯ + 1) / (2↑𝑦)) ∈ β„š)
190 opelxpi 5713 . . . . . . . . . . . . . . 15 (((π‘₯ / (2↑𝑦)) ∈ β„š ∧ ((π‘₯ + 1) / (2↑𝑦)) ∈ β„š) β†’ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩ ∈ (β„š Γ— β„š))
191182, 189, 190syl2anc 585 . . . . . . . . . . . . . 14 ((π‘₯ ∈ β„š ∧ (2↑𝑦) ∈ β„š ∧ (2↑𝑦) β‰  0) β†’ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩ ∈ (β„š Γ— β„š))
1921913expb 1121 . . . . . . . . . . . . 13 ((π‘₯ ∈ β„š ∧ ((2↑𝑦) ∈ β„š ∧ (2↑𝑦) β‰  0)) β†’ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩ ∈ (β„š Γ— β„š))
193175, 181, 192syl2an 597 . . . . . . . . . . . 12 ((π‘₯ ∈ β„€ ∧ 𝑦 ∈ β„•0) β†’ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩ ∈ (β„š Γ— β„š))
194193rgen2 3198 . . . . . . . . . . 11 βˆ€π‘₯ ∈ β„€ βˆ€π‘¦ ∈ β„•0 ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩ ∈ (β„š Γ— β„š)
19540fmpo 8051 . . . . . . . . . . 11 (βˆ€π‘₯ ∈ β„€ βˆ€π‘¦ ∈ β„•0 ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩ ∈ (β„š Γ— β„š) ↔ (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩):(β„€ Γ— β„•0)⟢(β„š Γ— β„š))
196194, 195mpbi 229 . . . . . . . . . 10 (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩):(β„€ Γ— β„•0)⟢(β„š Γ— β„š)
197 frn 6722 . . . . . . . . . 10 ((π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩):(β„€ Γ— β„•0)⟢(β„š Γ— β„š) β†’ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) βŠ† (β„š Γ— β„š))
198196, 197ax-mp 5 . . . . . . . . 9 ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) βŠ† (β„š Γ— β„š)
19919, 198sstri 3991 . . . . . . . 8 {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} βŠ† (β„š Γ— β„š)
20018, 199sstri 3991 . . . . . . 7 {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} βŠ† (β„š Γ— β„š)
201 ssdomg 8993 . . . . . . 7 ((β„š Γ— β„š) ∈ V β†’ ({π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} βŠ† (β„š Γ— β„š) β†’ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} β‰Ό (β„š Γ— β„š)))
202174, 200, 201mp2 9 . . . . . 6 {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} β‰Ό (β„š Γ— β„š)
203 qnnen 16153 . . . . . . . 8 β„š β‰ˆ β„•
204 xpen 9137 . . . . . . . 8 ((β„š β‰ˆ β„• ∧ β„š β‰ˆ β„•) β†’ (β„š Γ— β„š) β‰ˆ (β„• Γ— β„•))
205203, 203, 204mp2an 691 . . . . . . 7 (β„š Γ— β„š) β‰ˆ (β„• Γ— β„•)
206 xpnnen 16151 . . . . . . 7 (β„• Γ— β„•) β‰ˆ β„•
207205, 206entri 9001 . . . . . 6 (β„š Γ— β„š) β‰ˆ β„•
208 domentr 9006 . . . . . 6 (({π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} β‰Ό (β„š Γ— β„š) ∧ (β„š Γ— β„š) β‰ˆ β„•) β†’ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} β‰Ό β„•)
209202, 207, 208mp2an 691 . . . . 5 {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} β‰Ό β„•
210172, 209jctil 521 . . . 4 ((𝐴 ∈ (topGenβ€˜ran (,)) ∧ 𝐴 β‰  βˆ…) β†’ ({π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} β‰Ό β„• ∧ Β¬ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} β‰Ί β„•))
211 bren2 8976 . . . 4 ({π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} β‰ˆ β„• ↔ ({π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} β‰Ό β„• ∧ Β¬ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} β‰Ί β„•))
212210, 211sylibr 233 . . 3 ((𝐴 ∈ (topGenβ€˜ran (,)) ∧ 𝐴 β‰  βˆ…) β†’ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} β‰ˆ β„•)
213212ensymd 8998 . 2 ((𝐴 ∈ (topGenβ€˜ran (,)) ∧ 𝐴 β‰  βˆ…) β†’ β„• β‰ˆ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)})
214 bren 8946 . 2 (β„• β‰ˆ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} ↔ βˆƒπ‘“ 𝑓:ℕ–1-1-ontoβ†’{π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)})
215213, 214sylib 217 1 ((𝐴 ∈ (topGenβ€˜ran (,)) ∧ 𝐴 β‰  βˆ…) β†’ βˆƒπ‘“ 𝑓:ℕ–1-1-ontoβ†’{π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)})
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1088   = wceq 1542  βˆƒwex 1782   ∈ wcel 2107   β‰  wne 2941  βˆ€wral 3062  βˆƒwrex 3071  {crab 3433  Vcvv 3475   βŠ† wss 3948  βˆ…c0 4322  π’« cpw 4602  βŸ¨cop 4634  βˆͺ cuni 4908  βˆͺ ciun 4997   class class class wbr 5148   Γ— cxp 5674  ran crn 5677   β€œ cima 5679  Rel wrel 5681  Fun wfun 6535   Fn wfn 6536  βŸΆwf 6537  β€“1-1-ontoβ†’wf1o 6540  β€˜cfv 6541  (class class class)co 7406   ∈ cmpo 7408  Ο‰com 7852  1st c1st 7970  2nd c2nd 7971   β‰ˆ cen 8933   β‰Ό cdom 8934   β‰Ί csdm 8935  Fincfn 8936  β„‚cc 11105  β„cr 11106  0cc0 11107  1c1 11108   + caddc 11110  β„*cxr 11244   < clt 11245   ≀ cle 11246   / cdiv 11868  β„•cn 12209  2c2 12264  β„•0cn0 12469  β„€cz 12555  β„šcq 12929  (,)cioo 13321  [,]cicc 13324  β†‘cexp 14024  topGenctg 17380  Topctop 22387  Clsdccld 22512  Conncconn 22907
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7722  ax-inf2 9633  ax-cnex 11163  ax-resscn 11164  ax-1cn 11165  ax-icn 11166  ax-addcl 11167  ax-addrcl 11168  ax-mulcl 11169  ax-mulrcl 11170  ax-mulcom 11171  ax-addass 11172  ax-mulass 11173  ax-distr 11174  ax-i2m1 11175  ax-1ne0 11176  ax-1rid 11177  ax-rnegex 11178  ax-rrecex 11179  ax-cnre 11180  ax-pre-lttri 11181  ax-pre-lttrn 11182  ax-pre-ltadd 11183  ax-pre-mulgt0 11184  ax-pre-sup 11185
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-iin 5000  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-se 5632  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6298  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6493  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-isom 6550  df-riota 7362  df-ov 7409  df-oprab 7410  df-mpo 7411  df-om 7853  df-1st 7972  df-2nd 7973  df-frecs 8263  df-wrecs 8294  df-recs 8368  df-rdg 8407  df-1o 8463  df-oadd 8467  df-omul 8468  df-er 8700  df-map 8819  df-en 8937  df-dom 8938  df-sdom 8939  df-fin 8940  df-fi 9403  df-sup 9434  df-inf 9435  df-oi 9502  df-card 9931  df-acn 9934  df-pnf 11247  df-mnf 11248  df-xr 11249  df-ltxr 11250  df-le 11251  df-sub 11443  df-neg 11444  df-div 11869  df-nn 12210  df-2 12272  df-3 12273  df-n0 12470  df-z 12556  df-uz 12820  df-q 12930  df-rp 12972  df-xneg 13089  df-xadd 13090  df-xmul 13091  df-ioo 13325  df-ico 13327  df-icc 13328  df-fz 13482  df-fzo 13625  df-fl 13754  df-seq 13964  df-exp 14025  df-hash 14288  df-cj 15043  df-re 15044  df-im 15045  df-sqrt 15179  df-abs 15180  df-clim 15429  df-sum 15630  df-rest 17365  df-topgen 17386  df-psmet 20929  df-xmet 20930  df-met 20931  df-bl 20932  df-mopn 20933  df-top 22388  df-topon 22405  df-bases 22441  df-cld 22515  df-cmp 22883  df-conn 22908  df-ovol 24973
This theorem is referenced by:  mblfinlem2  36515
  Copyright terms: Public domain W3C validator