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 8340

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 6835	. . . 4 ⊢ (𝑦 = suc 𝐵 → (𝐹‘𝑦) = (𝐹‘suc 𝐵))
2		reseq2 5934	. . . . 5 ⊢ (𝑦 = suc 𝐵 → (𝐹 ↾ 𝑦) = (𝐹 ↾ suc 𝐵))
3	2	fveq2d 6839	. . . 4 ⊢ (𝑦 = suc 𝐵 → (𝐺‘(𝐹 ↾ 𝑦)) = (𝐺‘(𝐹 ↾ suc 𝐵)))
4	1, 3	eqeq12d 2753	. . 3 ⊢ (𝑦 = suc 𝐵 → ((𝐹‘𝑦) = (𝐺‘(𝐹 ↾ 𝑦)) ↔ (𝐹‘suc 𝐵) = (𝐺‘(𝐹 ↾ suc 𝐵))))
5		tz7.44.2	. . 3 ⊢ (𝑦 ∈ 𝑋 → (𝐹‘𝑦) = (𝐺‘(𝐹 ↾ 𝑦)))
6	4, 5	vtoclga 3533	. 2 ⊢ (suc 𝐵 ∈ 𝑋 → (𝐹‘suc 𝐵) = (𝐺‘(𝐹 ↾ suc 𝐵)))
7		tz7.44.1	. . 3 ⊢ 𝐺 = (𝑥 ∈ V ↦ if(𝑥 = ∅, 𝐴, if(Lim dom 𝑥, ∪ ran 𝑥, (𝐻‘(𝑥‘∪ dom 𝑥)))))
8		eqeq1 2741	. . . 4 ⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → (𝑥 = ∅ ↔ (𝐹 ↾ suc 𝐵) = ∅))
9		dmeq 5853	. . . . . 6 ⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → dom 𝑥 = dom (𝐹 ↾ suc 𝐵))
10		limeq 6330	. . . . . 6 ⊢ (dom 𝑥 = dom (𝐹 ↾ suc 𝐵) → (Lim dom 𝑥 ↔ Lim dom (𝐹 ↾ suc 𝐵)))
11	9, 10	syl 17	. . . . 5 ⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → (Lim dom 𝑥 ↔ Lim dom (𝐹 ↾ suc 𝐵)))
12		rneq 5886	. . . . . 6 ⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → ran 𝑥 = ran (𝐹 ↾ suc 𝐵))
13	12	unieqd 4877	. . . . 5 ⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → ∪ ran 𝑥 = ∪ ran (𝐹 ↾ suc 𝐵))
14		fveq1 6834	. . . . . . 7 ⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → (𝑥‘∪ dom 𝑥) = ((𝐹 ↾ suc 𝐵)‘∪ dom 𝑥))
15	9	unieqd 4877	. . . . . . . 8 ⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → ∪ dom 𝑥 = ∪ dom (𝐹 ↾ suc 𝐵))
16	15	fveq2d 6839	. . . . . . 7 ⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → ((𝐹 ↾ suc 𝐵)‘∪ dom 𝑥) = ((𝐹 ↾ suc 𝐵)‘∪ dom (𝐹 ↾ suc 𝐵)))
17	14, 16	eqtrd 2772	. . . . . 6 ⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → (𝑥‘∪ dom 𝑥) = ((𝐹 ↾ suc 𝐵)‘∪ dom (𝐹 ↾ suc 𝐵)))
18	17	fveq2d 6839	. . . . 5 ⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → (𝐻‘(𝑥‘∪ dom 𝑥)) = (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom (𝐹 ↾ suc 𝐵))))
19	11, 13, 18	ifbieq12d 4509	. . . 4 ⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → if(Lim dom 𝑥, ∪ ran 𝑥, (𝐻‘(𝑥‘∪ dom 𝑥))) = if(Lim dom (𝐹 ↾ suc 𝐵), ∪ ran (𝐹 ↾ suc 𝐵), (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom (𝐹 ↾ suc 𝐵)))))
20	8, 19	ifbieq2d 4507	. . 3 ⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → if(𝑥 = ∅, 𝐴, if(Lim dom 𝑥, ∪ ran 𝑥, (𝐻‘(𝑥‘∪ dom 𝑥)))) = if((𝐹 ↾ suc 𝐵) = ∅, 𝐴, if(Lim dom (𝐹 ↾ suc 𝐵), ∪ ran (𝐹 ↾ suc 𝐵), (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom (𝐹 ↾ suc 𝐵))))))
21	2	eleq1d 2822	. . . 4 ⊢ (𝑦 = suc 𝐵 → ((𝐹 ↾ 𝑦) ∈ V ↔ (𝐹 ↾ suc 𝐵) ∈ V))
22		tz7.44.3	. . . 4 ⊢ (𝑦 ∈ 𝑋 → (𝐹 ↾ 𝑦) ∈ V)
23	21, 22	vtoclga 3533	. . 3 ⊢ (suc 𝐵 ∈ 𝑋 → (𝐹 ↾ suc 𝐵) ∈ V)
24		noel 4291	. . . . . . 7 ⊢ ¬ 𝐵 ∈ ∅
25		dmeq 5853	. . . . . . . . 9 ⊢ ((𝐹 ↾ suc 𝐵) = ∅ → dom (𝐹 ↾ suc 𝐵) = dom ∅)
26		dm0 5870	. . . . . . . . 9 ⊢ dom ∅ = ∅
27	25, 26	eqtrdi 2788	. . . . . . . 8 ⊢ ((𝐹 ↾ suc 𝐵) = ∅ → dom (𝐹 ↾ suc 𝐵) = ∅)
28		tz7.44.5	. . . . . . . . . . . . 13 ⊢ Ord 𝑋
29		ordsson 7730	. . . . . . . . . . . . 13 ⊢ (Ord 𝑋 → 𝑋 ⊆ On)
30	28, 29	ax-mp 5	. . . . . . . . . . . 12 ⊢ 𝑋 ⊆ On
31		ordtr 6332	. . . . . . . . . . . . . 14 ⊢ (Ord 𝑋 → Tr 𝑋)
32	28, 31	ax-mp 5	. . . . . . . . . . . . 13 ⊢ Tr 𝑋
33		trsuc 6407	. . . . . . . . . . . . 13 ⊢ ((Tr 𝑋 ∧ suc 𝐵 ∈ 𝑋) → 𝐵 ∈ 𝑋)
34	32, 33	mpan 691	. . . . . . . . . . . 12 ⊢ (suc 𝐵 ∈ 𝑋 → 𝐵 ∈ 𝑋)
35	30, 34	sselid 3932	. . . . . . . . . . 11 ⊢ (suc 𝐵 ∈ 𝑋 → 𝐵 ∈ On)
36		sucidg 6401	. . . . . . . . . . 11 ⊢ (𝐵 ∈ On → 𝐵 ∈ suc 𝐵)
37	35, 36	syl 17	. . . . . . . . . 10 ⊢ (suc 𝐵 ∈ 𝑋 → 𝐵 ∈ suc 𝐵)
38		dmres 5972	. . . . . . . . . . 11 ⊢ dom (𝐹 ↾ suc 𝐵) = (suc 𝐵 ∩ dom 𝐹)
39		ordelss 6334	. . . . . . . . . . . . . 14 ⊢ ((Ord 𝑋 ∧ suc 𝐵 ∈ 𝑋) → suc 𝐵 ⊆ 𝑋)
40	28, 39	mpan 691	. . . . . . . . . . . . 13 ⊢ (suc 𝐵 ∈ 𝑋 → suc 𝐵 ⊆ 𝑋)
41		tz7.44.4	. . . . . . . . . . . . . 14 ⊢ 𝐹 Fn 𝑋
42	41	fndmi 6597	. . . . . . . . . . . . 13 ⊢ dom 𝐹 = 𝑋
43	40, 42	sseqtrrdi 3976	. . . . . . . . . . . 12 ⊢ (suc 𝐵 ∈ 𝑋 → suc 𝐵 ⊆ dom 𝐹)
44		dfss2 3920	. . . . . . . . . . . 12 ⊢ (suc 𝐵 ⊆ dom 𝐹 ↔ (suc 𝐵 ∩ dom 𝐹) = suc 𝐵)
45	43, 44	sylib 218	. . . . . . . . . . 11 ⊢ (suc 𝐵 ∈ 𝑋 → (suc 𝐵 ∩ dom 𝐹) = suc 𝐵)
46	38, 45	eqtrid 2784	. . . . . . . . . 10 ⊢ (suc 𝐵 ∈ 𝑋 → dom (𝐹 ↾ suc 𝐵) = suc 𝐵)
47	37, 46	eleqtrrd 2840	. . . . . . . . 9 ⊢ (suc 𝐵 ∈ 𝑋 → 𝐵 ∈ dom (𝐹 ↾ suc 𝐵))
48		eleq2 2826	. . . . . . . . 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 4491	. . . . 5 ⊢ (suc 𝐵 ∈ 𝑋 → if((𝐹 ↾ suc 𝐵) = ∅, 𝐴, if(Lim dom (𝐹 ↾ suc 𝐵), ∪ ran (𝐹 ↾ suc 𝐵), (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom (𝐹 ↾ suc 𝐵))))) = if(Lim dom (𝐹 ↾ suc 𝐵), ∪ ran (𝐹 ↾ suc 𝐵), (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom (𝐹 ↾ suc 𝐵)))))
53		nlimsucg 7786	. . . . . . . 8 ⊢ (𝐵 ∈ On → ¬ Lim suc 𝐵)
54	35, 53	syl 17	. . . . . . 7 ⊢ (suc 𝐵 ∈ 𝑋 → ¬ Lim suc 𝐵)
55		limeq 6330	. . . . . . . 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 4491	. . . . 5 ⊢ (suc 𝐵 ∈ 𝑋 → if(Lim dom (𝐹 ↾ suc 𝐵), ∪ ran (𝐹 ↾ suc 𝐵), (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom (𝐹 ↾ suc 𝐵)))) = (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom (𝐹 ↾ suc 𝐵))))
59	46	unieqd 4877	. . . . . . . . 9 ⊢ (suc 𝐵 ∈ 𝑋 → ∪ dom (𝐹 ↾ suc 𝐵) = ∪ suc 𝐵)
60		eloni 6328	. . . . . . . . . 10 ⊢ (𝐵 ∈ On → Ord 𝐵)
61		ordunisuc 7776	. . . . . . . . . 10 ⊢ (Ord 𝐵 → ∪ suc 𝐵 = 𝐵)
62	35, 60, 61	3syl 18	. . . . . . . . 9 ⊢ (suc 𝐵 ∈ 𝑋 → ∪ suc 𝐵 = 𝐵)
63	59, 62	eqtrd 2772	. . . . . . . 8 ⊢ (suc 𝐵 ∈ 𝑋 → ∪ dom (𝐹 ↾ suc 𝐵) = 𝐵)
64	63	fveq2d 6839	. . . . . . 7 ⊢ (suc 𝐵 ∈ 𝑋 → ((𝐹 ↾ suc 𝐵)‘∪ dom (𝐹 ↾ suc 𝐵)) = ((𝐹 ↾ suc 𝐵)‘𝐵))
65	37	fvresd 6855	. . . . . . 7 ⊢ (suc 𝐵 ∈ 𝑋 → ((𝐹 ↾ suc 𝐵)‘𝐵) = (𝐹‘𝐵))
66	64, 65	eqtrd 2772	. . . . . 6 ⊢ (suc 𝐵 ∈ 𝑋 → ((𝐹 ↾ suc 𝐵)‘∪ dom (𝐹 ↾ suc 𝐵)) = (𝐹‘𝐵))
67	66	fveq2d 6839	. . . . 5 ⊢ (suc 𝐵 ∈ 𝑋 → (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom (𝐹 ↾ suc 𝐵))) = (𝐻‘(𝐹‘𝐵)))
68	52, 58, 67	3eqtrd 2776	. . . 4 ⊢ (suc 𝐵 ∈ 𝑋 → if((𝐹 ↾ suc 𝐵) = ∅, 𝐴, if(Lim dom (𝐹 ↾ suc 𝐵), ∪ ran (𝐹 ↾ suc 𝐵), (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom (𝐹 ↾ suc 𝐵))))) = (𝐻‘(𝐹‘𝐵)))
69		fvex 6848	. . . 4 ⊢ (𝐻‘(𝐹‘𝐵)) ∈ V
70	68, 69	eqeltrdi 2845	. . 3 ⊢ (suc 𝐵 ∈ 𝑋 → if((𝐹 ↾ suc 𝐵) = ∅, 𝐴, if(Lim dom (𝐹 ↾ suc 𝐵), ∪ ran (𝐹 ↾ suc 𝐵), (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom (𝐹 ↾ suc 𝐵))))) ∈ V)
71	7, 20, 23, 70	fvmptd3 6966	. 2 ⊢ (suc 𝐵 ∈ 𝑋 → (𝐺‘(𝐹 ↾ suc 𝐵)) = if((𝐹 ↾ suc 𝐵) = ∅, 𝐴, if(Lim dom (𝐹 ↾ suc 𝐵), ∪ ran (𝐹 ↾ suc 𝐵), (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom (𝐹 ↾ suc 𝐵))))))
72	6, 71, 68	3eqtrd 2776	1 ⊢ (suc 𝐵 ∈ 𝑋 → (𝐹‘suc 𝐵) = (𝐻‘(𝐹‘𝐵)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 = wceq 1542 ∈ wcel 2114 Vcvv 3441 ∩ cin 3901 ⊆ wss 3902 ∅c0 4286 ifcif 4480 ∪ cuni 4864 ↦ cmpt 5180 Tr wtr 5206 dom cdm 5625 ran crn 5626 ↾ cres 5627 Ord word 6317 Oncon0 6318 Lim wlim 6319 suc csuc 6320 Fn wfn 6488 ‘cfv 6493

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-sep 5242 ax-nul 5252 ax-pr 5378 ax-un 7682

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-ral 3053 df-rex 3062 df-rab 3401 df-v 3443 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4287 df-if 4481 df-pw 4557 df-sn 4582 df-pr 4584 df-op 4588 df-uni 4865 df-br 5100 df-opab 5162 df-mpt 5181 df-tr 5207 df-id 5520 df-eprel 5525 df-po 5533 df-so 5534 df-fr 5578 df-we 5580 df-xp 5631 df-rel 5632 df-cnv 5633 df-co 5634 df-dm 5635 df-rn 5636 df-res 5637 df-ord 6321 df-on 6322 df-lim 6323 df-suc 6324 df-iota 6449 df-fun 6495 df-fn 6496 df-fv 6501

This theorem is referenced by: rdgsucg 8356

W3C validator