Theorem tfinds 7881

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. Theorem 1.19 of [Schloeder] p. 3. (Contributed by NM, 16-Apr-1995.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)

Hypotheses

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

Assertion

Ref	Expression
tfinds	⊢ (𝐴 ∈ On → 𝜏)

Distinct variable groups:   𝑥,𝑦   𝑥,𝐴   𝜒,𝑥   𝜏,𝑥   𝜑,𝑦

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑥,𝑦)   𝜒(𝑦)   𝜃(𝑥,𝑦)   𝜏(𝑦)   𝐴(𝑦)

Proof of Theorem tfinds

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		tfinds.2	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))
2		tfinds.4	. 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏))
3		dflim3 7868	. . . . 5 ⊢ (Lim 𝑥 ↔ (Ord 𝑥 ∧ ¬ (𝑥 = ∅ ∨ ∃𝑦 ∈ On 𝑥 = suc 𝑦)))
4	3	notbii 320	. . . 4 ⊢ (¬ Lim 𝑥 ↔ ¬ (Ord 𝑥 ∧ ¬ (𝑥 = ∅ ∨ ∃𝑦 ∈ On 𝑥 = suc 𝑦)))
5		iman 401	. . . . 5 ⊢ ((Ord 𝑥 → (𝑥 = ∅ ∨ ∃𝑦 ∈ On 𝑥 = suc 𝑦)) ↔ ¬ (Ord 𝑥 ∧ ¬ (𝑥 = ∅ ∨ ∃𝑦 ∈ On 𝑥 = suc 𝑦)))
6		eloni 6396	. . . . . . 7 ⊢ (𝑥 ∈ On → Ord 𝑥)
7		pm2.27 42	. . . . . . 7 ⊢ (Ord 𝑥 → ((Ord 𝑥 → (𝑥 = ∅ ∨ ∃𝑦 ∈ On 𝑥 = suc 𝑦)) → (𝑥 = ∅ ∨ ∃𝑦 ∈ On 𝑥 = suc 𝑦)))
8	6, 7	syl 17	. . . . . 6 ⊢ (𝑥 ∈ On → ((Ord 𝑥 → (𝑥 = ∅ ∨ ∃𝑦 ∈ On 𝑥 = suc 𝑦)) → (𝑥 = ∅ ∨ ∃𝑦 ∈ On 𝑥 = suc 𝑦)))
9		tfinds.5	. . . . . . . . 9 ⊢ 𝜓
10		tfinds.1	. . . . . . . . 9 ⊢ (𝑥 = ∅ → (𝜑 ↔ 𝜓))
11	9, 10	mpbiri 258	. . . . . . . 8 ⊢ (𝑥 = ∅ → 𝜑)
12	11	a1d 25	. . . . . . 7 ⊢ (𝑥 = ∅ → (∀𝑦 ∈ 𝑥 𝜒 → 𝜑))
13		nfra1 3282	. . . . . . . . 9 ⊢ Ⅎ𝑦∀𝑦 ∈ 𝑥 𝜒
14		nfv 1912	. . . . . . . . 9 ⊢ Ⅎ𝑦𝜑
15	13, 14	nfim 1894	. . . . . . . 8 ⊢ Ⅎ𝑦(∀𝑦 ∈ 𝑥 𝜒 → 𝜑)
16		vex 3482	. . . . . . . . . . . . 13 ⊢ 𝑦 ∈ V
17	16	sucid 6468	. . . . . . . . . . . 12 ⊢ 𝑦 ∈ suc 𝑦
18	1	rspcv 3618	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ suc 𝑦 → (∀𝑥 ∈ suc 𝑦𝜑 → 𝜒))
19	17, 18	ax-mp 5	. . . . . . . . . . 11 ⊢ (∀𝑥 ∈ suc 𝑦𝜑 → 𝜒)
20		tfinds.6	. . . . . . . . . . 11 ⊢ (𝑦 ∈ On → (𝜒 → 𝜃))
21	19, 20	syl5 34	. . . . . . . . . 10 ⊢ (𝑦 ∈ On → (∀𝑥 ∈ suc 𝑦𝜑 → 𝜃))
22		raleq 3321	. . . . . . . . . . . 12 ⊢ (𝑥 = suc 𝑦 → (∀𝑧 ∈ 𝑥 [𝑧 / 𝑥]𝜑 ↔ ∀𝑧 ∈ suc 𝑦[𝑧 / 𝑥]𝜑))
23		nfv 1912	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥𝜒
24	23, 1	sbiev 2313	. . . . . . . . . . . . . 14 ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜒)
25		sbequ 2081	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑧 → ([𝑦 / 𝑥]𝜑 ↔ [𝑧 / 𝑥]𝜑))
26	24, 25	bitr3id 285	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑧 → (𝜒 ↔ [𝑧 / 𝑥]𝜑))
27	26	cbvralvw 3235	. . . . . . . . . . . 12 ⊢ (∀𝑦 ∈ 𝑥 𝜒 ↔ ∀𝑧 ∈ 𝑥 [𝑧 / 𝑥]𝜑)
28		cbvralsvw 3315	. . . . . . . . . . . 12 ⊢ (∀𝑥 ∈ suc 𝑦𝜑 ↔ ∀𝑧 ∈ suc 𝑦[𝑧 / 𝑥]𝜑)
29	22, 27, 28	3bitr4g 314	. . . . . . . . . . 11 ⊢ (𝑥 = suc 𝑦 → (∀𝑦 ∈ 𝑥 𝜒 ↔ ∀𝑥 ∈ suc 𝑦𝜑))
30	29	imbi1d 341	. . . . . . . . . 10 ⊢ (𝑥 = suc 𝑦 → ((∀𝑦 ∈ 𝑥 𝜒 → 𝜃) ↔ (∀𝑥 ∈ suc 𝑦𝜑 → 𝜃)))
31	21, 30	syl5ibrcom 247	. . . . . . . . 9 ⊢ (𝑦 ∈ On → (𝑥 = suc 𝑦 → (∀𝑦 ∈ 𝑥 𝜒 → 𝜃)))
32		tfinds.3	. . . . . . . . . . 11 ⊢ (𝑥 = suc 𝑦 → (𝜑 ↔ 𝜃))
33	32	biimprd 248	. . . . . . . . . 10 ⊢ (𝑥 = suc 𝑦 → (𝜃 → 𝜑))
34	33	a1i 11	. . . . . . . . 9 ⊢ (𝑦 ∈ On → (𝑥 = suc 𝑦 → (𝜃 → 𝜑)))
35	31, 34	syldd 72	. . . . . . . 8 ⊢ (𝑦 ∈ On → (𝑥 = suc 𝑦 → (∀𝑦 ∈ 𝑥 𝜒 → 𝜑)))
36	15, 35	rexlimi 3257	. . . . . . 7 ⊢ (∃𝑦 ∈ On 𝑥 = suc 𝑦 → (∀𝑦 ∈ 𝑥 𝜒 → 𝜑))
37	12, 36	jaoi 857	. . . . . 6 ⊢ ((𝑥 = ∅ ∨ ∃𝑦 ∈ On 𝑥 = suc 𝑦) → (∀𝑦 ∈ 𝑥 𝜒 → 𝜑))
38	8, 37	syl6 35	. . . . 5 ⊢ (𝑥 ∈ On → ((Ord 𝑥 → (𝑥 = ∅ ∨ ∃𝑦 ∈ On 𝑥 = suc 𝑦)) → (∀𝑦 ∈ 𝑥 𝜒 → 𝜑)))
39	5, 38	biimtrrid 243	. . . 4 ⊢ (𝑥 ∈ On → (¬ (Ord 𝑥 ∧ ¬ (𝑥 = ∅ ∨ ∃𝑦 ∈ On 𝑥 = suc 𝑦)) → (∀𝑦 ∈ 𝑥 𝜒 → 𝜑)))
40	4, 39	biimtrid 242	. . 3 ⊢ (𝑥 ∈ On → (¬ Lim 𝑥 → (∀𝑦 ∈ 𝑥 𝜒 → 𝜑)))
41		tfinds.7	. . 3 ⊢ (Lim 𝑥 → (∀𝑦 ∈ 𝑥 𝜒 → 𝜑))
42	40, 41	pm2.61d2 181	. 2 ⊢ (𝑥 ∈ On → (∀𝑦 ∈ 𝑥 𝜒 → 𝜑))
43	1, 2, 42	tfis3 7879	1 ⊢ (𝐴 ∈ On → 𝜏)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   = wceq 1537  [wsb 2062   ∈ wcel 2106  ∀wral 3059  ∃wrex 3068  ∅c0 4339  Ord word 6385  Oncon0 6386  Lim wlim 6387  suc csuc 6388

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438  ax-un 7754

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-opab 5211  df-tr 5266  df-eprel 5589  df-po 5597  df-so 5598  df-fr 5641  df-we 5643  df-ord 6389  df-on 6390  df-lim 6391  df-suc 6392

This theorem is referenced by:  tfindsg  7882  tfindes  7884  tfinds3  7886  oa0r  8575  om0r  8576  om1r  8580  oe1m  8582  oeoalem  8633  r1sdom  9812  r1tr  9814  alephon  10107  alephcard  10108  alephordi  10112  constrsscn  33745  constr01  33747  constrmon  33749  constrconj  33750  rdgprc  35776