Metamath Proof Explorer

Theorem mblfinlem1

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

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

Proof

Step Hyp Ref Expression
1 peano2re ⊢ ( 𝑛 ∈ ℝ → ( 𝑛 + 1 ) ∈ ℝ )
2 ltp1 ⊢ ( 𝑛 ∈ ℝ → 𝑛 < ( 𝑛 + 1 ) )
3 breq2 ⊢ ( 𝑧 = ( 𝑛 + 1 ) → ( 𝑛 < 𝑧 ↔ 𝑛 < ( 𝑛 + 1 ) ) )
4 3 rspcev ⊢ ( ( ( 𝑛 + 1 ) ∈ ℝ ∧ 𝑛 < ( 𝑛 + 1 ) ) → ∃ 𝑧 ∈ ℝ 𝑛 < 𝑧 )
5 1 2 4 syl2anc ⊢ ( 𝑛 ∈ ℝ → ∃ 𝑧 ∈ ℝ 𝑛 < 𝑧 )
6 5 rgen ⊢ ∀ 𝑛 ∈ ℝ ∃ 𝑧 ∈ ℝ 𝑛 < 𝑧
7 ltnle ⊢ ( ( 𝑛 ∈ ℝ ∧ 𝑧 ∈ ℝ ) → ( 𝑛 < 𝑧 ↔ ¬ 𝑧 ≤ 𝑛 ) )
8 7 rexbidva ⊢ ( 𝑛 ∈ ℝ → ( ∃ 𝑧 ∈ ℝ 𝑛 < 𝑧 ↔ ∃ 𝑧 ∈ ℝ ¬ 𝑧 ≤ 𝑛 ) )
9 rexnal ⊢ ( ∃ 𝑧 ∈ ℝ ¬ 𝑧 ≤ 𝑛 ↔ ¬ ∀ 𝑧 ∈ ℝ 𝑧 ≤ 𝑛 )
10 8 9 bitrdi ⊢ ( 𝑛 ∈ ℝ → ( ∃ 𝑧 ∈ ℝ 𝑛 < 𝑧 ↔ ¬ ∀ 𝑧 ∈ ℝ 𝑧 ≤ 𝑛 ) )
11 10 ralbiia ⊢ ( ∀ 𝑛 ∈ ℝ ∃ 𝑧 ∈ ℝ 𝑛 < 𝑧 ↔ ∀ 𝑛 ∈ ℝ ¬ ∀ 𝑧 ∈ ℝ 𝑧 ≤ 𝑛 )
12 ralnex ⊢ ( ∀ 𝑛 ∈ ℝ ¬ ∀ 𝑧 ∈ ℝ 𝑧 ≤ 𝑛 ↔ ¬ ∃ 𝑛 ∈ ℝ ∀ 𝑧 ∈ ℝ 𝑧 ≤ 𝑛 )
13 11 12 bitri ⊢ ( ∀ 𝑛 ∈ ℝ ∃ 𝑧 ∈ ℝ 𝑛 < 𝑧 ↔ ¬ ∃ 𝑛 ∈ ℝ ∀ 𝑧 ∈ ℝ 𝑧 ≤ 𝑛 )
14 6 13 mpbi ⊢ ¬ ∃ 𝑛 ∈ ℝ ∀ 𝑧 ∈ ℝ 𝑧 ≤ 𝑛
15 raleq ⊢ ( 𝐴 = ℝ → ( ∀ 𝑧 ∈ 𝐴 𝑧 ≤ 𝑛 ↔ ∀ 𝑧 ∈ ℝ 𝑧 ≤ 𝑛 ) )
16 15 rexbidv ⊢ ( 𝐴 = ℝ → ( ∃ 𝑛 ∈ ℝ ∀ 𝑧 ∈ 𝐴 𝑧 ≤ 𝑛 ↔ ∃ 𝑛 ∈ ℝ ∀ 𝑧 ∈ ℝ 𝑧 ≤ 𝑛 ) )
17 14 16 mtbiri ⊢ ( 𝐴 = ℝ → ¬ ∃ 𝑛 ∈ ℝ ∀ 𝑧 ∈ 𝐴 𝑧 ≤ 𝑛 )
18 ssrab2 ⊢ { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } ⊆ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 }
19 ssrab2 ⊢ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ⊆ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ )
20 zre ⊢ ( 𝑥 ∈ ℤ → 𝑥 ∈ ℝ )
21 2re ⊢ 2 ∈ ℝ
22 reexpcl ⊢ ( ( 2 ∈ ℝ ∧ 𝑦 ∈ ℕ0 ) → ( 2 ↑ 𝑦 ) ∈ ℝ )
23 21 22 mpan ⊢ ( 𝑦 ∈ ℕ0 → ( 2 ↑ 𝑦 ) ∈ ℝ )
24 nn0z ⊢ ( 𝑦 ∈ ℕ0 → 𝑦 ∈ ℤ )
25 2cn ⊢ 2 ∈ ℂ
26 2ne0 ⊢ 2 ≠ 0
27 expne0i ⊢ ( ( 2 ∈ ℂ ∧ 2 ≠ 0 ∧ 𝑦 ∈ ℤ ) → ( 2 ↑ 𝑦 ) ≠ 0 )
28 25 26 27 mp3an12 ⊢ ( 𝑦 ∈ ℤ → ( 2 ↑ 𝑦 ) ≠ 0 )
29 24 28 syl ⊢ ( 𝑦 ∈ ℕ0 → ( 2 ↑ 𝑦 ) ≠ 0 )
30 23 29 jca ⊢ ( 𝑦 ∈ ℕ0 → ( ( 2 ↑ 𝑦 ) ∈ ℝ ∧ ( 2 ↑ 𝑦 ) ≠ 0 ) )
31 redivcl ⊢ ( ( 𝑥 ∈ ℝ ∧ ( 2 ↑ 𝑦 ) ∈ ℝ ∧ ( 2 ↑ 𝑦 ) ≠ 0 ) → ( 𝑥 / ( 2 ↑ 𝑦 ) ) ∈ ℝ )
32 peano2re ⊢ ( 𝑥 ∈ ℝ → ( 𝑥 + 1 ) ∈ ℝ )
33 redivcl ⊢ ( ( ( 𝑥 + 1 ) ∈ ℝ ∧ ( 2 ↑ 𝑦 ) ∈ ℝ ∧ ( 2 ↑ 𝑦 ) ≠ 0 ) → ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ∈ ℝ )
34 32 33 syl3an1 ⊢ ( ( 𝑥 ∈ ℝ ∧ ( 2 ↑ 𝑦 ) ∈ ℝ ∧ ( 2 ↑ 𝑦 ) ≠ 0 ) → ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ∈ ℝ )
35 opelxpi ⊢ ( ( ( 𝑥 / ( 2 ↑ 𝑦 ) ) ∈ ℝ ∧ ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ∈ ℝ ) → ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ∈ ( ℝ × ℝ ) )
36 31 34 35 syl2anc ⊢ ( ( 𝑥 ∈ ℝ ∧ ( 2 ↑ 𝑦 ) ∈ ℝ ∧ ( 2 ↑ 𝑦 ) ≠ 0 ) → ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ∈ ( ℝ × ℝ ) )
37 36 3expb ⊢ ( ( 𝑥 ∈ ℝ ∧ ( ( 2 ↑ 𝑦 ) ∈ ℝ ∧ ( 2 ↑ 𝑦 ) ≠ 0 ) ) → ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ∈ ( ℝ × ℝ ) )
38 20 30 37 syl2an ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ0 ) → ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ∈ ( ℝ × ℝ ) )
39 38 rgen2 ⊢ ∀ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ℕ0 ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ∈ ( ℝ × ℝ )
40 eqid ⊢ ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) = ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ )
41 40 fmpo ⊢ ( ∀ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ℕ0 ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ∈ ( ℝ × ℝ ) ↔ ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) : ( ℤ × ℕ0 ) ⟶ ( ℝ × ℝ ) )
42 39 41 mpbi ⊢ ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) : ( ℤ × ℕ0 ) ⟶ ( ℝ × ℝ )
43 frn ⊢ ( ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) : ( ℤ × ℕ0 ) ⟶ ( ℝ × ℝ ) → ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ⊆ ( ℝ × ℝ ) )
44 42 43 ax-mp ⊢ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ⊆ ( ℝ × ℝ )
45 19 44 sstri ⊢ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ⊆ ( ℝ × ℝ )
46 18 45 sstri ⊢ { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } ⊆ ( ℝ × ℝ )
47 rnss ⊢ ( { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } ⊆ ( ℝ × ℝ ) → ran { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } ⊆ ran ( ℝ × ℝ ) )
48 rnxpid ⊢ ran ( ℝ × ℝ ) = ℝ
49 47 48 sseqtrdi ⊢ ( { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } ⊆ ( ℝ × ℝ ) → ran { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } ⊆ ℝ )
50 46 49 ax-mp ⊢ ran { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } ⊆ ℝ
51 rnfi ⊢ ( { 𝑎 ∈ { 𝑏 ∈ 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 ⊢ ( ( 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 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } 𝑢 ≤ 𝑛 )
53 50 51 52 sylancr ⊢ ( { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } ∈ Fin → ∃ 𝑛 ∈ ℝ ∀ 𝑢 ∈ ran { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } 𝑢 ≤ 𝑛 )
54 53 adantl ⊢ ( ( ∪ ( [,] “ { 𝑎 ∈ { 𝑏 ∈ 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 ⊢ ( 𝑧 ∈ ∪ ( [,] “ { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } ) ↔ ∃ 𝑢 ∈ ( [,] “ { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } ) 𝑧 ∈ 𝑢 )
56 iccf ⊢ [,] : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ*
57 ffn ⊢ ( [,] : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ* → [,] Fn ( ℝ* × ℝ* ) )
58 56 57 ax-mp ⊢ [,] Fn ( ℝ* × ℝ* )
59 rexpssxrxp ⊢ ( ℝ × ℝ ) ⊆ ( ℝ* × ℝ* )
60 46 59 sstri ⊢ { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } ⊆ ( ℝ* × ℝ* )
61 eleq2 ⊢ ( 𝑢 = ( [,] ‘ 𝑣 ) → ( 𝑧 ∈ 𝑢 ↔ 𝑧 ∈ ( [,] ‘ 𝑣 ) ) )
62 61 rexima ⊢ ( ( [,] 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 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } 𝑧 ∈ ( [,] ‘ 𝑣 ) ) )
63 58 60 62 mp2an ⊢ ( ∃ 𝑢 ∈ ( [,] “ { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } ) 𝑧 ∈ 𝑢 ↔ ∃ 𝑣 ∈ { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } 𝑧 ∈ ( [,] ‘ 𝑣 ) )
64 55 63 bitri ⊢ ( 𝑧 ∈ ∪ ( [,] “ { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } ) ↔ ∃ 𝑣 ∈ { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } 𝑧 ∈ ( [,] ‘ 𝑣 ) )
65 46 sseli ⊢ ( 𝑣 ∈ { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } → 𝑣 ∈ ( ℝ × ℝ ) )
66 1st2nd2 ⊢ ( 𝑣 ∈ ( ℝ × ℝ ) → 𝑣 = ⟨ ( 1st ‘ 𝑣 ) , ( 2nd ‘ 𝑣 ) ⟩ )
67 66 fveq2d ⊢ ( 𝑣 ∈ ( ℝ × ℝ ) → ( [,] ‘ 𝑣 ) = ( [,] ‘ ⟨ ( 1st ‘ 𝑣 ) , ( 2nd ‘ 𝑣 ) ⟩ ) )
68 df-ov ⊢ ( ( 1st ‘ 𝑣 ) [,] ( 2nd ‘ 𝑣 ) ) = ( [,] ‘ ⟨ ( 1st ‘ 𝑣 ) , ( 2nd ‘ 𝑣 ) ⟩ )
69 67 68 eqtr4di ⊢ ( 𝑣 ∈ ( ℝ × ℝ ) → ( [,] ‘ 𝑣 ) = ( ( 1st ‘ 𝑣 ) [,] ( 2nd ‘ 𝑣 ) ) )
70 69 eleq2d ⊢ ( 𝑣 ∈ ( ℝ × ℝ ) → ( 𝑧 ∈ ( [,] ‘ 𝑣 ) ↔ 𝑧 ∈ ( ( 1st ‘ 𝑣 ) [,] ( 2nd ‘ 𝑣 ) ) ) )
71 65 70 syl ⊢ ( 𝑣 ∈ { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } → ( 𝑧 ∈ ( [,] ‘ 𝑣 ) ↔ 𝑧 ∈ ( ( 1st ‘ 𝑣 ) [,] ( 2nd ‘ 𝑣 ) ) ) )
72 71 biimpd ⊢ ( 𝑣 ∈ { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } → ( 𝑧 ∈ ( [,] ‘ 𝑣 ) → 𝑧 ∈ ( ( 1st ‘ 𝑣 ) [,] ( 2nd ‘ 𝑣 ) ) ) )
73 72 imdistani ⊢ ( ( 𝑣 ∈ { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } ∧ 𝑧 ∈ ( [,] ‘ 𝑣 ) ) → ( 𝑣 ∈ { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } ∧ 𝑧 ∈ ( ( 1st ‘ 𝑣 ) [,] ( 2nd ‘ 𝑣 ) ) ) )
74 eliccxr ⊢ ( 𝑧 ∈ ( ( 1st ‘ 𝑣 ) [,] ( 2nd ‘ 𝑣 ) ) → 𝑧 ∈ ℝ* )
75 74 ad2antll ⊢ ( ( ( ( ∪ ( [,] “ { 𝑎 ∈ { 𝑏 ∈ 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 ⊢ ( 𝑣 ∈ ( ℝ × ℝ ) → ( 2nd ‘ 𝑣 ) ∈ ℝ )
77 76 rexrd ⊢ ( 𝑣 ∈ ( ℝ × ℝ ) → ( 2nd ‘ 𝑣 ) ∈ ℝ* )
78 65 77 syl ⊢ ( 𝑣 ∈ { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } → ( 2nd ‘ 𝑣 ) ∈ ℝ* )
79 78 ad2antrl ⊢ ( ( ( ( ∪ ( [,] “ { 𝑎 ∈ { 𝑏 ∈ 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 ⊢ ( ( ( ( ∪ ( [,] “ { 𝑎 ∈ { 𝑏 ∈ 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 ‘ 𝑣 ) ) ) ) → 𝑛 ∈ ℝ )
81 80 rexrd ⊢ ( ( ( ( ∪ ( [,] “ { 𝑎 ∈ { 𝑏 ∈ 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 ⊢ ( 𝑣 ∈ ( ℝ × ℝ ) → ( 1st ‘ 𝑣 ) ∈ ℝ )
83 82 rexrd ⊢ ( 𝑣 ∈ ( ℝ × ℝ ) → ( 1st ‘ 𝑣 ) ∈ ℝ* )
84 83 77 jca ⊢ ( 𝑣 ∈ ( ℝ × ℝ ) → ( ( 1st ‘ 𝑣 ) ∈ ℝ* ∧ ( 2nd ‘ 𝑣 ) ∈ ℝ* ) )
85 65 84 syl ⊢ ( 𝑣 ∈ { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } → ( ( 1st ‘ 𝑣 ) ∈ ℝ* ∧ ( 2nd ‘ 𝑣 ) ∈ ℝ* ) )
86 iccleub ⊢ ( ( ( 1st ‘ 𝑣 ) ∈ ℝ* ∧ ( 2nd ‘ 𝑣 ) ∈ ℝ* ∧ 𝑧 ∈ ( ( 1st ‘ 𝑣 ) [,] ( 2nd ‘ 𝑣 ) ) ) → 𝑧 ≤ ( 2nd ‘ 𝑣 ) )
87 86 3expa ⊢ ( ( ( ( 1st ‘ 𝑣 ) ∈ ℝ* ∧ ( 2nd ‘ 𝑣 ) ∈ ℝ* ) ∧ 𝑧 ∈ ( ( 1st ‘ 𝑣 ) [,] ( 2nd ‘ 𝑣 ) ) ) → 𝑧 ≤ ( 2nd ‘ 𝑣 ) )
88 85 87 sylan ⊢ ( ( 𝑣 ∈ { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } ∧ 𝑧 ∈ ( ( 1st ‘ 𝑣 ) [,] ( 2nd ‘ 𝑣 ) ) ) → 𝑧 ≤ ( 2nd ‘ 𝑣 ) )
89 88 adantl ⊢ ( ( ( ( ∪ ( [,] “ { 𝑎 ∈ { 𝑏 ∈ 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 ⊢ ( ℝ × ℝ ) ⊆ ( V × V )
91 46 90 sstri ⊢ { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } ⊆ ( V × V )
92 df-rel ⊢ ( Rel { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } ↔ { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } ⊆ ( V × V ) )
93 91 92 mpbir ⊢ Rel { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) }
94 2ndrn ⊢ ( ( 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 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } )
95 93 94 mpan ⊢ ( 𝑣 ∈ { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } → ( 2nd ‘ 𝑣 ) ∈ ran { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } )
96 breq1 ⊢ ( 𝑢 = ( 2nd ‘ 𝑣 ) → ( 𝑢 ≤ 𝑛 ↔ ( 2nd ‘ 𝑣 ) ≤ 𝑛 ) )
97 96 rspccva ⊢ ( ( ∀ 𝑢 ∈ ran { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } 𝑢 ≤ 𝑛 ∧ ( 2nd ‘ 𝑣 ) ∈ ran { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } ) → ( 2nd ‘ 𝑣 ) ≤ 𝑛 )
98 95 97 sylan2 ⊢ ( ( ∀ 𝑢 ∈ ran { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } 𝑢 ≤ 𝑛 ∧ 𝑣 ∈ { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } ) → ( 2nd ‘ 𝑣 ) ≤ 𝑛 )
99 98 ad2ant2lr ⊢ ( ( ( ( ∪ ( [,] “ { 𝑎 ∈ { 𝑏 ∈ 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 ‘ 𝑣 ) ≤ 𝑛 )
100 75 79 81 89 99 xrletrd ⊢ ( ( ( ( ∪ ( [,] “ { 𝑎 ∈ { 𝑏 ∈ 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 ‘ 𝑣 ) ) ) ) → 𝑧 ≤ 𝑛 )
101 73 100 sylan2 ⊢ ( ( ( ( ∪ ( [,] “ { 𝑎 ∈ { 𝑏 ∈ 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 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } ∧ 𝑧 ∈ ( [,] ‘ 𝑣 ) ) ) → 𝑧 ≤ 𝑛 )
102 101 rexlimdvaa ⊢ ( ( ( ∪ ( [,] “ { 𝑎 ∈ { 𝑏 ∈ 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 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } 𝑧 ∈ ( [,] ‘ 𝑣 ) → 𝑧 ≤ 𝑛 ) )
103 64 102 biimtrid ⊢ ( ( ( ∪ ( [,] “ { 𝑎 ∈ { 𝑏 ∈ 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 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } ) → 𝑧 ≤ 𝑛 ) )
104 103 ralrimiv ⊢ ( ( ( ∪ ( [,] “ { 𝑎 ∈ { 𝑏 ∈ 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 ⊢ ( ∪ ( [,] “ { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } ) = 𝐴 → ( ∀ 𝑧 ∈ ∪ ( [,] “ { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } ) 𝑧 ≤ 𝑛 ↔ ∀ 𝑧 ∈ 𝐴 𝑧 ≤ 𝑛 ) )
106 105 ad2antrr ⊢ ( ( ( ∪ ( [,] “ { 𝑎 ∈ { 𝑏 ∈ 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 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } ) 𝑧 ≤ 𝑛 ↔ ∀ 𝑧 ∈ 𝐴 𝑧 ≤ 𝑛 ) )
107 104 106 mpbid ⊢ ( ( ( ∪ ( [,] “ { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } ) = 𝐴 ∧ 𝑛 ∈ ℝ ) ∧ ∀ 𝑢 ∈ ran { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } 𝑢 ≤ 𝑛 ) → ∀ 𝑧 ∈ 𝐴 𝑧 ≤ 𝑛 )
108 107 ex ⊢ ( ( ∪ ( [,] “ { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } ) = 𝐴 ∧ 𝑛 ∈ ℝ ) → ( ∀ 𝑢 ∈ ran { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } 𝑢 ≤ 𝑛 → ∀ 𝑧 ∈ 𝐴 𝑧 ≤ 𝑛 ) )
109 108 reximdva ⊢ ( ∪ ( [,] “ { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } ) = 𝐴 → ( ∃ 𝑛 ∈ ℝ ∀ 𝑢 ∈ ran { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } 𝑢 ≤ 𝑛 → ∃ 𝑛 ∈ ℝ ∀ 𝑧 ∈ 𝐴 𝑧 ≤ 𝑛 ) )
110 109 adantr ⊢ ( ( ∪ ( [,] “ { 𝑎 ∈ { 𝑏 ∈ 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 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } 𝑢 ≤ 𝑛 → ∃ 𝑛 ∈ ℝ ∀ 𝑧 ∈ 𝐴 𝑧 ≤ 𝑛 ) )
111 54 110 mpd ⊢ ( ( ∪ ( [,] “ { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } ) = 𝐴 ∧ { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } ∈ Fin ) → ∃ 𝑛 ∈ ℝ ∀ 𝑧 ∈ 𝐴 𝑧 ≤ 𝑛 )
112 17 111 nsyl ⊢ ( 𝐴 = ℝ → ¬ ( ∪ ( [,] “ { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } ) = 𝐴 ∧ { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } ∈ Fin ) )
113 112 adantl ⊢ ( ( ( 𝐴 ∈ ( 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 ⊢ ℝ = ∪ ( topGen ‘ ran (,) )
115 retopconn ⊢ ( topGen ‘ ran (,) ) ∈ Conn
116 115 a1i ⊢ ( ( ( 𝐴 ∈ ( 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 ⊢ ( ( ( 𝐴 ∈ ( 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 ⊢ ( ( ( 𝐴 ∈ ( 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 ⊢ ( ( ( 𝐴 ∈ ( 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 ⊢ ( [,] : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ* → Fun [,] )
121 funiunfv ⊢ ( Fun [,] → ∪ 𝑧 ∈ { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } ( [,] ‘ 𝑧 ) = ∪ ( [,] “ { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } ) )
122 56 120 121 mp2b ⊢ ∪ 𝑧 ∈ { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } ( [,] ‘ 𝑧 ) = ∪ ( [,] “ { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } )
123 retop ⊢ ( topGen ‘ ran (,) ) ∈ Top
124 46 sseli ⊢ ( 𝑧 ∈ { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } → 𝑧 ∈ ( ℝ × ℝ ) )
125 1st2nd2 ⊢ ( 𝑧 ∈ ( ℝ × ℝ ) → 𝑧 = ⟨ ( 1st ‘ 𝑧 ) , ( 2nd ‘ 𝑧 ) ⟩ )
126 125 fveq2d ⊢ ( 𝑧 ∈ ( ℝ × ℝ ) → ( [,] ‘ 𝑧 ) = ( [,] ‘ ⟨ ( 1st ‘ 𝑧 ) , ( 2nd ‘ 𝑧 ) ⟩ ) )
127 df-ov ⊢ ( ( 1st ‘ 𝑧 ) [,] ( 2nd ‘ 𝑧 ) ) = ( [,] ‘ ⟨ ( 1st ‘ 𝑧 ) , ( 2nd ‘ 𝑧 ) ⟩ )
128 126 127 eqtr4di ⊢ ( 𝑧 ∈ ( ℝ × ℝ ) → ( [,] ‘ 𝑧 ) = ( ( 1st ‘ 𝑧 ) [,] ( 2nd ‘ 𝑧 ) ) )
129 xp1st ⊢ ( 𝑧 ∈ ( ℝ × ℝ ) → ( 1st ‘ 𝑧 ) ∈ ℝ )
130 xp2nd ⊢ ( 𝑧 ∈ ( ℝ × ℝ ) → ( 2nd ‘ 𝑧 ) ∈ ℝ )
131 icccld ⊢ ( ( ( 1st ‘ 𝑧 ) ∈ ℝ ∧ ( 2nd ‘ 𝑧 ) ∈ ℝ ) → ( ( 1st ‘ 𝑧 ) [,] ( 2nd ‘ 𝑧 ) ) ∈ ( Clsd ‘ ( topGen ‘ ran (,) ) ) )
132 129 130 131 syl2anc ⊢ ( 𝑧 ∈ ( ℝ × ℝ ) → ( ( 1st ‘ 𝑧 ) [,] ( 2nd ‘ 𝑧 ) ) ∈ ( Clsd ‘ ( topGen ‘ ran (,) ) ) )
133 128 132 eqeltrd ⊢ ( 𝑧 ∈ ( ℝ × ℝ ) → ( [,] ‘ 𝑧 ) ∈ ( Clsd ‘ ( topGen ‘ ran (,) ) ) )
134 124 133 syl ⊢ ( 𝑧 ∈ { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } → ( [,] ‘ 𝑧 ) ∈ ( Clsd ‘ ( topGen ‘ ran (,) ) ) )
135 134 rgen ⊢ ∀ 𝑧 ∈ { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } ( [,] ‘ 𝑧 ) ∈ ( Clsd ‘ ( topGen ‘ ran (,) ) )
136 114 iuncld ⊢ ( ( ( 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 (,) ) ) )
137 123 135 136 mp3an13 ⊢ ( { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } ∈ Fin → ∪ 𝑧 ∈ { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } ( [,] ‘ 𝑧 ) ∈ ( Clsd ‘ ( topGen ‘ ran (,) ) ) )
138 122 137 eqeltrrid ⊢ ( { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } ∈ Fin → ∪ ( [,] “ { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } ) ∈ ( Clsd ‘ ( topGen ‘ ran (,) ) ) )
139 138 ad2antll ⊢ ( ( ( 𝐴 ∈ ( 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 (,) ) ) )
140 119 139 eqeltrrd ⊢ ( ( ( 𝐴 ∈ ( 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 (,) ) ) )
141 114 116 117 118 140 connclo ⊢ ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝐴 ≠ ∅ ) ∧ ( ∪ ( [,] “ { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } ) = 𝐴 ∧ { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } ∈ Fin ) ) → 𝐴 = ℝ )
142 141 ex ⊢ ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝐴 ≠ ∅ ) → ( ( ∪ ( [,] “ { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } ) = 𝐴 ∧ { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } ∈ Fin ) → 𝐴 = ℝ ) )
143 142 necon3ad ⊢ ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝐴 ≠ ∅ ) → ( 𝐴 ≠ ℝ → ¬ ( ∪ ( [,] “ { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } ) = 𝐴 ∧ { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } ∈ Fin ) ) )
144 143 imp ⊢ ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝐴 ≠ ∅ ) ∧ 𝐴 ≠ ℝ ) → ¬ ( ∪ ( [,] “ { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } ) = 𝐴 ∧ { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } ∈ Fin ) )
145 113 144 pm2.61dane ⊢ ( ( 𝐴 ∈ ( 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 ⊢ ( 𝑥 = 𝑢 → ( 𝑥 / ( 2 ↑ 𝑦 ) ) = ( 𝑢 / ( 2 ↑ 𝑦 ) ) )
147 oveq1 ⊢ ( 𝑥 = 𝑢 → ( 𝑥 + 1 ) = ( 𝑢 + 1 ) )
148 147 oveq1d ⊢ ( 𝑥 = 𝑢 → ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) = ( ( 𝑢 + 1 ) / ( 2 ↑ 𝑦 ) ) )
149 146 148 opeq12d ⊢ ( 𝑥 = 𝑢 → ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ = ⟨ ( 𝑢 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑢 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ )
150 oveq2 ⊢ ( 𝑦 = 𝑣 → ( 2 ↑ 𝑦 ) = ( 2 ↑ 𝑣 ) )
151 150 oveq2d ⊢ ( 𝑦 = 𝑣 → ( 𝑢 / ( 2 ↑ 𝑦 ) ) = ( 𝑢 / ( 2 ↑ 𝑣 ) ) )
152 150 oveq2d ⊢ ( 𝑦 = 𝑣 → ( ( 𝑢 + 1 ) / ( 2 ↑ 𝑦 ) ) = ( ( 𝑢 + 1 ) / ( 2 ↑ 𝑣 ) ) )
153 151 152 opeq12d ⊢ ( 𝑦 = 𝑣 → ⟨ ( 𝑢 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑢 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ = ⟨ ( 𝑢 / ( 2 ↑ 𝑣 ) ) , ( ( 𝑢 + 1 ) / ( 2 ↑ 𝑣 ) ) ⟩ )
154 149 153 cbvmpov ⊢ ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) = ( 𝑢 ∈ ℤ , 𝑣 ∈ ℕ0 ↦ ⟨ ( 𝑢 / ( 2 ↑ 𝑣 ) ) , ( ( 𝑢 + 1 ) / ( 2 ↑ 𝑣 ) ) ⟩ )
155 fveq2 ⊢ ( 𝑎 = 𝑧 → ( [,] ‘ 𝑎 ) = ( [,] ‘ 𝑧 ) )
156 155 sseq1d ⊢ ( 𝑎 = 𝑧 → ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) ↔ ( [,] ‘ 𝑧 ) ⊆ ( [,] ‘ 𝑐 ) ) )
157 equequ1 ⊢ ( 𝑎 = 𝑧 → ( 𝑎 = 𝑐 ↔ 𝑧 = 𝑐 ) )
158 156 157 imbi12d ⊢ ( 𝑎 = 𝑧 → ( ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) ↔ ( ( [,] ‘ 𝑧 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑧 = 𝑐 ) ) )
159 158 ralbidv ⊢ ( 𝑎 = 𝑧 → ( ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) ↔ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑧 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑧 = 𝑐 ) ) )
160 159 cbvrabv ⊢ { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } = { 𝑧 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑧 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑧 = 𝑐 ) }
161 19 a1i ⊢ ( 𝐴 ∈ ( topGen ‘ ran (,) ) → { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ⊆ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) )
162 154 160 161 dyadmbllem ⊢ ( 𝐴 ∈ ( topGen ‘ ran (,) ) → ∪ ( [,] “ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ) = ∪ ( [,] “ { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } ) )
163 opnmbllem0 ⊢ ( 𝐴 ∈ ( topGen ‘ ran (,) ) → ∪ ( [,] “ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ) = 𝐴 )
164 162 163 eqtr3d ⊢ ( 𝐴 ∈ ( topGen ‘ ran (,) ) → ∪ ( [,] “ { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } ) = 𝐴 )
165 164 adantr ⊢ ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝐴 ≠ ∅ ) → ∪ ( [,] “ { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } ) = 𝐴 )
166 nnenom ⊢ ℕ ≈ ω
167 sdomentr ⊢ ( ( { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } ≺ ℕ ∧ ℕ ≈ ω ) → { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } ≺ ω )
168 166 167 mpan2 ⊢ ( { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } ≺ ℕ → { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } ≺ ω )
169 isfinite ⊢ ( { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } ∈ Fin ↔ { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } ≺ ω )
170 168 169 sylibr ⊢ ( { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } ≺ ℕ → { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } ∈ Fin )
171 165 170 anim12i ⊢ ( ( ( 𝐴 ∈ ( 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 ) )
172 145 171 mtand ⊢ ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝐴 ≠ ∅ ) → ¬ { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } ≺ ℕ )
173 qex ⊢ ℚ ∈ V
174 173 173 xpex ⊢ ( ℚ × ℚ ) ∈ V
175 zq ⊢ ( 𝑥 ∈ ℤ → 𝑥 ∈ ℚ )
176 2nn ⊢ 2 ∈ ℕ
177 nnq ⊢ ( 2 ∈ ℕ → 2 ∈ ℚ )
178 176 177 ax-mp ⊢ 2 ∈ ℚ
179 qexpcl ⊢ ( ( 2 ∈ ℚ ∧ 𝑦 ∈ ℕ0 ) → ( 2 ↑ 𝑦 ) ∈ ℚ )
180 178 179 mpan ⊢ ( 𝑦 ∈ ℕ0 → ( 2 ↑ 𝑦 ) ∈ ℚ )
181 180 29 jca ⊢ ( 𝑦 ∈ ℕ0 → ( ( 2 ↑ 𝑦 ) ∈ ℚ ∧ ( 2 ↑ 𝑦 ) ≠ 0 ) )
182 qdivcl ⊢ ( ( 𝑥 ∈ ℚ ∧ ( 2 ↑ 𝑦 ) ∈ ℚ ∧ ( 2 ↑ 𝑦 ) ≠ 0 ) → ( 𝑥 / ( 2 ↑ 𝑦 ) ) ∈ ℚ )
183 1z ⊢ 1 ∈ ℤ
184 zq ⊢ ( 1 ∈ ℤ → 1 ∈ ℚ )
185 183 184 ax-mp ⊢ 1 ∈ ℚ
186 qaddcl ⊢ ( ( 𝑥 ∈ ℚ ∧ 1 ∈ ℚ ) → ( 𝑥 + 1 ) ∈ ℚ )
187 185 186 mpan2 ⊢ ( 𝑥 ∈ ℚ → ( 𝑥 + 1 ) ∈ ℚ )
188 qdivcl ⊢ ( ( ( 𝑥 + 1 ) ∈ ℚ ∧ ( 2 ↑ 𝑦 ) ∈ ℚ ∧ ( 2 ↑ 𝑦 ) ≠ 0 ) → ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ∈ ℚ )
189 187 188 syl3an1 ⊢ ( ( 𝑥 ∈ ℚ ∧ ( 2 ↑ 𝑦 ) ∈ ℚ ∧ ( 2 ↑ 𝑦 ) ≠ 0 ) → ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ∈ ℚ )
190 opelxpi ⊢ ( ( ( 𝑥 / ( 2 ↑ 𝑦 ) ) ∈ ℚ ∧ ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ∈ ℚ ) → ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ∈ ( ℚ × ℚ ) )
191 182 189 190 syl2anc ⊢ ( ( 𝑥 ∈ ℚ ∧ ( 2 ↑ 𝑦 ) ∈ ℚ ∧ ( 2 ↑ 𝑦 ) ≠ 0 ) → ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ∈ ( ℚ × ℚ ) )
192 191 3expb ⊢ ( ( 𝑥 ∈ ℚ ∧ ( ( 2 ↑ 𝑦 ) ∈ ℚ ∧ ( 2 ↑ 𝑦 ) ≠ 0 ) ) → ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ∈ ( ℚ × ℚ ) )
193 175 181 192 syl2an ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ0 ) → ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ∈ ( ℚ × ℚ ) )
194 193 rgen2 ⊢ ∀ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ℕ0 ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ∈ ( ℚ × ℚ )
195 40 fmpo ⊢ ( ∀ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ℕ0 ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ∈ ( ℚ × ℚ ) ↔ ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) : ( ℤ × ℕ0 ) ⟶ ( ℚ × ℚ ) )
196 194 195 mpbi ⊢ ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) : ( ℤ × ℕ0 ) ⟶ ( ℚ × ℚ )
197 frn ⊢ ( ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) : ( ℤ × ℕ0 ) ⟶ ( ℚ × ℚ ) → ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ⊆ ( ℚ × ℚ ) )
198 196 197 ax-mp ⊢ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ⊆ ( ℚ × ℚ )
199 19 198 sstri ⊢ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ⊆ ( ℚ × ℚ )
200 18 199 sstri ⊢ { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } ⊆ ( ℚ × ℚ )
201 ssdomg ⊢ ( ( ℚ × ℚ ) ∈ V → ( { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } ⊆ ( ℚ × ℚ ) → { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } ≼ ( ℚ × ℚ ) ) )
202 174 200 201 mp2 ⊢ { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } ≼ ( ℚ × ℚ )
203 qnnen ⊢ ℚ ≈ ℕ
204 xpen ⊢ ( ( ℚ ≈ ℕ ∧ ℚ ≈ ℕ ) → ( ℚ × ℚ ) ≈ ( ℕ × ℕ ) )
205 203 203 204 mp2an ⊢ ( ℚ × ℚ ) ≈ ( ℕ × ℕ )
206 xpnnen ⊢ ( ℕ × ℕ ) ≈ ℕ
207 205 206 entri ⊢ ( ℚ × ℚ ) ≈ ℕ
208 domentr ⊢ ( ( { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } ≼ ( ℚ × ℚ ) ∧ ( ℚ × ℚ ) ≈ ℕ ) → { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } ≼ ℕ )
209 202 207 208 mp2an ⊢ { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } ≼ ℕ
210 172 209 jctil ⊢ ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝐴 ≠ ∅ ) → ( { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } ≼ ℕ ∧ ¬ { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } ≺ ℕ ) )
211 bren2 ⊢ ( { 𝑎 ∈ { 𝑏 ∈ 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 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } ≺ ℕ ) )
212 210 211 sylibr ⊢ ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝐴 ≠ ∅ ) → { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } ≈ ℕ )
213 212 ensymd ⊢ ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝐴 ≠ ∅ ) → ℕ ≈ { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } )
214 bren ⊢ ( ℕ ≈ { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } ↔ ∃ 𝑓 𝑓 : ℕ –1-1-onto→ { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } )
215 213 214 sylib ⊢ ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝐴 ≠ ∅ ) → ∃ 𝑓 𝑓 : ℕ –1-1-onto→ { 𝑎 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ∣ ∀ 𝑐 ∈ { 𝑏 ∈ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] ‘ 𝑏 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑐 ) → 𝑎 = 𝑐 ) } )