This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 biimtrrid ⊢ ( Lim 𝑦 → ( ∀ 𝑧 ∈ 𝑦 [ 𝑧 / 𝑥 ] 𝜑 → [ 𝑦 / 𝑥 ] 𝜑 ) )
25 4 5 6 7 1 19 24 tfinds ⊢ ( 𝑥 ∈ On → 𝜑 )