Metamath Proof Explorer

Theorem tfindsg

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 B instead of zero. Remark in TakeutiZaring p. 57. (Contributed by NM, 5-Mar-2004)

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

Proof

Step Hyp Ref Expression
1 tfindsg.1 ⊢ ( 𝑥 = 𝐵 → ( 𝜑 ↔ 𝜓 ) )
2 tfindsg.2 ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜒 ) )
3 tfindsg.3 ⊢ ( 𝑥 = suc 𝑦 → ( 𝜑 ↔ 𝜃 ) )
4 tfindsg.4 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜏 ) )
5 tfindsg.5 ⊢ ( 𝐵 ∈ On → 𝜓 )
6 tfindsg.6 ⊢ ( ( ( 𝑦 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐵 ⊆ 𝑦 ) → ( 𝜒 → 𝜃 ) )
7 tfindsg.7 ⊢ ( ( ( Lim 𝑥 ∧ 𝐵 ∈ On ) ∧ 𝐵 ⊆ 𝑥 ) → ( ∀ 𝑦 ∈ 𝑥 ( 𝐵 ⊆ 𝑦 → 𝜒 ) → 𝜑 ) )
8 sseq2 ⊢ ( 𝑥 = ∅ → ( 𝐵 ⊆ 𝑥 ↔ 𝐵 ⊆ ∅ ) )
9 8 adantl ⊢ ( ( 𝐵 = ∅ ∧ 𝑥 = ∅ ) → ( 𝐵 ⊆ 𝑥 ↔ 𝐵 ⊆ ∅ ) )
10 eqeq2 ⊢ ( 𝐵 = ∅ → ( 𝑥 = 𝐵 ↔ 𝑥 = ∅ ) )
11 10 1 biimtrrdi ⊢ ( 𝐵 = ∅ → ( 𝑥 = ∅ → ( 𝜑 ↔ 𝜓 ) ) )
12 11 imp ⊢ ( ( 𝐵 = ∅ ∧ 𝑥 = ∅ ) → ( 𝜑 ↔ 𝜓 ) )
13 9 12 imbi12d ⊢ ( ( 𝐵 = ∅ ∧ 𝑥 = ∅ ) → ( ( 𝐵 ⊆ 𝑥 → 𝜑 ) ↔ ( 𝐵 ⊆ ∅ → 𝜓 ) ) )
14 8 imbi1d ⊢ ( 𝑥 = ∅ → ( ( 𝐵 ⊆ 𝑥 → 𝜑 ) ↔ ( 𝐵 ⊆ ∅ → 𝜑 ) ) )
15 ss0 ⊢ ( 𝐵 ⊆ ∅ → 𝐵 = ∅ )
16 15 con3i ⊢ ( ¬ 𝐵 = ∅ → ¬ 𝐵 ⊆ ∅ )
17 16 pm2.21d ⊢ ( ¬ 𝐵 = ∅ → ( 𝐵 ⊆ ∅ → ( 𝜑 ↔ 𝜓 ) ) )
18 17 pm5.74d ⊢ ( ¬ 𝐵 = ∅ → ( ( 𝐵 ⊆ ∅ → 𝜑 ) ↔ ( 𝐵 ⊆ ∅ → 𝜓 ) ) )
19 14 18 sylan9bbr ⊢ ( ( ¬ 𝐵 = ∅ ∧ 𝑥 = ∅ ) → ( ( 𝐵 ⊆ 𝑥 → 𝜑 ) ↔ ( 𝐵 ⊆ ∅ → 𝜓 ) ) )
20 13 19 pm2.61ian ⊢ ( 𝑥 = ∅ → ( ( 𝐵 ⊆ 𝑥 → 𝜑 ) ↔ ( 𝐵 ⊆ ∅ → 𝜓 ) ) )
21 20 imbi2d ⊢ ( 𝑥 = ∅ → ( ( 𝐵 ∈ On → ( 𝐵 ⊆ 𝑥 → 𝜑 ) ) ↔ ( 𝐵 ∈ On → ( 𝐵 ⊆ ∅ → 𝜓 ) ) ) )
22 sseq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐵 ⊆ 𝑥 ↔ 𝐵 ⊆ 𝑦 ) )
23 22 2 imbi12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐵 ⊆ 𝑥 → 𝜑 ) ↔ ( 𝐵 ⊆ 𝑦 → 𝜒 ) ) )
24 23 imbi2d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐵 ∈ On → ( 𝐵 ⊆ 𝑥 → 𝜑 ) ) ↔ ( 𝐵 ∈ On → ( 𝐵 ⊆ 𝑦 → 𝜒 ) ) ) )
25 sseq2 ⊢ ( 𝑥 = suc 𝑦 → ( 𝐵 ⊆ 𝑥 ↔ 𝐵 ⊆ suc 𝑦 ) )
26 25 3 imbi12d ⊢ ( 𝑥 = suc 𝑦 → ( ( 𝐵 ⊆ 𝑥 → 𝜑 ) ↔ ( 𝐵 ⊆ suc 𝑦 → 𝜃 ) ) )
27 26 imbi2d ⊢ ( 𝑥 = suc 𝑦 → ( ( 𝐵 ∈ On → ( 𝐵 ⊆ 𝑥 → 𝜑 ) ) ↔ ( 𝐵 ∈ On → ( 𝐵 ⊆ suc 𝑦 → 𝜃 ) ) ) )
28 sseq2 ⊢ ( 𝑥 = 𝐴 → ( 𝐵 ⊆ 𝑥 ↔ 𝐵 ⊆ 𝐴 ) )
29 28 4 imbi12d ⊢ ( 𝑥 = 𝐴 → ( ( 𝐵 ⊆ 𝑥 → 𝜑 ) ↔ ( 𝐵 ⊆ 𝐴 → 𝜏 ) ) )
30 29 imbi2d ⊢ ( 𝑥 = 𝐴 → ( ( 𝐵 ∈ On → ( 𝐵 ⊆ 𝑥 → 𝜑 ) ) ↔ ( 𝐵 ∈ On → ( 𝐵 ⊆ 𝐴 → 𝜏 ) ) ) )
31 5 a1d ⊢ ( 𝐵 ∈ On → ( 𝐵 ⊆ ∅ → 𝜓 ) )
32 vex ⊢ 𝑦 ∈ V
33 32 sucex ⊢ suc 𝑦 ∈ V
34 33 eqvinc ⊢ ( suc 𝑦 = 𝐵 ↔ ∃ 𝑥 ( 𝑥 = suc 𝑦 ∧ 𝑥 = 𝐵 ) )
35 5 1 imbitrrid ⊢ ( 𝑥 = 𝐵 → ( 𝐵 ∈ On → 𝜑 ) )
36 3 biimpd ⊢ ( 𝑥 = suc 𝑦 → ( 𝜑 → 𝜃 ) )
37 35 36 sylan9r ⊢ ( ( 𝑥 = suc 𝑦 ∧ 𝑥 = 𝐵 ) → ( 𝐵 ∈ On → 𝜃 ) )
38 37 exlimiv ⊢ ( ∃ 𝑥 ( 𝑥 = suc 𝑦 ∧ 𝑥 = 𝐵 ) → ( 𝐵 ∈ On → 𝜃 ) )
39 34 38 sylbi ⊢ ( suc 𝑦 = 𝐵 → ( 𝐵 ∈ On → 𝜃 ) )
40 39 eqcoms ⊢ ( 𝐵 = suc 𝑦 → ( 𝐵 ∈ On → 𝜃 ) )
41 40 imim2i ⊢ ( ( 𝐵 ⊆ suc 𝑦 → 𝐵 = suc 𝑦 ) → ( 𝐵 ⊆ suc 𝑦 → ( 𝐵 ∈ On → 𝜃 ) ) )
42 41 a1d ⊢ ( ( 𝐵 ⊆ suc 𝑦 → 𝐵 = suc 𝑦 ) → ( ( 𝐵 ⊆ 𝑦 → 𝜒 ) → ( 𝐵 ⊆ suc 𝑦 → ( 𝐵 ∈ On → 𝜃 ) ) ) )
43 42 com4r ⊢ ( 𝐵 ∈ On → ( ( 𝐵 ⊆ suc 𝑦 → 𝐵 = suc 𝑦 ) → ( ( 𝐵 ⊆ 𝑦 → 𝜒 ) → ( 𝐵 ⊆ suc 𝑦 → 𝜃 ) ) ) )
44 43 adantl ⊢ ( ( 𝑦 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝐵 ⊆ suc 𝑦 → 𝐵 = suc 𝑦 ) → ( ( 𝐵 ⊆ 𝑦 → 𝜒 ) → ( 𝐵 ⊆ suc 𝑦 → 𝜃 ) ) ) )
45 df-ne ⊢ ( 𝐵 ≠ suc 𝑦 ↔ ¬ 𝐵 = suc 𝑦 )
46 45 anbi2i ⊢ ( ( 𝐵 ⊆ suc 𝑦 ∧ 𝐵 ≠ suc 𝑦 ) ↔ ( 𝐵 ⊆ suc 𝑦 ∧ ¬ 𝐵 = suc 𝑦 ) )
47 annim ⊢ ( ( 𝐵 ⊆ suc 𝑦 ∧ ¬ 𝐵 = suc 𝑦 ) ↔ ¬ ( 𝐵 ⊆ suc 𝑦 → 𝐵 = suc 𝑦 ) )
48 46 47 bitri ⊢ ( ( 𝐵 ⊆ suc 𝑦 ∧ 𝐵 ≠ suc 𝑦 ) ↔ ¬ ( 𝐵 ⊆ suc 𝑦 → 𝐵 = suc 𝑦 ) )
49 onsssuc ⊢ ( ( 𝐵 ∈ On ∧ 𝑦 ∈ On ) → ( 𝐵 ⊆ 𝑦 ↔ 𝐵 ∈ suc 𝑦 ) )
50 onsuc ⊢ ( 𝑦 ∈ On → suc 𝑦 ∈ On )
51 onelpss ⊢ ( ( 𝐵 ∈ On ∧ suc 𝑦 ∈ On ) → ( 𝐵 ∈ suc 𝑦 ↔ ( 𝐵 ⊆ suc 𝑦 ∧ 𝐵 ≠ suc 𝑦 ) ) )
52 50 51 sylan2 ⊢ ( ( 𝐵 ∈ On ∧ 𝑦 ∈ On ) → ( 𝐵 ∈ suc 𝑦 ↔ ( 𝐵 ⊆ suc 𝑦 ∧ 𝐵 ≠ suc 𝑦 ) ) )
53 49 52 bitrd ⊢ ( ( 𝐵 ∈ On ∧ 𝑦 ∈ On ) → ( 𝐵 ⊆ 𝑦 ↔ ( 𝐵 ⊆ suc 𝑦 ∧ 𝐵 ≠ suc 𝑦 ) ) )
54 53 ancoms ⊢ ( ( 𝑦 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐵 ⊆ 𝑦 ↔ ( 𝐵 ⊆ suc 𝑦 ∧ 𝐵 ≠ suc 𝑦 ) ) )
55 6 ex ⊢ ( ( 𝑦 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐵 ⊆ 𝑦 → ( 𝜒 → 𝜃 ) ) )
56 55 a1ddd ⊢ ( ( 𝑦 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐵 ⊆ 𝑦 → ( 𝜒 → ( 𝐵 ⊆ suc 𝑦 → 𝜃 ) ) ) )
57 56 a2d ⊢ ( ( 𝑦 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝐵 ⊆ 𝑦 → 𝜒 ) → ( 𝐵 ⊆ 𝑦 → ( 𝐵 ⊆ suc 𝑦 → 𝜃 ) ) ) )
58 57 com23 ⊢ ( ( 𝑦 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐵 ⊆ 𝑦 → ( ( 𝐵 ⊆ 𝑦 → 𝜒 ) → ( 𝐵 ⊆ suc 𝑦 → 𝜃 ) ) ) )
59 54 58 sylbird ⊢ ( ( 𝑦 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝐵 ⊆ suc 𝑦 ∧ 𝐵 ≠ suc 𝑦 ) → ( ( 𝐵 ⊆ 𝑦 → 𝜒 ) → ( 𝐵 ⊆ suc 𝑦 → 𝜃 ) ) ) )
60 48 59 biimtrrid ⊢ ( ( 𝑦 ∈ On ∧ 𝐵 ∈ On ) → ( ¬ ( 𝐵 ⊆ suc 𝑦 → 𝐵 = suc 𝑦 ) → ( ( 𝐵 ⊆ 𝑦 → 𝜒 ) → ( 𝐵 ⊆ suc 𝑦 → 𝜃 ) ) ) )
61 44 60 pm2.61d ⊢ ( ( 𝑦 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝐵 ⊆ 𝑦 → 𝜒 ) → ( 𝐵 ⊆ suc 𝑦 → 𝜃 ) ) )
62 61 ex ⊢ ( 𝑦 ∈ On → ( 𝐵 ∈ On → ( ( 𝐵 ⊆ 𝑦 → 𝜒 ) → ( 𝐵 ⊆ suc 𝑦 → 𝜃 ) ) ) )
63 62 a2d ⊢ ( 𝑦 ∈ On → ( ( 𝐵 ∈ On → ( 𝐵 ⊆ 𝑦 → 𝜒 ) ) → ( 𝐵 ∈ On → ( 𝐵 ⊆ suc 𝑦 → 𝜃 ) ) ) )
64 pm2.27 ⊢ ( 𝐵 ∈ On → ( ( 𝐵 ∈ On → ( 𝐵 ⊆ 𝑦 → 𝜒 ) ) → ( 𝐵 ⊆ 𝑦 → 𝜒 ) ) )
65 64 ralimdv ⊢ ( 𝐵 ∈ On → ( ∀ 𝑦 ∈ 𝑥 ( 𝐵 ∈ On → ( 𝐵 ⊆ 𝑦 → 𝜒 ) ) → ∀ 𝑦 ∈ 𝑥 ( 𝐵 ⊆ 𝑦 → 𝜒 ) ) )
66 65 ad2antlr ⊢ ( ( ( Lim 𝑥 ∧ 𝐵 ∈ On ) ∧ 𝐵 ⊆ 𝑥 ) → ( ∀ 𝑦 ∈ 𝑥 ( 𝐵 ∈ On → ( 𝐵 ⊆ 𝑦 → 𝜒 ) ) → ∀ 𝑦 ∈ 𝑥 ( 𝐵 ⊆ 𝑦 → 𝜒 ) ) )
67 66 7 syld ⊢ ( ( ( Lim 𝑥 ∧ 𝐵 ∈ On ) ∧ 𝐵 ⊆ 𝑥 ) → ( ∀ 𝑦 ∈ 𝑥 ( 𝐵 ∈ On → ( 𝐵 ⊆ 𝑦 → 𝜒 ) ) → 𝜑 ) )
68 67 exp31 ⊢ ( Lim 𝑥 → ( 𝐵 ∈ On → ( 𝐵 ⊆ 𝑥 → ( ∀ 𝑦 ∈ 𝑥 ( 𝐵 ∈ On → ( 𝐵 ⊆ 𝑦 → 𝜒 ) ) → 𝜑 ) ) ) )
69 68 com3l ⊢ ( 𝐵 ∈ On → ( 𝐵 ⊆ 𝑥 → ( Lim 𝑥 → ( ∀ 𝑦 ∈ 𝑥 ( 𝐵 ∈ On → ( 𝐵 ⊆ 𝑦 → 𝜒 ) ) → 𝜑 ) ) ) )
70 69 com4t ⊢ ( Lim 𝑥 → ( ∀ 𝑦 ∈ 𝑥 ( 𝐵 ∈ On → ( 𝐵 ⊆ 𝑦 → 𝜒 ) ) → ( 𝐵 ∈ On → ( 𝐵 ⊆ 𝑥 → 𝜑 ) ) ) )
71 21 24 27 30 31 63 70 tfinds ⊢ ( 𝐴 ∈ On → ( 𝐵 ∈ On → ( 𝐵 ⊆ 𝐴 → 𝜏 ) ) )
72 71 imp31 ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐵 ⊆ 𝐴 ) → 𝜏 )