frpoinsg

Description: Well-Founded Induction Schema (variant). If a property passes from all elements less than y of a well-founded set-like partial order class A to y itself (induction hypothesis), then the property holds for all elements of A . (Contributed by Scott Fenton, 11-Feb-2022)

		Ref	Expression
	Hypothesis	frpoinsg.1	$⊢ ((R Fr A \land R Po A \land R Se A) \land y \in A) \to (\forall z \in Pred (R, A, y) \underset{˙}{[} z / y \underset{˙}{]} φ \to φ)$
	Assertion	frpoinsg	$⊢ (R Fr A \land R Po A \land R Se A) \to \forall y \in A φ$

Proof

Step	Hyp	Ref	Expression
1		frpoinsg.1	$⊢ ((R Fr A \land R Po A \land R Se A) \land y \in A) \to (\forall z \in Pred (R, A, y) \underset{˙}{[} z / y \underset{˙}{]} φ \to φ)$
2		dfss3	$⊢ Pred (R, A, w) \subseteq \{y \in A \| φ\} \leftrightarrow \forall z \in Pred (R, A, w) z \in \{y \in A \| φ\}$
3		nfcv	$⊢ \underline{Ⅎ} y A$
4	3	elrabsf	$⊢ z \in \{y \in A \| φ\} \leftrightarrow (z \in A \land \underset{˙}{[} z / y \underset{˙}{]} φ)$
5	4	simprbi	$⊢ z \in \{y \in A \| φ\} \to \underset{˙}{[} z / y \underset{˙}{]} φ$
6	5	ralimi	$⊢ \forall z \in Pred (R, A, w) z \in \{y \in A \| φ\} \to \forall z \in Pred (R, A, w) \underset{˙}{[} z / y \underset{˙}{]} φ$
7	2 6	sylbi	$⊢ Pred (R, A, w) \subseteq \{y \in A \| φ\} \to \forall z \in Pred (R, A, w) \underset{˙}{[} z / y \underset{˙}{]} φ$
8		nfv	$⊢ Ⅎ y ((R Fr A \land R Po A \land R Se A) \land w \in A)$
9		nfcv	$⊢ \underline{Ⅎ} y Pred (R, A, w)$
10		nfsbc1v	$⊢ Ⅎ y \underset{˙}{[} z / y \underset{˙}{]} φ$
11	9 10	nfralw	$⊢ Ⅎ y \forall z \in Pred (R, A, w) \underset{˙}{[} z / y \underset{˙}{]} φ$
12		nfsbc1v	$⊢ Ⅎ y \underset{˙}{[} w / y \underset{˙}{]} φ$
13	11 12	nfim	$⊢ Ⅎ y (\forall z \in Pred (R, A, w) \underset{˙}{[} z / y \underset{˙}{]} φ \to \underset{˙}{[} w / y \underset{˙}{]} φ)$
14	8 13	nfim	$⊢ Ⅎ y (((R Fr A \land R Po A \land R Se A) \land w \in A) \to (\forall z \in Pred (R, A, w) \underset{˙}{[} z / y \underset{˙}{]} φ \to \underset{˙}{[} w / y \underset{˙}{]} φ))$
15		eleq1w	$⊢ y = w \to (y \in A \leftrightarrow w \in A)$
16	15	anbi2d	$⊢ y = w \to (((R Fr A \land R Po A \land R Se A) \land y \in A) \leftrightarrow ((R Fr A \land R Po A \land R Se A) \land w \in A))$
17		predeq3	$⊢ y = w \to Pred (R, A, y) = Pred (R, A, w)$
18	17	raleqdv	$⊢ y = w \to (\forall z \in Pred (R, A, y) \underset{˙}{[} z / y \underset{˙}{]} φ \leftrightarrow \forall z \in Pred (R, A, w) \underset{˙}{[} z / y \underset{˙}{]} φ)$
19		sbceq1a	$⊢ y = w \to (φ \leftrightarrow \underset{˙}{[} w / y \underset{˙}{]} φ)$
20	18 19	imbi12d	$⊢ y = w \to ((\forall z \in Pred (R, A, y) \underset{˙}{[} z / y \underset{˙}{]} φ \to φ) \leftrightarrow (\forall z \in Pred (R, A, w) \underset{˙}{[} z / y \underset{˙}{]} φ \to \underset{˙}{[} w / y \underset{˙}{]} φ))$
21	16 20	imbi12d	$⊢ y = w \to ((((R Fr A \land R Po A \land R Se A) \land y \in A) \to (\forall z \in Pred (R, A, y) \underset{˙}{[} z / y \underset{˙}{]} φ \to φ)) \leftrightarrow (((R Fr A \land R Po A \land R Se A) \land w \in A) \to (\forall z \in Pred (R, A, w) \underset{˙}{[} z / y \underset{˙}{]} φ \to \underset{˙}{[} w / y \underset{˙}{]} φ)))$
22	14 21 1	chvarfv	$⊢ ((R Fr A \land R Po A \land R Se A) \land w \in A) \to (\forall z \in Pred (R, A, w) \underset{˙}{[} z / y \underset{˙}{]} φ \to \underset{˙}{[} w / y \underset{˙}{]} φ)$
23	7 22	syl5	$⊢ ((R Fr A \land R Po A \land R Se A) \land w \in A) \to (Pred (R, A, w) \subseteq \{y \in A \| φ\} \to \underset{˙}{[} w / y \underset{˙}{]} φ)$
24		simpr	$⊢ ((R Fr A \land R Po A \land R Se A) \land w \in A) \to w \in A$
25	23 24	jctild	$⊢ ((R Fr A \land R Po A \land R Se A) \land w \in A) \to (Pred (R, A, w) \subseteq \{y \in A \| φ\} \to (w \in A \land \underset{˙}{[} w / y \underset{˙}{]} φ))$
26	3	elrabsf	$⊢ w \in \{y \in A \| φ\} \leftrightarrow (w \in A \land \underset{˙}{[} w / y \underset{˙}{]} φ)$
27	25 26	imbitrrdi	$⊢ ((R Fr A \land R Po A \land R Se A) \land w \in A) \to (Pred (R, A, w) \subseteq \{y \in A \| φ\} \to w \in \{y \in A \| φ\})$
28	27	ralrimiva	$⊢ (R Fr A \land R Po A \land R Se A) \to \forall w \in A (Pred (R, A, w) \subseteq \{y \in A \| φ\} \to w \in \{y \in A \| φ\})$
29		ssrab2	$⊢ \{y \in A \| φ\} \subseteq A$
30	28 29	jctil	$⊢ (R Fr A \land R Po A \land R Se A) \to (\{y \in A \| φ\} \subseteq A \land \forall w \in A (Pred (R, A, w) \subseteq \{y \in A \| φ\} \to w \in \{y \in A \| φ\}))$
31		frpoind	$⊢ ((R Fr A \land R Po A \land R Se A) \land (\{y \in A \| φ\} \subseteq A \land \forall w \in A (Pred (R, A, w) \subseteq \{y \in A \| φ\} \to w \in \{y \in A \| φ\}))) \to A = \{y \in A \| φ\}$
32	30 31	mpdan	$⊢ (R Fr A \land R Po A \land R Se A) \to A = \{y \in A \| φ\}$
33		rabid2	$⊢ A = \{y \in A \| φ\} \leftrightarrow \forall y \in A φ$
34	32 33	sylib	$⊢ (R Fr A \land R Po A \land R Se A) \to \forall y \in A φ$

Metamath Proof Explorer

Theorem frpoinsg

Proof