Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
GIF version

Theorem tz7.44-2 2967

Description: The value of F at a successor ordinal. Part 2 of Theorem 7.44 of [TakeutiZaring] p. 49.

**Hypotheses**
Ref	Expression
tz7.44.1	⊢ G = {⟨x, y⟩∣((x = ∅ ∧ y = A) ∨ (¬ (x = ∅ ∨ Lim dom x) ∧ y = (H ‘(x ‘∪dom x))) ∨ (Lim dom x ∧ y = ∪ran x))}
tz7.44.2	⊢ F Fn On
tz7.44.3	⊢ (x ∈ On → (F ‘x) = (G ‘(F ↾ x)))
tz7.44.5	⊢ B ∈ On

**Assertion**
Ref	Expression
tz7.44-2	⊢ (F ‘suc B) = (H ‘(F ‘B))

Distinct variable group(s): x,y,A x,F x,G y,H x,B,y y,F x,H

**Proof of Theorem tz7.44-2**
Step	Hyp	Ref	Expression
1		tz7.44.5	. . . 4 ⊢ B ∈ On
2	1	onsuc 2353	. . 3 ⊢ suc B ∈ On
3		fveq2 2832	. . . . 5 ⊢ (x = suc B → (F ‘x) = (F ‘suc B))
4		reseq2 2576	. . . . . 6 ⊢ (x = suc B → (F ↾ x) = (F ↾ suc B))
5	4	fveq2d 2836	. . . . 5 ⊢ (x = suc B → (G ‘(F ↾ x)) = (G ‘(F ↾ suc B)))
6	3, 5	cleq12d 1115	. . . 4 ⊢ (x = suc B → ((F ‘x) = (G ‘(F ↾ x)) ↔ (F ‘suc B) = (G ‘(F ↾ suc B))))
7		tz7.44.3	. . . 4 ⊢ (x ∈ On → (F ‘x) = (G ‘(F ↾ x)))
8	6, 7	vtoclga 1387	. . 3 ⊢ (suc B ∈ On → (F ‘suc B) = (G ‘(F ↾ suc B)))
9	2, 8	ax-mp 6	. 2 ⊢ (F ‘suc B) = (G ‘(F ↾ suc B))
10		tz7.44.1	. . . 4 ⊢ G = {⟨x, y⟩∣((x = ∅ ∧ y = A) ∨ (¬ (x = ∅ ∨ Lim dom x) ∧ y = (H ‘(x ‘∪dom x))) ∨ (Lim dom x ∧ y = ∪ran x))}
11	10	tz7.44lem1 2965	. . 3 ⊢ Fun G
12		3mix2 601	. . . . . 6 ⊢ ((¬ (x = ∅ ∨ Lim dom x) ∧ y = (H ‘(x ‘∪dom x))) → ((x = ∅ ∧ y = A) ∨ (¬ (x = ∅ ∨ Lim dom x) ∧ y = (H ‘(x ‘∪dom x))) ∨ (Lim dom x ∧ y = ∪ran x)))
13	12	ssopab2i 2120	. . . . 5 ⊢ {⟨x, y⟩∣(¬ (x = ∅ ∨ Lim dom x) ∧ y = (H ‘(x ‘∪dom x)))} ⊆ {⟨x, y⟩∣((x = ∅ ∧ y = A) ∨ (¬ (x = ∅ ∨ Lim dom x) ∧ y = (H ‘(x ‘∪dom x))) ∨ (Lim dom x ∧ y = ∪ran x))}
14	13, 10	sseqtr4 1533	. . . 4 ⊢ {⟨x, y⟩∣(¬ (x = ∅ ∨ Lim dom x) ∧ y = (H ‘(x ‘∪dom x)))} ⊆ G
15		nsuceq0 2306	. . . . . . . . 9 ⊢ ¬ suc B = ∅
16		tz7.44.2	. . . . . . . . . . . . 13 ⊢ F Fn On
17		fndm 2723	. . . . . . . . . . . . 13 ⊢ (F Fn On → dom F = On)
18	16, 17	ax-mp 6	. . . . . . . . . . . 12 ⊢ dom F = On
19	18	ineq2i 1642	. . . . . . . . . . 11 ⊢ (suc B ∩ dom F) = (suc B ∩ On)
20		dmres 2584	. . . . . . . . . . 11 ⊢ dom (F ↾ suc B) = (suc B ∩ dom F)
21	2	onss 2347	. . . . . . . . . . . 12 ⊢ suc B ⊆ On
22		dfss 1493	. . . . . . . . . . . 12 ⊢ (suc B ⊆ On ↔ suc B = (suc B ∩ On))
23	21, 22	mpbi 164	. . . . . . . . . . 11 ⊢ suc B = (suc B ∩ On)
24	19, 20, 23	3eqtr4 1126	. . . . . . . . . 10 ⊢ dom (F ↾ suc B) = suc B
25	24	cleq1i 1108	. . . . . . . . 9 ⊢ (dom (F ↾ suc B) = ∅ ↔ suc B = ∅)
26	15, 25	mtbir 167	. . . . . . . 8 ⊢ ¬ dom (F ↾ suc B) = ∅
27		dmeq 2531	. . . . . . . . 9 ⊢ ((F ↾ suc B) = ∅ → dom (F ↾ suc B) = dom ∅)
28		dm0 2542	. . . . . . . . 9 ⊢ dom ∅ = ∅
29	27, 28	syl6eq 1140	. . . . . . . 8 ⊢ ((F ↾ suc B) = ∅ → dom (F ↾ suc B) = ∅)
30	26, 29	mto 93	. . . . . . 7 ⊢ ¬ (F ↾ suc B) = ∅
31	1	elisseti 1355	. . . . . . . . 9 ⊢ B ∈ V
32	31	nlimsuc 2363	. . . . . . . 8 ⊢ ¬ Lim suc B
33		limeq 2211	. . . . . . . . 9 ⊢ (dom (F ↾ suc B) = suc B → (Lim dom (F ↾ suc B) ↔ Lim suc B))
34	24, 33	ax-mp 6	. . . . . . . 8 ⊢ (Lim dom (F ↾ suc B) ↔ Lim suc B)
35	32, 34	mtbir 167	. . . . . . 7 ⊢ ¬ Lim dom (F ↾ suc B)
36	30, 35	pm3.2ni 440	. . . . . 6 ⊢ ¬ ((F ↾ suc B) = ∅ ∨ Lim dom (F ↾ suc B))
37	31	sucid 2304	. . . . . . . . 9 ⊢ B ∈ suc B
38		fvres 2840	. . . . . . . . 9 ⊢ (B ∈ suc B → ((F ↾ suc B) ‘B) = (F ‘B))
39	37, 38	ax-mp 6	. . . . . . . 8 ⊢ ((F ↾ suc B) ‘B) = (F ‘B)
40	24	unieqi 1928	. . . . . . . . . 10 ⊢ ∪dom (F ↾ suc B) = ∪suc B
41	1	onunisuc 2354	. . . . . . . . . 10 ⊢ ∪suc B = B
42	40, 41	eqtr2 1120	. . . . . . . . 9 ⊢ B = ∪dom (F ↾ suc B)
43	42	fveq2i 2835	. . . . . . . 8 ⊢ ((F ↾ suc B) ‘B) = ((F ↾ suc B) ‘∪dom (F ↾ suc B))
44	39, 43	eqtr3 1121	. . . . . . 7 ⊢ (F ‘B) = ((F ↾ suc B) ‘∪dom (F ↾ suc B))
45	44	fveq2i 2835	. . . . . 6 ⊢ (H ‘(F ‘B)) = (H ‘((F ↾ suc B) ‘∪dom (F ↾ suc B)))
46	36, 45	pm3.2i 234	. . . . 5 ⊢ (¬ ((F ↾ suc B) = ∅ ∨ Lim dom (F ↾ suc B)) ∧ (H ‘(F ‘B)) = (H ‘((F ↾ suc B) ‘∪dom (F ↾ suc B))))
47		fnfun 2721	. . . . . . . 8 ⊢ (F Fn On → Fun F)
48	16, 47	ax-mp 6	. . . . . . 7 ⊢ Fun F
49		resfunexg 2717	. . . . . . 7 ⊢ (suc B ∈ On → (Fun F → (F ↾ suc B) ∈ V))
50	2, 48, 49	mp2 43	. . . . . 6 ⊢ (F ↾ suc B) ∈ V
51		fvex 2838	. . . . . 6 ⊢ (H ‘(F ‘B)) ∈ V
52		cleq1 1107	. . . . . . . . 9 ⊢ (x = (F ↾ suc B) → (x = ∅ ↔ (F ↾ suc B) = ∅))
53		dmeq 2531	. . . . . . . . . 10 ⊢ (x = (F ↾ suc B) → dom x = dom (F ↾ suc B))
54		limeq 2211	. . . . . . . . . 10 ⊢ (dom x = dom (F ↾ suc B) → (Lim dom x ↔ Lim dom (F ↾ suc B)))
55	53, 54	syl 12	. . . . . . . . 9 ⊢ (x = (F ↾ suc B) → (Lim dom x ↔ Lim dom (F ↾ suc B)))
56	52, 55	orbi12d 475	. . . . . . . 8 ⊢ (x = (F ↾ suc B) → ((x = ∅ ∨ Lim dom x) ↔ ((F ↾ suc B) = ∅ ∨ Lim dom (F ↾ suc B))))
57	56	negbid 463	. . . . . . 7 ⊢ (x = (F ↾ suc B) → (¬ (x = ∅ ∨ Lim dom x) ↔ ¬ ((F ↾ suc B) = ∅ ∨ Lim dom (F ↾ suc B))))
58		unieq 1927	. . . . . . . . . . 11 ⊢ (dom x = dom (F ↾ suc B) → ∪dom x = ∪dom (F ↾ suc B))
59		fveq2 2832	. . . . . . . . . . 11 ⊢ (∪dom x = ∪dom (F ↾ suc B) → (x ‘∪dom x) = (x ‘∪dom (F ↾ suc B)))
60	53, 58, 59	3syl 21	. . . . . . . . . 10 ⊢ (x = (F ↾ suc B) → (x ‘∪dom x) = (x ‘∪dom (F ↾ suc B)))
61		fveq1 2831	. . . . . . . . . 10 ⊢ (x = (F ↾ suc B) → (x ‘∪dom (F ↾ suc B)) = ((F ↾ suc B) ‘∪dom (F ↾ suc B)))
62	60, 61	eqtrd 1128	. . . . . . . . 9 ⊢ (x = (F ↾ suc B) → (x ‘∪dom x) = ((F ↾ suc B) ‘∪dom (F ↾ suc B)))
63	62	fveq2d 2836	. . . . . . . 8 ⊢ (x = (F ↾ suc B) → (H ‘(x ‘∪dom x)) = (H ‘((F ↾ suc B) ‘∪dom (F ↾ suc B))))
64	63	cleq2d 1112	. . . . . . 7 ⊢ (x = (F ↾ suc B) → (y = (H ‘(x ‘∪dom x)) ↔ y = (H ‘((F ↾ suc B) ‘∪dom (F ↾ suc B)))))
65	57, 64	anbi12d 476	. . . . . 6 ⊢ (x = (F ↾ suc B) → ((¬ (x = ∅ ∨ Lim dom x) ∧ y = (H ‘(x ‘∪dom x))) ↔ (¬ ((F ↾ suc B) = ∅ ∨ Lim dom (F ↾ suc B)) ∧ y = (H ‘((F ↾ suc B) ‘∪dom (F ↾ suc B))))))
66		cleq1 1107	. . . . . . 7 ⊢ (y = (H ‘(F ‘B)) → (y = (H ‘((F ↾ suc B) ‘∪dom (F ↾ suc B))) ↔ (H ‘(F ‘B)) = (H ‘((F ↾ suc B) ‘∪dom (F ↾ suc B)))))
67	66	anbi2d 468	. . . . . 6 ⊢ (y = (H ‘(F ‘B)) → ((¬ ((F ↾ suc B) = ∅ ∨ Lim dom (F ↾ suc B)) ∧ y = (H ‘((F ↾ suc B) ‘∪dom (F ↾ suc B)))) ↔ (¬ ((F ↾ suc B) = ∅ ∨ Lim dom (F ↾ suc B)) ∧ (H ‘(F ‘B)) = (H ‘((F ↾ suc B) ‘∪dom (F ↾ suc B))))))
68	50, 51, 65, 67	opelopab 2117	. . . . 5 ⊢ (⟨(F ↾ suc B), (H ‘(F ‘B))⟩ ∈ {⟨x, y⟩∣(¬ (x = ∅ ∨ Lim dom x) ∧ y = (H ‘(x ‘∪dom x)))} ↔ (¬ ((F ↾ suc B) = ∅ ∨ Lim dom (F ↾ suc B)) ∧ (H ‘(F ‘B)) = (H ‘((F ↾ suc B) ‘∪dom (F ↾ suc B)))))
69	46, 68	mpbir 165	. . . 4 ⊢ ⟨(F ↾ suc B), (H ‘(F ‘B))⟩ ∈ {⟨x, y⟩∣(¬ (x = ∅ ∨ Lim dom x) ∧ y = (H ‘(x ‘∪dom x)))}
70	14, 69	sselii 1505	. . 3 ⊢ ⟨(F ↾ suc B), (H ‘(F ‘B))⟩ ∈ G
71	51	funfvopi 2853	. . 3 ⊢ (Fun G → (⟨(F ↾ suc B), (H ‘(F ‘B))⟩ ∈ G → (G ‘(F ↾ suc B)) = (H ‘(F ‘B))))
72	11, 70, 71	mp2 43	. 2 ⊢ (G ‘(F ↾ suc B)) = (H ‘(F ‘B))
73	9, 72	eqtr 1119	1 ⊢ (F ‘suc B) = (H ‘(F ‘B))

Colors of variables: wff set class

Syntax hints: ¬ wn 1 → wi 2 ↔ wb 127 ∨ wo 195 ∧ wa 196 ∨ w3o 580 = wceq 1091 ∈ wcel 1092 Vcvv 1348 ∩ cin 1486 ⊆ wss 1487 ∅c0 1707 ⟨cop 1810 ∪cuni 1919 {copab 2055 Oncon0 2199 Lim wlim 2200 suc csuc 2201 dom cdm 2410 ran crn 2411 ↾ cres 2412 Fun wfun 2416 Fn wfn 2417 ‘cfv 2422

This theorem is referenced by: rdgsuc 2980

This theorem was proved from axioms: ax-1 3 ax-2 4 ax-3 5 ax-mp 6 ax-4 673 ax-5 674 ax-6 675 ax-7 676 ax-gen 677 ax-8 798 ax-9 799 ax-10 800 ax-11 801 ax-12 802 ax-13 804 ax-14 805 ax-16 922 ax-17 925 ax-ext 1074 ax-rep 1075 ax-un 1076 ax-pow 1077

This theorem depends on definitions: df-bi 128 df-or 197 df-an 198 df-3or 582 df-3an 583 df-ex 679 df-sb 853 df-eu 1009 df-mo 1010 df-clab 1093 df-cleq 1097 df-clel 1099 df-ral 1205 df-rex 1206 df-v 1349 df-dif 1489 df-un 1490 df-in 1491 df-ss 1492 df-nul 1708 df-pw 1799 df-sn 1811 df-pr 1812 df-tp 1814 df-op 1815 df-uni 1920 df-tr 2042 df-br 2063 df-opab 2098 df-eprel 2122 df-id 2125 df-po 2128 df-so 2138 df-fr 2169 df-we 2186 df-ord 2202 df-on 2203 df-lim 2204 df-suc 2205 df-xp 2424 df-rel 2425 df-cnv 2426 df-co 2427 df-dm 2428 df-rn 2429 df-res 2430 df-ima 2431 df-fun 2432 df-fn 2433 df-fv 2438

metamath.org