tfrlem9 - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
GIF version

Theorem tfrlem9 3933

Description: Lemma for transfinite recursion. Here we compute the value of F (the union of all acceptable functions).

**Hypotheses**
Ref	Expression
tfrlem.1	⊢ A = {f∣∃x ∈ On (f Fn x ⋀ ∀y ∈ x (f ‘y) = (G ‘(f ↾ y)))}
tfrlem.2	⊢ F = ∪A

**Assertion**
Ref	Expression
tfrlem9	⊢ (y ∈ dom F → (F ‘y) = (G ‘(F ↾ y)))

Distinct variable groups: x,y,f,A x,F,y,f x,G,y,f

**Proof of Theorem tfrlem9**
Step	Hyp	Ref	Expression
1		visset 1820	. . 3 ⊢ y ∈ V
2	1	eldm2 3322	. 2 ⊢ (y ∈ dom F ↔ ∃z⟨y, z⟩ ∈ F)
3		tfrlem.2	. . . . . . 7 ⊢ F = ∪A
4		tfrlem.1	. . . . . . . 8 ⊢ A = {f∣∃x ∈ On (f Fn x ⋀ ∀y ∈ x (f ‘y) = (G ‘(f ↾ y)))}
5	4	unieqi 2523	. . . . . . 7 ⊢ ∪A = ∪{f∣∃x ∈ On (f Fn x ⋀ ∀y ∈ x (f ‘y) = (G ‘(f ↾ y)))}
6	3, 5	eqtr 1502	. . . . . 6 ⊢ F = ∪{f∣∃x ∈ On (f Fn x ⋀ ∀y ∈ x (f ‘y) = (G ‘(f ↾ y)))}
7	6	eleq2i 1545	. . . . 5 ⊢ (⟨y, z⟩ ∈ F ↔ ⟨y, z⟩ ∈ ∪{f∣∃x ∈ On (f Fn x ⋀ ∀y ∈ x (f ‘y) = (G ‘(f ↾ y)))})
8		eluniab 2525	. . . . 5 ⊢ (⟨y, z⟩ ∈ ∪{f∣∃x ∈ On (f Fn x ⋀ ∀y ∈ x (f ‘y) = (G ‘(f ↾ y)))} ↔ ∃f(⟨y, z⟩ ∈ f ⋀ ∃x ∈ On (f Fn x ⋀ ∀y ∈ x (f ‘y) = (G ‘(f ↾ y)))))
9	7, 8	bitr 173	. . . 4 ⊢ (⟨y, z⟩ ∈ F ↔ ∃f(⟨y, z⟩ ∈ f ⋀ ∃x ∈ On (f Fn x ⋀ ∀y ∈ x (f ‘y) = (G ‘(f ↾ y)))))
10		fnop 3605	. . . . . . . . . . . . . 14 ⊢ ((f Fn x ⋀ ⟨y, z⟩ ∈ f) → y ∈ x)
11		ra4e 1702	. . . . . . . . . . . . . . . 16 ⊢ ((x ∈ On ⋀ (f Fn x ⋀ ∀y ∈ x (f ‘y) = (G ‘(f ↾ y)))) → ∃x ∈ On (f Fn x ⋀ ∀y ∈ x (f ‘y) = (G ‘(f ↾ y))))
12	4	abeq2i 1577	. . . . . . . . . . . . . . . . 17 ⊢ (f ∈ A ↔ ∃x ∈ On (f Fn x ⋀ ∀y ∈ x (f ‘y) = (G ‘(f ↾ y))))
13		elssuni 2538	. . . . . . . . . . . . . . . . . 18 ⊢ (f ∈ A → f ⊆ ∪A)
14	13, 3	syl6ssr 2117	. . . . . . . . . . . . . . . . 17 ⊢ (f ∈ A → f ⊆ F)
15	12, 14	sylbir 201	. . . . . . . . . . . . . . . 16 ⊢ (∃x ∈ On (f Fn x ⋀ ∀y ∈ x (f ‘y) = (G ‘(f ↾ y))) → f ⊆ F)
16	11, 15	syl 10	. . . . . . . . . . . . . . 15 ⊢ ((x ∈ On ⋀ (f Fn x ⋀ ∀y ∈ x (f ‘y) = (G ‘(f ↾ y)))) → f ⊆ F)
17		ra4 1701	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀y ∈ x (f ‘y) = (G ‘(f ↾ y)) → (y ∈ x → (f ‘y) = (G ‘(f ↾ y))))
18	17	com12 11	. . . . . . . . . . . . . . . . . 18 ⊢ (y ∈ x → (∀y ∈ x (f ‘y) = (G ‘(f ↾ y)) → (f ‘y) = (G ‘(f ↾ y))))
19		fndm 3601	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (f Fn x → dom f = x)
20	19	eleq2d 1548	. . . . . . . . . . . . . . . . . . . 20 ⊢ (f Fn x → (y ∈ dom f ↔ y ∈ x))
21	4, 3	tfrlem7 3931	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ Fun F
22		funssfv 3749	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((Fun F ⋀ f ⊆ F ⋀ y ∈ dom f) → (F ‘y) = (f ‘y))
23	21, 22	mp3an1 907	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((f ⊆ F ⋀ y ∈ dom f) → (F ‘y) = (f ‘y))
24	23	adantrl 396	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((f ⊆ F ⋀ ((f Fn x ⋀ x ∈ On) ⋀ y ∈ dom f)) → (F ‘y) = (f ‘y))
25		fun2ssres 3567	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((Fun F ⋀ f ⊆ F ⋀ y ⊆ dom f) → (F ↾ y) = (f ↾ y))
26	25	fveq2d 3742	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((Fun F ⋀ f ⊆ F ⋀ y ⊆ dom f) → (G ‘(F ↾ y)) = (G ‘(f ↾ y)))
27	21, 26	mp3an1 907	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((f ⊆ F ⋀ y ⊆ dom f) → (G ‘(F ↾ y)) = (G ‘(f ↾ y)))
28	19	eleq1d 1547	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (f Fn x → (dom f ∈ On ↔ x ∈ On))
29		onelsst 3014	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (dom f ∈ On → (y ∈ dom f → y ⊆ dom f))
30	28, 29	syl6bir 215	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (f Fn x → (x ∈ On → (y ∈ dom f → y ⊆ dom f)))
31	30	imp31 362	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((f Fn x ⋀ x ∈ On) ⋀ y ∈ dom f) → y ⊆ dom f)
32	27, 31	sylan2 454	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((f ⊆ F ⋀ ((f Fn x ⋀ x ∈ On) ⋀ y ∈ dom f)) → (G ‘(F ↾ y)) = (G ‘(f ↾ y)))
33	24, 32	eqeq12d 1496	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((f ⊆ F ⋀ ((f Fn x ⋀ x ∈ On) ⋀ y ∈ dom f)) → ((F ‘y) = (G ‘(F ↾ y)) ↔ (f ‘y) = (G ‘(f ↾ y))))
34	33	biimprd 154	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((f ⊆ F ⋀ ((f Fn x ⋀ x ∈ On) ⋀ y ∈ dom f)) → ((f ‘y) = (G ‘(f ↾ y)) → (F ‘y) = (G ‘(F ↾ y))))
35	34	ex 373	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (f ⊆ F → (((f Fn x ⋀ x ∈ On) ⋀ y ∈ dom f) → ((f ‘y) = (G ‘(f ↾ y)) → (F ‘y) = (G ‘(F ↾ y)))))
36	35	com3l 34	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((f Fn x ⋀ x ∈ On) ⋀ y ∈ dom f) → ((f ‘y) = (G ‘(f ↾ y)) → (f ⊆ F → (F ‘y) = (G ‘(F ↾ y)))))
37	36	exp31 378	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (f Fn x → (x ∈ On → (y ∈ dom f → ((f ‘y) = (G ‘(f ↾ y)) → (f ⊆ F → (F ‘y) = (G ‘(F ↾ y)))))))
38	37	com34 36	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (f Fn x → (x ∈ On → ((f ‘y) = (G ‘(f ↾ y)) → (y ∈ dom f → (f ⊆ F → (F ‘y) = (G ‘(F ↾ y)))))))
39	38	com24 37	. . . . . . . . . . . . . . . . . . . 20 ⊢ (f Fn x → (y ∈ dom f → ((f ‘y) = (G ‘(f ↾ y)) → (x ∈ On → (f ⊆ F → (F ‘y) = (G ‘(F ↾ y)))))))
40	20, 39	sylbird 205	. . . . . . . . . . . . . . . . . . 19 ⊢ (f Fn x → (y ∈ x → ((f ‘y) = (G ‘(f ↾ y)) → (x ∈ On → (f ⊆ F → (F ‘y) = (G ‘(F ↾ y)))))))
41	40	com3l 34	. . . . . . . . . . . . . . . . . 18 ⊢ (y ∈ x → ((f ‘y) = (G ‘(f ↾ y)) → (f Fn x → (x ∈ On → (f ⊆ F → (F ‘y) = (G ‘(F ↾ y)))))))
42	18, 41	syld 27	. . . . . . . . . . . . . . . . 17 ⊢ (y ∈ x → (∀y ∈ x (f ‘y) = (G ‘(f ↾ y)) → (f Fn x → (x ∈ On → (f ⊆ F → (F ‘y) = (G ‘(F ↾ y)))))))
43	42	com24 37	. . . . . . . . . . . . . . . 16 ⊢ (y ∈ x → (x ∈ On → (f Fn x → (∀y ∈ x (f ‘y) = (G ‘(f ↾ y)) → (f ⊆ F → (F ‘y) = (G ‘(F ↾ y)))))))
44	43	imp4d 367	. . . . . . . . . . . . . . 15 ⊢ (y ∈ x → ((x ∈ On ⋀ (f Fn x ⋀ ∀y ∈ x (f ‘y) = (G ‘(f ↾ y)))) → (f ⊆ F → (F ‘y) = (G ‘(F ↾ y)))))
45	16, 44	mpdi 48	. . . . . . . . . . . . . 14 ⊢ (y ∈ x → ((x ∈ On ⋀ (f Fn x ⋀ ∀y ∈ x (f ‘y) = (G ‘(f ↾ y)))) → (F ‘y) = (G ‘(F ↾ y))))
46	10, 45	syl 10	. . . . . . . . . . . . 13 ⊢ ((f Fn x ⋀ ⟨y, z⟩ ∈ f) → ((x ∈ On ⋀ (f Fn x ⋀ ∀y ∈ x (f ‘y) = (G ‘(f ↾ y)))) → (F ‘y) = (G ‘(F ↾ y))))
47	46	exp4d 383	. . . . . . . . . . . 12 ⊢ ((f Fn x ⋀ ⟨y, z⟩ ∈ f) → (x ∈ On → (f Fn x → (∀y ∈ x (f ‘y) = (G ‘(f ↾ y)) → (F ‘y) = (G ‘(F ↾ y))))))
48	47	ex 373	. . . . . . . . . . 11 ⊢ (f Fn x → (⟨y, z⟩ ∈ f → (x ∈ On → (f Fn x → (∀y ∈ x (f ‘y) = (G ‘(f ↾ y)) → (F ‘y) = (G ‘(F ↾ y)))))))
49	48	com4r 41	. . . . . . . . . 10 ⊢ (f Fn x → (f Fn x → (⟨y, z⟩ ∈ f → (x ∈ On → (∀y ∈ x (f ‘y) = (G ‘(f ↾ y)) → (F ‘y) = (G ‘(F ↾ y)))))))
50	49	pm2.43i 64	. . . . . . . . 9 ⊢ (f Fn x → (⟨y, z⟩ ∈ f → (x ∈ On → (∀y ∈ x (f ‘y) = (G ‘(f ↾ y)) → (F ‘y) = (G ‘(F ↾ y))))))
51	50	com3l 34	. . . . . . . 8 ⊢ (⟨y, z⟩ ∈ f → (x ∈ On → (f Fn x → (∀y ∈ x (f ‘y) = (G ‘(f ↾ y)) → (F ‘y) = (G ‘(F ↾ y))))))
52	51	imp4a 364	. . . . . . 7 ⊢ (⟨y, z⟩ ∈ f → (x ∈ On → ((f Fn x ⋀ ∀y ∈ x (f ‘y) = (G ‘(f ↾ y))) → (F ‘y) = (G ‘(F ↾ y)))))
53	52	r19.23adv 1753	. . . . . 6 ⊢ (⟨y, z⟩ ∈ f → (∃x ∈ On (f Fn x ⋀ ∀y ∈ x (f ‘y) = (G ‘(f ↾ y))) → (F ‘y) = (G ‘(F ↾ y))))
54	53	imp 350	. . . . 5 ⊢ ((⟨y, z⟩ ∈ f ⋀ ∃x ∈ On (f Fn x ⋀ ∀y ∈ x (f ‘y) = (G ‘(f ↾ y)))) → (F ‘y) = (G ‘(F ↾ y)))
55	54	19.23aiv 1301	. . . 4 ⊢ (∃f(⟨y, z⟩ ∈ f ⋀ ∃x ∈ On (f Fn x ⋀ ∀y ∈ x (f ‘y) = (G ‘(f ↾ y)))) → (F ‘y) = (G ‘(F ↾ y)))
56	9, 55	sylbi 199	. . 3 ⊢ (⟨y, z⟩ ∈ F → (F ‘y) = (G ‘(F ↾ y)))
57	56	19.23aiv 1301	. 2 ⊢ (∃z⟨y, z⟩ ∈ F → (F ‘y) = (G ‘(F ↾ y)))
58	2, 57	sylbi 199	1 ⊢ (y ∈ dom F → (F ‘y) = (G ‘(F ↾ y)))

Colors of variables: wff set class

Syntax hints: → wi 3 ⋀ wa 223 ⋀ w3a 779 = wceq 960 ∈ wcel 962 ∃wex 984 {cab 1470 ∀wral 1652 ∃wrex 1653 ⊆ wss 2056 ⟨cop 2421 ∪cuni 2515 Oncon0 2962 dom cdm 3184 ↾ cres 3186 Fun wfun 3190 Fn wfn 3191 ‘cfv 3196

This theorem is referenced by: tfrlem11 3935 tfr2 3939

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 966 ax-gen 967 ax-8 968 ax-9 969 ax-10 970 ax-11 971 ax-12 972 ax-13 973 ax-14 974 ax-17 975 ax-4 977 ax-5o 979 ax-6o 982 ax-9o 1129 ax-10o 1146 ax-16 1216 ax-11o 1224 ax-ext 1466 ax-sep 2716 ax-pow 2756 ax-pr 2793 ax-un 2880

This theorem depends on definitions: df-bi 147 df-or 224 df-an 225 df-3or 780 df-3an 781 df-ex 985 df-sb 1178 df-eu 1388 df-mo 1389 df-clab 1471 df-cleq 1476 df-clel 1479 df-ne 1594 df-ral 1656 df-rex 1657 df-rab 1659 df-v 1819 df-sbc 1949 df-dif 2058 df-un 2059 df-in 2060 df-ss 2062 df-nul 2290 df-pw 2412 df-sn 2422 df-pr 2423 df-tp 2425 df-op 2426 df-uni 2516 df-br 2633 df-opab 2680 df-tr 2694 df-eprel 2846 df-id 2849 df-po 2854 df-so 2864 df-fr 2931 df-we 2948 df-ord 2965 df-on 2966 df-xp 3198 df-rel 3199 df-cnv 3200 df-co 3201 df-dm 3202 df-rn 3203 df-res 3204 df-ima 3205 df-fun 3206 df-fn 3207 df-fv 3212