Theorem tfinds 7437

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. (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 7425	. . . . 5 ⊢ (Lim 𝑥 ↔ (Ord 𝑥 ∧ ¬ (𝑥 = ∅ ∨ ∃𝑦 ∈ On 𝑥 = suc 𝑦)))
4	3	notbii 321	. . . 4 ⊢ (¬ Lim 𝑥 ↔ ¬ (Ord 𝑥 ∧ ¬ (𝑥 = ∅ ∨ ∃𝑦 ∈ On 𝑥 = suc 𝑦)))
5		iman 402	. . . . 5 ⊢ ((Ord 𝑥 → (𝑥 = ∅ ∨ ∃𝑦 ∈ On 𝑥 = suc 𝑦)) ↔ ¬ (Ord 𝑥 ∧ ¬ (𝑥 = ∅ ∨ ∃𝑦 ∈ On 𝑥 = suc 𝑦)))
6		eloni 6083	. . . . . . 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 259	. . . . . . . 8 ⊢ (𝑥 = ∅ → 𝜑)
12	11	a1d 25	. . . . . . 7 ⊢ (𝑥 = ∅ → (∀𝑦 ∈ 𝑥 𝜒 → 𝜑))
13		nfra1 3188	. . . . . . . . 9 ⊢ Ⅎ𝑦∀𝑦 ∈ 𝑥 𝜒
14		nfv 1896	. . . . . . . . 9 ⊢ Ⅎ𝑦𝜑
15	13, 14	nfim 1882	. . . . . . . 8 ⊢ Ⅎ𝑦(∀𝑦 ∈ 𝑥 𝜒 → 𝜑)
16		vex 3443	. . . . . . . . . . . . 13 ⊢ 𝑦 ∈ V
17	16	sucid 6152	. . . . . . . . . . . 12 ⊢ 𝑦 ∈ suc 𝑦
18	1	rspcv 3557	. . . . . . . . . . . 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 3367	. . . . . . . . . . . 12 ⊢ (𝑥 = suc 𝑦 → (∀𝑧 ∈ 𝑥 [𝑧 / 𝑥]𝜑 ↔ ∀𝑧 ∈ suc 𝑦[𝑧 / 𝑥]𝜑))
23		nfv 1896	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥𝜒
24	23, 1	sbie 2500	. . . . . . . . . . . . . 14 ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜒)
25		sbequ 2065	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑧 → ([𝑦 / 𝑥]𝜑 ↔ [𝑧 / 𝑥]𝜑))
26	24, 25	syl5bbr 286	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑧 → (𝜒 ↔ [𝑧 / 𝑥]𝜑))
27	26	cbvralv 3405	. . . . . . . . . . . 12 ⊢ (∀𝑦 ∈ 𝑥 𝜒 ↔ ∀𝑧 ∈ 𝑥 [𝑧 / 𝑥]𝜑)
28		cbvralsv 3417	. . . . . . . . . . . 12 ⊢ (∀𝑥 ∈ suc 𝑦𝜑 ↔ ∀𝑧 ∈ suc 𝑦[𝑧 / 𝑥]𝜑)
29	22, 27, 28	3bitr4g 315	. . . . . . . . . . 11 ⊢ (𝑥 = suc 𝑦 → (∀𝑦 ∈ 𝑥 𝜒 ↔ ∀𝑥 ∈ suc 𝑦𝜑))
30	29	imbi1d 343	. . . . . . . . . 10 ⊢ (𝑥 = suc 𝑦 → ((∀𝑦 ∈ 𝑥 𝜒 → 𝜃) ↔ (∀𝑥 ∈ suc 𝑦𝜑 → 𝜃)))
31	21, 30	syl5ibrcom 248	. . . . . . . . 9 ⊢ (𝑦 ∈ On → (𝑥 = suc 𝑦 → (∀𝑦 ∈ 𝑥 𝜒 → 𝜃)))
32		tfinds.3	. . . . . . . . . . 11 ⊢ (𝑥 = suc 𝑦 → (𝜑 ↔ 𝜃))
33	32	biimprd 249	. . . . . . . . . 10 ⊢ (𝑥 = suc 𝑦 → (𝜃 → 𝜑))
34	33	a1i 11	. . . . . . . . 9 ⊢ (𝑦 ∈ On → (𝑥 = suc 𝑦 → (𝜃 → 𝜑)))
35	31, 34	syldd 72	. . . . . . . 8 ⊢ (𝑦 ∈ On → (𝑥 = suc 𝑦 → (∀𝑦 ∈ 𝑥 𝜒 → 𝜑)))
36	15, 35	rexlimi 3278	. . . . . . 7 ⊢ (∃𝑦 ∈ On 𝑥 = suc 𝑦 → (∀𝑦 ∈ 𝑥 𝜒 → 𝜑))
37	12, 36	jaoi 852	. . . . . 6 ⊢ ((𝑥 = ∅ ∨ ∃𝑦 ∈ On 𝑥 = suc 𝑦) → (∀𝑦 ∈ 𝑥 𝜒 → 𝜑))
38	8, 37	syl6 35	. . . . 5 ⊢ (𝑥 ∈ On → ((Ord 𝑥 → (𝑥 = ∅ ∨ ∃𝑦 ∈ On 𝑥 = suc 𝑦)) → (∀𝑦 ∈ 𝑥 𝜒 → 𝜑)))
39	5, 38	syl5bir 244	. . . 4 ⊢ (𝑥 ∈ On → (¬ (Ord 𝑥 ∧ ¬ (𝑥 = ∅ ∨ ∃𝑦 ∈ On 𝑥 = suc 𝑦)) → (∀𝑦 ∈ 𝑥 𝜒 → 𝜑)))
40	4, 39	syl5bi 243	. . 3 ⊢ (𝑥 ∈ On → (¬ Lim 𝑥 → (∀𝑦 ∈ 𝑥 𝜒 → 𝜑)))
41		tfinds.7	. . 3 ⊢ (Lim 𝑥 → (∀𝑦 ∈ 𝑥 𝜒 → 𝜑))
42	40, 41	pm2.61d2 182	. 2 ⊢ (𝑥 ∈ On → (∀𝑦 ∈ 𝑥 𝜒 → 𝜑))
43	1, 2, 42	tfis3 7435	1 ⊢ (𝐴 ∈ On → 𝜏)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 207   ∧ wa 396   ∨ wo 842   = wceq 1525  [wsb 2044   ∈ wcel 2083  ∀wral 3107  ∃wrex 3108  ∅c0 4217  Ord word 6072  Oncon0 6073  Lim wlim 6074  suc csuc 6075

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-13 2346  ax-ext 2771  ax-sep 5101  ax-nul 5108  ax-pr 5228  ax-un 7326

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-mo 2578  df-eu 2614  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-ne 2987  df-ral 3112  df-rex 3113  df-rab 3116  df-v 3442  df-sbc 3712  df-dif 3868  df-un 3870  df-in 3872  df-ss 3880  df-pss 3882  df-nul 4218  df-if 4388  df-pw 4461  df-sn 4479  df-pr 4481  df-tp 4483  df-op 4485  df-uni 4752  df-br 4969  df-opab 5031  df-tr 5071  df-eprel 5360  df-po 5369  df-so 5370  df-fr 5409  df-we 5411  df-ord 6076  df-on 6077  df-lim 6078  df-suc 6079

This theorem is referenced by:  tfindsg  7438  tfindes  7440  tfinds3  7442  oa0r  8021  om0r  8022  om1r  8026  oe1m  8028  oeoalem  8079  r1sdom  9056  r1tr  9058  alephon  9348  alephcard  9349  alephordi  9353  rdgprc  32650