Theorem tfis2d

Description: Transfinite Induction Schema, using implicit substitution. (Contributed by Emmett Weisz, 3-May-2020)

	Ref	Expression
Hypotheses	tfis2d.1	|- ( ph -> ( x = y -> ( ps <-> ch ) ) )
	tfis2d.2	|- ( ph -> ( x e. On -> ( A. y e. x ch -> ps ) ) )
Assertion	tfis2d	|- ( ph -> ( x e. On -> ps ) )

Proof

Step	Hyp	Ref	Expression
1		tfis2d.1	|- ( ph -> ( x = y -> ( ps <-> ch ) ) )
2		tfis2d.2	|- ( ph -> ( x e. On -> ( A. y e. x ch -> ps ) ) )
3	1	com12	|- ( x = y -> ( ph -> ( ps <-> ch ) ) )
4	3	pm5.74d	|- ( x = y -> ( ( ph -> ps ) <-> ( ph -> ch ) ) )
5		r19.21v	|- ( A. y e. x ( ph -> ch ) <-> ( ph -> A. y e. x ch ) )
6	2	com12	|- ( x e. On -> ( ph -> ( A. y e. x ch -> ps ) ) )
7	6	a2d	|- ( x e. On -> ( ( ph -> A. y e. x ch ) -> ( ph -> ps ) ) )
8	5 7	syl5bi	|- ( x e. On -> ( A. y e. x ( ph -> ch ) -> ( ph -> ps ) ) )
9	4 8	tfis2	|- ( x e. On -> ( ph -> ps ) )
10	9	com12	|- ( ph -> ( x e. On -> ps ) )