Theorem tfinds 7836

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 7823	. . . . 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 6342	. . . . . . 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 3261	. . . . . . . . 9 ⊢ Ⅎ𝑦∀𝑦 ∈ 𝑥 𝜒
14		nfv 1914	. . . . . . . . 9 ⊢ Ⅎ𝑦𝜑
15	13, 14	nfim 1896	. . . . . . . 8 ⊢ Ⅎ𝑦(∀𝑦 ∈ 𝑥 𝜒 → 𝜑)
16		vex 3451	. . . . . . . . . . . . 13 ⊢ 𝑦 ∈ V
17	16	sucid 6416	. . . . . . . . . . . 12 ⊢ 𝑦 ∈ suc 𝑦
18	1	rspcv 3584	. . . . . . . . . . . 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 3296	. . . . . . . . . . . 12 ⊢ (𝑥 = suc 𝑦 → (∀𝑧 ∈ 𝑥 [𝑧 / 𝑥]𝜑 ↔ ∀𝑧 ∈ suc 𝑦[𝑧 / 𝑥]𝜑))
23		nfv 1914	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥𝜒
24	23, 1	sbiev 2313	. . . . . . . . . . . . . 14 ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜒)
25		sbequ 2084	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑧 → ([𝑦 / 𝑥]𝜑 ↔ [𝑧 / 𝑥]𝜑))
26	24, 25	bitr3id 285	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑧 → (𝜒 ↔ [𝑧 / 𝑥]𝜑))
27	26	cbvralvw 3215	. . . . . . . . . . . 12 ⊢ (∀𝑦 ∈ 𝑥 𝜒 ↔ ∀𝑧 ∈ 𝑥 [𝑧 / 𝑥]𝜑)
28		cbvralsvw 3290	. . . . . . . . . . . 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 3237	. . . . . . 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 7834	1 ⊢ (𝐴 ∈ On → 𝜏)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   = wceq 1540  [wsb 2065   ∈ wcel 2109  ∀wral 3044  ∃wrex 3053  ∅c0 4296  Ord word 6331  Oncon0 6332  Lim wlim 6333  suc csuc 6334

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387  ax-un 7711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3934  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-tr 5215  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-we 5593  df-ord 6335  df-on 6336  df-lim 6337  df-suc 6338

This theorem is referenced by:  tfindsg  7837  tfindes  7839  tfinds3  7841  oa0r  8502  om0r  8503  om1r  8507  oe1m  8509  oeoalem  8560  r1sdom  9727  r1tr  9729  alephon  10022  alephcard  10023  alephordi  10027  constrsscn  33730  constr01  33732  constrmon  33734  constrconj  33735  rdgprc  35782