Theorem tfindes

Description: Transfinite Induction with explicit substitution. The first hypothesis is the basis, the second is the induction step for successors, and the third is the induction step for limit ordinals. Theorem Schema 4 of Suppes p. 197. (Contributed by NM, 5-Mar-2004)

	Ref	Expression
Hypotheses	tfindes.1	⊢ [ ∅ / 𝑥 ] 𝜑
	tfindes.2	⊢ ( 𝑥 ∈ On → ( 𝜑 → [ suc 𝑥 / 𝑥 ] 𝜑 ) )
	tfindes.3	⊢ ( Lim 𝑦 → ( ∀ 𝑥 ∈ 𝑦 𝜑 → [ 𝑦 / 𝑥 ] 𝜑 ) )
Assertion	tfindes	⊢ ( 𝑥 ∈ On → 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		tfindes.1	⊢ [ ∅ / 𝑥 ] 𝜑
2		tfindes.2	⊢ ( 𝑥 ∈ On → ( 𝜑 → [ suc 𝑥 / 𝑥 ] 𝜑 ) )
3		tfindes.3	⊢ ( Lim 𝑦 → ( ∀ 𝑥 ∈ 𝑦 𝜑 → [ 𝑦 / 𝑥 ] 𝜑 ) )
4		dfsbcq	⊢ ( 𝑦 = ∅ → ( [ 𝑦 / 𝑥 ] 𝜑 ↔ [ ∅ / 𝑥 ] 𝜑 ) )
5		dfsbcq	⊢ ( 𝑦 = 𝑧 → ( [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝑧 / 𝑥 ] 𝜑 ) )
6		dfsbcq	⊢ ( 𝑦 = suc 𝑧 → ( [ 𝑦 / 𝑥 ] 𝜑 ↔ [ suc 𝑧 / 𝑥 ] 𝜑 ) )
7		sbceq2a	⊢ ( 𝑦 = 𝑥 → ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜑 ) )
8		nfv	⊢ Ⅎ 𝑥 𝑧 ∈ On
9		nfsbc1v	⊢ Ⅎ 𝑥 [ 𝑧 / 𝑥 ] 𝜑
10		nfsbc1v	⊢ Ⅎ 𝑥 [ suc 𝑧 / 𝑥 ] 𝜑
11	9 10	nfim	⊢ Ⅎ 𝑥 ( [ 𝑧 / 𝑥 ] 𝜑 → [ suc 𝑧 / 𝑥 ] 𝜑 )
12	8 11	nfim	⊢ Ⅎ 𝑥 ( 𝑧 ∈ On → ( [ 𝑧 / 𝑥 ] 𝜑 → [ suc 𝑧 / 𝑥 ] 𝜑 ) )
13		eleq1w	⊢ ( 𝑥 = 𝑧 → ( 𝑥 ∈ On ↔ 𝑧 ∈ On ) )
14		sbceq1a	⊢ ( 𝑥 = 𝑧 → ( 𝜑 ↔ [ 𝑧 / 𝑥 ] 𝜑 ) )
15		suceq	⊢ ( 𝑥 = 𝑧 → suc 𝑥 = suc 𝑧 )
16	15	sbceq1d	⊢ ( 𝑥 = 𝑧 → ( [ suc 𝑥 / 𝑥 ] 𝜑 ↔ [ suc 𝑧 / 𝑥 ] 𝜑 ) )
17	14 16	imbi12d	⊢ ( 𝑥 = 𝑧 → ( ( 𝜑 → [ suc 𝑥 / 𝑥 ] 𝜑 ) ↔ ( [ 𝑧 / 𝑥 ] 𝜑 → [ suc 𝑧 / 𝑥 ] 𝜑 ) ) )
18	13 17	imbi12d	⊢ ( 𝑥 = 𝑧 → ( ( 𝑥 ∈ On → ( 𝜑 → [ suc 𝑥 / 𝑥 ] 𝜑 ) ) ↔ ( 𝑧 ∈ On → ( [ 𝑧 / 𝑥 ] 𝜑 → [ suc 𝑧 / 𝑥 ] 𝜑 ) ) ) )
19	12 18 2	chvarfv	⊢ ( 𝑧 ∈ On → ( [ 𝑧 / 𝑥 ] 𝜑 → [ suc 𝑧 / 𝑥 ] 𝜑 ) )
20		cbvralsvw	⊢ ( ∀ 𝑥 ∈ 𝑦 𝜑 ↔ ∀ 𝑧 ∈ 𝑦 [ 𝑧 / 𝑥 ] 𝜑 )
21		sbsbc	⊢ ( [ 𝑧 / 𝑥 ] 𝜑 ↔ [ 𝑧 / 𝑥 ] 𝜑 )
22	21	ralbii	⊢ ( ∀ 𝑧 ∈ 𝑦 [ 𝑧 / 𝑥 ] 𝜑 ↔ ∀ 𝑧 ∈ 𝑦 [ 𝑧 / 𝑥 ] 𝜑 )
23	20 22	bitri	⊢ ( ∀ 𝑥 ∈ 𝑦 𝜑 ↔ ∀ 𝑧 ∈ 𝑦 [ 𝑧 / 𝑥 ] 𝜑 )
24	23 3	syl5bir	⊢ ( Lim 𝑦 → ( ∀ 𝑧 ∈ 𝑦 [ 𝑧 / 𝑥 ] 𝜑 → [ 𝑦 / 𝑥 ] 𝜑 ) )
25	4 5 6 7 1 19 24	tfinds	⊢ ( 𝑥 ∈ On → 𝜑 )