How rigorous must my set theory proof be? I'm working on a problem from the book "Introduction to Topology" by Bert Mendelson:

If $A_1\subset A_2, A_2\subset A_3, \ldots , A_{n-1}\subset A_n$, and $A_n \subset A_1$, prove that $A_1=A_2=\cdots=A_n$.

I know how to prove this, but my question is how rigorous my proof should be. For example, to make my proof easier, I proved the following "lemma":

If $H$ and $J$ are sets, $H \subset J$, and $J\subset H$, then $H=J$.

My proof went like this:

From the givens, we can determine that
  $$\alpha \in J, \forall \alpha \in H$$
  $$\beta \in H, \forall \beta \in J$$
  Which means that
  $$\alpha \in J, \forall \alpha \in H$$
  $$\neg \beta \notin H, \forall \beta \in J$$
  and so $H=J$.

I then went on to prove that
$$A_k\subset A_{k+1}, A_{k+1}\subset A_k, \forall k \le n$$
Is my "lemma" proof enough of a proof? This is such a basic lemma that it seems like it should be obvious... but then again, when something seems obvious, it sometimes isn't. Is this rigorous enough? Is it too rigorous?
 A: Opinion based answer.
I think you are confusing "rigor" with "write stuff using quantification symbols and other symbols rather than words". 
You ask about your lemma, which is indeed nearly obvious. If I were required to prove it I'd say
To prove two sets equal I have to prove they contain the same elements. The first inclusion says that every element of $H$ is in $J$, the second says that every element of $J$ is in $H$, so done.
A: In set-theory the notation $A\subseteq B$ is actually an abbreviation for:$$\forall x[x\in A\implies x\in B]$$
This makes $\subseteq$ a preorder on the sets (reflexive and transitive).
Then the axiom of extensionality is the statement that this relation is also anti-symmetric: $$A\subseteq B\wedge B\subseteq A\implies A=B\tag1$$
This makes the relation $\subseteq$ a partial order.
In my view $(1)$ is not a statement that can be proved, but is a statement based on an abbreviation and an axiom.
A: I would say this depends on your audience. 
One kind of audience may be familiar enough with that Lemma that you don't have to provide a whole separate proof for it. And indeed, for some audiences, once you have shown that $A_1\subset A_2, A_2\subset A_3, \ldots , A_{n-1}\subset A_n$, and $A_n \subset A_1$, then to them it is immediately obvious that $A_1=A_2=\cdots=A_n$, so there is nothing to prove here at all. But for others (possibly your  instructor who grades the proof!), more detail is required.
Presumably the context (e.g. the 'level' at which the textbook is written ... and how much detail has gone into other proofs in the text) will give you a fairly good idea as how detailed you should be.
A: My book defines the axiom of extensionality (i.e. the axiom that defines what it means for sets to be identical) as:
$\forall A \ \forall B \ (\forall x (x \in A \leftrightarrow x \in B) \rightarrow A = B)$
and $A \subseteq B$ is defined as:
$\forall A \ \forall B \ (A \subseteq B  \rightarrow \forall x (x \in A \rightarrow x \in B))$
so with these, you can derive $A=B$ from $A \subseteq B$ and $B \subseteq A$
A: If you really wanted to be formal, you'd write:
-- Agda version 2.5.2
data List (A : Set) : Set where
    Nil : List A
    Cons : A → List A → List A

record ⊤ : Set where
    constructor tt

record _∧_ (A B : Set) : Set where
    constructor _,_
    field
        fst : A
        snd : B

All : {A : Set} → List A → (A → Set) → Set
All Nil P = ⊤
All (Cons x xs) P = P x ∧ All xs P

chain : {A : Set} → (A → A → Set) → List A → Set
chain op Nil = ⊤
chain {A} op (Cons x ss) = go x ss
    where go : A → List A → Set
          go s Nil = ⊤
          go s (Cons x ss) = op s x ∧ go x ss

append : {A : Set} → A → List A → List A
append x Nil = Cons x Nil
append x (Cons y xs) = Cons y (append x xs)

thm : {A : Set} → (R : A → A → Set) → ({x y z : A} → R x y → R y z → R x z)
    → (x : A) → (xs : List A) → chain R (Cons x (append x xs)) → All xs (λ y → R x y ∧ R y x)
thm R trans x Nil p = tt
thm {A} R trans x (Cons y xs) (rxy , rs) = let (ryx , p) = go y xs rxy rs in (rxy , ryx) , p
  where go : (y : A) → (xs : List A) → R x y → chain R (Cons y (append x xs)) → R y x ∧ All xs (λ z → R x z ∧ R z x)
        go y Nil rxy (ryx , tt) = ryx , tt
        go y (Cons z xs) rxy (ryz , rs) = let (rzx , p) = go z xs (trans rxy ryz) rs in trans ryz rzx , ((trans rxy ryz , rzx) , p)

Which (constructively) proves for any transitive relation $\sqsubseteq$, if $x_0 \sqsubseteq x_1 \land x_1 \sqsubseteq x_2 \land \cdots \land x_n \sqsubseteq x_0$ then $x_0 \sqsubseteq x_i \land x_i \sqsubseteq x_0$ for all $i\in\{1,\dots,n\}$. For $\sqsubseteq\,=\,\subseteq$, this almost your result. It proves that $x_0 = x_i$ for all $i\in\{1,\dots,n\}$ which clearly implies that they are all equal to each other.
A: If you really wanted formal, get rid of the $\ldots$ and prove it by induction:
For $n=2$ (the minimal case) we have $A_1 \subset A_2$ and $A_2 \subset A_1$.
This means $A_1 = A_2$ by definition of $=$.
Suppose we have the statement holding for $n$ sets, and take $n+1$ sets obeying the hypotheses: $A_1 \subset A_2 \subset, \ldots \subset A_{n-1} \subset A_n \subset A_{n+1}$ and $A_{n+1} \subset A_1$. As $A_n \subset A_{n+1} \subset A_1$ simple transitivity of $\subset$ gives us $A_n \subset A_1$. But then forgetting $A_{n+1}$ for a while, we have $n$ sets obeying the hypotheses, and so we are allowed to conclude $A_1 = A_n$. So $A_{n+1} \subset A_1 = A_n \subset A_{n+1}$ and we have $A_1 = A_{n+1}$ as required. This concludes the induction step.    
So it holds for all $n$. 
A: Assume $(A_i)$ is an indexed family of $n$ sets, with $i \in \Bbb Z_n$ (mod n  addition) and that for every $i$, $A_i \subset A_{i+1}$.
If we can show that for any $i, j \in \Bbb Z_n$,  $A_i \text{( = B)} \subset A_j \text{( = C)}$, then we will have proved that all the sets are equal. If $j = i +1$, no demonstration is necessary. So assume $j \ne i +1$. Since $A_i \subset A_{i+1}$ and $A_{i+1} \subset A_{i+2}$, $\;A_i \subset A_{i+2}$. We can therefore remove $A_{i+1}$ and reindex the cyclic inclusion chain with a new $\Bbb Z_{n-1}$, keeping track of the index assigned to both $B$ and $C$. 
Now simply continue removing sets until $C$ is 'on the right' of $B$.
A: Two Formal Proof (no re-indexing of the set subscripts is necessary here) depending on the same lemma.
Let $(A_i)$ be a fixed indexed family of $n$ sets, with $i \in [1, n]$, such that for every $i \lt n$,
$A_i \subset A_{i+1} \text{ AND } A_n \subset A_1 $.
Lemma: If $n \gt 2$, then the indexed family $(A_i)$ with $i \in [1, n-1]$ satisfies the same cyclic inclusion chain: for every $i \lt n-1$, $\,A_i \subset A_{i+1} \text{ AND } A_{n-1} \subset A_1 $.
Proof: Use transitivity of the inclusion relation.
Note that you can keep applying this lemma until you are 'down to' just two sets, $A_1$ and $A_2$ each contained in the other, so that $A_1 = A_2$.
Proof 1:
The equality relation is (always) transitive, so in particular,
$\text{IF } z = x \text{ AND } x = y \text{ THEN } z = y$
So, if we can show that $A_i = A_1$ for all $i$, the proof will be complete. To obtain a contradiction, suppose we have  $A_1 = A_{i}$ for $1 \lt i \lt k \le n$, but $A_1 \ne A_k$. By the lemma, we can assume $k = n$ since the setup still holds. But if $k = n$ we have $A_k = A_n \subset A_1$, and $A_1 = A_{k-1} \subset A_k$, so that $A_1 = A_k$, a contradiction. 
Proof 2:
Using the lemma you get that $A_1 = A_2$. But letting $n$ back up to $3$, there are now only two sets (to examine), and since each is contained in the other, they are equal. Now let $n$ ascend, one step at a time, back up to the full $n$ sets under consideration, and checking just two at a time, they will all be equal.
