Theorem tfindsd

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

	Ref	Expression
Hypotheses	tfindsd.1	⊢ ( 𝑥 = ∅ → ( 𝜓 ↔ 𝜒 ) )
	tfindsd.2	⊢ ( 𝑥 = 𝑦 → ( 𝜓 ↔ 𝜃 ) )
	tfindsd.3	⊢ ( 𝑥 = suc 𝑦 → ( 𝜓 ↔ 𝜏 ) )
	tfindsd.4	⊢ ( 𝑥 = 𝐴 → ( 𝜓 ↔ 𝜂 ) )
	tfindsd.5	⊢ ( 𝜑 → 𝜒 )
	tfindsd.6	⊢ ( ( 𝜑 ∧ 𝑦 ∈ On ∧ 𝜃 ) → 𝜏 )
	tfindsd.7	⊢ ( ( 𝜑 ∧ Lim 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 𝜃 ) → 𝜓 )
	tfindsd.8	⊢ ( 𝜑 → 𝐴 ∈ On )
Assertion	tfindsd	⊢ ( 𝜑 → 𝜂 )

Proof

Step	Hyp	Ref	Expression
1		tfindsd.1	⊢ ( 𝑥 = ∅ → ( 𝜓 ↔ 𝜒 ) )
2		tfindsd.2	⊢ ( 𝑥 = 𝑦 → ( 𝜓 ↔ 𝜃 ) )
3		tfindsd.3	⊢ ( 𝑥 = suc 𝑦 → ( 𝜓 ↔ 𝜏 ) )
4		tfindsd.4	⊢ ( 𝑥 = 𝐴 → ( 𝜓 ↔ 𝜂 ) )
5		tfindsd.5	⊢ ( 𝜑 → 𝜒 )
6		tfindsd.6	⊢ ( ( 𝜑 ∧ 𝑦 ∈ On ∧ 𝜃 ) → 𝜏 )
7		tfindsd.7	⊢ ( ( 𝜑 ∧ Lim 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 𝜃 ) → 𝜓 )
8		tfindsd.8	⊢ ( 𝜑 → 𝐴 ∈ On )
9	6	3exp	⊢ ( 𝜑 → ( 𝑦 ∈ On → ( 𝜃 → 𝜏 ) ) )
10	9	com12	⊢ ( 𝑦 ∈ On → ( 𝜑 → ( 𝜃 → 𝜏 ) ) )
11	7	3exp	⊢ ( 𝜑 → ( Lim 𝑥 → ( ∀ 𝑦 ∈ 𝑥 𝜃 → 𝜓 ) ) )
12	11	com12	⊢ ( Lim 𝑥 → ( 𝜑 → ( ∀ 𝑦 ∈ 𝑥 𝜃 → 𝜓 ) ) )
13	1 2 3 4 5 10 12	tfinds3	⊢ ( 𝐴 ∈ On → ( 𝜑 → 𝜂 ) )
14	8 13	mpcom	⊢ ( 𝜑 → 𝜂 )