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 8375

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 6858	. . . 4 ⊢ (𝑦 = suc 𝐵 → (𝐹‘𝑦) = (𝐹‘suc 𝐵))
2		reseq2 5945	. . . . 5 ⊢ (𝑦 = suc 𝐵 → (𝐹 ↾ 𝑦) = (𝐹 ↾ suc 𝐵))
3	2	fveq2d 6862	. . . 4 ⊢ (𝑦 = suc 𝐵 → (𝐺‘(𝐹 ↾ 𝑦)) = (𝐺‘(𝐹 ↾ suc 𝐵)))
4	1, 3	eqeq12d 2745	. . 3 ⊢ (𝑦 = suc 𝐵 → ((𝐹‘𝑦) = (𝐺‘(𝐹 ↾ 𝑦)) ↔ (𝐹‘suc 𝐵) = (𝐺‘(𝐹 ↾ suc 𝐵))))
5		tz7.44.2	. . 3 ⊢ (𝑦 ∈ 𝑋 → (𝐹‘𝑦) = (𝐺‘(𝐹 ↾ 𝑦)))
6	4, 5	vtoclga 3543	. 2 ⊢ (suc 𝐵 ∈ 𝑋 → (𝐹‘suc 𝐵) = (𝐺‘(𝐹 ↾ suc 𝐵)))
7		tz7.44.1	. . 3 ⊢ 𝐺 = (𝑥 ∈ V ↦ if(𝑥 = ∅, 𝐴, if(Lim dom 𝑥, ∪ ran 𝑥, (𝐻‘(𝑥‘∪ dom 𝑥)))))
8		eqeq1 2733	. . . 4 ⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → (𝑥 = ∅ ↔ (𝐹 ↾ suc 𝐵) = ∅))
9		dmeq 5867	. . . . . 6 ⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → dom 𝑥 = dom (𝐹 ↾ suc 𝐵))
10		limeq 6344	. . . . . 6 ⊢ (dom 𝑥 = dom (𝐹 ↾ suc 𝐵) → (Lim dom 𝑥 ↔ Lim dom (𝐹 ↾ suc 𝐵)))
11	9, 10	syl 17	. . . . 5 ⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → (Lim dom 𝑥 ↔ Lim dom (𝐹 ↾ suc 𝐵)))
12		rneq 5900	. . . . . 6 ⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → ran 𝑥 = ran (𝐹 ↾ suc 𝐵))
13	12	unieqd 4884	. . . . 5 ⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → ∪ ran 𝑥 = ∪ ran (𝐹 ↾ suc 𝐵))
14		fveq1 6857	. . . . . . 7 ⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → (𝑥‘∪ dom 𝑥) = ((𝐹 ↾ suc 𝐵)‘∪ dom 𝑥))
15	9	unieqd 4884	. . . . . . . 8 ⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → ∪ dom 𝑥 = ∪ dom (𝐹 ↾ suc 𝐵))
16	15	fveq2d 6862	. . . . . . 7 ⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → ((𝐹 ↾ suc 𝐵)‘∪ dom 𝑥) = ((𝐹 ↾ suc 𝐵)‘∪ dom (𝐹 ↾ suc 𝐵)))
17	14, 16	eqtrd 2764	. . . . . 6 ⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → (𝑥‘∪ dom 𝑥) = ((𝐹 ↾ suc 𝐵)‘∪ dom (𝐹 ↾ suc 𝐵)))
18	17	fveq2d 6862	. . . . 5 ⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → (𝐻‘(𝑥‘∪ dom 𝑥)) = (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom (𝐹 ↾ suc 𝐵))))
19	11, 13, 18	ifbieq12d 4517	. . . 4 ⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → if(Lim dom 𝑥, ∪ ran 𝑥, (𝐻‘(𝑥‘∪ dom 𝑥))) = if(Lim dom (𝐹 ↾ suc 𝐵), ∪ ran (𝐹 ↾ suc 𝐵), (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom (𝐹 ↾ suc 𝐵)))))
20	8, 19	ifbieq2d 4515	. . 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 3543	. . 3 ⊢ (suc 𝐵 ∈ 𝑋 → (𝐹 ↾ suc 𝐵) ∈ V)
24		noel 4301	. . . . . . 7 ⊢ ¬ 𝐵 ∈ ∅
25		dmeq 5867	. . . . . . . . 9 ⊢ ((𝐹 ↾ suc 𝐵) = ∅ → dom (𝐹 ↾ suc 𝐵) = dom ∅)
26		dm0 5884	. . . . . . . . 9 ⊢ dom ∅ = ∅
27	25, 26	eqtrdi 2780	. . . . . . . 8 ⊢ ((𝐹 ↾ suc 𝐵) = ∅ → dom (𝐹 ↾ suc 𝐵) = ∅)
28		tz7.44.5	. . . . . . . . . . . . 13 ⊢ Ord 𝑋
29		ordsson 7759	. . . . . . . . . . . . 13 ⊢ (Ord 𝑋 → 𝑋 ⊆ On)
30	28, 29	ax-mp 5	. . . . . . . . . . . 12 ⊢ 𝑋 ⊆ On
31		ordtr 6346	. . . . . . . . . . . . . 14 ⊢ (Ord 𝑋 → Tr 𝑋)
32	28, 31	ax-mp 5	. . . . . . . . . . . . 13 ⊢ Tr 𝑋
33		trsuc 6421	. . . . . . . . . . . . 13 ⊢ ((Tr 𝑋 ∧ suc 𝐵 ∈ 𝑋) → 𝐵 ∈ 𝑋)
34	32, 33	mpan 690	. . . . . . . . . . . 12 ⊢ (suc 𝐵 ∈ 𝑋 → 𝐵 ∈ 𝑋)
35	30, 34	sselid 3944	. . . . . . . . . . 11 ⊢ (suc 𝐵 ∈ 𝑋 → 𝐵 ∈ On)
36		sucidg 6415	. . . . . . . . . . 11 ⊢ (𝐵 ∈ On → 𝐵 ∈ suc 𝐵)
37	35, 36	syl 17	. . . . . . . . . 10 ⊢ (suc 𝐵 ∈ 𝑋 → 𝐵 ∈ suc 𝐵)
38		dmres 5983	. . . . . . . . . . 11 ⊢ dom (𝐹 ↾ suc 𝐵) = (suc 𝐵 ∩ dom 𝐹)
39		ordelss 6348	. . . . . . . . . . . . . 14 ⊢ ((Ord 𝑋 ∧ suc 𝐵 ∈ 𝑋) → suc 𝐵 ⊆ 𝑋)
40	28, 39	mpan 690	. . . . . . . . . . . . 13 ⊢ (suc 𝐵 ∈ 𝑋 → suc 𝐵 ⊆ 𝑋)
41		tz7.44.4	. . . . . . . . . . . . . 14 ⊢ 𝐹 Fn 𝑋
42	41	fndmi 6622	. . . . . . . . . . . . 13 ⊢ dom 𝐹 = 𝑋
43	40, 42	sseqtrrdi 3988	. . . . . . . . . . . 12 ⊢ (suc 𝐵 ∈ 𝑋 → suc 𝐵 ⊆ dom 𝐹)
44		dfss2 3932	. . . . . . . . . . . 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 4499	. . . . 5 ⊢ (suc 𝐵 ∈ 𝑋 → if((𝐹 ↾ suc 𝐵) = ∅, 𝐴, if(Lim dom (𝐹 ↾ suc 𝐵), ∪ ran (𝐹 ↾ suc 𝐵), (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom (𝐹 ↾ suc 𝐵))))) = if(Lim dom (𝐹 ↾ suc 𝐵), ∪ ran (𝐹 ↾ suc 𝐵), (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom (𝐹 ↾ suc 𝐵)))))
53		nlimsucg 7818	. . . . . . . 8 ⊢ (𝐵 ∈ On → ¬ Lim suc 𝐵)
54	35, 53	syl 17	. . . . . . 7 ⊢ (suc 𝐵 ∈ 𝑋 → ¬ Lim suc 𝐵)
55		limeq 6344	. . . . . . . 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 4499	. . . . 5 ⊢ (suc 𝐵 ∈ 𝑋 → if(Lim dom (𝐹 ↾ suc 𝐵), ∪ ran (𝐹 ↾ suc 𝐵), (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom (𝐹 ↾ suc 𝐵)))) = (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom (𝐹 ↾ suc 𝐵))))
59	46	unieqd 4884	. . . . . . . . 9 ⊢ (suc 𝐵 ∈ 𝑋 → ∪ dom (𝐹 ↾ suc 𝐵) = ∪ suc 𝐵)
60		eloni 6342	. . . . . . . . . 10 ⊢ (𝐵 ∈ On → Ord 𝐵)
61		ordunisuc 7807	. . . . . . . . . 10 ⊢ (Ord 𝐵 → ∪ suc 𝐵 = 𝐵)
62	35, 60, 61	3syl 18	. . . . . . . . 9 ⊢ (suc 𝐵 ∈ 𝑋 → ∪ suc 𝐵 = 𝐵)
63	59, 62	eqtrd 2764	. . . . . . . 8 ⊢ (suc 𝐵 ∈ 𝑋 → ∪ dom (𝐹 ↾ suc 𝐵) = 𝐵)
64	63	fveq2d 6862	. . . . . . 7 ⊢ (suc 𝐵 ∈ 𝑋 → ((𝐹 ↾ suc 𝐵)‘∪ dom (𝐹 ↾ suc 𝐵)) = ((𝐹 ↾ suc 𝐵)‘𝐵))
65	37	fvresd 6878	. . . . . . 7 ⊢ (suc 𝐵 ∈ 𝑋 → ((𝐹 ↾ suc 𝐵)‘𝐵) = (𝐹‘𝐵))
66	64, 65	eqtrd 2764	. . . . . 6 ⊢ (suc 𝐵 ∈ 𝑋 → ((𝐹 ↾ suc 𝐵)‘∪ dom (𝐹 ↾ suc 𝐵)) = (𝐹‘𝐵))
67	66	fveq2d 6862	. . . . 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 6871	. . . 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 6991	. 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 3447 ∩ cin 3913 ⊆ wss 3914 ∅c0 4296 ifcif 4488 ∪ cuni 4871 ↦ cmpt 5188 Tr wtr 5214 dom cdm 5638 ran crn 5639 ↾ cres 5640 Ord word 6331 Oncon0 6332 Lim wlim 6333 suc csuc 6334 Fn wfn 6506 ‘cfv 6511

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 5251 ax-nul 5261 ax-pr 5387 ax-un 7711

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 3406 df-v 3449 df-dif 3917 df-un 3919 df-in 3921 df-ss 3931 df-pss 3934 df-nul 4297 df-if 4489 df-pw 4565 df-sn 4590 df-pr 4592 df-op 4596 df-uni 4872 df-br 5108 df-opab 5170 df-mpt 5189 df-tr 5215 df-id 5533 df-eprel 5538 df-po 5546 df-so 5547 df-fr 5591 df-we 5593 df-xp 5644 df-rel 5645 df-cnv 5646 df-co 5647 df-dm 5648 df-rn 5649 df-res 5650 df-ord 6335 df-on 6336 df-lim 6337 df-suc 6338 df-iota 6464 df-fun 6513 df-fn 6514 df-fv 6519

This theorem is referenced by: rdgsucg 8391

W3C validator