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 37015
Description: Lemma for ismblfin 37019, 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 5142 . . . . . . . . . . . . . 14 (𝑧 = (𝑛 + 1) β†’ (𝑛 < 𝑧 ↔ 𝑛 < (𝑛 + 1)))
43rspcev 3604 . . . . . . . . . . . . 13 (((𝑛 + 1) ∈ ℝ ∧ 𝑛 < (𝑛 + 1)) β†’ βˆƒπ‘§ ∈ ℝ 𝑛 < 𝑧)
51, 2, 4syl2anc 583 . . . . . . . . . . . 12 (𝑛 ∈ ℝ β†’ βˆƒπ‘§ ∈ ℝ 𝑛 < 𝑧)
65rgen 3055 . . . . . . . . . . 11 βˆ€π‘› ∈ ℝ βˆƒπ‘§ ∈ ℝ 𝑛 < 𝑧
7 ltnle 11290 . . . . . . . . . . . . . . 15 ((𝑛 ∈ ℝ ∧ 𝑧 ∈ ℝ) β†’ (𝑛 < 𝑧 ↔ Β¬ 𝑧 ≀ 𝑛))
87rexbidva 3168 . . . . . . . . . . . . . 14 (𝑛 ∈ ℝ β†’ (βˆƒπ‘§ ∈ ℝ 𝑛 < 𝑧 ↔ βˆƒπ‘§ ∈ ℝ Β¬ 𝑧 ≀ 𝑛))
9 rexnal 3092 . . . . . . . . . . . . . 14 (βˆƒπ‘§ ∈ ℝ Β¬ 𝑧 ≀ 𝑛 ↔ Β¬ βˆ€π‘§ ∈ ℝ 𝑧 ≀ 𝑛)
108, 9bitrdi 287 . . . . . . . . . . . . 13 (𝑛 ∈ ℝ β†’ (βˆƒπ‘§ ∈ ℝ 𝑛 < 𝑧 ↔ Β¬ βˆ€π‘§ ∈ ℝ 𝑧 ≀ 𝑛))
1110ralbiia 3083 . . . . . . . . . . . 12 (βˆ€π‘› ∈ ℝ βˆƒπ‘§ ∈ ℝ 𝑛 < 𝑧 ↔ βˆ€π‘› ∈ ℝ Β¬ βˆ€π‘§ ∈ ℝ 𝑧 ≀ 𝑛)
12 ralnex 3064 . . . . . . . . . . . 12 (βˆ€π‘› ∈ ℝ Β¬ βˆ€π‘§ ∈ ℝ 𝑧 ≀ 𝑛 ↔ Β¬ βˆƒπ‘› ∈ ℝ βˆ€π‘§ ∈ ℝ 𝑧 ≀ 𝑛)
1311, 12bitri 275 . . . . . . . . . . 11 (βˆ€π‘› ∈ ℝ βˆƒπ‘§ ∈ ℝ 𝑛 < 𝑧 ↔ Β¬ βˆƒπ‘› ∈ ℝ βˆ€π‘§ ∈ ℝ 𝑧 ≀ 𝑛)
146, 13mpbi 229 . . . . . . . . . 10 Β¬ βˆƒπ‘› ∈ ℝ βˆ€π‘§ ∈ ℝ 𝑧 ≀ 𝑛
15 raleq 3314 . . . . . . . . . . 11 (𝐴 = ℝ β†’ (βˆ€π‘§ ∈ 𝐴 𝑧 ≀ 𝑛 ↔ βˆ€π‘§ ∈ ℝ 𝑧 ≀ 𝑛))
1615rexbidv 3170 . . . . . . . . . 10 (𝐴 = ℝ β†’ (βˆƒπ‘› ∈ ℝ βˆ€π‘§ ∈ 𝐴 𝑧 ≀ 𝑛 ↔ βˆƒπ‘› ∈ ℝ βˆ€π‘§ ∈ ℝ 𝑧 ≀ 𝑛))
1714, 16mtbiri 327 . . . . . . . . 9 (𝐴 = ℝ β†’ Β¬ βˆƒπ‘› ∈ ℝ βˆ€π‘§ ∈ 𝐴 𝑧 ≀ 𝑛)
18 ssrab2 4069 . . . . . . . . . . . . . 14 {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} βŠ† {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴}
19 ssrab2 4069 . . . . . . . . . . . . . . 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 687 . . . . . . . . . . . . . . . . . . . 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 1447 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ β„€ β†’ (2↑𝑦) β‰  0)
2924, 28syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ β„•0 β†’ (2↑𝑦) β‰  0)
3023, 29jca 511 . . . . . . . . . . . . . . . . . . 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 1160 . . . . . . . . . . . . . . . . . . . . 21 ((π‘₯ ∈ ℝ ∧ (2↑𝑦) ∈ ℝ ∧ (2↑𝑦) β‰  0) β†’ ((π‘₯ + 1) / (2↑𝑦)) ∈ ℝ)
35 opelxpi 5703 . . . . . . . . . . . . . . . . . . . . 21 (((π‘₯ / (2↑𝑦)) ∈ ℝ ∧ ((π‘₯ + 1) / (2↑𝑦)) ∈ ℝ) β†’ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩ ∈ (ℝ Γ— ℝ))
3631, 34, 35syl2anc 583 . . . . . . . . . . . . . . . . . . . 20 ((π‘₯ ∈ ℝ ∧ (2↑𝑦) ∈ ℝ ∧ (2↑𝑦) β‰  0) β†’ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩ ∈ (ℝ Γ— ℝ))
37363expb 1117 . . . . . . . . . . . . . . . . . . 19 ((π‘₯ ∈ ℝ ∧ ((2↑𝑦) ∈ ℝ ∧ (2↑𝑦) β‰  0)) β†’ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩ ∈ (ℝ Γ— ℝ))
3820, 30, 37syl2an 595 . . . . . . . . . . . . . . . . . 18 ((π‘₯ ∈ β„€ ∧ 𝑦 ∈ β„•0) β†’ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩ ∈ (ℝ Γ— ℝ))
3938rgen2 3189 . . . . . . . . . . . . . . . . 17 βˆ€π‘₯ ∈ β„€ βˆ€π‘¦ ∈ β„•0 ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩ ∈ (ℝ Γ— ℝ)
40 eqid 2724 . . . . . . . . . . . . . . . . . 18 (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) = (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩)
4140fmpo 8047 . . . . . . . . . . . . . . . . 17 (βˆ€π‘₯ ∈ β„€ βˆ€π‘¦ ∈ β„•0 ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩ ∈ (ℝ Γ— ℝ) ↔ (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩):(β„€ Γ— β„•0)⟢(ℝ Γ— ℝ))
4239, 41mpbi 229 . . . . . . . . . . . . . . . 16 (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩):(β„€ Γ— β„•0)⟢(ℝ Γ— ℝ)
43 frn 6714 . . . . . . . . . . . . . . . 16 ((π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩):(β„€ Γ— β„•0)⟢(ℝ Γ— ℝ) β†’ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) βŠ† (ℝ Γ— ℝ))
4442, 43ax-mp 5 . . . . . . . . . . . . . . 15 ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) βŠ† (ℝ Γ— ℝ)
4519, 44sstri 3983 . . . . . . . . . . . . . 14 {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} βŠ† (ℝ Γ— ℝ)
4618, 45sstri 3983 . . . . . . . . . . . . 13 {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} βŠ† (ℝ Γ— ℝ)
47 rnss 5928 . . . . . . . . . . . . . 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 6162 . . . . . . . . . . . . . 14 ran (ℝ Γ— ℝ) = ℝ
4947, 48sseqtrdi 4024 . . . . . . . . . . . . 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 9331 . . . . . . . . . . . 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 586 . . . . . . . . . . 11 ({π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} ∈ Fin β†’ βˆƒπ‘› ∈ ℝ βˆ€π‘’ ∈ ran {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)}𝑒 ≀ 𝑛)
5453adantl 481 . . . . . . . . . 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 4903 . . . . . . . . . . . . . . . . 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 6707 . . . . . . . . . . . . . . . . . . 19 ([,]:(ℝ* Γ— ℝ*)βŸΆπ’« ℝ* β†’ [,] Fn (ℝ* Γ— ℝ*))
5856, 57ax-mp 5 . . . . . . . . . . . . . . . . . 18 [,] Fn (ℝ* Γ— ℝ*)
59 rexpssxrxp 11256 . . . . . . . . . . . . . . . . . . 19 (ℝ Γ— ℝ) βŠ† (ℝ* Γ— ℝ*)
6046, 59sstri 3983 . . . . . . . . . . . . . . . . . 18 {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} βŠ† (ℝ* Γ— ℝ*)
61 eleq2 2814 . . . . . . . . . . . . . . . . . . 19 (𝑒 = ([,]β€˜π‘£) β†’ (𝑧 ∈ 𝑒 ↔ 𝑧 ∈ ([,]β€˜π‘£)))
6261rexima 7230 . . . . . . . . . . . . . . . . . 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 689 . . . . . . . . . . . . . . . . 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 3970 . . . . . . . . . . . . . . . . . . . . 21 (𝑣 ∈ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} β†’ 𝑣 ∈ (ℝ Γ— ℝ))
66 1st2nd2 8007 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑣 ∈ (ℝ Γ— ℝ) β†’ 𝑣 = ⟨(1st β€˜π‘£), (2nd β€˜π‘£)⟩)
6766fveq2d 6885 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑣 ∈ (ℝ Γ— ℝ) β†’ ([,]β€˜π‘£) = ([,]β€˜βŸ¨(1st β€˜π‘£), (2nd β€˜π‘£)⟩))
68 df-ov 7404 . . . . . . . . . . . . . . . . . . . . . . 23 ((1st β€˜π‘£)[,](2nd β€˜π‘£)) = ([,]β€˜βŸ¨(1st β€˜π‘£), (2nd β€˜π‘£)⟩)
6967, 68eqtr4di 2782 . . . . . . . . . . . . . . . . . . . . . 22 (𝑣 ∈ (ℝ Γ— ℝ) β†’ ([,]β€˜π‘£) = ((1st β€˜π‘£)[,](2nd β€˜π‘£)))
7069eleq2d 2811 . . . . . . . . . . . . . . . . . . . . 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 568 . . . . . . . . . . . . . . . . . 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 726 . . . . . . . . . . . . . . . . . . 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 8001 . . . . . . . . . . . . . . . . . . . . . 22 (𝑣 ∈ (ℝ Γ— ℝ) β†’ (2nd β€˜π‘£) ∈ ℝ)
7776rexrd 11261 . . . . . . . . . . . . . . . . . . . . 21 (𝑣 ∈ (ℝ Γ— ℝ) β†’ (2nd β€˜π‘£) ∈ ℝ*)
7865, 77syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝑣 ∈ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} β†’ (2nd β€˜π‘£) ∈ ℝ*)
7978ad2antrl 725 . . . . . . . . . . . . . . . . . . 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 773 . . . . . . . . . . . . . . . . . . . 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 8000 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑣 ∈ (ℝ Γ— ℝ) β†’ (1st β€˜π‘£) ∈ ℝ)
8382rexrd 11261 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑣 ∈ (ℝ Γ— ℝ) β†’ (1st β€˜π‘£) ∈ ℝ*)
8483, 77jca 511 . . . . . . . . . . . . . . . . . . . . . 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 1115 . . . . . . . . . . . . . . . . . . . . 21 ((((1st β€˜π‘£) ∈ ℝ* ∧ (2nd β€˜π‘£) ∈ ℝ*) ∧ 𝑧 ∈ ((1st β€˜π‘£)[,](2nd β€˜π‘£))) β†’ 𝑧 ≀ (2nd β€˜π‘£))
8885, 87sylan 579 . . . . . . . . . . . . . . . . . . . 20 ((𝑣 ∈ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} ∧ 𝑧 ∈ ((1st β€˜π‘£)[,](2nd β€˜π‘£))) β†’ 𝑧 ≀ (2nd β€˜π‘£))
8988adantl 481 . . . . . . . . . . . . . . . . . . 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 5682 . . . . . . . . . . . . . . . . . . . . . . . 24 (ℝ Γ— ℝ) βŠ† (V Γ— V)
9146, 90sstri 3983 . . . . . . . . . . . . . . . . . . . . . . 23 {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} βŠ† (V Γ— V)
92 df-rel 5673 . . . . . . . . . . . . . . . . . . . . . . 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 8020 . . . . . . . . . . . . . . . . . . . . . 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 687 . . . . . . . . . . . . . . . . . . . . 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 5141 . . . . . . . . . . . . . . . . . . . . . 22 (𝑒 = (2nd β€˜π‘£) β†’ (𝑒 ≀ 𝑛 ↔ (2nd β€˜π‘£) ≀ 𝑛))
9796rspccva 3603 . . . . . . . . . . . . . . . . . . . . 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 592 . . . . . . . . . . . . . . . . . . . 20 ((βˆ€π‘’ ∈ ran {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)}𝑒 ≀ 𝑛 ∧ 𝑣 ∈ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)}) β†’ (2nd β€˜π‘£) ≀ 𝑛)
9998ad2ant2lr 745 . . . . . . . . . . . . . . . . . . 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 592 . . . . . . . . . . . . . . . . 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 3148 . . . . . . . . . . . . . . . 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 3137 . . . . . . . . . . . . . 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 3314 . . . . . . . . . . . . . . 15 (βˆͺ ([,] β€œ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)}) = 𝐴 β†’ (βˆ€π‘§ ∈ βˆͺ ([,] β€œ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)})𝑧 ≀ 𝑛 ↔ βˆ€π‘§ ∈ 𝐴 𝑧 ≀ 𝑛))
106105ad2antrr 723 . . . . . . . . . . . . . 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 412 . . . . . . . . . . . 12 ((βˆͺ ([,] β€œ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)}) = 𝐴 ∧ 𝑛 ∈ ℝ) β†’ (βˆ€π‘’ ∈ ran {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)}𝑒 ≀ 𝑛 β†’ βˆ€π‘§ ∈ 𝐴 𝑧 ≀ 𝑛))
109108reximdva 3160 . . . . . . . . . . 11 (βˆͺ ([,] β€œ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)}) = 𝐴 β†’ (βˆƒπ‘› ∈ ℝ βˆ€π‘’ ∈ ran {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)}𝑒 ≀ 𝑛 β†’ βˆƒπ‘› ∈ ℝ βˆ€π‘§ ∈ 𝐴 𝑧 ≀ 𝑛))
110109adantr 480 . . . . . . . . . 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 481 . . . . . . 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 24601 . . . . . . . . . . 11 ℝ = βˆͺ (topGenβ€˜ran (,))
115 retopconn 24667 . . . . . . . . . . . 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 764 . . . . . . . . . . 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 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)) β†’ 𝐴 β‰  βˆ…)
119 simprl 768 . . . . . . . . . . . 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 6710 . . . . . . . . . . . . . . 15 ([,]:(ℝ* Γ— ℝ*)βŸΆπ’« ℝ* β†’ Fun [,])
121 funiunfv 7239 . . . . . . . . . . . . . . 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 24600 . . . . . . . . . . . . . . 15 (topGenβ€˜ran (,)) ∈ Top
12446sseli 3970 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} β†’ 𝑧 ∈ (ℝ Γ— ℝ))
125 1st2nd2 8007 . . . . . . . . . . . . . . . . . . . 20 (𝑧 ∈ (ℝ Γ— ℝ) β†’ 𝑧 = ⟨(1st β€˜π‘§), (2nd β€˜π‘§)⟩)
126125fveq2d 6885 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ (ℝ Γ— ℝ) β†’ ([,]β€˜π‘§) = ([,]β€˜βŸ¨(1st β€˜π‘§), (2nd β€˜π‘§)⟩))
127 df-ov 7404 . . . . . . . . . . . . . . . . . . 19 ((1st β€˜π‘§)[,](2nd β€˜π‘§)) = ([,]β€˜βŸ¨(1st β€˜π‘§), (2nd β€˜π‘§)⟩)
128126, 127eqtr4di 2782 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ (ℝ Γ— ℝ) β†’ ([,]β€˜π‘§) = ((1st β€˜π‘§)[,](2nd β€˜π‘§)))
129 xp1st 8000 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ (ℝ Γ— ℝ) β†’ (1st β€˜π‘§) ∈ ℝ)
130 xp2nd 8001 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ (ℝ Γ— ℝ) β†’ (2nd β€˜π‘§) ∈ ℝ)
131 icccld 24605 . . . . . . . . . . . . . . . . . . 19 (((1st β€˜π‘§) ∈ ℝ ∧ (2nd β€˜π‘§) ∈ ℝ) β†’ ((1st β€˜π‘§)[,](2nd β€˜π‘§)) ∈ (Clsdβ€˜(topGenβ€˜ran (,))))
132129, 130, 131syl2anc 583 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ (ℝ Γ— ℝ) β†’ ((1st β€˜π‘§)[,](2nd β€˜π‘§)) ∈ (Clsdβ€˜(topGenβ€˜ran (,))))
133128, 132eqeltrd 2825 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ (ℝ Γ— ℝ) β†’ ([,]β€˜π‘§) ∈ (Clsdβ€˜(topGenβ€˜ran (,))))
134124, 133syl 17 . . . . . . . . . . . . . . . 16 (𝑧 ∈ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} β†’ ([,]β€˜π‘§) ∈ (Clsdβ€˜(topGenβ€˜ran (,))))
135134rgen 3055 . . . . . . . . . . . . . . 15 βˆ€π‘§ ∈ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} ([,]β€˜π‘§) ∈ (Clsdβ€˜(topGenβ€˜ran (,)))
136114iuncld 22871 . . . . . . . . . . . . . . 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 1448 . . . . . . . . . . . . . 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 2830 . . . . . . . . . . . . 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 726 . . . . . . . . . . . 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 2826 . . . . . . . . . . 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 23241 . . . . . . . . . 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 412 . . . . . . . . 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 2945 . . . . . . . 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 406 . . . . . . 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 3021 . . . . . 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 7408 . . . . . . . . . . . 12 (π‘₯ = 𝑒 β†’ (π‘₯ / (2↑𝑦)) = (𝑒 / (2↑𝑦)))
147 oveq1 7408 . . . . . . . . . . . . 13 (π‘₯ = 𝑒 β†’ (π‘₯ + 1) = (𝑒 + 1))
148147oveq1d 7416 . . . . . . . . . . . 12 (π‘₯ = 𝑒 β†’ ((π‘₯ + 1) / (2↑𝑦)) = ((𝑒 + 1) / (2↑𝑦)))
149146, 148opeq12d 4873 . . . . . . . . . . 11 (π‘₯ = 𝑒 β†’ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩ = ⟨(𝑒 / (2↑𝑦)), ((𝑒 + 1) / (2↑𝑦))⟩)
150 oveq2 7409 . . . . . . . . . . . . 13 (𝑦 = 𝑣 β†’ (2↑𝑦) = (2↑𝑣))
151150oveq2d 7417 . . . . . . . . . . . 12 (𝑦 = 𝑣 β†’ (𝑒 / (2↑𝑦)) = (𝑒 / (2↑𝑣)))
152150oveq2d 7417 . . . . . . . . . . . 12 (𝑦 = 𝑣 β†’ ((𝑒 + 1) / (2↑𝑦)) = ((𝑒 + 1) / (2↑𝑣)))
153151, 152opeq12d 4873 . . . . . . . . . . 11 (𝑦 = 𝑣 β†’ ⟨(𝑒 / (2↑𝑦)), ((𝑒 + 1) / (2↑𝑦))⟩ = ⟨(𝑒 / (2↑𝑣)), ((𝑒 + 1) / (2↑𝑣))⟩)
154149, 153cbvmpov 7496 . . . . . . . . . 10 (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) = (𝑒 ∈ β„€, 𝑣 ∈ β„•0 ↦ ⟨(𝑒 / (2↑𝑣)), ((𝑒 + 1) / (2↑𝑣))⟩)
155 fveq2 6881 . . . . . . . . . . . . . 14 (π‘Ž = 𝑧 β†’ ([,]β€˜π‘Ž) = ([,]β€˜π‘§))
156155sseq1d 4005 . . . . . . . . . . . . 13 (π‘Ž = 𝑧 β†’ (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) ↔ ([,]β€˜π‘§) βŠ† ([,]β€˜π‘)))
157 equequ1 2020 . . . . . . . . . . . . 13 (π‘Ž = 𝑧 β†’ (π‘Ž = 𝑐 ↔ 𝑧 = 𝑐))
158156, 157imbi12d 344 . . . . . . . . . . . 12 (π‘Ž = 𝑧 β†’ ((([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐) ↔ (([,]β€˜π‘§) βŠ† ([,]β€˜π‘) β†’ 𝑧 = 𝑐)))
159158ralbidv 3169 . . . . . . . . . . 11 (π‘Ž = 𝑧 β†’ (βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐) ↔ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘§) βŠ† ([,]β€˜π‘) β†’ 𝑧 = 𝑐)))
160159cbvrabv 3434 . . . . . . . . . 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 25450 . . . . . . . . 9 (𝐴 ∈ (topGenβ€˜ran (,)) β†’ βˆͺ ([,] β€œ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴}) = βˆͺ ([,] β€œ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)}))
163 opnmbllem0 37014 . . . . . . . . 9 (𝐴 ∈ (topGenβ€˜ran (,)) β†’ βˆͺ ([,] β€œ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴}) = 𝐴)
164162, 163eqtr3d 2766 . . . . . . . 8 (𝐴 ∈ (topGenβ€˜ran (,)) β†’ βˆͺ ([,] β€œ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)}) = 𝐴)
165164adantr 480 . . . . . . 7 ((𝐴 ∈ (topGenβ€˜ran (,)) ∧ 𝐴 β‰  βˆ…) β†’ βˆͺ ([,] β€œ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)}) = 𝐴)
166 nnenom 13942 . . . . . . . . 9 β„• β‰ˆ Ο‰
167 sdomentr 9107 . . . . . . . . 9 (({π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} β‰Ί β„• ∧ β„• β‰ˆ Ο‰) β†’ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} β‰Ί Ο‰)
168166, 167mpan2 688 . . . . . . . 8 ({π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} β‰Ί β„• β†’ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} β‰Ί Ο‰)
169 isfinite 9643 . . . . . . . 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 612 . . . . . 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 813 . . . . 5 ((𝐴 ∈ (topGenβ€˜ran (,)) ∧ 𝐴 β‰  βˆ…) β†’ Β¬ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} β‰Ί β„•)
173 qex 12942 . . . . . . . 8 β„š ∈ V
174173, 173xpex 7733 . . . . . . 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 687 . . . . . . . . . . . . . 14 (𝑦 ∈ β„•0 β†’ (2↑𝑦) ∈ β„š)
181180, 29jca 511 . . . . . . . . . . . . 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 688 . . . . . . . . . . . . . . . 16 (π‘₯ ∈ β„š β†’ (π‘₯ + 1) ∈ β„š)
188 qdivcl 12951 . . . . . . . . . . . . . . . 16 (((π‘₯ + 1) ∈ β„š ∧ (2↑𝑦) ∈ β„š ∧ (2↑𝑦) β‰  0) β†’ ((π‘₯ + 1) / (2↑𝑦)) ∈ β„š)
189187, 188syl3an1 1160 . . . . . . . . . . . . . . 15 ((π‘₯ ∈ β„š ∧ (2↑𝑦) ∈ β„š ∧ (2↑𝑦) β‰  0) β†’ ((π‘₯ + 1) / (2↑𝑦)) ∈ β„š)
190 opelxpi 5703 . . . . . . . . . . . . . . 15 (((π‘₯ / (2↑𝑦)) ∈ β„š ∧ ((π‘₯ + 1) / (2↑𝑦)) ∈ β„š) β†’ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩ ∈ (β„š Γ— β„š))
191182, 189, 190syl2anc 583 . . . . . . . . . . . . . 14 ((π‘₯ ∈ β„š ∧ (2↑𝑦) ∈ β„š ∧ (2↑𝑦) β‰  0) β†’ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩ ∈ (β„š Γ— β„š))
1921913expb 1117 . . . . . . . . . . . . 13 ((π‘₯ ∈ β„š ∧ ((2↑𝑦) ∈ β„š ∧ (2↑𝑦) β‰  0)) β†’ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩ ∈ (β„š Γ— β„š))
193175, 181, 192syl2an 595 . . . . . . . . . . . 12 ((π‘₯ ∈ β„€ ∧ 𝑦 ∈ β„•0) β†’ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩ ∈ (β„š Γ— β„š))
194193rgen2 3189 . . . . . . . . . . 11 βˆ€π‘₯ ∈ β„€ βˆ€π‘¦ ∈ β„•0 ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩ ∈ (β„š Γ— β„š)
19540fmpo 8047 . . . . . . . . . . 11 (βˆ€π‘₯ ∈ β„€ βˆ€π‘¦ ∈ β„•0 ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩ ∈ (β„š Γ— β„š) ↔ (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩):(β„€ Γ— β„•0)⟢(β„š Γ— β„š))
196194, 195mpbi 229 . . . . . . . . . 10 (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩):(β„€ Γ— β„•0)⟢(β„š Γ— β„š)
197 frn 6714 . . . . . . . . . 10 ((π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩):(β„€ Γ— β„•0)⟢(β„š Γ— β„š) β†’ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) βŠ† (β„š Γ— β„š))
198196, 197ax-mp 5 . . . . . . . . 9 ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) βŠ† (β„š Γ— β„š)
19919, 198sstri 3983 . . . . . . . 8 {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} βŠ† (β„š Γ— β„š)
20018, 199sstri 3983 . . . . . . 7 {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} βŠ† (β„š Γ— β„š)
201 ssdomg 8992 . . . . . . 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 9136 . . . . . . . 8 ((β„š β‰ˆ β„• ∧ β„š β‰ˆ β„•) β†’ (β„š Γ— β„š) β‰ˆ (β„• Γ— β„•))
205203, 203, 204mp2an 689 . . . . . . 7 (β„š Γ— β„š) β‰ˆ (β„• Γ— β„•)
206 xpnnen 16151 . . . . . . 7 (β„• Γ— β„•) β‰ˆ β„•
207205, 206entri 9000 . . . . . 6 (β„š Γ— β„š) β‰ˆ β„•
208 domentr 9005 . . . . . 6 (({π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} β‰Ό (β„š Γ— β„š) ∧ (β„š Γ— β„š) β‰ˆ β„•) β†’ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} β‰Ό β„•)
209202, 207, 208mp2an 689 . . . . 5 {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)} β‰Ό β„•
210172, 209jctil 519 . . . 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 8975 . . . 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 8997 . 2 ((𝐴 ∈ (topGenβ€˜ran (,)) ∧ 𝐴 β‰  βˆ…) β†’ β„• β‰ˆ {π‘Ž ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} ∣ βˆ€π‘ ∈ {𝑏 ∈ ran (π‘₯ ∈ β„€, 𝑦 ∈ β„•0 ↦ ⟨(π‘₯ / (2↑𝑦)), ((π‘₯ + 1) / (2↑𝑦))⟩) ∣ ([,]β€˜π‘) βŠ† 𝐴} (([,]β€˜π‘Ž) βŠ† ([,]β€˜π‘) β†’ π‘Ž = 𝑐)})
214 bren 8945 . 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 395   ∧ w3a 1084   = wceq 1533  βˆƒwex 1773   ∈ wcel 2098   β‰  wne 2932  βˆ€wral 3053  βˆƒwrex 3062  {crab 3424  Vcvv 3466   βŠ† wss 3940  βˆ…c0 4314  π’« cpw 4594  βŸ¨cop 4626  βˆͺ cuni 4899  βˆͺ ciun 4987   class class class wbr 5138   Γ— cxp 5664  ran crn 5667   β€œ cima 5669  Rel wrel 5671  Fun wfun 6527   Fn wfn 6528  βŸΆwf 6529  β€“1-1-ontoβ†’wf1o 6532  β€˜cfv 6533  (class class class)co 7401   ∈ cmpo 7403  Ο‰com 7848  1st c1st 7966  2nd c2nd 7967   β‰ˆ cen 8932   β‰Ό cdom 8933   β‰Ί csdm 8934  Fincfn 8935  β„‚cc 11104  β„cr 11105  0cc0 11106  1c1 11107   + caddc 11109  β„*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 17382  Topctop 22717  Clsdccld 22842  Conncconn 23237
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-rep 5275  ax-sep 5289  ax-nul 5296  ax-pow 5353  ax-pr 5417  ax-un 7718  ax-inf2 9632  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183  ax-pre-sup 11184
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-nel 3039  df-ral 3054  df-rex 3063  df-rmo 3368  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-pss 3959  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-op 4627  df-uni 4900  df-int 4941  df-iun 4989  df-iin 4990  df-br 5139  df-opab 5201  df-mpt 5222  df-tr 5256  df-id 5564  df-eprel 5570  df-po 5578  df-so 5579  df-fr 5621  df-se 5622  df-we 5623  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6290  df-ord 6357  df-on 6358  df-lim 6359  df-suc 6360  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-isom 6542  df-riota 7357  df-ov 7404  df-oprab 7405  df-mpo 7406  df-om 7849  df-1st 7968  df-2nd 7969  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-rdg 8405  df-1o 8461  df-oadd 8465  df-omul 8466  df-er 8699  df-map 8818  df-en 8936  df-dom 8937  df-sdom 8938  df-fin 8939  df-fi 9402  df-sup 9433  df-inf 9434  df-oi 9501  df-card 9930  df-acn 9933  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 17367  df-topgen 17388  df-psmet 21220  df-xmet 21221  df-met 21222  df-bl 21223  df-mopn 21224  df-top 22718  df-topon 22735  df-bases 22771  df-cld 22845  df-cmp 23213  df-conn 23238  df-ovol 25315
This theorem is referenced by:  mblfinlem2  37016
  Copyright terms: Public domain W3C validator