setind

Description: Set (epsilon) induction. Theorem 5.22 of TakeutiZaring p. 21. (Contributed by NM, 17-Sep-2003)

		Ref	Expression
	Assertion	setind	$⊢ \forall x (x \subseteq A \to x \in A) \to A = V$

Step	Hyp	Ref	Expression
1		ssindif0	$⊢ y \subseteq A \leftrightarrow y \cap (V ∖ A) = \emptyset$
2		sseq1	$⊢ x = y \to (x \subseteq A \leftrightarrow y \subseteq A)$
3		eleq1w	$⊢ x = y \to (x \in A \leftrightarrow y \in A)$
4	2 3	imbi12d	$⊢ x = y \to ((x \subseteq A \to x \in A) \leftrightarrow (y \subseteq A \to y \in A))$
5	4	spvv	$⊢ \forall x (x \subseteq A \to x \in A) \to (y \subseteq A \to y \in A)$
6	1 5	biimtrrid	$⊢ \forall x (x \subseteq A \to x \in A) \to (y \cap (V ∖ A) = \emptyset \to y \in A)$
7		eldifn	$⊢ y \in (V ∖ A) \to \neg y \in A$
8	6 7	nsyli	$⊢ \forall x (x \subseteq A \to x \in A) \to (y \in (V ∖ A) \to \neg y \cap (V ∖ A) = \emptyset)$
9	8	imp	$⊢ (\forall x (x \subseteq A \to x \in A) \land y \in (V ∖ A)) \to \neg y \cap (V ∖ A) = \emptyset$
10	9	nrexdv	$⊢ \forall x (x \subseteq A \to x \in A) \to \neg \exists y \in (V ∖ A) y \cap (V ∖ A) = \emptyset$
11		zfregs	$⊢ V ∖ A \neq \emptyset \to \exists y \in (V ∖ A) y \cap (V ∖ A) = \emptyset$
12	11	necon1bi	$⊢ \neg \exists y \in (V ∖ A) y \cap (V ∖ A) = \emptyset \to V ∖ A = \emptyset$
13	10 12	syl	$⊢ \forall x (x \subseteq A \to x \in A) \to V ∖ A = \emptyset$
14		vdif0	$⊢ A = V \leftrightarrow V ∖ A = \emptyset$
15	13 14	sylibr	$⊢ \forall x (x \subseteq A \to x \in A) \to A = V$

Metamath Proof Explorer