Theorem tfindsg 7850

Description: 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. The basis of this version is an arbitrary ordinal 𝐵 instead of zero. Remark in [TakeutiZaring] p. 57. (Contributed by NM, 5-Mar-2004.)

Hypotheses

Ref	Expression
tfindsg.1	⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜓))
tfindsg.2	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))
tfindsg.3	⊢ (𝑥 = suc 𝑦 → (𝜑 ↔ 𝜃))
tfindsg.4	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏))
tfindsg.5	⊢ (𝐵 ∈ On → 𝜓)
tfindsg.6	⊢ (((𝑦 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 ⊆ 𝑦) → (𝜒 → 𝜃))
tfindsg.7	⊢ (((Lim 𝑥 ∧ 𝐵 ∈ On) ∧ 𝐵 ⊆ 𝑥) → (∀𝑦 ∈ 𝑥 (𝐵 ⊆ 𝑦 → 𝜒) → 𝜑))

Assertion

Ref	Expression
tfindsg	⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 ⊆ 𝐴) → 𝜏)

Distinct variable groups:   𝑥,𝐴   𝑥,𝑦,𝐵   𝜒,𝑥   𝜃,𝑥   𝜏,𝑥   𝜑,𝑦

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

Proof of Theorem tfindsg

Step	Hyp	Ref	Expression
1		sseq2 4009	. . . . . . 7 ⊢ (𝑥 = ∅ → (𝐵 ⊆ 𝑥 ↔ 𝐵 ⊆ ∅))
2	1	adantl 483	. . . . . 6 ⊢ ((𝐵 = ∅ ∧ 𝑥 = ∅) → (𝐵 ⊆ 𝑥 ↔ 𝐵 ⊆ ∅))
3		eqeq2 2745	. . . . . . . 8 ⊢ (𝐵 = ∅ → (𝑥 = 𝐵 ↔ 𝑥 = ∅))
4		tfindsg.1	. . . . . . . 8 ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜓))
5	3, 4	syl6bir 254	. . . . . . 7 ⊢ (𝐵 = ∅ → (𝑥 = ∅ → (𝜑 ↔ 𝜓)))
6	5	imp 408	. . . . . 6 ⊢ ((𝐵 = ∅ ∧ 𝑥 = ∅) → (𝜑 ↔ 𝜓))
7	2, 6	imbi12d 345	. . . . 5 ⊢ ((𝐵 = ∅ ∧ 𝑥 = ∅) → ((𝐵 ⊆ 𝑥 → 𝜑) ↔ (𝐵 ⊆ ∅ → 𝜓)))
8	1	imbi1d 342	. . . . . 6 ⊢ (𝑥 = ∅ → ((𝐵 ⊆ 𝑥 → 𝜑) ↔ (𝐵 ⊆ ∅ → 𝜑)))
9		ss0 4399	. . . . . . . . 9 ⊢ (𝐵 ⊆ ∅ → 𝐵 = ∅)
10	9	con3i 154	. . . . . . . 8 ⊢ (¬ 𝐵 = ∅ → ¬ 𝐵 ⊆ ∅)
11	10	pm2.21d 121	. . . . . . 7 ⊢ (¬ 𝐵 = ∅ → (𝐵 ⊆ ∅ → (𝜑 ↔ 𝜓)))
12	11	pm5.74d 273	. . . . . 6 ⊢ (¬ 𝐵 = ∅ → ((𝐵 ⊆ ∅ → 𝜑) ↔ (𝐵 ⊆ ∅ → 𝜓)))
13	8, 12	sylan9bbr 512	. . . . 5 ⊢ ((¬ 𝐵 = ∅ ∧ 𝑥 = ∅) → ((𝐵 ⊆ 𝑥 → 𝜑) ↔ (𝐵 ⊆ ∅ → 𝜓)))
14	7, 13	pm2.61ian 811	. . . 4 ⊢ (𝑥 = ∅ → ((𝐵 ⊆ 𝑥 → 𝜑) ↔ (𝐵 ⊆ ∅ → 𝜓)))
15	14	imbi2d 341	. . 3 ⊢ (𝑥 = ∅ → ((𝐵 ∈ On → (𝐵 ⊆ 𝑥 → 𝜑)) ↔ (𝐵 ∈ On → (𝐵 ⊆ ∅ → 𝜓))))
16		sseq2 4009	. . . . 5 ⊢ (𝑥 = 𝑦 → (𝐵 ⊆ 𝑥 ↔ 𝐵 ⊆ 𝑦))
17		tfindsg.2	. . . . 5 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))
18	16, 17	imbi12d 345	. . . 4 ⊢ (𝑥 = 𝑦 → ((𝐵 ⊆ 𝑥 → 𝜑) ↔ (𝐵 ⊆ 𝑦 → 𝜒)))
19	18	imbi2d 341	. . 3 ⊢ (𝑥 = 𝑦 → ((𝐵 ∈ On → (𝐵 ⊆ 𝑥 → 𝜑)) ↔ (𝐵 ∈ On → (𝐵 ⊆ 𝑦 → 𝜒))))
20		sseq2 4009	. . . . 5 ⊢ (𝑥 = suc 𝑦 → (𝐵 ⊆ 𝑥 ↔ 𝐵 ⊆ suc 𝑦))
21		tfindsg.3	. . . . 5 ⊢ (𝑥 = suc 𝑦 → (𝜑 ↔ 𝜃))
22	20, 21	imbi12d 345	. . . 4 ⊢ (𝑥 = suc 𝑦 → ((𝐵 ⊆ 𝑥 → 𝜑) ↔ (𝐵 ⊆ suc 𝑦 → 𝜃)))
23	22	imbi2d 341	. . 3 ⊢ (𝑥 = suc 𝑦 → ((𝐵 ∈ On → (𝐵 ⊆ 𝑥 → 𝜑)) ↔ (𝐵 ∈ On → (𝐵 ⊆ suc 𝑦 → 𝜃))))
24		sseq2 4009	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝐵 ⊆ 𝑥 ↔ 𝐵 ⊆ 𝐴))
25		tfindsg.4	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏))
26	24, 25	imbi12d 345	. . . 4 ⊢ (𝑥 = 𝐴 → ((𝐵 ⊆ 𝑥 → 𝜑) ↔ (𝐵 ⊆ 𝐴 → 𝜏)))
27	26	imbi2d 341	. . 3 ⊢ (𝑥 = 𝐴 → ((𝐵 ∈ On → (𝐵 ⊆ 𝑥 → 𝜑)) ↔ (𝐵 ∈ On → (𝐵 ⊆ 𝐴 → 𝜏))))
28		tfindsg.5	. . . 4 ⊢ (𝐵 ∈ On → 𝜓)
29	28	a1d 25	. . 3 ⊢ (𝐵 ∈ On → (𝐵 ⊆ ∅ → 𝜓))
30		vex 3479	. . . . . . . . . . . . . 14 ⊢ 𝑦 ∈ V
31	30	sucex 7794	. . . . . . . . . . . . 13 ⊢ suc 𝑦 ∈ V
32	31	eqvinc 3638	. . . . . . . . . . . 12 ⊢ (suc 𝑦 = 𝐵 ↔ ∃𝑥(𝑥 = suc 𝑦 ∧ 𝑥 = 𝐵))
33	28, 4	imbitrrid 245	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝐵 → (𝐵 ∈ On → 𝜑))
34	21	biimpd 228	. . . . . . . . . . . . . 14 ⊢ (𝑥 = suc 𝑦 → (𝜑 → 𝜃))
35	33, 34	sylan9r 510	. . . . . . . . . . . . 13 ⊢ ((𝑥 = suc 𝑦 ∧ 𝑥 = 𝐵) → (𝐵 ∈ On → 𝜃))
36	35	exlimiv 1934	. . . . . . . . . . . 12 ⊢ (∃𝑥(𝑥 = suc 𝑦 ∧ 𝑥 = 𝐵) → (𝐵 ∈ On → 𝜃))
37	32, 36	sylbi 216	. . . . . . . . . . 11 ⊢ (suc 𝑦 = 𝐵 → (𝐵 ∈ On → 𝜃))
38	37	eqcoms 2741	. . . . . . . . . 10 ⊢ (𝐵 = suc 𝑦 → (𝐵 ∈ On → 𝜃))
39	38	imim2i 16	. . . . . . . . 9 ⊢ ((𝐵 ⊆ suc 𝑦 → 𝐵 = suc 𝑦) → (𝐵 ⊆ suc 𝑦 → (𝐵 ∈ On → 𝜃)))
40	39	a1d 25	. . . . . . . 8 ⊢ ((𝐵 ⊆ suc 𝑦 → 𝐵 = suc 𝑦) → ((𝐵 ⊆ 𝑦 → 𝜒) → (𝐵 ⊆ suc 𝑦 → (𝐵 ∈ On → 𝜃))))
41	40	com4r 94	. . . . . . 7 ⊢ (𝐵 ∈ On → ((𝐵 ⊆ suc 𝑦 → 𝐵 = suc 𝑦) → ((𝐵 ⊆ 𝑦 → 𝜒) → (𝐵 ⊆ suc 𝑦 → 𝜃))))
42	41	adantl 483	. . . . . 6 ⊢ ((𝑦 ∈ On ∧ 𝐵 ∈ On) → ((𝐵 ⊆ suc 𝑦 → 𝐵 = suc 𝑦) → ((𝐵 ⊆ 𝑦 → 𝜒) → (𝐵 ⊆ suc 𝑦 → 𝜃))))
43		df-ne 2942	. . . . . . . . 9 ⊢ (𝐵 ≠ suc 𝑦 ↔ ¬ 𝐵 = suc 𝑦)
44	43	anbi2i 624	. . . . . . . 8 ⊢ ((𝐵 ⊆ suc 𝑦 ∧ 𝐵 ≠ suc 𝑦) ↔ (𝐵 ⊆ suc 𝑦 ∧ ¬ 𝐵 = suc 𝑦))
45		annim 405	. . . . . . . 8 ⊢ ((𝐵 ⊆ suc 𝑦 ∧ ¬ 𝐵 = suc 𝑦) ↔ ¬ (𝐵 ⊆ suc 𝑦 → 𝐵 = suc 𝑦))
46	44, 45	bitri 275	. . . . . . 7 ⊢ ((𝐵 ⊆ suc 𝑦 ∧ 𝐵 ≠ suc 𝑦) ↔ ¬ (𝐵 ⊆ suc 𝑦 → 𝐵 = suc 𝑦))
47		onsssuc 6455	. . . . . . . . . 10 ⊢ ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐵 ⊆ 𝑦 ↔ 𝐵 ∈ suc 𝑦))
48		onsuc 7799	. . . . . . . . . . 11 ⊢ (𝑦 ∈ On → suc 𝑦 ∈ On)
49		onelpss 6405	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ On ∧ suc 𝑦 ∈ On) → (𝐵 ∈ suc 𝑦 ↔ (𝐵 ⊆ suc 𝑦 ∧ 𝐵 ≠ suc 𝑦)))
50	48, 49	sylan2 594	. . . . . . . . . 10 ⊢ ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐵 ∈ suc 𝑦 ↔ (𝐵 ⊆ suc 𝑦 ∧ 𝐵 ≠ suc 𝑦)))
51	47, 50	bitrd 279	. . . . . . . . 9 ⊢ ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐵 ⊆ 𝑦 ↔ (𝐵 ⊆ suc 𝑦 ∧ 𝐵 ≠ suc 𝑦)))
52	51	ancoms 460	. . . . . . . 8 ⊢ ((𝑦 ∈ On ∧ 𝐵 ∈ On) → (𝐵 ⊆ 𝑦 ↔ (𝐵 ⊆ suc 𝑦 ∧ 𝐵 ≠ suc 𝑦)))
53		tfindsg.6	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 ⊆ 𝑦) → (𝜒 → 𝜃))
54	53	ex 414	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ On ∧ 𝐵 ∈ On) → (𝐵 ⊆ 𝑦 → (𝜒 → 𝜃)))
55	54	a1ddd 80	. . . . . . . . . 10 ⊢ ((𝑦 ∈ On ∧ 𝐵 ∈ On) → (𝐵 ⊆ 𝑦 → (𝜒 → (𝐵 ⊆ suc 𝑦 → 𝜃))))
56	55	a2d 29	. . . . . . . . 9 ⊢ ((𝑦 ∈ On ∧ 𝐵 ∈ On) → ((𝐵 ⊆ 𝑦 → 𝜒) → (𝐵 ⊆ 𝑦 → (𝐵 ⊆ suc 𝑦 → 𝜃))))
57	56	com23 86	. . . . . . . 8 ⊢ ((𝑦 ∈ On ∧ 𝐵 ∈ On) → (𝐵 ⊆ 𝑦 → ((𝐵 ⊆ 𝑦 → 𝜒) → (𝐵 ⊆ suc 𝑦 → 𝜃))))
58	52, 57	sylbird 260	. . . . . . 7 ⊢ ((𝑦 ∈ On ∧ 𝐵 ∈ On) → ((𝐵 ⊆ suc 𝑦 ∧ 𝐵 ≠ suc 𝑦) → ((𝐵 ⊆ 𝑦 → 𝜒) → (𝐵 ⊆ suc 𝑦 → 𝜃))))
59	46, 58	biimtrrid 242	. . . . . 6 ⊢ ((𝑦 ∈ On ∧ 𝐵 ∈ On) → (¬ (𝐵 ⊆ suc 𝑦 → 𝐵 = suc 𝑦) → ((𝐵 ⊆ 𝑦 → 𝜒) → (𝐵 ⊆ suc 𝑦 → 𝜃))))
60	42, 59	pm2.61d 179	. . . . 5 ⊢ ((𝑦 ∈ On ∧ 𝐵 ∈ On) → ((𝐵 ⊆ 𝑦 → 𝜒) → (𝐵 ⊆ suc 𝑦 → 𝜃)))
61	60	ex 414	. . . 4 ⊢ (𝑦 ∈ On → (𝐵 ∈ On → ((𝐵 ⊆ 𝑦 → 𝜒) → (𝐵 ⊆ suc 𝑦 → 𝜃))))
62	61	a2d 29	. . 3 ⊢ (𝑦 ∈ On → ((𝐵 ∈ On → (𝐵 ⊆ 𝑦 → 𝜒)) → (𝐵 ∈ On → (𝐵 ⊆ suc 𝑦 → 𝜃))))
63		pm2.27 42	. . . . . . . . 9 ⊢ (𝐵 ∈ On → ((𝐵 ∈ On → (𝐵 ⊆ 𝑦 → 𝜒)) → (𝐵 ⊆ 𝑦 → 𝜒)))
64	63	ralimdv 3170	. . . . . . . 8 ⊢ (𝐵 ∈ On → (∀𝑦 ∈ 𝑥 (𝐵 ∈ On → (𝐵 ⊆ 𝑦 → 𝜒)) → ∀𝑦 ∈ 𝑥 (𝐵 ⊆ 𝑦 → 𝜒)))
65	64	ad2antlr 726	. . . . . . 7 ⊢ (((Lim 𝑥 ∧ 𝐵 ∈ On) ∧ 𝐵 ⊆ 𝑥) → (∀𝑦 ∈ 𝑥 (𝐵 ∈ On → (𝐵 ⊆ 𝑦 → 𝜒)) → ∀𝑦 ∈ 𝑥 (𝐵 ⊆ 𝑦 → 𝜒)))
66		tfindsg.7	. . . . . . 7 ⊢ (((Lim 𝑥 ∧ 𝐵 ∈ On) ∧ 𝐵 ⊆ 𝑥) → (∀𝑦 ∈ 𝑥 (𝐵 ⊆ 𝑦 → 𝜒) → 𝜑))
67	65, 66	syld 47	. . . . . 6 ⊢ (((Lim 𝑥 ∧ 𝐵 ∈ On) ∧ 𝐵 ⊆ 𝑥) → (∀𝑦 ∈ 𝑥 (𝐵 ∈ On → (𝐵 ⊆ 𝑦 → 𝜒)) → 𝜑))
68	67	exp31 421	. . . . 5 ⊢ (Lim 𝑥 → (𝐵 ∈ On → (𝐵 ⊆ 𝑥 → (∀𝑦 ∈ 𝑥 (𝐵 ∈ On → (𝐵 ⊆ 𝑦 → 𝜒)) → 𝜑))))
69	68	com3l 89	. . . 4 ⊢ (𝐵 ∈ On → (𝐵 ⊆ 𝑥 → (Lim 𝑥 → (∀𝑦 ∈ 𝑥 (𝐵 ∈ On → (𝐵 ⊆ 𝑦 → 𝜒)) → 𝜑))))
70	69	com4t 93	. . 3 ⊢ (Lim 𝑥 → (∀𝑦 ∈ 𝑥 (𝐵 ∈ On → (𝐵 ⊆ 𝑦 → 𝜒)) → (𝐵 ∈ On → (𝐵 ⊆ 𝑥 → 𝜑))))
71	15, 19, 23, 27, 29, 62, 70	tfinds 7849	. 2 ⊢ (𝐴 ∈ On → (𝐵 ∈ On → (𝐵 ⊆ 𝐴 → 𝜏)))
72	71	imp31 419	1 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 ⊆ 𝐴) → 𝜏)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542  ∃wex 1782   ∈ wcel 2107   ≠ wne 2941  ∀wral 3062   ⊆ wss 3949  ∅c0 4323  Oncon0 6365  Lim wlim 6366  suc csuc 6367

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428  ax-un 7725

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-tr 5267  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371

This theorem is referenced by:  tfindsg2  7851  oaordi  8546  infensuc  9155  r1ordg  9773