Metamath Proof Explorer

Theorem tfinds

Description: Principle of Transfinite Induction (inference schema), using implicit substitutions. The first four hypotheses establish the substitutions we need. The last three are the basis, the induction step for successors, and the induction step for limit ordinals. Theorem Schema 4 of Suppes p. 197. (Contributed by NM, 16-Apr-1995) (Proof shortened by Andrew Salmon, 27-Aug-2011)

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

Proof

Step Hyp Ref Expression
1 tfinds.1 ⊢ ( 𝑥 = ∅ → ( 𝜑 ↔ 𝜓 ) )
2 tfinds.2 ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜒 ) )
3 tfinds.3 ⊢ ( 𝑥 = suc 𝑦 → ( 𝜑 ↔ 𝜃 ) )
4 tfinds.4 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜏 ) )
5 tfinds.5 ⊢ 𝜓
6 tfinds.6 ⊢ ( 𝑦 ∈ On → ( 𝜒 → 𝜃 ) )
7 tfinds.7 ⊢ ( Lim 𝑥 → ( ∀ 𝑦 ∈ 𝑥 𝜒 → 𝜑 ) )
8 dflim3 ⊢ ( Lim 𝑥 ↔ ( Ord 𝑥 ∧ ¬ ( 𝑥 = ∅ ∨ ∃ 𝑦 ∈ On 𝑥 = suc 𝑦 ) ) )
9 8 notbii ⊢ ( ¬ Lim 𝑥 ↔ ¬ ( Ord 𝑥 ∧ ¬ ( 𝑥 = ∅ ∨ ∃ 𝑦 ∈ On 𝑥 = suc 𝑦 ) ) )
10 iman ⊢ ( ( Ord 𝑥 → ( 𝑥 = ∅ ∨ ∃ 𝑦 ∈ On 𝑥 = suc 𝑦 ) ) ↔ ¬ ( Ord 𝑥 ∧ ¬ ( 𝑥 = ∅ ∨ ∃ 𝑦 ∈ On 𝑥 = suc 𝑦 ) ) )
11 eloni ⊢ ( 𝑥 ∈ On → Ord 𝑥 )
12 pm2.27 ⊢ ( Ord 𝑥 → ( ( Ord 𝑥 → ( 𝑥 = ∅ ∨ ∃ 𝑦 ∈ On 𝑥 = suc 𝑦 ) ) → ( 𝑥 = ∅ ∨ ∃ 𝑦 ∈ On 𝑥 = suc 𝑦 ) ) )
13 11 12 syl ⊢ ( 𝑥 ∈ On → ( ( Ord 𝑥 → ( 𝑥 = ∅ ∨ ∃ 𝑦 ∈ On 𝑥 = suc 𝑦 ) ) → ( 𝑥 = ∅ ∨ ∃ 𝑦 ∈ On 𝑥 = suc 𝑦 ) ) )
14 5 1 mpbiri ⊢ ( 𝑥 = ∅ → 𝜑 )
15 14 a1d ⊢ ( 𝑥 = ∅ → ( ∀ 𝑦 ∈ 𝑥 𝜒 → 𝜑 ) )
16 nfra1 ⊢ Ⅎ 𝑦 ∀ 𝑦 ∈ 𝑥 𝜒
17 nfv ⊢ Ⅎ 𝑦 𝜑
18 16 17 nfim ⊢ Ⅎ 𝑦 ( ∀ 𝑦 ∈ 𝑥 𝜒 → 𝜑 )
19 vex ⊢ 𝑦 ∈ V
20 19 sucid ⊢ 𝑦 ∈ suc 𝑦
21 2 rspcv ⊢ ( 𝑦 ∈ suc 𝑦 → ( ∀ 𝑥 ∈ suc 𝑦 𝜑 → 𝜒 ) )
22 20 21 ax-mp ⊢ ( ∀ 𝑥 ∈ suc 𝑦 𝜑 → 𝜒 )
23 22 6 syl5 ⊢ ( 𝑦 ∈ On → ( ∀ 𝑥 ∈ suc 𝑦 𝜑 → 𝜃 ) )
24 raleq ⊢ ( 𝑥 = suc 𝑦 → ( ∀ 𝑧 ∈ 𝑥 [ 𝑧 / 𝑥 ] 𝜑 ↔ ∀ 𝑧 ∈ suc 𝑦 [ 𝑧 / 𝑥 ] 𝜑 ) )
25 nfv ⊢ Ⅎ 𝑥 𝜒
26 25 2 sbiev ⊢ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜒 )
27 sbequ ⊢ ( 𝑦 = 𝑧 → ( [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝑧 / 𝑥 ] 𝜑 ) )
28 26 27 bitr3id ⊢ ( 𝑦 = 𝑧 → ( 𝜒 ↔ [ 𝑧 / 𝑥 ] 𝜑 ) )
29 28 cbvralvw ⊢ ( ∀ 𝑦 ∈ 𝑥 𝜒 ↔ ∀ 𝑧 ∈ 𝑥 [ 𝑧 / 𝑥 ] 𝜑 )
30 cbvralsvw ⊢ ( ∀ 𝑥 ∈ suc 𝑦 𝜑 ↔ ∀ 𝑧 ∈ suc 𝑦 [ 𝑧 / 𝑥 ] 𝜑 )
31 24 29 30 3bitr4g ⊢ ( 𝑥 = suc 𝑦 → ( ∀ 𝑦 ∈ 𝑥 𝜒 ↔ ∀ 𝑥 ∈ suc 𝑦 𝜑 ) )
32 31 imbi1d ⊢ ( 𝑥 = suc 𝑦 → ( ( ∀ 𝑦 ∈ 𝑥 𝜒 → 𝜃 ) ↔ ( ∀ 𝑥 ∈ suc 𝑦 𝜑 → 𝜃 ) ) )
33 23 32 syl5ibrcom ⊢ ( 𝑦 ∈ On → ( 𝑥 = suc 𝑦 → ( ∀ 𝑦 ∈ 𝑥 𝜒 → 𝜃 ) ) )
34 3 biimprd ⊢ ( 𝑥 = suc 𝑦 → ( 𝜃 → 𝜑 ) )
35 34 a1i ⊢ ( 𝑦 ∈ On → ( 𝑥 = suc 𝑦 → ( 𝜃 → 𝜑 ) ) )
36 33 35 syldd ⊢ ( 𝑦 ∈ On → ( 𝑥 = suc 𝑦 → ( ∀ 𝑦 ∈ 𝑥 𝜒 → 𝜑 ) ) )
37 18 36 rexlimi ⊢ ( ∃ 𝑦 ∈ On 𝑥 = suc 𝑦 → ( ∀ 𝑦 ∈ 𝑥 𝜒 → 𝜑 ) )
38 15 37 jaoi ⊢ ( ( 𝑥 = ∅ ∨ ∃ 𝑦 ∈ On 𝑥 = suc 𝑦 ) → ( ∀ 𝑦 ∈ 𝑥 𝜒 → 𝜑 ) )
39 13 38 syl6 ⊢ ( 𝑥 ∈ On → ( ( Ord 𝑥 → ( 𝑥 = ∅ ∨ ∃ 𝑦 ∈ On 𝑥 = suc 𝑦 ) ) → ( ∀ 𝑦 ∈ 𝑥 𝜒 → 𝜑 ) ) )
40 10 39 syl5bir ⊢ ( 𝑥 ∈ On → ( ¬ ( Ord 𝑥 ∧ ¬ ( 𝑥 = ∅ ∨ ∃ 𝑦 ∈ On 𝑥 = suc 𝑦 ) ) → ( ∀ 𝑦 ∈ 𝑥 𝜒 → 𝜑 ) ) )
41 9 40 syl5bi ⊢ ( 𝑥 ∈ On → ( ¬ Lim 𝑥 → ( ∀ 𝑦 ∈ 𝑥 𝜒 → 𝜑 ) ) )
42 41 7 pm2.61d2 ⊢ ( 𝑥 ∈ On → ( ∀ 𝑦 ∈ 𝑥 𝜒 → 𝜑 ) )
43 2 4 42 tfis3 ⊢ ( 𝐴 ∈ On → 𝜏 )