Theorem tfinds 7857

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 7844	. . . . 5 ⊢ (Lim 𝑥 ↔ (Ord 𝑥 ∧ ¬ (𝑥 = ∅ ∨ ∃𝑦 ∈ On 𝑥 = suc 𝑦)))
4	3	notbii 323	. . . 4 ⊢ (¬ Lim 𝑥 ↔ ¬ (Ord 𝑥 ∧ ¬ (𝑥 = ∅ ∨ ∃𝑦 ∈ On 𝑥 = suc 𝑦)))
5		iman 407	. . . . 5 ⊢ ((Ord 𝑥 → (𝑥 = ∅ ∨ ∃𝑦 ∈ On 𝑥 = suc 𝑦)) ↔ ¬ (Ord 𝑥 ∧ ¬ (𝑥 = ∅ ∨ ∃𝑦 ∈ On 𝑥 = suc 𝑦)))
6		eloni 6367	. . . . . . 7 ⊢ (𝑥 ∈ On → Ord 𝑥)
7		pm2.27 43	. . . . . . 7 ⊢ (Ord 𝑥 → ((Ord 𝑥 → (𝑥 = ∅ ∨ ∃𝑦 ∈ On 𝑥 = suc 𝑦)) → (𝑥 = ∅ ∨ ∃𝑦 ∈ On 𝑥 = suc 𝑦)))
8	6, 7	syl 18	. . . . . 6 ⊢ (𝑥 ∈ On → ((Ord 𝑥 → (𝑥 = ∅ ∨ ∃𝑦 ∈ On 𝑥 = suc 𝑦)) → (𝑥 = ∅ ∨ ∃𝑦 ∈ On 𝑥 = suc 𝑦)))
9		tfinds.5	. . . . . . . . 9 ⊢ 𝜓
10		tfinds.1	. . . . . . . . 9 ⊢ (𝑥 = ∅ → (𝜑 ↔ 𝜓))
11	9, 10	mpbiri 261	. . . . . . . 8 ⊢ (𝑥 = ∅ → 𝜑)
12	11	a1d 26	. . . . . . 7 ⊢ (𝑥 = ∅ → (∀𝑦 ∈ 𝑥 𝜒 → 𝜑))
13		nfra1 3286	. . . . . . . . 9 ⊢ Ⅎ𝑦∀𝑦 ∈ 𝑥 𝜒
14		nfv 1947	. . . . . . . . 9 ⊢ Ⅎ𝑦𝜑
15	13, 14	nfim 1929	. . . . . . . 8 ⊢ Ⅎ𝑦(∀𝑦 ∈ 𝑥 𝜒 → 𝜑)
16		vex 3454	. . . . . . . . . . . . 13 ⊢ 𝑦 ∈ V
17	16	sucid 6442	. . . . . . . . . . . 12 ⊢ 𝑦 ∈ suc 𝑦
18	1	rspcv 3572	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ suc 𝑦 → (∀𝑥 ∈ suc 𝑦𝜑 → 𝜒))
19	17, 18	ax-mp 5	. . . . . . . . . . 11 ⊢ (∀𝑥 ∈ suc 𝑦𝜑 → 𝜒)
20		tfinds.6	. . . . . . . . . . 11 ⊢ (𝑦 ∈ On → (𝜒 → 𝜃))
21	19, 20	syl5 35	. . . . . . . . . 10 ⊢ (𝑦 ∈ On → (∀𝑥 ∈ suc 𝑦𝜑 → 𝜃))
22		raleq 3316	. . . . . . . . . . . 12 ⊢ (𝑥 = suc 𝑦 → (∀𝑧 ∈ 𝑥 [𝑧 / 𝑥]𝜑 ↔ ∀𝑧 ∈ suc 𝑦[𝑧 / 𝑥]𝜑))
23		nfv 1947	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥𝜒
24	23, 1	sbiev 2345	. . . . . . . . . . . . . 14 ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜒)
25		sbequ 2120	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑧 → ([𝑦 / 𝑥]𝜑 ↔ [𝑧 / 𝑥]𝜑))
26	24, 25	bitr3id 288	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑧 → (𝜒 ↔ [𝑧 / 𝑥]𝜑))
27	26	cbvralvw 3240	. . . . . . . . . . . 12 ⊢ (∀𝑦 ∈ 𝑥 𝜒 ↔ ∀𝑧 ∈ 𝑥 [𝑧 / 𝑥]𝜑)
28		cbvralsvw 3313	. . . . . . . . . . . 12 ⊢ (∀𝑥 ∈ suc 𝑦𝜑 ↔ ∀𝑧 ∈ suc 𝑦[𝑧 / 𝑥]𝜑)
29	22, 27, 28	3bitr4g 317	. . . . . . . . . . 11 ⊢ (𝑥 = suc 𝑦 → (∀𝑦 ∈ 𝑥 𝜒 ↔ ∀𝑥 ∈ suc 𝑦𝜑))
30	29	imbi1d 344	. . . . . . . . . 10 ⊢ (𝑥 = suc 𝑦 → ((∀𝑦 ∈ 𝑥 𝜒 → 𝜃) ↔ (∀𝑥 ∈ suc 𝑦𝜑 → 𝜃)))
31	21, 30	syl5ibrcom 250	. . . . . . . . 9 ⊢ (𝑦 ∈ On → (𝑥 = suc 𝑦 → (∀𝑦 ∈ 𝑥 𝜒 → 𝜃)))
32		tfinds.3	. . . . . . . . . . 11 ⊢ (𝑥 = suc 𝑦 → (𝜑 ↔ 𝜃))
33	32	biimprd 251	. . . . . . . . . 10 ⊢ (𝑥 = suc 𝑦 → (𝜃 → 𝜑))
34	33	a1i 11	. . . . . . . . 9 ⊢ (𝑦 ∈ On → (𝑥 = suc 𝑦 → (𝜃 → 𝜑)))
35	31, 34	syldd 73	. . . . . . . 8 ⊢ (𝑦 ∈ On → (𝑥 = suc 𝑦 → (∀𝑦 ∈ 𝑥 𝜒 → 𝜑)))
36	15, 35	rexlimi 3262	. . . . . . 7 ⊢ (∃𝑦 ∈ On 𝑥 = suc 𝑦 → (∀𝑦 ∈ 𝑥 𝜒 → 𝜑))
37	12, 36	jaoi 871	. . . . . 6 ⊢ ((𝑥 = ∅ ∨ ∃𝑦 ∈ On 𝑥 = suc 𝑦) → (∀𝑦 ∈ 𝑥 𝜒 → 𝜑))
38	8, 37	syl6 36	. . . . 5 ⊢ (𝑥 ∈ On → ((Ord 𝑥 → (𝑥 = ∅ ∨ ∃𝑦 ∈ On 𝑥 = suc 𝑦)) → (∀𝑦 ∈ 𝑥 𝜒 → 𝜑)))
39	5, 38	biimtrrid 246	. . . 4 ⊢ (𝑥 ∈ On → (¬ (Ord 𝑥 ∧ ¬ (𝑥 = ∅ ∨ ∃𝑦 ∈ On 𝑥 = suc 𝑦)) → (∀𝑦 ∈ 𝑥 𝜒 → 𝜑)))
40	4, 39	biimtrid 245	. . 3 ⊢ (𝑥 ∈ On → (¬ Lim 𝑥 → (∀𝑦 ∈ 𝑥 𝜒 → 𝜑)))
41		tfinds.7	. . 3 ⊢ (Lim 𝑥 → (∀𝑦 ∈ 𝑥 𝜒 → 𝜑))
42	40, 41	pm2.61d2 183	. 2 ⊢ (𝑥 ∈ On → (∀𝑦 ∈ 𝑥 𝜒 → 𝜑))
43	1, 2, 42	tfis3 7855	1 ⊢ (𝐴 ∈ On → 𝜏)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861   = wceq 1570  [wsb 2099   ∈ wcel 2145  ∀wral 3076  ∃wrex 3086  ∅c0 4279  Ord word 6356  Oncon0 6357  Lim wlim 6358  suc csuc 6359

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-nul 5263  ax-pr 5398  ax-un 7737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-tr 5213  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363

This theorem is used by:  tfindsg  7858  tfindes  7860  tfinds3  7862  oa0r  8528  om0r  8529  om1r  8533  oe1m  8535  oeoalem  8587  r1sdom  9759  r1tr  9761  alephon  10075  alephcard  10076  alephordi  10080  constrsscn  34253  constr01  34255  constrmon  34257  constrconj  34258  rdgprc  36374