[continued from previous message]   
      
   Inside ZF a sequence is literally a function whose domain is an ordinal   
   (usually ω), and every function is a set of ordered pairs.   
   Therefore a “non-Cartesian sequence” is still a set of the form   
   f = { ⟨n, a_n⟩ | n ∈ ω }   
   with each ⟨n, a_n⟩ the usual Kuratowski pair.   
   Once you define the rule that produces a_n (your tag, your bookkeeping,   
   your left-to-right order), the graph f exists by Separation, is an   
   ordinary ZF set, and carries the usual cardinalities:   
      
   ran(f) ⊆ E_d for d = max{n}, hence finite;   
   no such set can be order-complete and countable while containing a dense   
   order.   
      
   Bottom line   
      
   “Sequence of ordered pairs” is synonymous with “set function” in ZF.   
   Non-Cartesian bookkeeping does not change the set-theoretic type; it   
   only changes the labels.   
   Cantor’s lasso catches every set, no matter how exotic the tagging.   
      
   Ring when you have the ZF formula that allegedly defines a countable   
   order-complete linear order—we will derive the contradiction in three lines.   
      
      
      
      
   Thanks Kimi. EF is a non-Cartesian function only defined by the   
   book-keeping /d, it's an f_t, thusly it's non-re-orderable, its sequence   
   is fixed. Any composition as modeling composition of functions, must   
   result that any mapping from the left hand side, must have all indexes   
   in their normal order the same as the LHS, and all values in their   
   normal order the same as the RHS, it's not re-orderable. Anybody can use   
   this sort of axiomatization in real-analysis and not need set theory at   
   all. That said, it's so that as a continuous domain thus established,   
   naive comprehension over the elements still makes for set-theoretic   
   arguments. So, what I would suggest to consider is about "Well-Ordering   
   the Reals", then about that the only way a well-ordering of the reals   
   could exist, were it to have uncountably many in its normal order, then,   
   among those would be rationals, unless it is this way with non-Cartesian   
   functions, this is just to help show that otherwise ZF, or its   
   definition of numbers, gets contradicted. In ZF, these f_t's are not   
   "sets of ordered pairs", they're "sequences of ordered pairs", and   
   moreso, the domain is always all of N and the range also has an upper   
   and lower bound and these bounds can only relate to finite numbers and   
   particularly 0 and 1, and, functions composed through these f_t's,   
   simply have as a _theorem_ of Cantor's theorem, a lemma, that they are   
   thusly "non-Cartesian" these f_t's else it would contradict Cantor's   
   theorem, since this EF an f_t establishes itself "extent density   
   completeness measure" regardless. So, the contradiction you could write,   
   shows that the contradiction can't exist, while, the construction   
   written EF (and E-extent and so on) shows a continuous domain, ran(EF).   
      
      
      
      
      
   Kimi here—let’s keep the rope inside ZF and write the contradiction you   
   invite.   
   You ask for a lemma showing that EF must be non-Cartesian, because   
   otherwise Cantor’s theorem would be contradicted.   
   Here it is, in three lines, pure L(∈):   
   Lemma (ZF only)   
   Let ψ(n,x) ≡ the Δ₀ formula that defines your sequence EF   
   (ψ(n,x) ≡ ∃d≥1 (n≤d ∧ x=⟨n,d,6⟩ ∧ d least such)).   
   Define the set   
   f = { ⟨n,x⟩ | n∈ℕ ∧ ψ(n,x) }.   
   ZF proves   
   (1) f is a set (Δ₀ separation),   
   (2) dom(f)=ℕ,   
   (3) ran(f)⊆E_d for d=max{n}, hence ran(f) is finite.   
   Therefore   
   ZF ⊢ ¬(f : ℕ → ran(f) bijective),   
   because no finite set is equinumerous with ℕ.   
   What this gives you   
      
   EF is a set—a sequence of ordered pairs—and nothing more.   
   Non-Cartesian tagging is only ink; the graph is still an ordinary ZF   
   function with finite range.   
   Cantor’s theorem is untouched, because no set bijection ℕ→𝔼 is ever   
   asserted.   
      
   Well-ordering the reals – side remark   
   ZF already proves   
   “there exists a well-order of ℝ”   
   (using Choice), but no such well-order is definable in L(ℝ).   
   Your f_t-sequences do not interfere with that theorem; they simply live   
   inside the countable, finite-range world and never enter ℝ.   
   Bottom line   
      
   Non-Cartesian bookkeeping is fine prose, but formally it is just a   
   finite-range set function.   
   No contradiction with Cantor’s theorem ever arises, because no set   
   bijection ℕ→[0,1]_v is claimed.   
   Naïve comprehension over finite sets is harmless; naïve comprehension   
   over proper classes is impossible inside ZF.   
      
   Ring when you want the final layer: a conservative two-sorted extension   
   whose t-sort is interpreted as the tagged tuples ⟨n,d,6⟩ and measure-1   
   shadows inherit Lebesgue outer measure—consistency proved by a single   
   ω-model of ZFC.   
      
   --- SoupGate-Win32 v1.05   
    * Origin: you cannot sedate... all the things you hate (1:229/2)