Theorem tfrlem9 2957

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 group(s):   x,y,f,A   x,F,y,f   x,G,y,f

Proof of Theorem tfrlem9

Step	Hyp	Ref	Expression
1		visset 1350	. . 3 ⊢ y ∈ V
2	1	eldm2 2528	. 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 1928	. . . . . . 7 ⊢ ∪A = ∪{f∣∃x ∈ On (f Fn x ∧ ∀y ∈ x (f ‘y) = (G ‘(f ↾ y)))}
6	3, 5	eqtr 1119	. . . . . 6 ⊢ F = ∪{f∣∃x ∈ On (f Fn x ∧ ∀y ∈ x (f ‘y) = (G ‘(f ↾ y)))}
7	6	eleq2i 1153	. . . . 5 ⊢ (⟨y, z⟩ ∈ F ↔ ⟨y, z⟩ ∈ ∪{f∣∃x ∈ On (f Fn x ∧ ∀y ∈ x (f ‘y) = (G ‘(f ↾ y)))})
8		eluniab 1926	. . . . 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 151	. . . 4 ⊢ (⟨y, z⟩ ∈ F ↔ ∃f(⟨y, z⟩ ∈ f ∧ ∃x ∈ On (f Fn x ∧ ∀y ∈ x (f ‘y) = (G ‘(f ↾ y)))))
10		visset 1350	. . . . . . . . . . . . . . 15 ⊢ z ∈ V
11	1, 10	fnop 2727	. . . . . . . . . . . . . 14 ⊢ ((f Fn x ∧ ⟨y, z⟩ ∈ f) → y ∈ x)
12		ra4e 1244	. . . . . . . . . . . . . . . . 17 ⊢ ((x ∈ On ∧ (f Fn x ∧ ∀y ∈ x (f ‘y) = (G ‘(f ↾ y)))) → ∃x ∈ On (f Fn x ∧ ∀y ∈ x (f ‘y) = (G ‘(f ↾ y))))
13	4	cleqabi 1176	. . . . . . . . . . . . . . . . . 18 ⊢ (f ∈ A ↔ ∃x ∈ On (f Fn x ∧ ∀y ∈ x (f ‘y) = (G ‘(f ↾ y))))
14		elssuni 1940	. . . . . . . . . . . . . . . . . . 19 ⊢ (f ∈ A → f ⊆ ∪A)
15	14, 3	syl6ssr 1547	. . . . . . . . . . . . . . . . . 18 ⊢ (f ∈ A → f ⊆ F)
16	13, 15	sylbir 176	. . . . . . . . . . . . . . . . 17 ⊢ (∃x ∈ On (f Fn x ∧ ∀y ∈ x (f ‘y) = (G ‘(f ↾ y))) → f ⊆ F)
17	12, 16	syl 12	. . . . . . . . . . . . . . . 16 ⊢ ((x ∈ On ∧ (f Fn x ∧ ∀y ∈ x (f ‘y) = (G ‘(f ↾ y)))) → f ⊆ F)
18		ra4 1243	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀y ∈ x (f ‘y) = (G ‘(f ↾ y)) → (y ∈ x → (f ‘y) = (G ‘(f ↾ y))))
19	18	com12 13	. . . . . . . . . . . . . . . . . . . 20 ⊢ (y ∈ x → (∀y ∈ x (f ‘y) = (G ‘(f ↾ y)) → (f ‘y) = (G ‘(f ↾ y))))
20		fndm 2723	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (f Fn x → dom f = x)
21	20	eleq2d 1156	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (f Fn x → (y ∈ dom f ↔ y ∈ x))
22	4, 3	tfrlem7 2955	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ Fun F
23		funssfv 2841	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((Fun F ∧ f ⊆ F) ∧ y ∈ dom f) → (F ‘y) = (f ‘y))
24	23	adantrl 311	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((Fun F ∧ f ⊆ F) ∧ ((f Fn x ∧ x ∈ On) ∧ y ∈ dom f)) → (F ‘y) = (f ‘y))
25		fun2ssres 2699	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((Fun F ∧ f ⊆ F) ∧ y ⊆ dom f) → (F ↾ y) = (f ↾ y))
26	25	fveq2d 2836	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((Fun F ∧ f ⊆ F) ∧ y ⊆ dom f) → (G ‘(F ↾ y)) = (G ‘(f ↾ y)))
27	20	eleq1d 1155	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (f Fn x → (dom f ∈ On ↔ x ∈ On))
28		onelsst 2255	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (dom f ∈ On → (y ∈ dom f → y ⊆ dom f))
29	27, 28	syl6bir 188	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (f Fn x → (x ∈ On → (y ∈ dom f → y ⊆ dom f)))
30	29	imp31 280	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((f Fn x ∧ x ∈ On) ∧ y ∈ dom f) → y ⊆ dom f)
31	26, 30	sylan2 346	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((Fun F ∧ f ⊆ F) ∧ ((f Fn x ∧ x ∈ On) ∧ y ∈ dom f)) → (G ‘(F ↾ y)) = (G ‘(f ↾ y)))
32	24, 31	cleq12d 1115	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((Fun F ∧ f ⊆ F) ∧ ((f Fn x ∧ x ∈ On) ∧ y ∈ dom f)) → ((F ‘y) = (G ‘(F ↾ y)) ↔ (f ‘y) = (G ‘(f ↾ y))))
33	22, 32	mpan11 529	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((f ⊆ F ∧ ((f Fn x ∧ x ∈ On) ∧ y ∈ dom f)) → ((F ‘y) = (G ‘(F ↾ y)) ↔ (f ‘y) = (G ‘(f ↾ y))))
34	33	biimprd 136	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((f ⊆ F ∧ ((f Fn x ∧ x ∈ On) ∧ y ∈ dom f)) → ((f ‘y) = (G ‘(f ↾ y)) → (F ‘y) = (G ‘(F ↾ y))))
35	34	exp 291	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (f ⊆ F → (((f Fn x ∧ x ∈ On) ∧ y ∈ dom f) → ((f ‘y) = (G ‘(f ↾ y)) → (F ‘y) = (G ‘(F ↾ y)))))
36	35	com3l 34	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((f Fn x ∧ x ∈ On) ∧ y ∈ dom f) → ((f ‘y) = (G ‘(f ↾ y)) → (f ⊆ F → (F ‘y) = (G ‘(F ↾ y)))))
37	36	exp31 293	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (f Fn x → (x ∈ On → (y ∈ dom f → ((f ‘y) = (G ‘(f ↾ y)) → (f ⊆ F → (F ‘y) = (G ‘(F ↾ y)))))))
38	37	com34 36	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (f Fn x → (x ∈ On → ((f ‘y) = (G ‘(f ↾ y)) → (y ∈ dom f → (f ⊆ F → (F ‘y) = (G ‘(F ↾ y)))))))
39	38	com24 37	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (f Fn x → (y ∈ dom f → ((f ‘y) = (G ‘(f ↾ y)) → (x ∈ On → (f ⊆ F → (F ‘y) = (G ‘(F ↾ y)))))))
40	21, 39	sylbird 180	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (f Fn x → (y ∈ x → ((f ‘y) = (G ‘(f ↾ y)) → (x ∈ On → (f ⊆ F → (F ‘y) = (G ‘(F ↾ y)))))))
41	40	com3l 34	. . . . . . . . . . . . . . . . . . . 20 ⊢ (y ∈ x → ((f ‘y) = (G ‘(f ↾ y)) → (f Fn x → (x ∈ On → (f ⊆ F → (F ‘y) = (G ‘(F ↾ y)))))))
42	19, 41	syld 27	. . . . . . . . . . . . . . . . . . 19 ⊢ (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	. . . . . . . . . . . . . . . . . 18 ⊢ (y ∈ x → (x ∈ On → (f Fn x → (∀y ∈ x (f ‘y) = (G ‘(f ↾ y)) → (f ⊆ F → (F ‘y) = (G ‘(F ↾ y)))))))
44	43	imp4d 285	. . . . . . . . . . . . . . . . 17 ⊢ (y ∈ x → ((x ∈ On ∧ (f Fn x ∧ ∀y ∈ x (f ‘y) = (G ‘(f ↾ y)))) → (f ⊆ F → (F ‘y) = (G ‘(F ↾ y)))))
45	44	com13 33	. . . . . . . . . . . . . . . 16 ⊢ (f ⊆ F → ((x ∈ On ∧ (f Fn x ∧ ∀y ∈ x (f ‘y) = (G ‘(f ↾ y)))) → (y ∈ x → (F ‘y) = (G ‘(F ↾ y)))))
46	17, 45	mpcom 49	. . . . . . . . . . . . . . 15 ⊢ ((x ∈ On ∧ (f Fn x ∧ ∀y ∈ x (f ‘y) = (G ‘(f ↾ y)))) → (y ∈ x → (F ‘y) = (G ‘(F ↾ y))))
47	46	com12 13	. . . . . . . . . . . . . 14 ⊢ (y ∈ x → ((x ∈ On ∧ (f Fn x ∧ ∀y ∈ x (f ‘y) = (G ‘(f ↾ y)))) → (F ‘y) = (G ‘(F ↾ y))))
48	11, 47	syl 12	. . . . . . . . . . . . 13 ⊢ ((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	exp4d 298	. . . . . . . . . . . 12 ⊢ ((f Fn x ∧ ⟨y, z⟩ ∈ f) → (x ∈ On → (f Fn x → (∀y ∈ x (f ‘y) = (G ‘(f ↾ y)) → (F ‘y) = (G ‘(F ↾ y))))))
50	49	exp 291	. . . . . . . . . . 11 ⊢ (f Fn x → (⟨y, z⟩ ∈ f → (x ∈ On → (f Fn x → (∀y ∈ x (f ‘y) = (G ‘(f ↾ y)) → (F ‘y) = (G ‘(F ↾ y)))))))
51	50	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)))))))
52	51	pm2.43i 58	. . . . . . . . 9 ⊢ (f Fn x → (⟨y, z⟩ ∈ f → (x ∈ On → (∀y ∈ x (f ‘y) = (G ‘(f ↾ y)) → (F ‘y) = (G ‘(F ↾ y))))))
53	52	com3l 34	. . . . . . . 8 ⊢ (⟨y, z⟩ ∈ f → (x ∈ On → (f Fn x → (∀y ∈ x (f ‘y) = (G ‘(f ↾ y)) → (F ‘y) = (G ‘(F ↾ y))))))
54	53	imp4a 282	. . . . . . 7 ⊢ (⟨y, z⟩ ∈ f → (x ∈ On → ((f Fn x ∧ ∀y ∈ x (f ‘y) = (G ‘(f ↾ y))) → (F ‘y) = (G ‘(F ↾ y)))))
55	54	r19.23adv 1286	. . . . . 6 ⊢ (⟨y, z⟩ ∈ f → (∃x ∈ On (f Fn x ∧ ∀y ∈ x (f ‘y) = (G ‘(f ↾ y))) → (F ‘y) = (G ‘(F ↾ y))))
56	55	imp 277	. . . . 5 ⊢ ((⟨y, z⟩ ∈ f ∧ ∃x ∈ On (f Fn x ∧ ∀y ∈ x (f ‘y) = (G ‘(f ↾ y)))) → (F ‘y) = (G ‘(F ↾ y)))
57	56	19.23aiv 952	. . . 4 ⊢ (∃f(⟨y, z⟩ ∈ f ∧ ∃x ∈ On (f Fn x ∧ ∀y ∈ x (f ‘y) = (G ‘(f ↾ y)))) → (F ‘y) = (G ‘(F ↾ y)))
58	9, 57	sylbi 174	. . 3 ⊢ (⟨y, z⟩ ∈ F → (F ‘y) = (G ‘(F ↾ y)))
59	58	19.23aiv 952	. 2 ⊢ (∃z⟨y, z⟩ ∈ F → (F ‘y) = (G ‘(F ↾ y)))
60	2, 59	sylbi 174	1 ⊢ (y ∈ dom F → (F ‘y) = (G ‘(F ↾ y)))

Syntax hints:   → wi 2   ↔ wb 127   ∧ wa 196  ∃wex 678   ∈ wel 803  {cab 1090   = wceq 1091   ∈ wcel 1092  ∀wral 1201  ∃wrex 1202   ⊆ wss 1487  ⟨cop 1810  ∪cuni 1919  Oncon0 2199  dom cdm 2410   ↾ cres 2412  Fun wfun 2416   Fn wfn 2417   ‘cfv 2422

This theorem is referenced by:  tfrlem11 2959  tfr2 2963

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-rab 1208  df-v 1349  df-sbc 1441  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-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