tfindsd

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

	Ref	Expression
Hypotheses	tfindsd.1	$⊢ x = \emptyset \to (ψ \leftrightarrow χ)$
	tfindsd.2	$⊢ x = y \to (ψ \leftrightarrow θ)$
	tfindsd.3	$⊢ x = suc y \to (ψ \leftrightarrow τ)$
	tfindsd.4	$⊢ x = A \to (ψ \leftrightarrow η)$
	tfindsd.5	$⊢ φ \to χ$
	tfindsd.6	$⊢ (φ \land y \in On \land θ) \to τ$
	tfindsd.7	$⊢ (φ \land Lim x \land \forall y \in x θ) \to ψ$
	tfindsd.8	$⊢ φ \to A \in On$
Assertion	tfindsd	$⊢ φ \to η$

Step	Hyp	Ref	Expression
1		tfindsd.1	$⊢ x = \emptyset \to (ψ \leftrightarrow χ)$
2		tfindsd.2	$⊢ x = y \to (ψ \leftrightarrow θ)$
3		tfindsd.3	$⊢ x = suc y \to (ψ \leftrightarrow τ)$
4		tfindsd.4	$⊢ x = A \to (ψ \leftrightarrow η)$
5		tfindsd.5	$⊢ φ \to χ$
6		tfindsd.6	$⊢ (φ \land y \in On \land θ) \to τ$
7		tfindsd.7	$⊢ (φ \land Lim x \land \forall y \in x θ) \to ψ$
8		tfindsd.8	$⊢ φ \to A \in On$
9	6	3exp	$⊢ φ \to (y \in On \to (θ \to τ))$
10	9	com12	$⊢ y \in On \to (φ \to (θ \to τ))$
11	7	3exp	$⊢ φ \to (Lim x \to (\forall y \in x θ \to ψ))$
12	11	com12	$⊢ Lim x \to (φ \to (\forall y \in x θ \to ψ))$
13	1 2 3 4 5 10 12	tfinds3	$⊢ A \in On \to (φ \to η)$
14	8 13	mpcom	$⊢ φ \to η$

Metamath Proof Explorer