Theorem tfinds2 7810

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 5243	. . . 4 ⊢ ∅ ∈ V
3		tfinds2.1	. . . . 5 ⊢ (𝑥 = ∅ → (𝜑 ↔ 𝜓))
4	3	imbi2d 340	. . . 4 ⊢ (𝑥 = ∅ → ((𝜏 → 𝜑) ↔ (𝜏 → 𝜓)))
5	2, 4	sbcie 3771	. . 3 ⊢ ([∅ / 𝑥](𝜏 → 𝜑) ↔ (𝜏 → 𝜓))
6	1, 5	mpbir 231	. 2 ⊢ [∅ / 𝑥](𝜏 → 𝜑)
7		tfinds2.5	. . . . . . . 8 ⊢ (𝑦 ∈ On → (𝜏 → (𝜒 → 𝜃)))
8	7	a2d 29	. . . . . . 7 ⊢ (𝑦 ∈ On → ((𝜏 → 𝜒) → (𝜏 → 𝜃)))
9	8	sbcth 3744	. . . . . 6 ⊢ (𝑥 ∈ V → [𝑥 / 𝑦](𝑦 ∈ On → ((𝜏 → 𝜒) → (𝜏 → 𝜃))))
10	9	elv 3435	. . . . 5 ⊢ [𝑥 / 𝑦](𝑦 ∈ On → ((𝜏 → 𝜒) → (𝜏 → 𝜃)))
11		sbcimg 3778	. . . . . 6 ⊢ (𝑥 ∈ V → ([𝑥 / 𝑦](𝑦 ∈ On → ((𝜏 → 𝜒) → (𝜏 → 𝜃))) ↔ ([𝑥 / 𝑦]𝑦 ∈ On → [𝑥 / 𝑦]((𝜏 → 𝜒) → (𝜏 → 𝜃)))))
12	11	elv 3435	. . . . 5 ⊢ ([𝑥 / 𝑦](𝑦 ∈ On → ((𝜏 → 𝜒) → (𝜏 → 𝜃))) ↔ ([𝑥 / 𝑦]𝑦 ∈ On → [𝑥 / 𝑦]((𝜏 → 𝜒) → (𝜏 → 𝜃))))
13	10, 12	mpbi 230	. . . 4 ⊢ ([𝑥 / 𝑦]𝑦 ∈ On → [𝑥 / 𝑦]((𝜏 → 𝜒) → (𝜏 → 𝜃)))
14		sbcel1v 3795	. . . 4 ⊢ ([𝑥 / 𝑦]𝑦 ∈ On ↔ 𝑥 ∈ On)
15		sbcimg 3778	. . . . 5 ⊢ (𝑥 ∈ V → ([𝑥 / 𝑦]((𝜏 → 𝜒) → (𝜏 → 𝜃)) ↔ ([𝑥 / 𝑦](𝜏 → 𝜒) → [𝑥 / 𝑦](𝜏 → 𝜃))))
16	15	elv 3435	. . . 4 ⊢ ([𝑥 / 𝑦]((𝜏 → 𝜒) → (𝜏 → 𝜃)) ↔ ([𝑥 / 𝑦](𝜏 → 𝜒) → [𝑥 / 𝑦](𝜏 → 𝜃)))
17	13, 14, 16	3imtr3i 291	. . 3 ⊢ (𝑥 ∈ On → ([𝑥 / 𝑦](𝜏 → 𝜒) → [𝑥 / 𝑦](𝜏 → 𝜃)))
18		vex 3434	. . . 4 ⊢ 𝑥 ∈ V
19		tfinds2.2	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))
20	19	bicomd 223	. . . . . 6 ⊢ (𝑥 = 𝑦 → (𝜒 ↔ 𝜑))
21	20	equcoms 2022	. . . . 5 ⊢ (𝑦 = 𝑥 → (𝜒 ↔ 𝜑))
22	21	imbi2d 340	. . . 4 ⊢ (𝑦 = 𝑥 → ((𝜏 → 𝜒) ↔ (𝜏 → 𝜑)))
23	18, 22	sbcie 3771	. . 3 ⊢ ([𝑥 / 𝑦](𝜏 → 𝜒) ↔ (𝜏 → 𝜑))
24		vex 3434	. . . . . . 7 ⊢ 𝑦 ∈ V
25	24	sucex 7755	. . . . . 6 ⊢ suc 𝑦 ∈ V
26		tfinds2.3	. . . . . . 7 ⊢ (𝑥 = suc 𝑦 → (𝜑 ↔ 𝜃))
27	26	imbi2d 340	. . . . . 6 ⊢ (𝑥 = suc 𝑦 → ((𝜏 → 𝜑) ↔ (𝜏 → 𝜃)))
28	25, 27	sbcie 3771	. . . . 5 ⊢ ([suc 𝑦 / 𝑥](𝜏 → 𝜑) ↔ (𝜏 → 𝜃))
29	28	sbcbii 3786	. . . 4 ⊢ ([𝑥 / 𝑦][suc 𝑦 / 𝑥](𝜏 → 𝜑) ↔ [𝑥 / 𝑦](𝜏 → 𝜃))
30		suceq 6387	. . . . 5 ⊢ (𝑥 = 𝑦 → suc 𝑥 = suc 𝑦)
31	30	sbcco2 3756	. . . 4 ⊢ ([𝑥 / 𝑦][suc 𝑦 / 𝑥](𝜏 → 𝜑) ↔ [suc 𝑥 / 𝑥](𝜏 → 𝜑))
32	29, 31	bitr3i 277	. . 3 ⊢ ([𝑥 / 𝑦](𝜏 → 𝜃) ↔ [suc 𝑥 / 𝑥](𝜏 → 𝜑))
33	17, 23, 32	3imtr3g 295	. 2 ⊢ (𝑥 ∈ On → ((𝜏 → 𝜑) → [suc 𝑥 / 𝑥](𝜏 → 𝜑)))
34	19	imbi2d 340	. . . . 5 ⊢ (𝑥 = 𝑦 → ((𝜏 → 𝜑) ↔ (𝜏 → 𝜒)))
35	34	sbralie 3316	. . . 4 ⊢ (∀𝑥 ∈ 𝑦 (𝜏 → 𝜑) ↔ [𝑦 / 𝑥]∀𝑦 ∈ 𝑥 (𝜏 → 𝜒))
36		sbsbc 3733	. . . 4 ⊢ ([𝑦 / 𝑥]∀𝑦 ∈ 𝑥 (𝜏 → 𝜒) ↔ [𝑦 / 𝑥]∀𝑦 ∈ 𝑥 (𝜏 → 𝜒))
37	35, 36	bitr2i 276	. . 3 ⊢ ([𝑦 / 𝑥]∀𝑦 ∈ 𝑥 (𝜏 → 𝜒) ↔ ∀𝑥 ∈ 𝑦 (𝜏 → 𝜑))
38		r19.21v 3163	. . . . . . . 8 ⊢ (∀𝑦 ∈ 𝑥 (𝜏 → 𝜒) ↔ (𝜏 → ∀𝑦 ∈ 𝑥 𝜒))
39		tfinds2.6	. . . . . . . . 9 ⊢ (Lim 𝑥 → (𝜏 → (∀𝑦 ∈ 𝑥 𝜒 → 𝜑)))
40	39	a2d 29	. . . . . . . 8 ⊢ (Lim 𝑥 → ((𝜏 → ∀𝑦 ∈ 𝑥 𝜒) → (𝜏 → 𝜑)))
41	38, 40	biimtrid 242	. . . . . . 7 ⊢ (Lim 𝑥 → (∀𝑦 ∈ 𝑥 (𝜏 → 𝜒) → (𝜏 → 𝜑)))
42	41	sbcth 3744	. . . . . 6 ⊢ (𝑦 ∈ V → [𝑦 / 𝑥](Lim 𝑥 → (∀𝑦 ∈ 𝑥 (𝜏 → 𝜒) → (𝜏 → 𝜑))))
43	42	elv 3435	. . . . 5 ⊢ [𝑦 / 𝑥](Lim 𝑥 → (∀𝑦 ∈ 𝑥 (𝜏 → 𝜒) → (𝜏 → 𝜑)))
44		sbcimg 3778	. . . . . 6 ⊢ (𝑦 ∈ V → ([𝑦 / 𝑥](Lim 𝑥 → (∀𝑦 ∈ 𝑥 (𝜏 → 𝜒) → (𝜏 → 𝜑))) ↔ ([𝑦 / 𝑥]Lim 𝑥 → [𝑦 / 𝑥](∀𝑦 ∈ 𝑥 (𝜏 → 𝜒) → (𝜏 → 𝜑)))))
45	44	elv 3435	. . . . 5 ⊢ ([𝑦 / 𝑥](Lim 𝑥 → (∀𝑦 ∈ 𝑥 (𝜏 → 𝜒) → (𝜏 → 𝜑))) ↔ ([𝑦 / 𝑥]Lim 𝑥 → [𝑦 / 𝑥](∀𝑦 ∈ 𝑥 (𝜏 → 𝜒) → (𝜏 → 𝜑))))
46	43, 45	mpbi 230	. . . 4 ⊢ ([𝑦 / 𝑥]Lim 𝑥 → [𝑦 / 𝑥](∀𝑦 ∈ 𝑥 (𝜏 → 𝜒) → (𝜏 → 𝜑)))
47		limeq 6331	. . . . 5 ⊢ (𝑥 = 𝑦 → (Lim 𝑥 ↔ Lim 𝑦))
48	24, 47	sbcie 3771	. . . 4 ⊢ ([𝑦 / 𝑥]Lim 𝑥 ↔ Lim 𝑦)
49		sbcimg 3778	. . . . 5 ⊢ (𝑦 ∈ V → ([𝑦 / 𝑥](∀𝑦 ∈ 𝑥 (𝜏 → 𝜒) → (𝜏 → 𝜑)) ↔ ([𝑦 / 𝑥]∀𝑦 ∈ 𝑥 (𝜏 → 𝜒) → [𝑦 / 𝑥](𝜏 → 𝜑))))
50	49	elv 3435	. . . 4 ⊢ ([𝑦 / 𝑥](∀𝑦 ∈ 𝑥 (𝜏 → 𝜒) → (𝜏 → 𝜑)) ↔ ([𝑦 / 𝑥]∀𝑦 ∈ 𝑥 (𝜏 → 𝜒) → [𝑦 / 𝑥](𝜏 → 𝜑)))
51	46, 48, 50	3imtr3i 291	. . 3 ⊢ (Lim 𝑦 → ([𝑦 / 𝑥]∀𝑦 ∈ 𝑥 (𝜏 → 𝜒) → [𝑦 / 𝑥](𝜏 → 𝜑)))
52	37, 51	biimtrrid 243	. 2 ⊢ (Lim 𝑦 → (∀𝑥 ∈ 𝑦 (𝜏 → 𝜑) → [𝑦 / 𝑥](𝜏 → 𝜑)))
53	6, 33, 52	tfindes 7809	1 ⊢ (𝑥 ∈ On → (𝜏 → 𝜑))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542  [wsb 2068   ∈ wcel 2114  ∀wral 3052  Vcvv 3430  [wsbc 3729  ∅c0 4274  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-sbc 3730  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:  inar1  10693  grur1a  10737