Theorem finds

Description: Principle of Finite Induction (inference schema), using implicit substitutions. The first four hypotheses establish the substitutions we need. The last two are the basis and the induction step. Theorem Schema 22 of Suppes p. 136. This is Metamath 100 proof #74. (Contributed by NM, 14-Apr-1995)

	Ref	Expression
Hypotheses	finds.1	⊢ ( 𝑥 = ∅ → ( 𝜑 ↔ 𝜓 ) )
	finds.2	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜒 ) )
	finds.3	⊢ ( 𝑥 = suc 𝑦 → ( 𝜑 ↔ 𝜃 ) )
	finds.4	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜏 ) )
	finds.5	⊢ 𝜓
	finds.6	⊢ ( 𝑦 ∈ ω → ( 𝜒 → 𝜃 ) )
Assertion	finds	⊢ ( 𝐴 ∈ ω → 𝜏 )

Proof

Step	Hyp	Ref	Expression
1		finds.1	⊢ ( 𝑥 = ∅ → ( 𝜑 ↔ 𝜓 ) )
2		finds.2	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜒 ) )
3		finds.3	⊢ ( 𝑥 = suc 𝑦 → ( 𝜑 ↔ 𝜃 ) )
4		finds.4	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜏 ) )
5		finds.5	⊢ 𝜓
6		finds.6	⊢ ( 𝑦 ∈ ω → ( 𝜒 → 𝜃 ) )
7		0ex	⊢ ∅ ∈ V
8	7 1	elab	⊢ ( ∅ ∈ { 𝑥 ∣ 𝜑 } ↔ 𝜓 )
9	5 8	mpbir	⊢ ∅ ∈ { 𝑥 ∣ 𝜑 }
10		vex	⊢ 𝑦 ∈ V
11	10 2	elab	⊢ ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝜒 )
12	10	sucex	⊢ suc 𝑦 ∈ V
13	12 3	elab	⊢ ( suc 𝑦 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝜃 )
14	6 11 13	3imtr4g	⊢ ( 𝑦 ∈ ω → ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } → suc 𝑦 ∈ { 𝑥 ∣ 𝜑 } ) )
15	14	rgen	⊢ ∀ 𝑦 ∈ ω ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } → suc 𝑦 ∈ { 𝑥 ∣ 𝜑 } )
16		peano5	⊢ ( ( ∅ ∈ { 𝑥 ∣ 𝜑 } ∧ ∀ 𝑦 ∈ ω ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } → suc 𝑦 ∈ { 𝑥 ∣ 𝜑 } ) ) → ω ⊆ { 𝑥 ∣ 𝜑 } )
17	9 15 16	mp2an	⊢ ω ⊆ { 𝑥 ∣ 𝜑 }
18	17	sseli	⊢ ( 𝐴 ∈ ω → 𝐴 ∈ { 𝑥 ∣ 𝜑 } )
19	4	elabg	⊢ ( 𝐴 ∈ ω → ( 𝐴 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝜏 ) )
20	18 19	mpbid	⊢ ( 𝐴 ∈ ω → 𝜏 )