frpoins2fg

Description: Well-Founded Induction schema, using implicit substitution. (Contributed by Scott Fenton, 24-Aug-2022)

	Ref	Expression
Hypotheses	frpoins2fg.1	$⊢ y \in A \to (\forall z \in Pred (R, A, y) ψ \to φ)$
	frpoins2fg.2	$⊢ Ⅎ y ψ$
	frpoins2fg.3	$⊢ y = z \to (φ \leftrightarrow ψ)$
Assertion	frpoins2fg	$⊢ (R Fr A \land R Po A \land R Se A) \to \forall y \in A φ$

Step	Hyp	Ref	Expression
1		frpoins2fg.1	$⊢ y \in A \to (\forall z \in Pred (R, A, y) ψ \to φ)$
2		frpoins2fg.2	$⊢ Ⅎ y ψ$
3		frpoins2fg.3	$⊢ y = z \to (φ \leftrightarrow ψ)$
4		sbsbc	$⊢ [z/ y] φ \leftrightarrow \underset{˙}{[} z / y \underset{˙}{]} φ$
5	2 3	sbiev	$⊢ [z/ y] φ \leftrightarrow ψ$
6	4 5	bitr3i	$⊢ \underset{˙}{[} z / y \underset{˙}{]} φ \leftrightarrow ψ$
7	6	ralbii	$⊢ \forall z \in Pred (R, A, y) \underset{˙}{[} z / y \underset{˙}{]} φ \leftrightarrow \forall z \in Pred (R, A, y) ψ$
8	1	adantl	$⊢ ((R Fr A \land R Po A \land R Se A) \land y \in A) \to (\forall z \in Pred (R, A, y) ψ \to φ)$
9	7 8	biimtrid	$⊢ ((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 φ)$
10	9	frpoinsg	$⊢ (R Fr A \land R Po A \land R Se A) \to \forall y \in A φ$

Metamath Proof Explorer