tz7.44-2 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > tz7.44-2		Structured version Visualization version GIF version

Theorem tz7.44-2 8329

Description: The value of 𝐹 at a successor ordinal. Part 2 of Theorem 7.44 of [TakeutiZaring] p. 49. (Contributed by NM, 23-Apr-1995.) Remove unnecessary distinct variable conditions. (Revised by David Abernethy, 19-Jun-2012.) (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 6822	. . . 4 ⊢ (𝑦 = suc 𝐵 → (𝐹‘𝑦) = (𝐹‘suc 𝐵))
2		reseq2 5925	. . . . 5 ⊢ (𝑦 = suc 𝐵 → (𝐹 ↾ 𝑦) = (𝐹 ↾ suc 𝐵))
3	2	fveq2d 6826	. . . 4 ⊢ (𝑦 = suc 𝐵 → (𝐺‘(𝐹 ↾ 𝑦)) = (𝐺‘(𝐹 ↾ suc 𝐵)))
4	1, 3	eqeq12d 2745	. . 3 ⊢ (𝑦 = suc 𝐵 → ((𝐹‘𝑦) = (𝐺‘(𝐹 ↾ 𝑦)) ↔ (𝐹‘suc 𝐵) = (𝐺‘(𝐹 ↾ suc 𝐵))))
5		tz7.44.2	. . 3 ⊢ (𝑦 ∈ 𝑋 → (𝐹‘𝑦) = (𝐺‘(𝐹 ↾ 𝑦)))
6	4, 5	vtoclga 3532	. 2 ⊢ (suc 𝐵 ∈ 𝑋 → (𝐹‘suc 𝐵) = (𝐺‘(𝐹 ↾ suc 𝐵)))
7		tz7.44.1	. . 3 ⊢ 𝐺 = (𝑥 ∈ V ↦ if(𝑥 = ∅, 𝐴, if(Lim dom 𝑥, ∪ ran 𝑥, (𝐻‘(𝑥‘∪ dom 𝑥)))))
8		eqeq1 2733	. . . 4 ⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → (𝑥 = ∅ ↔ (𝐹 ↾ suc 𝐵) = ∅))
9		dmeq 5846	. . . . . 6 ⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → dom 𝑥 = dom (𝐹 ↾ suc 𝐵))
10		limeq 6319	. . . . . 6 ⊢ (dom 𝑥 = dom (𝐹 ↾ suc 𝐵) → (Lim dom 𝑥 ↔ Lim dom (𝐹 ↾ suc 𝐵)))
11	9, 10	syl 17	. . . . 5 ⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → (Lim dom 𝑥 ↔ Lim dom (𝐹 ↾ suc 𝐵)))
12		rneq 5878	. . . . . 6 ⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → ran 𝑥 = ran (𝐹 ↾ suc 𝐵))
13	12	unieqd 4871	. . . . 5 ⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → ∪ ran 𝑥 = ∪ ran (𝐹 ↾ suc 𝐵))
14		fveq1 6821	. . . . . . 7 ⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → (𝑥‘∪ dom 𝑥) = ((𝐹 ↾ suc 𝐵)‘∪ dom 𝑥))
15	9	unieqd 4871	. . . . . . . 8 ⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → ∪ dom 𝑥 = ∪ dom (𝐹 ↾ suc 𝐵))
16	15	fveq2d 6826	. . . . . . 7 ⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → ((𝐹 ↾ suc 𝐵)‘∪ dom 𝑥) = ((𝐹 ↾ suc 𝐵)‘∪ dom (𝐹 ↾ suc 𝐵)))
17	14, 16	eqtrd 2764	. . . . . 6 ⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → (𝑥‘∪ dom 𝑥) = ((𝐹 ↾ suc 𝐵)‘∪ dom (𝐹 ↾ suc 𝐵)))
18	17	fveq2d 6826	. . . . 5 ⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → (𝐻‘(𝑥‘∪ dom 𝑥)) = (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom (𝐹 ↾ suc 𝐵))))
19	11, 13, 18	ifbieq12d 4505	. . . 4 ⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → if(Lim dom 𝑥, ∪ ran 𝑥, (𝐻‘(𝑥‘∪ dom 𝑥))) = if(Lim dom (𝐹 ↾ suc 𝐵), ∪ ran (𝐹 ↾ suc 𝐵), (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom (𝐹 ↾ suc 𝐵)))))
20	8, 19	ifbieq2d 4503	. . 3 ⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → if(𝑥 = ∅, 𝐴, if(Lim dom 𝑥, ∪ ran 𝑥, (𝐻‘(𝑥‘∪ dom 𝑥)))) = if((𝐹 ↾ suc 𝐵) = ∅, 𝐴, if(Lim dom (𝐹 ↾ suc 𝐵), ∪ ran (𝐹 ↾ suc 𝐵), (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom (𝐹 ↾ suc 𝐵))))))
21	2	eleq1d 2813	. . . 4 ⊢ (𝑦 = suc 𝐵 → ((𝐹 ↾ 𝑦) ∈ V ↔ (𝐹 ↾ suc 𝐵) ∈ V))
22		tz7.44.3	. . . 4 ⊢ (𝑦 ∈ 𝑋 → (𝐹 ↾ 𝑦) ∈ V)
23	21, 22	vtoclga 3532	. . 3 ⊢ (suc 𝐵 ∈ 𝑋 → (𝐹 ↾ suc 𝐵) ∈ V)
24		noel 4289	. . . . . . 7 ⊢ ¬ 𝐵 ∈ ∅
25		dmeq 5846	. . . . . . . . 9 ⊢ ((𝐹 ↾ suc 𝐵) = ∅ → dom (𝐹 ↾ suc 𝐵) = dom ∅)
26		dm0 5863	. . . . . . . . 9 ⊢ dom ∅ = ∅
27	25, 26	eqtrdi 2780	. . . . . . . 8 ⊢ ((𝐹 ↾ suc 𝐵) = ∅ → dom (𝐹 ↾ suc 𝐵) = ∅)
28		tz7.44.5	. . . . . . . . . . . . 13 ⊢ Ord 𝑋
29		ordsson 7719	. . . . . . . . . . . . 13 ⊢ (Ord 𝑋 → 𝑋 ⊆ On)
30	28, 29	ax-mp 5	. . . . . . . . . . . 12 ⊢ 𝑋 ⊆ On
31		ordtr 6321	. . . . . . . . . . . . . 14 ⊢ (Ord 𝑋 → Tr 𝑋)
32	28, 31	ax-mp 5	. . . . . . . . . . . . 13 ⊢ Tr 𝑋
33		trsuc 6396	. . . . . . . . . . . . 13 ⊢ ((Tr 𝑋 ∧ suc 𝐵 ∈ 𝑋) → 𝐵 ∈ 𝑋)
34	32, 33	mpan 690	. . . . . . . . . . . 12 ⊢ (suc 𝐵 ∈ 𝑋 → 𝐵 ∈ 𝑋)
35	30, 34	sselid 3933	. . . . . . . . . . 11 ⊢ (suc 𝐵 ∈ 𝑋 → 𝐵 ∈ On)
36		sucidg 6390	. . . . . . . . . . 11 ⊢ (𝐵 ∈ On → 𝐵 ∈ suc 𝐵)
37	35, 36	syl 17	. . . . . . . . . 10 ⊢ (suc 𝐵 ∈ 𝑋 → 𝐵 ∈ suc 𝐵)
38		dmres 5963	. . . . . . . . . . 11 ⊢ dom (𝐹 ↾ suc 𝐵) = (suc 𝐵 ∩ dom 𝐹)
39		ordelss 6323	. . . . . . . . . . . . . 14 ⊢ ((Ord 𝑋 ∧ suc 𝐵 ∈ 𝑋) → suc 𝐵 ⊆ 𝑋)
40	28, 39	mpan 690	. . . . . . . . . . . . 13 ⊢ (suc 𝐵 ∈ 𝑋 → suc 𝐵 ⊆ 𝑋)
41		tz7.44.4	. . . . . . . . . . . . . 14 ⊢ 𝐹 Fn 𝑋
42	41	fndmi 6586	. . . . . . . . . . . . 13 ⊢ dom 𝐹 = 𝑋
43	40, 42	sseqtrrdi 3977	. . . . . . . . . . . 12 ⊢ (suc 𝐵 ∈ 𝑋 → suc 𝐵 ⊆ dom 𝐹)
44		dfss2 3921	. . . . . . . . . . . 12 ⊢ (suc 𝐵 ⊆ dom 𝐹 ↔ (suc 𝐵 ∩ dom 𝐹) = suc 𝐵)
45	43, 44	sylib 218	. . . . . . . . . . 11 ⊢ (suc 𝐵 ∈ 𝑋 → (suc 𝐵 ∩ dom 𝐹) = suc 𝐵)
46	38, 45	eqtrid 2776	. . . . . . . . . 10 ⊢ (suc 𝐵 ∈ 𝑋 → dom (𝐹 ↾ suc 𝐵) = suc 𝐵)
47	37, 46	eleqtrrd 2831	. . . . . . . . 9 ⊢ (suc 𝐵 ∈ 𝑋 → 𝐵 ∈ dom (𝐹 ↾ suc 𝐵))
48		eleq2 2817	. . . . . . . . 9 ⊢ (dom (𝐹 ↾ suc 𝐵) = ∅ → (𝐵 ∈ dom (𝐹 ↾ suc 𝐵) ↔ 𝐵 ∈ ∅))
49	47, 48	syl5ibcom 245	. . . . . . . 8 ⊢ (suc 𝐵 ∈ 𝑋 → (dom (𝐹 ↾ suc 𝐵) = ∅ → 𝐵 ∈ ∅))
50	27, 49	syl5 34	. . . . . . 7 ⊢ (suc 𝐵 ∈ 𝑋 → ((𝐹 ↾ suc 𝐵) = ∅ → 𝐵 ∈ ∅))
51	24, 50	mtoi 199	. . . . . 6 ⊢ (suc 𝐵 ∈ 𝑋 → ¬ (𝐹 ↾ suc 𝐵) = ∅)
52	51	iffalsed 4487	. . . . 5 ⊢ (suc 𝐵 ∈ 𝑋 → if((𝐹 ↾ suc 𝐵) = ∅, 𝐴, if(Lim dom (𝐹 ↾ suc 𝐵), ∪ ran (𝐹 ↾ suc 𝐵), (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom (𝐹 ↾ suc 𝐵))))) = if(Lim dom (𝐹 ↾ suc 𝐵), ∪ ran (𝐹 ↾ suc 𝐵), (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom (𝐹 ↾ suc 𝐵)))))
53		nlimsucg 7775	. . . . . . . 8 ⊢ (𝐵 ∈ On → ¬ Lim suc 𝐵)
54	35, 53	syl 17	. . . . . . 7 ⊢ (suc 𝐵 ∈ 𝑋 → ¬ Lim suc 𝐵)
55		limeq 6319	. . . . . . . 8 ⊢ (dom (𝐹 ↾ suc 𝐵) = suc 𝐵 → (Lim dom (𝐹 ↾ suc 𝐵) ↔ Lim suc 𝐵))
56	46, 55	syl 17	. . . . . . 7 ⊢ (suc 𝐵 ∈ 𝑋 → (Lim dom (𝐹 ↾ suc 𝐵) ↔ Lim suc 𝐵))
57	54, 56	mtbird 325	. . . . . 6 ⊢ (suc 𝐵 ∈ 𝑋 → ¬ Lim dom (𝐹 ↾ suc 𝐵))
58	57	iffalsed 4487	. . . . 5 ⊢ (suc 𝐵 ∈ 𝑋 → if(Lim dom (𝐹 ↾ suc 𝐵), ∪ ran (𝐹 ↾ suc 𝐵), (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom (𝐹 ↾ suc 𝐵)))) = (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom (𝐹 ↾ suc 𝐵))))
59	46	unieqd 4871	. . . . . . . . 9 ⊢ (suc 𝐵 ∈ 𝑋 → ∪ dom (𝐹 ↾ suc 𝐵) = ∪ suc 𝐵)
60		eloni 6317	. . . . . . . . . 10 ⊢ (𝐵 ∈ On → Ord 𝐵)
61		ordunisuc 7765	. . . . . . . . . 10 ⊢ (Ord 𝐵 → ∪ suc 𝐵 = 𝐵)
62	35, 60, 61	3syl 18	. . . . . . . . 9 ⊢ (suc 𝐵 ∈ 𝑋 → ∪ suc 𝐵 = 𝐵)
63	59, 62	eqtrd 2764	. . . . . . . 8 ⊢ (suc 𝐵 ∈ 𝑋 → ∪ dom (𝐹 ↾ suc 𝐵) = 𝐵)
64	63	fveq2d 6826	. . . . . . 7 ⊢ (suc 𝐵 ∈ 𝑋 → ((𝐹 ↾ suc 𝐵)‘∪ dom (𝐹 ↾ suc 𝐵)) = ((𝐹 ↾ suc 𝐵)‘𝐵))
65	37	fvresd 6842	. . . . . . 7 ⊢ (suc 𝐵 ∈ 𝑋 → ((𝐹 ↾ suc 𝐵)‘𝐵) = (𝐹‘𝐵))
66	64, 65	eqtrd 2764	. . . . . 6 ⊢ (suc 𝐵 ∈ 𝑋 → ((𝐹 ↾ suc 𝐵)‘∪ dom (𝐹 ↾ suc 𝐵)) = (𝐹‘𝐵))
67	66	fveq2d 6826	. . . . 5 ⊢ (suc 𝐵 ∈ 𝑋 → (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom (𝐹 ↾ suc 𝐵))) = (𝐻‘(𝐹‘𝐵)))
68	52, 58, 67	3eqtrd 2768	. . . 4 ⊢ (suc 𝐵 ∈ 𝑋 → if((𝐹 ↾ suc 𝐵) = ∅, 𝐴, if(Lim dom (𝐹 ↾ suc 𝐵), ∪ ran (𝐹 ↾ suc 𝐵), (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom (𝐹 ↾ suc 𝐵))))) = (𝐻‘(𝐹‘𝐵)))
69		fvex 6835	. . . 4 ⊢ (𝐻‘(𝐹‘𝐵)) ∈ V
70	68, 69	eqeltrdi 2836	. . 3 ⊢ (suc 𝐵 ∈ 𝑋 → if((𝐹 ↾ suc 𝐵) = ∅, 𝐴, if(Lim dom (𝐹 ↾ suc 𝐵), ∪ ran (𝐹 ↾ suc 𝐵), (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom (𝐹 ↾ suc 𝐵))))) ∈ V)
71	7, 20, 23, 70	fvmptd3 6953	. 2 ⊢ (suc 𝐵 ∈ 𝑋 → (𝐺‘(𝐹 ↾ suc 𝐵)) = if((𝐹 ↾ suc 𝐵) = ∅, 𝐴, if(Lim dom (𝐹 ↾ suc 𝐵), ∪ ran (𝐹 ↾ suc 𝐵), (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom (𝐹 ↾ suc 𝐵))))))
72	6, 71, 68	3eqtrd 2768	1 ⊢ (suc 𝐵 ∈ 𝑋 → (𝐹‘suc 𝐵) = (𝐻‘(𝐹‘𝐵)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 = wceq 1540 ∈ wcel 2109 Vcvv 3436 ∩ cin 3902 ⊆ wss 3903 ∅c0 4284 ifcif 4476 ∪ cuni 4858 ↦ cmpt 5173 Tr wtr 5199 dom cdm 5619 ran crn 5620 ↾ cres 5621 Ord word 6306 Oncon0 6307 Lim wlim 6308 suc csuc 6309 Fn wfn 6477 ‘cfv 6482

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-sep 5235 ax-nul 5245 ax-pr 5371 ax-un 7671

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-ral 3045 df-rex 3054 df-rab 3395 df-v 3438 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-pss 3923 df-nul 4285 df-if 4477 df-pw 4553 df-sn 4578 df-pr 4580 df-op 4584 df-uni 4859 df-br 5093 df-opab 5155 df-mpt 5174 df-tr 5200 df-id 5514 df-eprel 5519 df-po 5527 df-so 5528 df-fr 5572 df-we 5574 df-xp 5625 df-rel 5626 df-cnv 5627 df-co 5628 df-dm 5629 df-rn 5630 df-res 5631 df-ord 6310 df-on 6311 df-lim 6312 df-suc 6313 df-iota 6438 df-fun 6484 df-fn 6485 df-fv 6490

This theorem is referenced by: rdgsucg 8345

W3C validator