Peano axiom V in Halmos's Naive Set Theory — does the proof only need transitivity, not the no-self-membership lemma?
Hello, everyone. I am an undergraduate in my first semester, and I've been self-studying Halmos' "Naive Set Theory." Yesterday, I discovered an alternate approach to a proof that works with fewer assumptions. I discussed this with my professor, who told me to share it here. He confirmed that my result was correct, but suggested I post it to see if there are any gaps.
I'm working through Halmos's Naive Set Theory. In Chapter 12 he proves the successor function is injective on ω using two lemmas:
- (i) No natural number contains itself
- (ii) Every natural number is transitive
His proof uses both. But I think the following works using only (ii) and Extensionality (which was established in the first chapter as an axiom).
Since n ⊆ m and m ⊆ n, Extensionality gives n = m directly, contradicting n ≠ m. Lemma (i) is never used.
Extensionality is an axiom; no proof burden, so this eliminates one lemma from the proof infrastructure entirely.
My question: is there a reason Halmos preferred his route? Is this observation already well known?