Metamath Proof Explorer

Theorem tfinds2

Description: Transfinite Induction (inference schema), using implicit substitutions. The first three hypotheses establish the substitutions we need. The last three are the basis and the induction hypotheses (for successor and limit ordinals respectively). Theorem Schema 4 of Suppes p. 197. The wff ta is an auxiliary antecedent to help shorten proofs using this theorem. (Contributed by NM, 4-Sep-2004)

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

Proof

Step Hyp Ref Expression
1 tfinds2.1 ⊢ ( 𝑥 = ∅ → ( 𝜑 ↔ 𝜓 ) )
2 tfinds2.2 ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜒 ) )
3 tfinds2.3 ⊢ ( 𝑥 = suc 𝑦 → ( 𝜑 ↔ 𝜃 ) )
4 tfinds2.4 ⊢ ( 𝜏 → 𝜓 )
5 tfinds2.5 ⊢ ( 𝑦 ∈ On → ( 𝜏 → ( 𝜒 → 𝜃 ) ) )
6 tfinds2.6 ⊢ ( Lim 𝑥 → ( 𝜏 → ( ∀ 𝑦 ∈ 𝑥 𝜒 → 𝜑 ) ) )
7 0ex ⊢ ∅ ∈ V
8 1 imbi2d ⊢ ( 𝑥 = ∅ → ( ( 𝜏 → 𝜑 ) ↔ ( 𝜏 → 𝜓 ) ) )
9 7 8 sbcie ⊢ ( [ ∅ / 𝑥 ] ( 𝜏 → 𝜑 ) ↔ ( 𝜏 → 𝜓 ) )
10 4 9 mpbir ⊢ [ ∅ / 𝑥 ] ( 𝜏 → 𝜑 )
11 5 a2d ⊢ ( 𝑦 ∈ On → ( ( 𝜏 → 𝜒 ) → ( 𝜏 → 𝜃 ) ) )
12 11 sbcth ⊢ ( 𝑥 ∈ V → [ 𝑥 / 𝑦 ] ( 𝑦 ∈ On → ( ( 𝜏 → 𝜒 ) → ( 𝜏 → 𝜃 ) ) ) )
13 12 elv ⊢ [ 𝑥 / 𝑦 ] ( 𝑦 ∈ On → ( ( 𝜏 → 𝜒 ) → ( 𝜏 → 𝜃 ) ) )
14 sbcimg ⊢ ( 𝑥 ∈ V → ( [ 𝑥 / 𝑦 ] ( 𝑦 ∈ On → ( ( 𝜏 → 𝜒 ) → ( 𝜏 → 𝜃 ) ) ) ↔ ( [ 𝑥 / 𝑦 ] 𝑦 ∈ On → [ 𝑥 / 𝑦 ] ( ( 𝜏 → 𝜒 ) → ( 𝜏 → 𝜃 ) ) ) ) )
15 14 elv ⊢ ( [ 𝑥 / 𝑦 ] ( 𝑦 ∈ On → ( ( 𝜏 → 𝜒 ) → ( 𝜏 → 𝜃 ) ) ) ↔ ( [ 𝑥 / 𝑦 ] 𝑦 ∈ On → [ 𝑥 / 𝑦 ] ( ( 𝜏 → 𝜒 ) → ( 𝜏 → 𝜃 ) ) ) )
16 13 15 mpbi ⊢ ( [ 𝑥 / 𝑦 ] 𝑦 ∈ On → [ 𝑥 / 𝑦 ] ( ( 𝜏 → 𝜒 ) → ( 𝜏 → 𝜃 ) ) )
17 sbcel1v ⊢ ( [ 𝑥 / 𝑦 ] 𝑦 ∈ On ↔ 𝑥 ∈ On )
18 sbcimg ⊢ ( 𝑥 ∈ V → ( [ 𝑥 / 𝑦 ] ( ( 𝜏 → 𝜒 ) → ( 𝜏 → 𝜃 ) ) ↔ ( [ 𝑥 / 𝑦 ] ( 𝜏 → 𝜒 ) → [ 𝑥 / 𝑦 ] ( 𝜏 → 𝜃 ) ) ) )
19 18 elv ⊢ ( [ 𝑥 / 𝑦 ] ( ( 𝜏 → 𝜒 ) → ( 𝜏 → 𝜃 ) ) ↔ ( [ 𝑥 / 𝑦 ] ( 𝜏 → 𝜒 ) → [ 𝑥 / 𝑦 ] ( 𝜏 → 𝜃 ) ) )
20 16 17 19 3imtr3i ⊢ ( 𝑥 ∈ On → ( [ 𝑥 / 𝑦 ] ( 𝜏 → 𝜒 ) → [ 𝑥 / 𝑦 ] ( 𝜏 → 𝜃 ) ) )
21 vex ⊢ 𝑥 ∈ V
22 2 bicomd ⊢ ( 𝑥 = 𝑦 → ( 𝜒 ↔ 𝜑 ) )
23 22 equcoms ⊢ ( 𝑦 = 𝑥 → ( 𝜒 ↔ 𝜑 ) )
24 23 imbi2d ⊢ ( 𝑦 = 𝑥 → ( ( 𝜏 → 𝜒 ) ↔ ( 𝜏 → 𝜑 ) ) )
25 21 24 sbcie ⊢ ( [ 𝑥 / 𝑦 ] ( 𝜏 → 𝜒 ) ↔ ( 𝜏 → 𝜑 ) )
26 vex ⊢ 𝑦 ∈ V
27 26 sucex ⊢ suc 𝑦 ∈ V
28 3 imbi2d ⊢ ( 𝑥 = suc 𝑦 → ( ( 𝜏 → 𝜑 ) ↔ ( 𝜏 → 𝜃 ) ) )
29 27 28 sbcie ⊢ ( [ suc 𝑦 / 𝑥 ] ( 𝜏 → 𝜑 ) ↔ ( 𝜏 → 𝜃 ) )
30 29 sbcbii ⊢ ( [ 𝑥 / 𝑦 ] [ suc 𝑦 / 𝑥 ] ( 𝜏 → 𝜑 ) ↔ [ 𝑥 / 𝑦 ] ( 𝜏 → 𝜃 ) )
31 suceq ⊢ ( 𝑥 = 𝑦 → suc 𝑥 = suc 𝑦 )
32 31 sbcco2 ⊢ ( [ 𝑥 / 𝑦 ] [ suc 𝑦 / 𝑥 ] ( 𝜏 → 𝜑 ) ↔ [ suc 𝑥 / 𝑥 ] ( 𝜏 → 𝜑 ) )
33 30 32 bitr3i ⊢ ( [ 𝑥 / 𝑦 ] ( 𝜏 → 𝜃 ) ↔ [ suc 𝑥 / 𝑥 ] ( 𝜏 → 𝜑 ) )
34 20 25 33 3imtr3g ⊢ ( 𝑥 ∈ On → ( ( 𝜏 → 𝜑 ) → [ suc 𝑥 / 𝑥 ] ( 𝜏 → 𝜑 ) ) )
35 2 imbi2d ⊢ ( 𝑥 = 𝑦 → ( ( 𝜏 → 𝜑 ) ↔ ( 𝜏 → 𝜒 ) ) )
36 35 sbralie ⊢ ( ∀ 𝑥 ∈ 𝑦 ( 𝜏 → 𝜑 ) ↔ [ 𝑦 / 𝑥 ] ∀ 𝑦 ∈ 𝑥 ( 𝜏 → 𝜒 ) )
37 sbsbc ⊢ ( [ 𝑦 / 𝑥 ] ∀ 𝑦 ∈ 𝑥 ( 𝜏 → 𝜒 ) ↔ [ 𝑦 / 𝑥 ] ∀ 𝑦 ∈ 𝑥 ( 𝜏 → 𝜒 ) )
38 36 37 bitr2i ⊢ ( [ 𝑦 / 𝑥 ] ∀ 𝑦 ∈ 𝑥 ( 𝜏 → 𝜒 ) ↔ ∀ 𝑥 ∈ 𝑦 ( 𝜏 → 𝜑 ) )
39 r19.21v ⊢ ( ∀ 𝑦 ∈ 𝑥 ( 𝜏 → 𝜒 ) ↔ ( 𝜏 → ∀ 𝑦 ∈ 𝑥 𝜒 ) )
40 6 a2d ⊢ ( Lim 𝑥 → ( ( 𝜏 → ∀ 𝑦 ∈ 𝑥 𝜒 ) → ( 𝜏 → 𝜑 ) ) )
41 39 40 syl5bi ⊢ ( Lim 𝑥 → ( ∀ 𝑦 ∈ 𝑥 ( 𝜏 → 𝜒 ) → ( 𝜏 → 𝜑 ) ) )
42 41 sbcth ⊢ ( 𝑦 ∈ V → [ 𝑦 / 𝑥 ] ( Lim 𝑥 → ( ∀ 𝑦 ∈ 𝑥 ( 𝜏 → 𝜒 ) → ( 𝜏 → 𝜑 ) ) ) )
43 42 elv ⊢ [ 𝑦 / 𝑥 ] ( Lim 𝑥 → ( ∀ 𝑦 ∈ 𝑥 ( 𝜏 → 𝜒 ) → ( 𝜏 → 𝜑 ) ) )
44 sbcimg ⊢ ( 𝑦 ∈ V → ( [ 𝑦 / 𝑥 ] ( Lim 𝑥 → ( ∀ 𝑦 ∈ 𝑥 ( 𝜏 → 𝜒 ) → ( 𝜏 → 𝜑 ) ) ) ↔ ( [ 𝑦 / 𝑥 ] Lim 𝑥 → [ 𝑦 / 𝑥 ] ( ∀ 𝑦 ∈ 𝑥 ( 𝜏 → 𝜒 ) → ( 𝜏 → 𝜑 ) ) ) ) )
45 44 elv ⊢ ( [ 𝑦 / 𝑥 ] ( Lim 𝑥 → ( ∀ 𝑦 ∈ 𝑥 ( 𝜏 → 𝜒 ) → ( 𝜏 → 𝜑 ) ) ) ↔ ( [ 𝑦 / 𝑥 ] Lim 𝑥 → [ 𝑦 / 𝑥 ] ( ∀ 𝑦 ∈ 𝑥 ( 𝜏 → 𝜒 ) → ( 𝜏 → 𝜑 ) ) ) )
46 43 45 mpbi ⊢ ( [ 𝑦 / 𝑥 ] Lim 𝑥 → [ 𝑦 / 𝑥 ] ( ∀ 𝑦 ∈ 𝑥 ( 𝜏 → 𝜒 ) → ( 𝜏 → 𝜑 ) ) )
47 limeq ⊢ ( 𝑥 = 𝑦 → ( Lim 𝑥 ↔ Lim 𝑦 ) )
48 26 47 sbcie ⊢ ( [ 𝑦 / 𝑥 ] Lim 𝑥 ↔ Lim 𝑦 )
49 sbcimg ⊢ ( 𝑦 ∈ V → ( [ 𝑦 / 𝑥 ] ( ∀ 𝑦 ∈ 𝑥 ( 𝜏 → 𝜒 ) → ( 𝜏 → 𝜑 ) ) ↔ ( [ 𝑦 / 𝑥 ] ∀ 𝑦 ∈ 𝑥 ( 𝜏 → 𝜒 ) → [ 𝑦 / 𝑥 ] ( 𝜏 → 𝜑 ) ) ) )
50 49 elv ⊢ ( [ 𝑦 / 𝑥 ] ( ∀ 𝑦 ∈ 𝑥 ( 𝜏 → 𝜒 ) → ( 𝜏 → 𝜑 ) ) ↔ ( [ 𝑦 / 𝑥 ] ∀ 𝑦 ∈ 𝑥 ( 𝜏 → 𝜒 ) → [ 𝑦 / 𝑥 ] ( 𝜏 → 𝜑 ) ) )
51 46 48 50 3imtr3i ⊢ ( Lim 𝑦 → ( [ 𝑦 / 𝑥 ] ∀ 𝑦 ∈ 𝑥 ( 𝜏 → 𝜒 ) → [ 𝑦 / 𝑥 ] ( 𝜏 → 𝜑 ) ) )
52 38 51 syl5bir ⊢ ( Lim 𝑦 → ( ∀ 𝑥 ∈ 𝑦 ( 𝜏 → 𝜑 ) → [ 𝑦 / 𝑥 ] ( 𝜏 → 𝜑 ) ) )
53 10 34 52 tfindes ⊢ ( 𝑥 ∈ On → ( 𝜏 → 𝜑 ) )