Theorem tz7.44-2 7390

Description: The value of 𝐹 at a successor ordinal. Part 2 of Theorem 7.44 of [TakeutiZaring] p. 49. (Unnecessary distinct variable restrictions were removed by David Abernethy, 19-Jun-2012.) (Contributed by NM, 23-Apr-1995.) (Revised by Mario Carneiro, 14-Nov-2014.)

Hypotheses

Ref	Expression
tz7.44.1	⊢ 𝐺 = (𝑥 ∈ V ↦ if(𝑥 = ∅, 𝐴, if(Lim dom 𝑥, ∪ ran 𝑥, (𝐻‘(𝑥‘∪ dom 𝑥)))))
tz7.44.2	⊢ (𝑦 ∈ 𝑋 → (𝐹‘𝑦) = (𝐺‘(𝐹 ↾ 𝑦)))
tz7.44.3	⊢ (𝑦 ∈ 𝑋 → (𝐹 ↾ 𝑦) ∈ V)
tz7.44.4	⊢ 𝐹 Fn 𝑋
tz7.44.5	⊢ Ord 𝑋

Assertion

Ref	Expression
tz7.44-2	⊢ (suc 𝐵 ∈ 𝑋 → (𝐹‘suc 𝐵) = (𝐻‘(𝐹‘𝐵)))

Distinct variable groups:   𝑥,𝐴   𝑥,𝑦,𝐵   𝑥,𝐹,𝑦   𝑦,𝐺   𝑥,𝐻   𝑦,𝑋

Allowed substitution hints:   𝐴(𝑦)   𝐺(𝑥)   𝐻(𝑦)   𝑋(𝑥)

Proof of Theorem tz7.44-2

Step	Hyp	Ref	Expression
1		fveq2 6103	. . . 4 ⊢ (𝑦 = suc 𝐵 → (𝐹‘𝑦) = (𝐹‘suc 𝐵))
2		reseq2 5312	. . . . 5 ⊢ (𝑦 = suc 𝐵 → (𝐹 ↾ 𝑦) = (𝐹 ↾ suc 𝐵))
3	2	fveq2d 6107	. . . 4 ⊢ (𝑦 = suc 𝐵 → (𝐺‘(𝐹 ↾ 𝑦)) = (𝐺‘(𝐹 ↾ suc 𝐵)))
4	1, 3	eqeq12d 2625	. . 3 ⊢ (𝑦 = suc 𝐵 → ((𝐹‘𝑦) = (𝐺‘(𝐹 ↾ 𝑦)) ↔ (𝐹‘suc 𝐵) = (𝐺‘(𝐹 ↾ suc 𝐵))))
5		tz7.44.2	. . 3 ⊢ (𝑦 ∈ 𝑋 → (𝐹‘𝑦) = (𝐺‘(𝐹 ↾ 𝑦)))
6	4, 5	vtoclga 3245	. 2 ⊢ (suc 𝐵 ∈ 𝑋 → (𝐹‘suc 𝐵) = (𝐺‘(𝐹 ↾ suc 𝐵)))
7	2	eleq1d 2672	. . . 4 ⊢ (𝑦 = suc 𝐵 → ((𝐹 ↾ 𝑦) ∈ V ↔ (𝐹 ↾ suc 𝐵) ∈ V))
8		tz7.44.3	. . . 4 ⊢ (𝑦 ∈ 𝑋 → (𝐹 ↾ 𝑦) ∈ V)
9	7, 8	vtoclga 3245	. . 3 ⊢ (suc 𝐵 ∈ 𝑋 → (𝐹 ↾ suc 𝐵) ∈ V)
10		noel 3878	. . . . . . 7 ⊢ ¬ 𝐵 ∈ ∅
11		dmeq 5246	. . . . . . . . 9 ⊢ ((𝐹 ↾ suc 𝐵) = ∅ → dom (𝐹 ↾ suc 𝐵) = dom ∅)
12		dm0 5260	. . . . . . . . 9 ⊢ dom ∅ = ∅
13	11, 12	syl6eq 2660	. . . . . . . 8 ⊢ ((𝐹 ↾ suc 𝐵) = ∅ → dom (𝐹 ↾ suc 𝐵) = ∅)
14		tz7.44.5	. . . . . . . . . . . . 13 ⊢ Ord 𝑋
15		ordsson 6881	. . . . . . . . . . . . 13 ⊢ (Ord 𝑋 → 𝑋 ⊆ On)
16	14, 15	ax-mp 5	. . . . . . . . . . . 12 ⊢ 𝑋 ⊆ On
17		ordtr 5654	. . . . . . . . . . . . . 14 ⊢ (Ord 𝑋 → Tr 𝑋)
18	14, 17	ax-mp 5	. . . . . . . . . . . . 13 ⊢ Tr 𝑋
19		trsuc 5727	. . . . . . . . . . . . 13 ⊢ ((Tr 𝑋 ∧ suc 𝐵 ∈ 𝑋) → 𝐵 ∈ 𝑋)
20	18, 19	mpan 702	. . . . . . . . . . . 12 ⊢ (suc 𝐵 ∈ 𝑋 → 𝐵 ∈ 𝑋)
21	16, 20	sseldi 3566	. . . . . . . . . . 11 ⊢ (suc 𝐵 ∈ 𝑋 → 𝐵 ∈ On)
22		sucidg 5720	. . . . . . . . . . 11 ⊢ (𝐵 ∈ On → 𝐵 ∈ suc 𝐵)
23	21, 22	syl 17	. . . . . . . . . 10 ⊢ (suc 𝐵 ∈ 𝑋 → 𝐵 ∈ suc 𝐵)
24		dmres 5339	. . . . . . . . . . 11 ⊢ dom (𝐹 ↾ suc 𝐵) = (suc 𝐵 ∩ dom 𝐹)
25		ordelss 5656	. . . . . . . . . . . . . 14 ⊢ ((Ord 𝑋 ∧ suc 𝐵 ∈ 𝑋) → suc 𝐵 ⊆ 𝑋)
26	14, 25	mpan 702	. . . . . . . . . . . . 13 ⊢ (suc 𝐵 ∈ 𝑋 → suc 𝐵 ⊆ 𝑋)
27		tz7.44.4	. . . . . . . . . . . . . 14 ⊢ 𝐹 Fn 𝑋
28		fndm 5904	. . . . . . . . . . . . . 14 ⊢ (𝐹 Fn 𝑋 → dom 𝐹 = 𝑋)
29	27, 28	ax-mp 5	. . . . . . . . . . . . 13 ⊢ dom 𝐹 = 𝑋
30	26, 29	syl6sseqr 3615	. . . . . . . . . . . 12 ⊢ (suc 𝐵 ∈ 𝑋 → suc 𝐵 ⊆ dom 𝐹)
31		df-ss 3554	. . . . . . . . . . . 12 ⊢ (suc 𝐵 ⊆ dom 𝐹 ↔ (suc 𝐵 ∩ dom 𝐹) = suc 𝐵)
32	30, 31	sylib 207	. . . . . . . . . . 11 ⊢ (suc 𝐵 ∈ 𝑋 → (suc 𝐵 ∩ dom 𝐹) = suc 𝐵)
33	24, 32	syl5eq 2656	. . . . . . . . . 10 ⊢ (suc 𝐵 ∈ 𝑋 → dom (𝐹 ↾ suc 𝐵) = suc 𝐵)
34	23, 33	eleqtrrd 2691	. . . . . . . . 9 ⊢ (suc 𝐵 ∈ 𝑋 → 𝐵 ∈ dom (𝐹 ↾ suc 𝐵))
35		eleq2 2677	. . . . . . . . 9 ⊢ (dom (𝐹 ↾ suc 𝐵) = ∅ → (𝐵 ∈ dom (𝐹 ↾ suc 𝐵) ↔ 𝐵 ∈ ∅))
36	34, 35	syl5ibcom 234	. . . . . . . 8 ⊢ (suc 𝐵 ∈ 𝑋 → (dom (𝐹 ↾ suc 𝐵) = ∅ → 𝐵 ∈ ∅))
37	13, 36	syl5 33	. . . . . . 7 ⊢ (suc 𝐵 ∈ 𝑋 → ((𝐹 ↾ suc 𝐵) = ∅ → 𝐵 ∈ ∅))
38	10, 37	mtoi 189	. . . . . 6 ⊢ (suc 𝐵 ∈ 𝑋 → ¬ (𝐹 ↾ suc 𝐵) = ∅)
39	38	iffalsed 4047	. . . . 5 ⊢ (suc 𝐵 ∈ 𝑋 → if((𝐹 ↾ suc 𝐵) = ∅, 𝐴, if(Lim dom (𝐹 ↾ suc 𝐵), ∪ ran (𝐹 ↾ suc 𝐵), (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom (𝐹 ↾ suc 𝐵))))) = if(Lim dom (𝐹 ↾ suc 𝐵), ∪ ran (𝐹 ↾ suc 𝐵), (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom (𝐹 ↾ suc 𝐵)))))
40		nlimsucg 6934	. . . . . . . 8 ⊢ (𝐵 ∈ On → ¬ Lim suc 𝐵)
41	21, 40	syl 17	. . . . . . 7 ⊢ (suc 𝐵 ∈ 𝑋 → ¬ Lim suc 𝐵)
42		limeq 5652	. . . . . . . 8 ⊢ (dom (𝐹 ↾ suc 𝐵) = suc 𝐵 → (Lim dom (𝐹 ↾ suc 𝐵) ↔ Lim suc 𝐵))
43	33, 42	syl 17	. . . . . . 7 ⊢ (suc 𝐵 ∈ 𝑋 → (Lim dom (𝐹 ↾ suc 𝐵) ↔ Lim suc 𝐵))
44	41, 43	mtbird 314	. . . . . 6 ⊢ (suc 𝐵 ∈ 𝑋 → ¬ Lim dom (𝐹 ↾ suc 𝐵))
45	44	iffalsed 4047	. . . . 5 ⊢ (suc 𝐵 ∈ 𝑋 → if(Lim dom (𝐹 ↾ suc 𝐵), ∪ ran (𝐹 ↾ suc 𝐵), (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom (𝐹 ↾ suc 𝐵)))) = (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom (𝐹 ↾ suc 𝐵))))
46	33	unieqd 4382	. . . . . . . . 9 ⊢ (suc 𝐵 ∈ 𝑋 → ∪ dom (𝐹 ↾ suc 𝐵) = ∪ suc 𝐵)
47		eloni 5650	. . . . . . . . . . 11 ⊢ (𝐵 ∈ On → Ord 𝐵)
48		ordunisuc 6924	. . . . . . . . . . 11 ⊢ (Ord 𝐵 → ∪ suc 𝐵 = 𝐵)
49	47, 48	syl 17	. . . . . . . . . 10 ⊢ (𝐵 ∈ On → ∪ suc 𝐵 = 𝐵)
50	21, 49	syl 17	. . . . . . . . 9 ⊢ (suc 𝐵 ∈ 𝑋 → ∪ suc 𝐵 = 𝐵)
51	46, 50	eqtrd 2644	. . . . . . . 8 ⊢ (suc 𝐵 ∈ 𝑋 → ∪ dom (𝐹 ↾ suc 𝐵) = 𝐵)
52	51	fveq2d 6107	. . . . . . 7 ⊢ (suc 𝐵 ∈ 𝑋 → ((𝐹 ↾ suc 𝐵)‘∪ dom (𝐹 ↾ suc 𝐵)) = ((𝐹 ↾ suc 𝐵)‘𝐵))
53		fvres 6117	. . . . . . . 8 ⊢ (𝐵 ∈ suc 𝐵 → ((𝐹 ↾ suc 𝐵)‘𝐵) = (𝐹‘𝐵))
54	23, 53	syl 17	. . . . . . 7 ⊢ (suc 𝐵 ∈ 𝑋 → ((𝐹 ↾ suc 𝐵)‘𝐵) = (𝐹‘𝐵))
55	52, 54	eqtrd 2644	. . . . . 6 ⊢ (suc 𝐵 ∈ 𝑋 → ((𝐹 ↾ suc 𝐵)‘∪ dom (𝐹 ↾ suc 𝐵)) = (𝐹‘𝐵))
56	55	fveq2d 6107	. . . . 5 ⊢ (suc 𝐵 ∈ 𝑋 → (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom (𝐹 ↾ suc 𝐵))) = (𝐻‘(𝐹‘𝐵)))
57	39, 45, 56	3eqtrd 2648	. . . 4 ⊢ (suc 𝐵 ∈ 𝑋 → if((𝐹 ↾ suc 𝐵) = ∅, 𝐴, if(Lim dom (𝐹 ↾ suc 𝐵), ∪ ran (𝐹 ↾ suc 𝐵), (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom (𝐹 ↾ suc 𝐵))))) = (𝐻‘(𝐹‘𝐵)))
58		fvex 6113	. . . 4 ⊢ (𝐻‘(𝐹‘𝐵)) ∈ V
59	57, 58	syl6eqel 2696	. . 3 ⊢ (suc 𝐵 ∈ 𝑋 → if((𝐹 ↾ suc 𝐵) = ∅, 𝐴, if(Lim dom (𝐹 ↾ suc 𝐵), ∪ ran (𝐹 ↾ suc 𝐵), (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom (𝐹 ↾ suc 𝐵))))) ∈ V)
60		eqeq1 2614	. . . . 5 ⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → (𝑥 = ∅ ↔ (𝐹 ↾ suc 𝐵) = ∅))
61		dmeq 5246	. . . . . . 7 ⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → dom 𝑥 = dom (𝐹 ↾ suc 𝐵))
62		limeq 5652	. . . . . . 7 ⊢ (dom 𝑥 = dom (𝐹 ↾ suc 𝐵) → (Lim dom 𝑥 ↔ Lim dom (𝐹 ↾ suc 𝐵)))
63	61, 62	syl 17	. . . . . 6 ⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → (Lim dom 𝑥 ↔ Lim dom (𝐹 ↾ suc 𝐵)))
64		rneq 5272	. . . . . . 7 ⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → ran 𝑥 = ran (𝐹 ↾ suc 𝐵))
65	64	unieqd 4382	. . . . . 6 ⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → ∪ ran 𝑥 = ∪ ran (𝐹 ↾ suc 𝐵))
66		fveq1 6102	. . . . . . . 8 ⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → (𝑥‘∪ dom 𝑥) = ((𝐹 ↾ suc 𝐵)‘∪ dom 𝑥))
67	61	unieqd 4382	. . . . . . . . 9 ⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → ∪ dom 𝑥 = ∪ dom (𝐹 ↾ suc 𝐵))
68	67	fveq2d 6107	. . . . . . . 8 ⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → ((𝐹 ↾ suc 𝐵)‘∪ dom 𝑥) = ((𝐹 ↾ suc 𝐵)‘∪ dom (𝐹 ↾ suc 𝐵)))
69	66, 68	eqtrd 2644	. . . . . . 7 ⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → (𝑥‘∪ dom 𝑥) = ((𝐹 ↾ suc 𝐵)‘∪ dom (𝐹 ↾ suc 𝐵)))
70	69	fveq2d 6107	. . . . . 6 ⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → (𝐻‘(𝑥‘∪ dom 𝑥)) = (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom (𝐹 ↾ suc 𝐵))))
71	63, 65, 70	ifbieq12d 4063	. . . . 5 ⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → if(Lim dom 𝑥, ∪ ran 𝑥, (𝐻‘(𝑥‘∪ dom 𝑥))) = if(Lim dom (𝐹 ↾ suc 𝐵), ∪ ran (𝐹 ↾ suc 𝐵), (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom (𝐹 ↾ suc 𝐵)))))
72	60, 71	ifbieq2d 4061	. . . 4 ⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → if(𝑥 = ∅, 𝐴, if(Lim dom 𝑥, ∪ ran 𝑥, (𝐻‘(𝑥‘∪ dom 𝑥)))) = if((𝐹 ↾ suc 𝐵) = ∅, 𝐴, if(Lim dom (𝐹 ↾ suc 𝐵), ∪ ran (𝐹 ↾ suc 𝐵), (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom (𝐹 ↾ suc 𝐵))))))
73		tz7.44.1	. . . 4 ⊢ 𝐺 = (𝑥 ∈ V ↦ if(𝑥 = ∅, 𝐴, if(Lim dom 𝑥, ∪ ran 𝑥, (𝐻‘(𝑥‘∪ dom 𝑥)))))
74	72, 73	fvmptg 6189	. . 3 ⊢ (((𝐹 ↾ suc 𝐵) ∈ V ∧ if((𝐹 ↾ suc 𝐵) = ∅, 𝐴, if(Lim dom (𝐹 ↾ suc 𝐵), ∪ ran (𝐹 ↾ suc 𝐵), (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom (𝐹 ↾ suc 𝐵))))) ∈ V) → (𝐺‘(𝐹 ↾ suc 𝐵)) = if((𝐹 ↾ suc 𝐵) = ∅, 𝐴, if(Lim dom (𝐹 ↾ suc 𝐵), ∪ ran (𝐹 ↾ suc 𝐵), (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom (𝐹 ↾ suc 𝐵))))))
75	9, 59, 74	syl2anc 691	. 2 ⊢ (suc 𝐵 ∈ 𝑋 → (𝐺‘(𝐹 ↾ suc 𝐵)) = if((𝐹 ↾ suc 𝐵) = ∅, 𝐴, if(Lim dom (𝐹 ↾ suc 𝐵), ∪ ran (𝐹 ↾ suc 𝐵), (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom (𝐹 ↾ suc 𝐵))))))
76	6, 75, 57	3eqtrd 2648	1 ⊢ (suc 𝐵 ∈ 𝑋 → (𝐹‘suc 𝐵) = (𝐻‘(𝐹‘𝐵)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   = wceq 1475   ∈ wcel 1977  Vcvv 3173   ∩ cin 3539   ⊆ wss 3540  ∅c0 3874  ifcif 4036  ∪ cuni 4372   ↦ cmpt 4643  Tr wtr 4680  dom cdm 5038  ran crn 5039   ↾ cres 5040  Ord word 5639  Oncon0 5640  Lim wlim 5641  suc csuc 5642   Fn wfn 5799  ‘cfv 5804

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833  ax-un 6847

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-fv 5812

This theorem is referenced by:  rdgsucg  7406