Theorem tfindsd

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

	Ref	Expression
Hypotheses	tfindsd.1	$$⊢x=\varnothing \to \left(\psi \leftrightarrow \chi \right)$$
	tfindsd.2	$$⊢x=y\to \left(\psi \leftrightarrow \theta \right)$$
	tfindsd.3	$$⊢x=\mathrm{suc}y\to \left(\psi \leftrightarrow \tau \right)$$
	tfindsd.4	$$⊢x=A\to \left(\psi \leftrightarrow \eta \right)$$
	tfindsd.5	$$⊢\phi \to \chi$$
	tfindsd.6	$$⊢\left(\phi \wedge y\in \mathrm{On}\wedge \theta \right)\to \tau$$
	tfindsd.7	$$⊢\left(\phi \wedge \mathrm{Lim}x\wedge \forall y\in x\theta \right)\to \psi$$
	tfindsd.8	$$⊢\phi \to A\in \mathrm{On}$$
Assertion	tfindsd	$$⊢\phi \to \eta$$

Proof

Step	Hyp	Ref	Expression
1		tfindsd.1	$$⊢x=\varnothing \to \left(\psi \leftrightarrow \chi \right)$$
2		tfindsd.2	$$⊢x=y\to \left(\psi \leftrightarrow \theta \right)$$
3		tfindsd.3	$$⊢x=\mathrm{suc}y\to \left(\psi \leftrightarrow \tau \right)$$
4		tfindsd.4	$$⊢x=A\to \left(\psi \leftrightarrow \eta \right)$$
5		tfindsd.5	$$⊢\phi \to \chi$$
6		tfindsd.6	$$⊢\left(\phi \wedge y\in \mathrm{On}\wedge \theta \right)\to \tau$$
7		tfindsd.7	$$⊢\left(\phi \wedge \mathrm{Lim}x\wedge \forall y\in x\theta \right)\to \psi$$
8		tfindsd.8	$$⊢\phi \to A\in \mathrm{On}$$
9	6	3exp	$$⊢\phi \to \left(y\in \mathrm{On}\to \left(\theta \to \tau \right)\right)$$
10	9	com12	$$⊢y\in \mathrm{On}\to \left(\phi \to \left(\theta \to \tau \right)\right)$$
11	7	3exp	$$⊢\phi \to \left(\mathrm{Lim}x\to \left(\forall y\in x\theta \to \psi \right)\right)$$
12	11	com12	$$⊢\mathrm{Lim}x\to \left(\phi \to \left(\forall y\in x\theta \to \psi \right)\right)$$
13	1 2 3 4 5 10 12	tfinds3	$$⊢A\in \mathrm{On}\to \left(\phi \to \eta \right)$$
14	8 13	mpcom	$$⊢\phi \to \eta$$