4 ms·

Not that it makes sense anyway. Somehow 𝑈⊆𝑋 and 𝑈∈𝑋.

• leanuser83 6y ago
  That is exactly the point being made. That you can spot right away that something "doesn't make sense".
• skissane 6y ago
  No, the point was that 𝑈∈𝑋 is a typo and 𝑈⊆𝑋 is what was intended. Type theory will reject the mistake but set theory will accept it. This is then presented as a reason why mathematicians should prefer type-theory-based proof assistants to set-theory-based ones, since the former will catch these kinds of mistakes while the later won't.
• bobbylarrybobby 6y ago
  That’s possible. For instance, X = {{}} and U = {}. Or in general, if X_0 = {} and X_{i+1} = {X_0, ..., X_i}, then X_i is both an element and a subset of X_j whenever i < j.
• contravariant 6y ago
  That happens all the time with ordinals.