Theorem tfinds2 7861

Description: Transfinite Induction (inference schema), using implicit substitutions. The first three hypotheses establish the substitutions we need. The last three are the basis and the induction hypotheses (for successor and limit ordinals respectively). Theorem Schema 4 of [Suppes] p. 197. The wff 𝜏 is an auxiliary antecedent to help shorten proofs using this theorem. (Contributed by NM, 4-Sep-2004.)

Hypotheses

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

Assertion

Ref	Expression
tfinds2	⊢ (𝑥 ∈ On → (𝜏 → 𝜑))

Distinct variable groups:   𝑥,𝑦,𝜏   𝜓,𝑥   𝜒,𝑥   𝜃,𝑥   𝜑,𝑦

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

Proof of Theorem tfinds2

Step	Hyp	Ref	Expression
1		tfinds2.4	. . 3 ⊢ (𝜏 → 𝜓)
2		0ex 5264	. . . 4 ⊢ ∅ ∈ V
3		tfinds2.1	. . . . 5 ⊢ (𝑥 = ∅ → (𝜑 ↔ 𝜓))
4	3	imbi2d 343	. . . 4 ⊢ (𝑥 = ∅ → ((𝜏 → 𝜑) ↔ (𝜏 → 𝜓)))
5	2, 4	sbcie 3780	. . 3 ⊢ ([∅ / 𝑥](𝜏 → 𝜑) ↔ (𝜏 → 𝜓))
6	1, 5	mpbir 234	. 2 ⊢ [∅ / 𝑥](𝜏 → 𝜑)
7		tfinds2.5	. . . . . . . 8 ⊢ (𝑦 ∈ On → (𝜏 → (𝜒 → 𝜃)))
8	7	a2d 30	. . . . . . 7 ⊢ (𝑦 ∈ On → ((𝜏 → 𝜒) → (𝜏 → 𝜃)))
9	8	sbcth 3754	. . . . . 6 ⊢ (𝑥 ∈ V → [𝑥 / 𝑦](𝑦 ∈ On → ((𝜏 → 𝜒) → (𝜏 → 𝜃))))
10	9	elv 3455	. . . . 5 ⊢ [𝑥 / 𝑦](𝑦 ∈ On → ((𝜏 → 𝜒) → (𝜏 → 𝜃)))
11		sbcimg 3787	. . . . . 6 ⊢ (𝑥 ∈ V → ([𝑥 / 𝑦](𝑦 ∈ On → ((𝜏 → 𝜒) → (𝜏 → 𝜃))) ↔ ([𝑥 / 𝑦]𝑦 ∈ On → [𝑥 / 𝑦]((𝜏 → 𝜒) → (𝜏 → 𝜃)))))
12	11	elv 3455	. . . . 5 ⊢ ([𝑥 / 𝑦](𝑦 ∈ On → ((𝜏 → 𝜒) → (𝜏 → 𝜃))) ↔ ([𝑥 / 𝑦]𝑦 ∈ On → [𝑥 / 𝑦]((𝜏 → 𝜒) → (𝜏 → 𝜃))))
13	10, 12	mpbi 233	. . . 4 ⊢ ([𝑥 / 𝑦]𝑦 ∈ On → [𝑥 / 𝑦]((𝜏 → 𝜒) → (𝜏 → 𝜃)))
14		sbcel1v 3804	. . . 4 ⊢ ([𝑥 / 𝑦]𝑦 ∈ On ↔ 𝑥 ∈ On)
15		sbcimg 3787	. . . . 5 ⊢ (𝑥 ∈ V → ([𝑥 / 𝑦]((𝜏 → 𝜒) → (𝜏 → 𝜃)) ↔ ([𝑥 / 𝑦](𝜏 → 𝜒) → [𝑥 / 𝑦](𝜏 → 𝜃))))
16	15	elv 3455	. . . 4 ⊢ ([𝑥 / 𝑦]((𝜏 → 𝜒) → (𝜏 → 𝜃)) ↔ ([𝑥 / 𝑦](𝜏 → 𝜒) → [𝑥 / 𝑦](𝜏 → 𝜃)))
17	13, 14, 16	3imtr3i 294	. . 3 ⊢ (𝑥 ∈ On → ([𝑥 / 𝑦](𝜏 → 𝜒) → [𝑥 / 𝑦](𝜏 → 𝜃)))
18		vex 3454	. . . 4 ⊢ 𝑥 ∈ V
19		tfinds2.2	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))
20	19	bicomd 226	. . . . . 6 ⊢ (𝑥 = 𝑦 → (𝜒 ↔ 𝜑))
21	20	equcoms 2053	. . . . 5 ⊢ (𝑦 = 𝑥 → (𝜒 ↔ 𝜑))
22	21	imbi2d 343	. . . 4 ⊢ (𝑦 = 𝑥 → ((𝜏 → 𝜒) ↔ (𝜏 → 𝜑)))
23	18, 22	sbcie 3780	. . 3 ⊢ ([𝑥 / 𝑦](𝜏 → 𝜒) ↔ (𝜏 → 𝜑))
24		vex 3454	. . . . . . 7 ⊢ 𝑦 ∈ V
25	24	sucex 7806	. . . . . 6 ⊢ suc 𝑦 ∈ V
26		tfinds2.3	. . . . . . 7 ⊢ (𝑥 = suc 𝑦 → (𝜑 ↔ 𝜃))
27	26	imbi2d 343	. . . . . 6 ⊢ (𝑥 = suc 𝑦 → ((𝜏 → 𝜑) ↔ (𝜏 → 𝜃)))
28	25, 27	sbcie 3780	. . . . 5 ⊢ ([suc 𝑦 / 𝑥](𝜏 → 𝜑) ↔ (𝜏 → 𝜃))
29	28	sbcbii 3795	. . . 4 ⊢ ([𝑥 / 𝑦][suc 𝑦 / 𝑥](𝜏 → 𝜑) ↔ [𝑥 / 𝑦](𝜏 → 𝜃))
30		suceq 6426	. . . . 5 ⊢ (𝑥 = 𝑦 → suc 𝑥 = suc 𝑦)
31	30	sbcco2 3766	. . . 4 ⊢ ([𝑥 / 𝑦][suc 𝑦 / 𝑥](𝜏 → 𝜑) ↔ [suc 𝑥 / 𝑥](𝜏 → 𝜑))
32	29, 31	bitr3i 280	. . 3 ⊢ ([𝑥 / 𝑦](𝜏 → 𝜃) ↔ [suc 𝑥 / 𝑥](𝜏 → 𝜑))
33	17, 23, 32	3imtr3g 298	. 2 ⊢ (𝑥 ∈ On → ((𝜏 → 𝜑) → [suc 𝑥 / 𝑥](𝜏 → 𝜑)))
34	19	imbi2d 343	. . . . 5 ⊢ (𝑥 = 𝑦 → ((𝜏 → 𝜑) ↔ (𝜏 → 𝜒)))
35	34	sbralie 3338	. . . 4 ⊢ (∀𝑥 ∈ 𝑦 (𝜏 → 𝜑) ↔ [𝑦 / 𝑥]∀𝑦 ∈ 𝑥 (𝜏 → 𝜒))
36		sbsbc 3743	. . . 4 ⊢ ([𝑦 / 𝑥]∀𝑦 ∈ 𝑥 (𝜏 → 𝜒) ↔ [𝑦 / 𝑥]∀𝑦 ∈ 𝑥 (𝜏 → 𝜒))
37	35, 36	bitr2i 279	. . 3 ⊢ ([𝑦 / 𝑥]∀𝑦 ∈ 𝑥 (𝜏 → 𝜒) ↔ ∀𝑥 ∈ 𝑦 (𝜏 → 𝜑))
38		r19.21v 3187	. . . . . . . 8 ⊢ (∀𝑦 ∈ 𝑥 (𝜏 → 𝜒) ↔ (𝜏 → ∀𝑦 ∈ 𝑥 𝜒))
39		tfinds2.6	. . . . . . . . 9 ⊢ (Lim 𝑥 → (𝜏 → (∀𝑦 ∈ 𝑥 𝜒 → 𝜑)))
40	39	a2d 30	. . . . . . . 8 ⊢ (Lim 𝑥 → ((𝜏 → ∀𝑦 ∈ 𝑥 𝜒) → (𝜏 → 𝜑)))
41	38, 40	biimtrid 245	. . . . . . 7 ⊢ (Lim 𝑥 → (∀𝑦 ∈ 𝑥 (𝜏 → 𝜒) → (𝜏 → 𝜑)))
42	41	sbcth 3754	. . . . . 6 ⊢ (𝑦 ∈ V → [𝑦 / 𝑥](Lim 𝑥 → (∀𝑦 ∈ 𝑥 (𝜏 → 𝜒) → (𝜏 → 𝜑))))
43	42	elv 3455	. . . . 5 ⊢ [𝑦 / 𝑥](Lim 𝑥 → (∀𝑦 ∈ 𝑥 (𝜏 → 𝜒) → (𝜏 → 𝜑)))
44		sbcimg 3787	. . . . . 6 ⊢ (𝑦 ∈ V → ([𝑦 / 𝑥](Lim 𝑥 → (∀𝑦 ∈ 𝑥 (𝜏 → 𝜒) → (𝜏 → 𝜑))) ↔ ([𝑦 / 𝑥]Lim 𝑥 → [𝑦 / 𝑥](∀𝑦 ∈ 𝑥 (𝜏 → 𝜒) → (𝜏 → 𝜑)))))
45	44	elv 3455	. . . . 5 ⊢ ([𝑦 / 𝑥](Lim 𝑥 → (∀𝑦 ∈ 𝑥 (𝜏 → 𝜒) → (𝜏 → 𝜑))) ↔ ([𝑦 / 𝑥]Lim 𝑥 → [𝑦 / 𝑥](∀𝑦 ∈ 𝑥 (𝜏 → 𝜒) → (𝜏 → 𝜑))))
46	43, 45	mpbi 233	. . . 4 ⊢ ([𝑦 / 𝑥]Lim 𝑥 → [𝑦 / 𝑥](∀𝑦 ∈ 𝑥 (𝜏 → 𝜒) → (𝜏 → 𝜑)))
47		limeq 6369	. . . . 5 ⊢ (𝑥 = 𝑦 → (Lim 𝑥 ↔ Lim 𝑦))
48	24, 47	sbcie 3780	. . . 4 ⊢ ([𝑦 / 𝑥]Lim 𝑥 ↔ Lim 𝑦)
49		sbcimg 3787	. . . . 5 ⊢ (𝑦 ∈ V → ([𝑦 / 𝑥](∀𝑦 ∈ 𝑥 (𝜏 → 𝜒) → (𝜏 → 𝜑)) ↔ ([𝑦 / 𝑥]∀𝑦 ∈ 𝑥 (𝜏 → 𝜒) → [𝑦 / 𝑥](𝜏 → 𝜑))))
50	49	elv 3455	. . . 4 ⊢ ([𝑦 / 𝑥](∀𝑦 ∈ 𝑥 (𝜏 → 𝜒) → (𝜏 → 𝜑)) ↔ ([𝑦 / 𝑥]∀𝑦 ∈ 𝑥 (𝜏 → 𝜒) → [𝑦 / 𝑥](𝜏 → 𝜑)))
51	46, 48, 50	3imtr3i 294	. . 3 ⊢ (Lim 𝑦 → ([𝑦 / 𝑥]∀𝑦 ∈ 𝑥 (𝜏 → 𝜒) → [𝑦 / 𝑥](𝜏 → 𝜑)))
52	37, 51	biimtrrid 246	. 2 ⊢ (Lim 𝑦 → (∀𝑥 ∈ 𝑦 (𝜏 → 𝜑) → [𝑦 / 𝑥](𝜏 → 𝜑)))
53	6, 33, 52	tfindes 7860	1 ⊢ (𝑥 ∈ On → (𝜏 → 𝜑))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570  [wsb 2099   ∈ wcel 2145  ∀wral 3076  Vcvv 3450  [wsbc 3739  ∅c0 4279  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-sbc 3740  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:  inar1  10787  grur1a  10831