Metamath Proof Explorer

Theorem tfindsg2

Description: 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. The basis of this version is an arbitrary ordinal suc B instead of zero. (Contributed by NM, 5-Jan-2005) Remove unnecessary distinct variable conditions. (Revised by David Abernethy, 19-Jun-2012)

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

Proof

Step Hyp Ref Expression
1 tfindsg2.1 ⊢ ( 𝑥 = suc 𝐵 → ( 𝜑 ↔ 𝜓 ) )
2 tfindsg2.2 ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜒 ) )
3 tfindsg2.3 ⊢ ( 𝑥 = suc 𝑦 → ( 𝜑 ↔ 𝜃 ) )
4 tfindsg2.4 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜏 ) )
5 tfindsg2.5 ⊢ ( 𝐵 ∈ On → 𝜓 )
6 tfindsg2.6 ⊢ ( ( 𝑦 ∈ On ∧ 𝐵 ∈ 𝑦 ) → ( 𝜒 → 𝜃 ) )
7 tfindsg2.7 ⊢ ( ( Lim 𝑥 ∧ 𝐵 ∈ 𝑥 ) → ( ∀ 𝑦 ∈ 𝑥 ( 𝐵 ∈ 𝑦 → 𝜒 ) → 𝜑 ) )
8 onelon ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ 𝐴 ) → 𝐵 ∈ On )
9 onsucb ⊢ ( 𝐵 ∈ On ↔ suc 𝐵 ∈ On )
10 8 9 sylib ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ 𝐴 ) → suc 𝐵 ∈ On )
11 eloni ⊢ ( 𝐴 ∈ On → Ord 𝐴 )
12 ordsucss ⊢ ( Ord 𝐴 → ( 𝐵 ∈ 𝐴 → suc 𝐵 ⊆ 𝐴 ) )
13 11 12 syl ⊢ ( 𝐴 ∈ On → ( 𝐵 ∈ 𝐴 → suc 𝐵 ⊆ 𝐴 ) )
14 13 imp ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ 𝐴 ) → suc 𝐵 ⊆ 𝐴 )
15 9 5 sylbir ⊢ ( suc 𝐵 ∈ On → 𝜓 )
16 eloni ⊢ ( 𝑦 ∈ On → Ord 𝑦 )
17 ordelsuc ⊢ ( ( 𝐵 ∈ On ∧ Ord 𝑦 ) → ( 𝐵 ∈ 𝑦 ↔ suc 𝐵 ⊆ 𝑦 ) )
18 16 17 sylan2 ⊢ ( ( 𝐵 ∈ On ∧ 𝑦 ∈ On ) → ( 𝐵 ∈ 𝑦 ↔ suc 𝐵 ⊆ 𝑦 ) )
19 18 ancoms ⊢ ( ( 𝑦 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐵 ∈ 𝑦 ↔ suc 𝐵 ⊆ 𝑦 ) )
20 6 ex ⊢ ( 𝑦 ∈ On → ( 𝐵 ∈ 𝑦 → ( 𝜒 → 𝜃 ) ) )
21 20 adantr ⊢ ( ( 𝑦 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐵 ∈ 𝑦 → ( 𝜒 → 𝜃 ) ) )
22 19 21 sylbird ⊢ ( ( 𝑦 ∈ On ∧ 𝐵 ∈ On ) → ( suc 𝐵 ⊆ 𝑦 → ( 𝜒 → 𝜃 ) ) )
23 9 22 sylan2br ⊢ ( ( 𝑦 ∈ On ∧ suc 𝐵 ∈ On ) → ( suc 𝐵 ⊆ 𝑦 → ( 𝜒 → 𝜃 ) ) )
24 23 imp ⊢ ( ( ( 𝑦 ∈ On ∧ suc 𝐵 ∈ On ) ∧ suc 𝐵 ⊆ 𝑦 ) → ( 𝜒 → 𝜃 ) )
25 7 ex ⊢ ( Lim 𝑥 → ( 𝐵 ∈ 𝑥 → ( ∀ 𝑦 ∈ 𝑥 ( 𝐵 ∈ 𝑦 → 𝜒 ) → 𝜑 ) ) )
26 25 adantr ⊢ ( ( Lim 𝑥 ∧ 𝐵 ∈ On ) → ( 𝐵 ∈ 𝑥 → ( ∀ 𝑦 ∈ 𝑥 ( 𝐵 ∈ 𝑦 → 𝜒 ) → 𝜑 ) ) )
27 vex ⊢ 𝑥 ∈ V
28 limelon ⊢ ( ( 𝑥 ∈ V ∧ Lim 𝑥 ) → 𝑥 ∈ On )
29 27 28 mpan ⊢ ( Lim 𝑥 → 𝑥 ∈ On )
30 eloni ⊢ ( 𝑥 ∈ On → Ord 𝑥 )
31 ordelsuc ⊢ ( ( 𝐵 ∈ On ∧ Ord 𝑥 ) → ( 𝐵 ∈ 𝑥 ↔ suc 𝐵 ⊆ 𝑥 ) )
32 30 31 sylan2 ⊢ ( ( 𝐵 ∈ On ∧ 𝑥 ∈ On ) → ( 𝐵 ∈ 𝑥 ↔ suc 𝐵 ⊆ 𝑥 ) )
33 onelon ⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ On )
34 33 16 syl ⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝑥 ) → Ord 𝑦 )
35 34 17 sylan2 ⊢ ( ( 𝐵 ∈ On ∧ ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝑥 ) ) → ( 𝐵 ∈ 𝑦 ↔ suc 𝐵 ⊆ 𝑦 ) )
36 35 anassrs ⊢ ( ( ( 𝐵 ∈ On ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝐵 ∈ 𝑦 ↔ suc 𝐵 ⊆ 𝑦 ) )
37 36 imbi1d ⊢ ( ( ( 𝐵 ∈ On ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ 𝑥 ) → ( ( 𝐵 ∈ 𝑦 → 𝜒 ) ↔ ( suc 𝐵 ⊆ 𝑦 → 𝜒 ) ) )
38 37 ralbidva ⊢ ( ( 𝐵 ∈ On ∧ 𝑥 ∈ On ) → ( ∀ 𝑦 ∈ 𝑥 ( 𝐵 ∈ 𝑦 → 𝜒 ) ↔ ∀ 𝑦 ∈ 𝑥 ( suc 𝐵 ⊆ 𝑦 → 𝜒 ) ) )
39 38 imbi1d ⊢ ( ( 𝐵 ∈ On ∧ 𝑥 ∈ On ) → ( ( ∀ 𝑦 ∈ 𝑥 ( 𝐵 ∈ 𝑦 → 𝜒 ) → 𝜑 ) ↔ ( ∀ 𝑦 ∈ 𝑥 ( suc 𝐵 ⊆ 𝑦 → 𝜒 ) → 𝜑 ) ) )
40 32 39 imbi12d ⊢ ( ( 𝐵 ∈ On ∧ 𝑥 ∈ On ) → ( ( 𝐵 ∈ 𝑥 → ( ∀ 𝑦 ∈ 𝑥 ( 𝐵 ∈ 𝑦 → 𝜒 ) → 𝜑 ) ) ↔ ( suc 𝐵 ⊆ 𝑥 → ( ∀ 𝑦 ∈ 𝑥 ( suc 𝐵 ⊆ 𝑦 → 𝜒 ) → 𝜑 ) ) ) )
41 29 40 sylan2 ⊢ ( ( 𝐵 ∈ On ∧ Lim 𝑥 ) → ( ( 𝐵 ∈ 𝑥 → ( ∀ 𝑦 ∈ 𝑥 ( 𝐵 ∈ 𝑦 → 𝜒 ) → 𝜑 ) ) ↔ ( suc 𝐵 ⊆ 𝑥 → ( ∀ 𝑦 ∈ 𝑥 ( suc 𝐵 ⊆ 𝑦 → 𝜒 ) → 𝜑 ) ) ) )
42 41 ancoms ⊢ ( ( Lim 𝑥 ∧ 𝐵 ∈ On ) → ( ( 𝐵 ∈ 𝑥 → ( ∀ 𝑦 ∈ 𝑥 ( 𝐵 ∈ 𝑦 → 𝜒 ) → 𝜑 ) ) ↔ ( suc 𝐵 ⊆ 𝑥 → ( ∀ 𝑦 ∈ 𝑥 ( suc 𝐵 ⊆ 𝑦 → 𝜒 ) → 𝜑 ) ) ) )
43 26 42 mpbid ⊢ ( ( Lim 𝑥 ∧ 𝐵 ∈ On ) → ( suc 𝐵 ⊆ 𝑥 → ( ∀ 𝑦 ∈ 𝑥 ( suc 𝐵 ⊆ 𝑦 → 𝜒 ) → 𝜑 ) ) )
44 9 43 sylan2br ⊢ ( ( Lim 𝑥 ∧ suc 𝐵 ∈ On ) → ( suc 𝐵 ⊆ 𝑥 → ( ∀ 𝑦 ∈ 𝑥 ( suc 𝐵 ⊆ 𝑦 → 𝜒 ) → 𝜑 ) ) )
45 44 imp ⊢ ( ( ( Lim 𝑥 ∧ suc 𝐵 ∈ On ) ∧ suc 𝐵 ⊆ 𝑥 ) → ( ∀ 𝑦 ∈ 𝑥 ( suc 𝐵 ⊆ 𝑦 → 𝜒 ) → 𝜑 ) )
46 1 2 3 4 15 24 45 tfindsg ⊢ ( ( ( 𝐴 ∈ On ∧ suc 𝐵 ∈ On ) ∧ suc 𝐵 ⊆ 𝐴 ) → 𝜏 )
47 46 expl ⊢ ( 𝐴 ∈ On → ( ( suc 𝐵 ∈ On ∧ suc 𝐵 ⊆ 𝐴 ) → 𝜏 ) )
48 47 adantr ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ 𝐴 ) → ( ( suc 𝐵 ∈ On ∧ suc 𝐵 ⊆ 𝐴 ) → 𝜏 ) )
49 10 14 48 mp2and ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ 𝐴 ) → 𝜏 )