Theorem tfindsd

Description: Deduction associated with tfinds . (Contributed by Rohan Ridenour, 8-Aug-2023)

	Ref	Expression
Hypotheses	tfindsd.1	|- ( x = (/) -> ( ps <-> ch ) )
	tfindsd.2	|- ( x = y -> ( ps <-> th ) )
	tfindsd.3	|- ( x = suc y -> ( ps <-> ta ) )
	tfindsd.4	|- ( x = A -> ( ps <-> et ) )
	tfindsd.5	|- ( ph -> ch )
	tfindsd.6	|- ( ( ph /\ y e. On /\ th ) -> ta )
	tfindsd.7	|- ( ( ph /\ Lim x /\ A. y e. x th ) -> ps )
	tfindsd.8	|- ( ph -> A e. On )
Assertion	tfindsd	|- ( ph -> et )

Proof

Step	Hyp	Ref	Expression
1		tfindsd.1	|- ( x = (/) -> ( ps <-> ch ) )
2		tfindsd.2	|- ( x = y -> ( ps <-> th ) )
3		tfindsd.3	|- ( x = suc y -> ( ps <-> ta ) )
4		tfindsd.4	|- ( x = A -> ( ps <-> et ) )
5		tfindsd.5	|- ( ph -> ch )
6		tfindsd.6	|- ( ( ph /\ y e. On /\ th ) -> ta )
7		tfindsd.7	|- ( ( ph /\ Lim x /\ A. y e. x th ) -> ps )
8		tfindsd.8	|- ( ph -> A e. On )
9	6	3exp	|- ( ph -> ( y e. On -> ( th -> ta ) ) )
10	9	com12	|- ( y e. On -> ( ph -> ( th -> ta ) ) )
11	7	3exp	|- ( ph -> ( Lim x -> ( A. y e. x th -> ps ) ) )
12	11	com12	|- ( Lim x -> ( ph -> ( A. y e. x th -> ps ) ) )
13	1 2 3 4 5 10 12	tfinds3	|- ( A e. On -> ( ph -> et ) )
14	8 13	mpcom	|- ( ph -> et )