Theorem tfinds 7806

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 7793	. . . . 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 6329	. . . . . . 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 3262	. . . . . . . . 9 ⊢ Ⅎ𝑦∀𝑦 ∈ 𝑥 𝜒
14		nfv 1916	. . . . . . . . 9 ⊢ Ⅎ𝑦𝜑
15	13, 14	nfim 1898	. . . . . . . 8 ⊢ Ⅎ𝑦(∀𝑦 ∈ 𝑥 𝜒 → 𝜑)
16		vex 3434	. . . . . . . . . . . . 13 ⊢ 𝑦 ∈ V
17	16	sucid 6403	. . . . . . . . . . . 12 ⊢ 𝑦 ∈ suc 𝑦
18	1	rspcv 3561	. . . . . . . . . . . 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 3293	. . . . . . . . . . . 12 ⊢ (𝑥 = suc 𝑦 → (∀𝑧 ∈ 𝑥 [𝑧 / 𝑥]𝜑 ↔ ∀𝑧 ∈ suc 𝑦[𝑧 / 𝑥]𝜑))
23		nfv 1916	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥𝜒
24	23, 1	sbiev 2320	. . . . . . . . . . . . . 14 ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜒)
25		sbequ 2089	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑧 → ([𝑦 / 𝑥]𝜑 ↔ [𝑧 / 𝑥]𝜑))
26	24, 25	bitr3id 285	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑧 → (𝜒 ↔ [𝑧 / 𝑥]𝜑))
27	26	cbvralvw 3216	. . . . . . . . . . . 12 ⊢ (∀𝑦 ∈ 𝑥 𝜒 ↔ ∀𝑧 ∈ 𝑥 [𝑧 / 𝑥]𝜑)
28		cbvralsvw 3289	. . . . . . . . . . . 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 3238	. . . . . . 7 ⊢ (∃𝑦 ∈ On 𝑥 = suc 𝑦 → (∀𝑦 ∈ 𝑥 𝜒 → 𝜑))
37	12, 36	jaoi 858	. . . . . 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 7804	1 ⊢ (𝐴 ∈ On → 𝜏)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 848   = wceq 1542  [wsb 2068   ∈ wcel 2114  ∀wral 3052  ∃wrex 3062  ∅c0 4274  Ord word 6318  Oncon0 6319  Lim wlim 6320  suc csuc 6321

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5232  ax-nul 5242  ax-pr 5372  ax-un 7684

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-tr 5194  df-eprel 5526  df-po 5534  df-so 5535  df-fr 5579  df-we 5581  df-ord 6322  df-on 6323  df-lim 6324  df-suc 6325

This theorem is referenced by:  tfindsg  7807  tfindes  7809  tfinds3  7811  oa0r  8468  om0r  8469  om1r  8473  oe1m  8475  oeoalem  8527  r1sdom  9693  r1tr  9695  alephon  9986  alephcard  9987  alephordi  9991  constrsscn  33904  constr01  33906  constrmon  33908  constrconj  33909  rdgprc  35994