frpoind

Description: The principle of well-founded induction over a partial order. This theorem is a version of frind that does not require the axiom of infinity and can be used to prove wfi and tfi . (Contributed by Scott Fenton, 11-Feb-2022)

		Ref	Expression
	Assertion	frpoind	$⊢ ((R Fr A \land R Po 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		frpomin2	$⊢ ((R Fr A \land R Po 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		indif2	$⊢ R^{-1} [\{y\}] \cap (A ∖ B) = (R^{-1} [\{y\}] \cap A) ∖ B$
9		df-pred	$⊢ Pred (R, (A ∖ B), y) = (A ∖ B) \cap R^{-1} [\{y\}]$
10		incom	$⊢ (A ∖ B) \cap R^{-1} [\{y\}] = R^{-1} [\{y\}] \cap (A ∖ B)$
11	9 10	eqtri	$⊢ Pred (R, (A ∖ B), y) = R^{-1} [\{y\}] \cap (A ∖ B)$
12		df-pred	$⊢ Pred (R, A, y) = A \cap R^{-1} [\{y\}]$
13		incom	$⊢ A \cap R^{-1} [\{y\}] = R^{-1} [\{y\}] \cap A$
14	12 13	eqtri	$⊢ Pred (R, A, y) = R^{-1} [\{y\}] \cap A$
15	14	difeq1i	$⊢ Pred (R, A, y) ∖ B = (R^{-1} [\{y\}] \cap A) ∖ B$
16	8 11 15	3eqtr4i	$⊢ Pred (R, (A ∖ B), y) = Pred (R, A, y) ∖ B$
17	16	eqeq1i	$⊢ Pred (R, (A ∖ B), y) = \emptyset \leftrightarrow Pred (R, A, y) ∖ B = \emptyset$
18		ssdif0	$⊢ Pred (R, A, y) \subseteq B \leftrightarrow Pred (R, A, y) ∖ B = \emptyset$
19	17 18	bitr4i	$⊢ Pred (R, (A ∖ B), y) = \emptyset \leftrightarrow Pred (R, A, y) \subseteq B$
20	19	anbi1ci	$⊢ (\neg y \in B \land Pred (R, (A ∖ B), y) = \emptyset) \leftrightarrow (Pred (R, A, y) \subseteq B \land \neg y \in B)$
21	20	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))$
22	6 7 21	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))$
23	22	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)$
24		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)$
25	23 24	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)$
26	4 25	sylib	$⊢ ((R Fr A \land R Po 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)$
27	26	ex	$⊢ (R Fr A \land R Po 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))$
28	3 27	mpani	$⊢ (R Fr A \land R Po 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))$
29	2 28	syl5bi	$⊢ (R Fr A \land R Po 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))$
30	29	con4d	$⊢ (R Fr A \land R Po A \land R Se A) \to (\forall y \in A (Pred (R, A, y) \subseteq B \to y \in B) \to A \subseteq B)$
31	30	imp	$⊢ ((R Fr A \land R Po A \land R Se A) \land \forall y \in A (Pred (R, A, y) \subseteq B \to y \in B)) \to A \subseteq B$
32	31	adantrl	$⊢ ((R Fr A \land R Po 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$
33		simprl	$⊢ ((R Fr A \land R Po 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$
34	32 33	eqssd	$⊢ ((R Fr A \land R Po 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 frpoind

Proof