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 8421

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 6876	. . . 4 ⊢ (𝑦 = suc 𝐵 → (𝐹‘𝑦) = (𝐹‘suc 𝐵))
2		reseq2 5961	. . . . 5 ⊢ (𝑦 = suc 𝐵 → (𝐹 ↾ 𝑦) = (𝐹 ↾ suc 𝐵))
3	2	fveq2d 6880	. . . 4 ⊢ (𝑦 = suc 𝐵 → (𝐺‘(𝐹 ↾ 𝑦)) = (𝐺‘(𝐹 ↾ suc 𝐵)))
4	1, 3	eqeq12d 2751	. . 3 ⊢ (𝑦 = suc 𝐵 → ((𝐹‘𝑦) = (𝐺‘(𝐹 ↾ 𝑦)) ↔ (𝐹‘suc 𝐵) = (𝐺‘(𝐹 ↾ suc 𝐵))))
5		tz7.44.2	. . 3 ⊢ (𝑦 ∈ 𝑋 → (𝐹‘𝑦) = (𝐺‘(𝐹 ↾ 𝑦)))
6	4, 5	vtoclga 3556	. 2 ⊢ (suc 𝐵 ∈ 𝑋 → (𝐹‘suc 𝐵) = (𝐺‘(𝐹 ↾ suc 𝐵)))
7		tz7.44.1	. . 3 ⊢ 𝐺 = (𝑥 ∈ V ↦ if(𝑥 = ∅, 𝐴, if(Lim dom 𝑥, ∪ ran 𝑥, (𝐻‘(𝑥‘∪ dom 𝑥)))))
8		eqeq1 2739	. . . 4 ⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → (𝑥 = ∅ ↔ (𝐹 ↾ suc 𝐵) = ∅))
9		dmeq 5883	. . . . . 6 ⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → dom 𝑥 = dom (𝐹 ↾ suc 𝐵))
10		limeq 6364	. . . . . 6 ⊢ (dom 𝑥 = dom (𝐹 ↾ suc 𝐵) → (Lim dom 𝑥 ↔ Lim dom (𝐹 ↾ suc 𝐵)))
11	9, 10	syl 17	. . . . 5 ⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → (Lim dom 𝑥 ↔ Lim dom (𝐹 ↾ suc 𝐵)))
12		rneq 5916	. . . . . 6 ⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → ran 𝑥 = ran (𝐹 ↾ suc 𝐵))
13	12	unieqd 4896	. . . . 5 ⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → ∪ ran 𝑥 = ∪ ran (𝐹 ↾ suc 𝐵))
14		fveq1 6875	. . . . . . 7 ⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → (𝑥‘∪ dom 𝑥) = ((𝐹 ↾ suc 𝐵)‘∪ dom 𝑥))
15	9	unieqd 4896	. . . . . . . 8 ⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → ∪ dom 𝑥 = ∪ dom (𝐹 ↾ suc 𝐵))
16	15	fveq2d 6880	. . . . . . 7 ⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → ((𝐹 ↾ suc 𝐵)‘∪ dom 𝑥) = ((𝐹 ↾ suc 𝐵)‘∪ dom (𝐹 ↾ suc 𝐵)))
17	14, 16	eqtrd 2770	. . . . . 6 ⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → (𝑥‘∪ dom 𝑥) = ((𝐹 ↾ suc 𝐵)‘∪ dom (𝐹 ↾ suc 𝐵)))
18	17	fveq2d 6880	. . . . 5 ⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → (𝐻‘(𝑥‘∪ dom 𝑥)) = (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom (𝐹 ↾ suc 𝐵))))
19	11, 13, 18	ifbieq12d 4529	. . . 4 ⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → if(Lim dom 𝑥, ∪ ran 𝑥, (𝐻‘(𝑥‘∪ dom 𝑥))) = if(Lim dom (𝐹 ↾ suc 𝐵), ∪ ran (𝐹 ↾ suc 𝐵), (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom (𝐹 ↾ suc 𝐵)))))
20	8, 19	ifbieq2d 4527	. . 3 ⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → if(𝑥 = ∅, 𝐴, if(Lim dom 𝑥, ∪ ran 𝑥, (𝐻‘(𝑥‘∪ dom 𝑥)))) = if((𝐹 ↾ suc 𝐵) = ∅, 𝐴, if(Lim dom (𝐹 ↾ suc 𝐵), ∪ ran (𝐹 ↾ suc 𝐵), (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom (𝐹 ↾ suc 𝐵))))))
21	2	eleq1d 2819	. . . 4 ⊢ (𝑦 = suc 𝐵 → ((𝐹 ↾ 𝑦) ∈ V ↔ (𝐹 ↾ suc 𝐵) ∈ V))
22		tz7.44.3	. . . 4 ⊢ (𝑦 ∈ 𝑋 → (𝐹 ↾ 𝑦) ∈ V)
23	21, 22	vtoclga 3556	. . 3 ⊢ (suc 𝐵 ∈ 𝑋 → (𝐹 ↾ suc 𝐵) ∈ V)
24		noel 4313	. . . . . . 7 ⊢ ¬ 𝐵 ∈ ∅
25		dmeq 5883	. . . . . . . . 9 ⊢ ((𝐹 ↾ suc 𝐵) = ∅ → dom (𝐹 ↾ suc 𝐵) = dom ∅)
26		dm0 5900	. . . . . . . . 9 ⊢ dom ∅ = ∅
27	25, 26	eqtrdi 2786	. . . . . . . 8 ⊢ ((𝐹 ↾ suc 𝐵) = ∅ → dom (𝐹 ↾ suc 𝐵) = ∅)
28		tz7.44.5	. . . . . . . . . . . . 13 ⊢ Ord 𝑋
29		ordsson 7777	. . . . . . . . . . . . 13 ⊢ (Ord 𝑋 → 𝑋 ⊆ On)
30	28, 29	ax-mp 5	. . . . . . . . . . . 12 ⊢ 𝑋 ⊆ On
31		ordtr 6366	. . . . . . . . . . . . . 14 ⊢ (Ord 𝑋 → Tr 𝑋)
32	28, 31	ax-mp 5	. . . . . . . . . . . . 13 ⊢ Tr 𝑋
33		trsuc 6441	. . . . . . . . . . . . 13 ⊢ ((Tr 𝑋 ∧ suc 𝐵 ∈ 𝑋) → 𝐵 ∈ 𝑋)
34	32, 33	mpan 690	. . . . . . . . . . . 12 ⊢ (suc 𝐵 ∈ 𝑋 → 𝐵 ∈ 𝑋)
35	30, 34	sselid 3956	. . . . . . . . . . 11 ⊢ (suc 𝐵 ∈ 𝑋 → 𝐵 ∈ On)
36		sucidg 6435	. . . . . . . . . . 11 ⊢ (𝐵 ∈ On → 𝐵 ∈ suc 𝐵)
37	35, 36	syl 17	. . . . . . . . . 10 ⊢ (suc 𝐵 ∈ 𝑋 → 𝐵 ∈ suc 𝐵)
38		dmres 5999	. . . . . . . . . . 11 ⊢ dom (𝐹 ↾ suc 𝐵) = (suc 𝐵 ∩ dom 𝐹)
39		ordelss 6368	. . . . . . . . . . . . . 14 ⊢ ((Ord 𝑋 ∧ suc 𝐵 ∈ 𝑋) → suc 𝐵 ⊆ 𝑋)
40	28, 39	mpan 690	. . . . . . . . . . . . 13 ⊢ (suc 𝐵 ∈ 𝑋 → suc 𝐵 ⊆ 𝑋)
41		tz7.44.4	. . . . . . . . . . . . . 14 ⊢ 𝐹 Fn 𝑋
42	41	fndmi 6642	. . . . . . . . . . . . 13 ⊢ dom 𝐹 = 𝑋
43	40, 42	sseqtrrdi 4000	. . . . . . . . . . . 12 ⊢ (suc 𝐵 ∈ 𝑋 → suc 𝐵 ⊆ dom 𝐹)
44		dfss2 3944	. . . . . . . . . . . 12 ⊢ (suc 𝐵 ⊆ dom 𝐹 ↔ (suc 𝐵 ∩ dom 𝐹) = suc 𝐵)
45	43, 44	sylib 218	. . . . . . . . . . 11 ⊢ (suc 𝐵 ∈ 𝑋 → (suc 𝐵 ∩ dom 𝐹) = suc 𝐵)
46	38, 45	eqtrid 2782	. . . . . . . . . 10 ⊢ (suc 𝐵 ∈ 𝑋 → dom (𝐹 ↾ suc 𝐵) = suc 𝐵)
47	37, 46	eleqtrrd 2837	. . . . . . . . 9 ⊢ (suc 𝐵 ∈ 𝑋 → 𝐵 ∈ dom (𝐹 ↾ suc 𝐵))
48		eleq2 2823	. . . . . . . . 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 4511	. . . . 5 ⊢ (suc 𝐵 ∈ 𝑋 → if((𝐹 ↾ suc 𝐵) = ∅, 𝐴, if(Lim dom (𝐹 ↾ suc 𝐵), ∪ ran (𝐹 ↾ suc 𝐵), (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom (𝐹 ↾ suc 𝐵))))) = if(Lim dom (𝐹 ↾ suc 𝐵), ∪ ran (𝐹 ↾ suc 𝐵), (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom (𝐹 ↾ suc 𝐵)))))
53		nlimsucg 7837	. . . . . . . 8 ⊢ (𝐵 ∈ On → ¬ Lim suc 𝐵)
54	35, 53	syl 17	. . . . . . 7 ⊢ (suc 𝐵 ∈ 𝑋 → ¬ Lim suc 𝐵)
55		limeq 6364	. . . . . . . 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 4511	. . . . 5 ⊢ (suc 𝐵 ∈ 𝑋 → if(Lim dom (𝐹 ↾ suc 𝐵), ∪ ran (𝐹 ↾ suc 𝐵), (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom (𝐹 ↾ suc 𝐵)))) = (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom (𝐹 ↾ suc 𝐵))))
59	46	unieqd 4896	. . . . . . . . 9 ⊢ (suc 𝐵 ∈ 𝑋 → ∪ dom (𝐹 ↾ suc 𝐵) = ∪ suc 𝐵)
60		eloni 6362	. . . . . . . . . 10 ⊢ (𝐵 ∈ On → Ord 𝐵)
61		ordunisuc 7826	. . . . . . . . . 10 ⊢ (Ord 𝐵 → ∪ suc 𝐵 = 𝐵)
62	35, 60, 61	3syl 18	. . . . . . . . 9 ⊢ (suc 𝐵 ∈ 𝑋 → ∪ suc 𝐵 = 𝐵)
63	59, 62	eqtrd 2770	. . . . . . . 8 ⊢ (suc 𝐵 ∈ 𝑋 → ∪ dom (𝐹 ↾ suc 𝐵) = 𝐵)
64	63	fveq2d 6880	. . . . . . 7 ⊢ (suc 𝐵 ∈ 𝑋 → ((𝐹 ↾ suc 𝐵)‘∪ dom (𝐹 ↾ suc 𝐵)) = ((𝐹 ↾ suc 𝐵)‘𝐵))
65	37	fvresd 6896	. . . . . . 7 ⊢ (suc 𝐵 ∈ 𝑋 → ((𝐹 ↾ suc 𝐵)‘𝐵) = (𝐹‘𝐵))
66	64, 65	eqtrd 2770	. . . . . 6 ⊢ (suc 𝐵 ∈ 𝑋 → ((𝐹 ↾ suc 𝐵)‘∪ dom (𝐹 ↾ suc 𝐵)) = (𝐹‘𝐵))
67	66	fveq2d 6880	. . . . 5 ⊢ (suc 𝐵 ∈ 𝑋 → (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom (𝐹 ↾ suc 𝐵))) = (𝐻‘(𝐹‘𝐵)))
68	52, 58, 67	3eqtrd 2774	. . . 4 ⊢ (suc 𝐵 ∈ 𝑋 → if((𝐹 ↾ suc 𝐵) = ∅, 𝐴, if(Lim dom (𝐹 ↾ suc 𝐵), ∪ ran (𝐹 ↾ suc 𝐵), (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom (𝐹 ↾ suc 𝐵))))) = (𝐻‘(𝐹‘𝐵)))
69		fvex 6889	. . . 4 ⊢ (𝐻‘(𝐹‘𝐵)) ∈ V
70	68, 69	eqeltrdi 2842	. . 3 ⊢ (suc 𝐵 ∈ 𝑋 → if((𝐹 ↾ suc 𝐵) = ∅, 𝐴, if(Lim dom (𝐹 ↾ suc 𝐵), ∪ ran (𝐹 ↾ suc 𝐵), (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom (𝐹 ↾ suc 𝐵))))) ∈ V)
71	7, 20, 23, 70	fvmptd3 7009	. 2 ⊢ (suc 𝐵 ∈ 𝑋 → (𝐺‘(𝐹 ↾ suc 𝐵)) = if((𝐹 ↾ suc 𝐵) = ∅, 𝐴, if(Lim dom (𝐹 ↾ suc 𝐵), ∪ ran (𝐹 ↾ suc 𝐵), (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom (𝐹 ↾ suc 𝐵))))))
72	6, 71, 68	3eqtrd 2774	1 ⊢ (suc 𝐵 ∈ 𝑋 → (𝐹‘suc 𝐵) = (𝐻‘(𝐹‘𝐵)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 = wceq 1540 ∈ wcel 2108 Vcvv 3459 ∩ cin 3925 ⊆ wss 3926 ∅c0 4308 ifcif 4500 ∪ cuni 4883 ↦ cmpt 5201 Tr wtr 5229 dom cdm 5654 ran crn 5655 ↾ cres 5656 Ord word 6351 Oncon0 6352 Lim wlim 6353 suc csuc 6354 Fn wfn 6526 ‘cfv 6531

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 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2707 ax-sep 5266 ax-nul 5276 ax-pr 5402 ax-un 7729

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 2065 df-mo 2539 df-eu 2568 df-clab 2714 df-cleq 2727 df-clel 2809 df-nfc 2885 df-ne 2933 df-ral 3052 df-rex 3061 df-rab 3416 df-v 3461 df-dif 3929 df-un 3931 df-in 3933 df-ss 3943 df-pss 3946 df-nul 4309 df-if 4501 df-pw 4577 df-sn 4602 df-pr 4604 df-op 4608 df-uni 4884 df-br 5120 df-opab 5182 df-mpt 5202 df-tr 5230 df-id 5548 df-eprel 5553 df-po 5561 df-so 5562 df-fr 5606 df-we 5608 df-xp 5660 df-rel 5661 df-cnv 5662 df-co 5663 df-dm 5664 df-rn 5665 df-res 5666 df-ord 6355 df-on 6356 df-lim 6357 df-suc 6358 df-iota 6484 df-fun 6533 df-fn 6534 df-fv 6539

This theorem is referenced by: rdgsucg 8437

W3C validator