setindtr

Description: Set induction for sets contained in a transitive set. If we are allowed to assume Infinity, then all sets have a transitive closure and this reduces to setind ; however, this version is useful without Infinity. (Contributed by Stefan O'Rear, 28-Oct-2014)

		Ref	Expression
	Assertion	setindtr	$⊢ \forall x (x \subseteq A \to x \in A) \to (\exists y (Tr y \land B \in y) \to B \in A)$

Proof

Step	Hyp	Ref	Expression
1		nfv	$⊢ Ⅎ x Tr y$
2		nfa1	$⊢ Ⅎ x \forall x (x \subseteq A \to x \in A)$
3	1 2	nfan	$⊢ Ⅎ x (Tr y \land \forall x (x \subseteq A \to x \in A))$
4		eldifn	$⊢ x \in (y ∖ A) \to \neg x \in A$
5	4	adantl	$⊢ ((Tr y \land \forall x (x \subseteq A \to x \in A)) \land x \in (y ∖ A)) \to \neg x \in A$
6		trss	$⊢ Tr y \to (x \in y \to x \subseteq y)$
7		eldifi	$⊢ x \in (y ∖ A) \to x \in y$
8	6 7	impel	$⊢ (Tr y \land x \in (y ∖ A)) \to x \subseteq y$
9		dfss2	$⊢ x \subseteq y \leftrightarrow x \cap y = x$
10	8 9	sylib	$⊢ (Tr y \land x \in (y ∖ A)) \to x \cap y = x$
11	10	adantlr	$⊢ ((Tr y \land \forall x (x \subseteq A \to x \in A)) \land x \in (y ∖ A)) \to x \cap y = x$
12	11	sseq1d	$⊢ ((Tr y \land \forall x (x \subseteq A \to x \in A)) \land x \in (y ∖ A)) \to (x \cap y \subseteq A \leftrightarrow x \subseteq A)$
13		sp	$⊢ \forall x (x \subseteq A \to x \in A) \to (x \subseteq A \to x \in A)$
14	13	ad2antlr	$⊢ ((Tr y \land \forall x (x \subseteq A \to x \in A)) \land x \in (y ∖ A)) \to (x \subseteq A \to x \in A)$
15	12 14	sylbid	$⊢ ((Tr y \land \forall x (x \subseteq A \to x \in A)) \land x \in (y ∖ A)) \to (x \cap y \subseteq A \to x \in A)$
16	5 15	mtod	$⊢ ((Tr y \land \forall x (x \subseteq A \to x \in A)) \land x \in (y ∖ A)) \to \neg x \cap y \subseteq A$
17		inssdif0	$⊢ x \cap y \subseteq A \leftrightarrow x \cap (y ∖ A) = \emptyset$
18	16 17	sylnib	$⊢ ((Tr y \land \forall x (x \subseteq A \to x \in A)) \land x \in (y ∖ A)) \to \neg x \cap (y ∖ A) = \emptyset$
19	18	ex	$⊢ (Tr y \land \forall x (x \subseteq A \to x \in A)) \to (x \in (y ∖ A) \to \neg x \cap (y ∖ A) = \emptyset)$
20	3 19	ralrimi	$⊢ (Tr y \land \forall x (x \subseteq A \to x \in A)) \to \forall x \in (y ∖ A) \neg x \cap (y ∖ A) = \emptyset$
21		ralnex	$⊢ \forall x \in (y ∖ A) \neg x \cap (y ∖ A) = \emptyset \leftrightarrow \neg \exists x \in (y ∖ A) x \cap (y ∖ A) = \emptyset$
22	20 21	sylib	$⊢ (Tr y \land \forall x (x \subseteq A \to x \in A)) \to \neg \exists x \in (y ∖ A) x \cap (y ∖ A) = \emptyset$
23		vex	$⊢ y \in V$
24	23	difexi	$⊢ y ∖ A \in V$
25		zfreg	$⊢ (y ∖ A \in V \land y ∖ A \neq \emptyset) \to \exists x \in (y ∖ A) x \cap (y ∖ A) = \emptyset$
26	24 25	mpan	$⊢ y ∖ A \neq \emptyset \to \exists x \in (y ∖ A) x \cap (y ∖ A) = \emptyset$
27	26	necon1bi	$⊢ \neg \exists x \in (y ∖ A) x \cap (y ∖ A) = \emptyset \to y ∖ A = \emptyset$
28	22 27	syl	$⊢ (Tr y \land \forall x (x \subseteq A \to x \in A)) \to y ∖ A = \emptyset$
29		ssdif0	$⊢ y \subseteq A \leftrightarrow y ∖ A = \emptyset$
30	28 29	sylibr	$⊢ (Tr y \land \forall x (x \subseteq A \to x \in A)) \to y \subseteq A$
31	30	adantlr	$⊢ ((Tr y \land B \in y) \land \forall x (x \subseteq A \to x \in A)) \to y \subseteq A$
32		simplr	$⊢ ((Tr y \land B \in y) \land \forall x (x \subseteq A \to x \in A)) \to B \in y$
33	31 32	sseldd	$⊢ ((Tr y \land B \in y) \land \forall x (x \subseteq A \to x \in A)) \to B \in A$
34	33	ex	$⊢ (Tr y \land B \in y) \to (\forall x (x \subseteq A \to x \in A) \to B \in A)$
35	34	exlimiv	$⊢ \exists y (Tr y \land B \in y) \to (\forall x (x \subseteq A \to x \in A) \to B \in A)$
36	35	com12	$⊢ \forall x (x \subseteq A \to x \in A) \to (\exists y (Tr y \land B \in y) \to B \in A)$

Metamath Proof Explorer

Theorem setindtr

Proof