Theorem tfrlemi1 5887

Description: We can define an acceptable function on any ordinal.

As with many of the transfinite recursion theorems, we have a hypothesis that states that 𝐹 is a function and that it is defined for all ordinals. (Contributed by Jim Kingdon, 4-Mar-2019.) (Proof shortened by Mario Carneiro, 24-May-2019.)

Hypotheses

Ref	Expression
tfrlemisucfn.1	⊢ A = {f ∣ ∃x ∈ On (f Fn x ∧ ∀y ∈ x (f‘y) = (𝐹‘(f ↾ y)))}
tfrlemisucfn.2	⊢ (φ → ∀x(Fun 𝐹 ∧ (𝐹‘x) ∈ V))

Assertion

Ref	Expression
tfrlemi1	⊢ ((φ ∧ 𝐶 ∈ On) → ∃g(g Fn 𝐶 ∧ ∀u ∈ 𝐶 (g‘u) = (𝐹‘(g ↾ u))))

Distinct variable groups:   f,g,u,x,y,A   f,𝐹,g,u,x,y   φ,y   𝐶,g,u   φ,f

Allowed substitution hints:   φ(x,u,g)   𝐶(x,y,f)

Proof of Theorem tfrlemi1

Dummy variables 𝑒 ℎ 𝑘 𝑡 v w z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpr 103	. . . . . . 7 ⊢ ((z = w ∧ g = 𝑘) → g = 𝑘)
2		simpl 102	. . . . . . 7 ⊢ ((z = w ∧ g = 𝑘) → z = w)
3	1, 2	fneq12d 4934	. . . . . 6 ⊢ ((z = w ∧ g = 𝑘) → (g Fn z ↔ 𝑘 Fn w))
4	1	fveq1d 5123	. . . . . . . 8 ⊢ ((z = w ∧ g = 𝑘) → (g‘u) = (𝑘‘u))
5	1	reseq1d 4554	. . . . . . . . 9 ⊢ ((z = w ∧ g = 𝑘) → (g ↾ u) = (𝑘 ↾ u))
6	5	fveq2d 5125	. . . . . . . 8 ⊢ ((z = w ∧ g = 𝑘) → (𝐹‘(g ↾ u)) = (𝐹‘(𝑘 ↾ u)))
7	4, 6	eqeq12d 2051	. . . . . . 7 ⊢ ((z = w ∧ g = 𝑘) → ((g‘u) = (𝐹‘(g ↾ u)) ↔ (𝑘‘u) = (𝐹‘(𝑘 ↾ u))))
8	2, 7	raleqbidv 2511	. . . . . 6 ⊢ ((z = w ∧ g = 𝑘) → (∀u ∈ z (g‘u) = (𝐹‘(g ↾ u)) ↔ ∀u ∈ w (𝑘‘u) = (𝐹‘(𝑘 ↾ u))))
9	3, 8	anbi12d 442	. . . . 5 ⊢ ((z = w ∧ g = 𝑘) → ((g Fn z ∧ ∀u ∈ z (g‘u) = (𝐹‘(g ↾ u))) ↔ (𝑘 Fn w ∧ ∀u ∈ w (𝑘‘u) = (𝐹‘(𝑘 ↾ u)))))
10	9	cbvexdva 1801	. . . 4 ⊢ (z = w → (∃g(g Fn z ∧ ∀u ∈ z (g‘u) = (𝐹‘(g ↾ u))) ↔ ∃𝑘(𝑘 Fn w ∧ ∀u ∈ w (𝑘‘u) = (𝐹‘(𝑘 ↾ u)))))
11	10	imbi2d 219	. . 3 ⊢ (z = w → ((φ → ∃g(g Fn z ∧ ∀u ∈ z (g‘u) = (𝐹‘(g ↾ u)))) ↔ (φ → ∃𝑘(𝑘 Fn w ∧ ∀u ∈ w (𝑘‘u) = (𝐹‘(𝑘 ↾ u))))))
12		fneq2 4931	. . . . . 6 ⊢ (z = 𝐶 → (g Fn z ↔ g Fn 𝐶))
13		raleq 2499	. . . . . 6 ⊢ (z = 𝐶 → (∀u ∈ z (g‘u) = (𝐹‘(g ↾ u)) ↔ ∀u ∈ 𝐶 (g‘u) = (𝐹‘(g ↾ u))))
14	12, 13	anbi12d 442	. . . . 5 ⊢ (z = 𝐶 → ((g Fn z ∧ ∀u ∈ z (g‘u) = (𝐹‘(g ↾ u))) ↔ (g Fn 𝐶 ∧ ∀u ∈ 𝐶 (g‘u) = (𝐹‘(g ↾ u)))))
15	14	exbidv 1703	. . . 4 ⊢ (z = 𝐶 → (∃g(g Fn z ∧ ∀u ∈ z (g‘u) = (𝐹‘(g ↾ u))) ↔ ∃g(g Fn 𝐶 ∧ ∀u ∈ 𝐶 (g‘u) = (𝐹‘(g ↾ u)))))
16	15	imbi2d 219	. . 3 ⊢ (z = 𝐶 → ((φ → ∃g(g Fn z ∧ ∀u ∈ z (g‘u) = (𝐹‘(g ↾ u)))) ↔ (φ → ∃g(g Fn 𝐶 ∧ ∀u ∈ 𝐶 (g‘u) = (𝐹‘(g ↾ u))))))
17		r19.21v 2390	. . . 4 ⊢ (∀w ∈ z (φ → ∃𝑘(𝑘 Fn w ∧ ∀u ∈ w (𝑘‘u) = (𝐹‘(𝑘 ↾ u)))) ↔ (φ → ∀w ∈ z ∃𝑘(𝑘 Fn w ∧ ∀u ∈ w (𝑘‘u) = (𝐹‘(𝑘 ↾ u)))))
18		tfrlemisucfn.1	. . . . . . . . 9 ⊢ A = {f ∣ ∃x ∈ On (f Fn x ∧ ∀y ∈ x (f‘y) = (𝐹‘(f ↾ y)))}
19	18	tfrlem3 5867	. . . . . . . 8 ⊢ A = {g ∣ ∃z ∈ On (g Fn z ∧ ∀𝑒 ∈ z (g‘𝑒) = (𝐹‘(g ↾ 𝑒)))}
20		tfrlemisucfn.2	. . . . . . . . . 10 ⊢ (φ → ∀x(Fun 𝐹 ∧ (𝐹‘x) ∈ V))
21		fveq2 5121	. . . . . . . . . . . . 13 ⊢ (x = z → (𝐹‘x) = (𝐹‘z))
22	21	eleq1d 2103	. . . . . . . . . . . 12 ⊢ (x = z → ((𝐹‘x) ∈ V ↔ (𝐹‘z) ∈ V))
23	22	anbi2d 437	. . . . . . . . . . 11 ⊢ (x = z → ((Fun 𝐹 ∧ (𝐹‘x) ∈ V) ↔ (Fun 𝐹 ∧ (𝐹‘z) ∈ V)))
24	23	cbvalv 1791	. . . . . . . . . 10 ⊢ (∀x(Fun 𝐹 ∧ (𝐹‘x) ∈ V) ↔ ∀z(Fun 𝐹 ∧ (𝐹‘z) ∈ V))
25	20, 24	sylib 127	. . . . . . . . 9 ⊢ (φ → ∀z(Fun 𝐹 ∧ (𝐹‘z) ∈ V))
26	25	adantr 261	. . . . . . . 8 ⊢ ((φ ∧ (z ∈ On ∧ ∀w ∈ z ∃𝑘(𝑘 Fn w ∧ ∀u ∈ w (𝑘‘u) = (𝐹‘(𝑘 ↾ u))))) → ∀z(Fun 𝐹 ∧ (𝐹‘z) ∈ V))
27		simpr 103	. . . . . . . . . . . . 13 ⊢ (((𝑡 = ℎ ∧ w = v) ∧ 𝑘 = f) → 𝑘 = f)
28		simplr 482	. . . . . . . . . . . . 13 ⊢ (((𝑡 = ℎ ∧ w = v) ∧ 𝑘 = f) → w = v)
29	27, 28	fneq12d 4934	. . . . . . . . . . . 12 ⊢ (((𝑡 = ℎ ∧ w = v) ∧ 𝑘 = f) → (𝑘 Fn w ↔ f Fn v))
30	27	eleq1d 2103	. . . . . . . . . . . 12 ⊢ (((𝑡 = ℎ ∧ w = v) ∧ 𝑘 = f) → (𝑘 ∈ A ↔ f ∈ A))
31		simpll 481	. . . . . . . . . . . . 13 ⊢ (((𝑡 = ℎ ∧ w = v) ∧ 𝑘 = f) → 𝑡 = ℎ)
32	27	fveq2d 5125	. . . . . . . . . . . . . . . 16 ⊢ (((𝑡 = ℎ ∧ w = v) ∧ 𝑘 = f) → (𝐹‘𝑘) = (𝐹‘f))
33	28, 32	opeq12d 3548	. . . . . . . . . . . . . . 15 ⊢ (((𝑡 = ℎ ∧ w = v) ∧ 𝑘 = f) → ⟨w, (𝐹‘𝑘)⟩ = ⟨v, (𝐹‘f)⟩)
34	33	sneqd 3380	. . . . . . . . . . . . . 14 ⊢ (((𝑡 = ℎ ∧ w = v) ∧ 𝑘 = f) → {⟨w, (𝐹‘𝑘)⟩} = {⟨v, (𝐹‘f)⟩})
35	27, 34	uneq12d 3092	. . . . . . . . . . . . 13 ⊢ (((𝑡 = ℎ ∧ w = v) ∧ 𝑘 = f) → (𝑘 ∪ {⟨w, (𝐹‘𝑘)⟩}) = (f ∪ {⟨v, (𝐹‘f)⟩}))
36	31, 35	eqeq12d 2051	. . . . . . . . . . . 12 ⊢ (((𝑡 = ℎ ∧ w = v) ∧ 𝑘 = f) → (𝑡 = (𝑘 ∪ {⟨w, (𝐹‘𝑘)⟩}) ↔ ℎ = (f ∪ {⟨v, (𝐹‘f)⟩})))
37	29, 30, 36	3anbi123d 1206	. . . . . . . . . . 11 ⊢ (((𝑡 = ℎ ∧ w = v) ∧ 𝑘 = f) → ((𝑘 Fn w ∧ 𝑘 ∈ A ∧ 𝑡 = (𝑘 ∪ {⟨w, (𝐹‘𝑘)⟩})) ↔ (f Fn v ∧ f ∈ A ∧ ℎ = (f ∪ {⟨v, (𝐹‘f)⟩}))))
38	37	cbvexdva 1801	. . . . . . . . . 10 ⊢ ((𝑡 = ℎ ∧ w = v) → (∃𝑘(𝑘 Fn w ∧ 𝑘 ∈ A ∧ 𝑡 = (𝑘 ∪ {⟨w, (𝐹‘𝑘)⟩})) ↔ ∃f(f Fn v ∧ f ∈ A ∧ ℎ = (f ∪ {⟨v, (𝐹‘f)⟩}))))
39	38	cbvrexdva 2534	. . . . . . . . 9 ⊢ (𝑡 = ℎ → (∃w ∈ z ∃𝑘(𝑘 Fn w ∧ 𝑘 ∈ A ∧ 𝑡 = (𝑘 ∪ {⟨w, (𝐹‘𝑘)⟩})) ↔ ∃v ∈ z ∃f(f Fn v ∧ f ∈ A ∧ ℎ = (f ∪ {⟨v, (𝐹‘f)⟩}))))
40	39	cbvabv 2158	. . . . . . . 8 ⊢ {𝑡 ∣ ∃w ∈ z ∃𝑘(𝑘 Fn w ∧ 𝑘 ∈ A ∧ 𝑡 = (𝑘 ∪ {⟨w, (𝐹‘𝑘)⟩}))} = {ℎ ∣ ∃v ∈ z ∃f(f Fn v ∧ f ∈ A ∧ ℎ = (f ∪ {⟨v, (𝐹‘f)⟩}))}
41		simpl 102	. . . . . . . . 9 ⊢ ((z ∈ On ∧ ∀w ∈ z ∃𝑘(𝑘 Fn w ∧ ∀u ∈ w (𝑘‘u) = (𝐹‘(𝑘 ↾ u)))) → z ∈ On)
42	41	adantl 262	. . . . . . . 8 ⊢ ((φ ∧ (z ∈ On ∧ ∀w ∈ z ∃𝑘(𝑘 Fn w ∧ ∀u ∈ w (𝑘‘u) = (𝐹‘(𝑘 ↾ u))))) → z ∈ On)
43		simpr 103	. . . . . . . . . 10 ⊢ ((z ∈ On ∧ ∀w ∈ z ∃𝑘(𝑘 Fn w ∧ ∀u ∈ w (𝑘‘u) = (𝐹‘(𝑘 ↾ u)))) → ∀w ∈ z ∃𝑘(𝑘 Fn w ∧ ∀u ∈ w (𝑘‘u) = (𝐹‘(𝑘 ↾ u))))
44		simpr 103	. . . . . . . . . . . . . 14 ⊢ ((w = v ∧ 𝑘 = f) → 𝑘 = f)
45		simpl 102	. . . . . . . . . . . . . 14 ⊢ ((w = v ∧ 𝑘 = f) → w = v)
46	44, 45	fneq12d 4934	. . . . . . . . . . . . 13 ⊢ ((w = v ∧ 𝑘 = f) → (𝑘 Fn w ↔ f Fn v))
47		simplr 482	. . . . . . . . . . . . . . . 16 ⊢ (((w = v ∧ 𝑘 = f) ∧ u = y) → 𝑘 = f)
48		simpr 103	. . . . . . . . . . . . . . . 16 ⊢ (((w = v ∧ 𝑘 = f) ∧ u = y) → u = y)
49	47, 48	fveq12d 5127	. . . . . . . . . . . . . . 15 ⊢ (((w = v ∧ 𝑘 = f) ∧ u = y) → (𝑘‘u) = (f‘y))
50	47, 48	reseq12d 4556	. . . . . . . . . . . . . . . 16 ⊢ (((w = v ∧ 𝑘 = f) ∧ u = y) → (𝑘 ↾ u) = (f ↾ y))
51	50	fveq2d 5125	. . . . . . . . . . . . . . 15 ⊢ (((w = v ∧ 𝑘 = f) ∧ u = y) → (𝐹‘(𝑘 ↾ u)) = (𝐹‘(f ↾ y)))
52	49, 51	eqeq12d 2051	. . . . . . . . . . . . . 14 ⊢ (((w = v ∧ 𝑘 = f) ∧ u = y) → ((𝑘‘u) = (𝐹‘(𝑘 ↾ u)) ↔ (f‘y) = (𝐹‘(f ↾ y))))
53		simpll 481	. . . . . . . . . . . . . 14 ⊢ (((w = v ∧ 𝑘 = f) ∧ u = y) → w = v)
54	52, 53	cbvraldva2 2531	. . . . . . . . . . . . 13 ⊢ ((w = v ∧ 𝑘 = f) → (∀u ∈ w (𝑘‘u) = (𝐹‘(𝑘 ↾ u)) ↔ ∀y ∈ v (f‘y) = (𝐹‘(f ↾ y))))
55	46, 54	anbi12d 442	. . . . . . . . . . . 12 ⊢ ((w = v ∧ 𝑘 = f) → ((𝑘 Fn w ∧ ∀u ∈ w (𝑘‘u) = (𝐹‘(𝑘 ↾ u))) ↔ (f Fn v ∧ ∀y ∈ v (f‘y) = (𝐹‘(f ↾ y)))))
56	55	cbvexdva 1801	. . . . . . . . . . 11 ⊢ (w = v → (∃𝑘(𝑘 Fn w ∧ ∀u ∈ w (𝑘‘u) = (𝐹‘(𝑘 ↾ u))) ↔ ∃f(f Fn v ∧ ∀y ∈ v (f‘y) = (𝐹‘(f ↾ y)))))
57	56	cbvralv 2527	. . . . . . . . . 10 ⊢ (∀w ∈ z ∃𝑘(𝑘 Fn w ∧ ∀u ∈ w (𝑘‘u) = (𝐹‘(𝑘 ↾ u))) ↔ ∀v ∈ z ∃f(f Fn v ∧ ∀y ∈ v (f‘y) = (𝐹‘(f ↾ y))))
58	43, 57	sylib 127	. . . . . . . . 9 ⊢ ((z ∈ On ∧ ∀w ∈ z ∃𝑘(𝑘 Fn w ∧ ∀u ∈ w (𝑘‘u) = (𝐹‘(𝑘 ↾ u)))) → ∀v ∈ z ∃f(f Fn v ∧ ∀y ∈ v (f‘y) = (𝐹‘(f ↾ y))))
59	58	adantl 262	. . . . . . . 8 ⊢ ((φ ∧ (z ∈ On ∧ ∀w ∈ z ∃𝑘(𝑘 Fn w ∧ ∀u ∈ w (𝑘‘u) = (𝐹‘(𝑘 ↾ u))))) → ∀v ∈ z ∃f(f Fn v ∧ ∀y ∈ v (f‘y) = (𝐹‘(f ↾ y))))
60	19, 26, 40, 42, 59	tfrlemiex 5886	. . . . . . 7 ⊢ ((φ ∧ (z ∈ On ∧ ∀w ∈ z ∃𝑘(𝑘 Fn w ∧ ∀u ∈ w (𝑘‘u) = (𝐹‘(𝑘 ↾ u))))) → ∃g(g Fn z ∧ ∀u ∈ z (g‘u) = (𝐹‘(g ↾ u))))
61	60	expr 357	. . . . . 6 ⊢ ((φ ∧ z ∈ On) → (∀w ∈ z ∃𝑘(𝑘 Fn w ∧ ∀u ∈ w (𝑘‘u) = (𝐹‘(𝑘 ↾ u))) → ∃g(g Fn z ∧ ∀u ∈ z (g‘u) = (𝐹‘(g ↾ u)))))
62	61	expcom 109	. . . . 5 ⊢ (z ∈ On → (φ → (∀w ∈ z ∃𝑘(𝑘 Fn w ∧ ∀u ∈ w (𝑘‘u) = (𝐹‘(𝑘 ↾ u))) → ∃g(g Fn z ∧ ∀u ∈ z (g‘u) = (𝐹‘(g ↾ u))))))
63	62	a2d 23	. . . 4 ⊢ (z ∈ On → ((φ → ∀w ∈ z ∃𝑘(𝑘 Fn w ∧ ∀u ∈ w (𝑘‘u) = (𝐹‘(𝑘 ↾ u)))) → (φ → ∃g(g Fn z ∧ ∀u ∈ z (g‘u) = (𝐹‘(g ↾ u))))))
64	17, 63	syl5bi 141	. . 3 ⊢ (z ∈ On → (∀w ∈ z (φ → ∃𝑘(𝑘 Fn w ∧ ∀u ∈ w (𝑘‘u) = (𝐹‘(𝑘 ↾ u)))) → (φ → ∃g(g Fn z ∧ ∀u ∈ z (g‘u) = (𝐹‘(g ↾ u))))))
65	11, 16, 64	tfis3 4252	. 2 ⊢ (𝐶 ∈ On → (φ → ∃g(g Fn 𝐶 ∧ ∀u ∈ 𝐶 (g‘u) = (𝐹‘(g ↾ u)))))
66	65	impcom 116	1 ⊢ ((φ ∧ 𝐶 ∈ On) → ∃g(g Fn 𝐶 ∧ ∀u ∈ 𝐶 (g‘u) = (𝐹‘(g ↾ u))))

Syntax hints:   → wi 4   ∧ wa 97   ∧ w3a 884  ∀wal 1240   = wceq 1242  ∃wex 1378   ∈ wcel 1390  {cab 2023  ∀wral 2300  ∃wrex 2301  Vcvv 2551   ∪ cun 2909  {csn 3367  ⟨cop 3370  Oncon0 4066   ↾ cres 4290  Fun wfun 4839   Fn wfn 4840  ‘cfv 4845

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bnd 1396  ax-4 1397  ax-13 1401  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-coll 3863  ax-sep 3866  ax-pow 3918  ax-pr 3935  ax-un 4136  ax-setind 4220

This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-fal 1248  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ne 2203  df-ral 2305  df-rex 2306  df-reu 2307  df-rab 2309  df-v 2553  df-sbc 2759  df-csb 2847  df-dif 2914  df-un 2916  df-in 2918  df-ss 2925  df-nul 3219  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-iun 3650  df-br 3756  df-opab 3810  df-mpt 3811  df-tr 3846  df-id 4021  df-iord 4069  df-on 4071  df-suc 4074  df-xp 4294  df-rel 4295  df-cnv 4296  df-co 4297  df-dm 4298  df-rn 4299  df-res 4300  df-ima 4301  df-iota 4810  df-fun 4847  df-fn 4848  df-f 4849  df-f1 4850  df-fo 4851  df-f1o 4852  df-fv 4853  df-recs 5861

This theorem is referenced by:  tfrlemi14d  5888  tfrexlem  5889