frind

Description: The principle of founded induction. Theorem 4.4 of Don Monk's notes (see frmin ). This principle states that if B is a subclass of a founded class A with the property that every element of B whose initial segment is included in A is itself equal to A . Compare wfi and tfi , which are special cases of this theorem that do not require the axiom of infinity to prove. (Contributed by Scott Fenton, 6-Feb-2011) (Revised by Mario Carneiro, 26-Jun-2015)

		Ref	Expression
	Assertion	frind	$⊢ ((R Fr A \land R Se A) \land (B \subseteq A \land \forall y \in A (Pred (R, A, y) \subseteq B \to y \in B))) \to A = B$

Proof

Step	Hyp	Ref	Expression
1		ssdif0	$⊢ A \subseteq B \leftrightarrow A ∖ B = \emptyset$
2	1	necon3bbii	$⊢ \neg A \subseteq B \leftrightarrow A ∖ B \neq \emptyset$
3		difss	$⊢ A ∖ B \subseteq A$
4		frmin	$⊢ ((R Fr A \land R Se A) \land (A ∖ B \subseteq A \land A ∖ B \neq \emptyset)) \to \exists y \in (A ∖ B) Pred (R, (A ∖ B), y) = \emptyset$
5		eldif	$⊢ y \in (A ∖ B) \leftrightarrow (y \in A \land \neg y \in B)$
6	5	anbi1i	$⊢ (y \in (A ∖ B) \land Pred (R, (A ∖ B), y) = \emptyset) \leftrightarrow ((y \in A \land \neg y \in B) \land Pred (R, (A ∖ B), y) = \emptyset)$
7		anass	$⊢ ((y \in A \land \neg y \in B) \land Pred (R, (A ∖ B), y) = \emptyset) \leftrightarrow (y \in A \land (\neg y \in B \land Pred (R, (A ∖ B), y) = \emptyset))$
8		ancom	$⊢ (\neg y \in B \land Pred (R, (A ∖ B), y) = \emptyset) \leftrightarrow (Pred (R, (A ∖ B), y) = \emptyset \land \neg y \in B)$
9		indif2	$⊢ R^{-1} [\{y\}] \cap (A ∖ B) = (R^{-1} [\{y\}] \cap A) ∖ B$
10		df-pred	$⊢ Pred (R, (A ∖ B), y) = (A ∖ B) \cap R^{-1} [\{y\}]$
11		incom	$⊢ (A ∖ B) \cap R^{-1} [\{y\}] = R^{-1} [\{y\}] \cap (A ∖ B)$
12	10 11	eqtri	$⊢ Pred (R, (A ∖ B), y) = R^{-1} [\{y\}] \cap (A ∖ B)$
13		df-pred	$⊢ Pred (R, A, y) = A \cap R^{-1} [\{y\}]$
14		incom	$⊢ A \cap R^{-1} [\{y\}] = R^{-1} [\{y\}] \cap A$
15	13 14	eqtri	$⊢ Pred (R, A, y) = R^{-1} [\{y\}] \cap A$
16	15	difeq1i	$⊢ Pred (R, A, y) ∖ B = (R^{-1} [\{y\}] \cap A) ∖ B$
17	9 12 16	3eqtr4i	$⊢ Pred (R, (A ∖ B), y) = Pred (R, A, y) ∖ B$
18	17	eqeq1i	$⊢ Pred (R, (A ∖ B), y) = \emptyset \leftrightarrow Pred (R, A, y) ∖ B = \emptyset$
19		ssdif0	$⊢ Pred (R, A, y) \subseteq B \leftrightarrow Pred (R, A, y) ∖ B = \emptyset$
20	18 19	bitr4i	$⊢ Pred (R, (A ∖ B), y) = \emptyset \leftrightarrow Pred (R, A, y) \subseteq B$
21	20	anbi1i	$⊢ (Pred (R, (A ∖ B), y) = \emptyset \land \neg y \in B) \leftrightarrow (Pred (R, A, y) \subseteq B \land \neg y \in B)$
22	8 21	bitri	$⊢ (\neg y \in B \land Pred (R, (A ∖ B), y) = \emptyset) \leftrightarrow (Pred (R, A, y) \subseteq B \land \neg y \in B)$
23	22	anbi2i	$⊢ (y \in A \land (\neg y \in B \land Pred (R, (A ∖ B), y) = \emptyset)) \leftrightarrow (y \in A \land (Pred (R, A, y) \subseteq B \land \neg y \in B))$
24	6 7 23	3bitri	$⊢ (y \in (A ∖ B) \land Pred (R, (A ∖ B), y) = \emptyset) \leftrightarrow (y \in A \land (Pred (R, A, y) \subseteq B \land \neg y \in B))$
25	24	rexbii2	$⊢ \exists y \in (A ∖ B) Pred (R, (A ∖ B), y) = \emptyset \leftrightarrow \exists y \in A (Pred (R, A, y) \subseteq B \land \neg y \in B)$
26		rexanali	$⊢ \exists y \in A (Pred (R, A, y) \subseteq B \land \neg y \in B) \leftrightarrow \neg \forall y \in A (Pred (R, A, y) \subseteq B \to y \in B)$
27	25 26	bitri	$⊢ \exists y \in (A ∖ B) Pred (R, (A ∖ B), y) = \emptyset \leftrightarrow \neg \forall y \in A (Pred (R, A, y) \subseteq B \to y \in B)$
28	4 27	sylib	$⊢ ((R Fr A \land R Se A) \land (A ∖ B \subseteq A \land A ∖ B \neq \emptyset)) \to \neg \forall y \in A (Pred (R, A, y) \subseteq B \to y \in B)$
29	28	ex	$⊢ (R Fr A \land R Se A) \to ((A ∖ B \subseteq A \land A ∖ B \neq \emptyset) \to \neg \forall y \in A (Pred (R, A, y) \subseteq B \to y \in B))$
30	3 29	mpani	$⊢ (R Fr A \land R Se A) \to (A ∖ B \neq \emptyset \to \neg \forall y \in A (Pred (R, A, y) \subseteq B \to y \in B))$
31	2 30	syl5bi	$⊢ (R Fr A \land R Se A) \to (\neg A \subseteq B \to \neg \forall y \in A (Pred (R, A, y) \subseteq B \to y \in B))$
32	31	con4d	$⊢ (R Fr A \land R Se A) \to (\forall y \in A (Pred (R, A, y) \subseteq B \to y \in B) \to A \subseteq B)$
33	32	imp	$⊢ ((R Fr A \land R Se A) \land \forall y \in A (Pred (R, A, y) \subseteq B \to y \in B)) \to A \subseteq B$
34	33	adantrl	$⊢ ((R Fr A \land R Se A) \land (B \subseteq A \land \forall y \in A (Pred (R, A, y) \subseteq B \to y \in B))) \to A \subseteq B$
35		simprl	$⊢ ((R Fr A \land R Se A) \land (B \subseteq A \land \forall y \in A (Pred (R, A, y) \subseteq B \to y \in B))) \to B \subseteq A$
36	34 35	eqssd	$⊢ ((R Fr A \land R Se A) \land (B \subseteq A \land \forall y \in A (Pred (R, A, y) \subseteq B \to y \in B))) \to A = B$

Metamath Proof Explorer

Theorem frind

Proof