Theorem tfrlemi1 6135

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	⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))}
tfrlemisucfn.2	⊢ (𝜑 → ∀𝑥(Fun 𝐹 ∧ (𝐹‘𝑥) ∈ V))

Assertion

Ref	Expression
tfrlemi1	⊢ ((𝜑 ∧ 𝐶 ∈ On) → ∃𝑔(𝑔 Fn 𝐶 ∧ ∀𝑢 ∈ 𝐶 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢))))

Distinct variable groups:   𝑓,𝑔,𝑢,𝑥,𝑦,𝐴   𝑓,𝐹,𝑔,𝑢,𝑥,𝑦   𝜑,𝑦   𝐶,𝑔,𝑢   𝜑,𝑓

Allowed substitution hints:   𝜑(𝑥,𝑢,𝑔)   𝐶(𝑥,𝑦,𝑓)

Proof of Theorem tfrlemi1

Dummy variables 𝑒 ℎ 𝑘 𝑡 𝑣 𝑤 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpr 109	. . . . . . 7 ⊢ ((𝑧 = 𝑤 ∧ 𝑔 = 𝑘) → 𝑔 = 𝑘)
2		simpl 108	. . . . . . 7 ⊢ ((𝑧 = 𝑤 ∧ 𝑔 = 𝑘) → 𝑧 = 𝑤)
3	1, 2	fneq12d 5140	. . . . . 6 ⊢ ((𝑧 = 𝑤 ∧ 𝑔 = 𝑘) → (𝑔 Fn 𝑧 ↔ 𝑘 Fn 𝑤))
4	1	fveq1d 5342	. . . . . . . 8 ⊢ ((𝑧 = 𝑤 ∧ 𝑔 = 𝑘) → (𝑔‘𝑢) = (𝑘‘𝑢))
5	1	reseq1d 4744	. . . . . . . . 9 ⊢ ((𝑧 = 𝑤 ∧ 𝑔 = 𝑘) → (𝑔 ↾ 𝑢) = (𝑘 ↾ 𝑢))
6	5	fveq2d 5344	. . . . . . . 8 ⊢ ((𝑧 = 𝑤 ∧ 𝑔 = 𝑘) → (𝐹‘(𝑔 ↾ 𝑢)) = (𝐹‘(𝑘 ↾ 𝑢)))
7	4, 6	eqeq12d 2109	. . . . . . 7 ⊢ ((𝑧 = 𝑤 ∧ 𝑔 = 𝑘) → ((𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢)) ↔ (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢))))
8	2, 7	raleqbidv 2588	. . . . . 6 ⊢ ((𝑧 = 𝑤 ∧ 𝑔 = 𝑘) → (∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢)) ↔ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢))))
9	3, 8	anbi12d 458	. . . . 5 ⊢ ((𝑧 = 𝑤 ∧ 𝑔 = 𝑘) → ((𝑔 Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢))) ↔ (𝑘 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢)))))
10	9	cbvexdva 1859	. . . 4 ⊢ (𝑧 = 𝑤 → (∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢))) ↔ ∃𝑘(𝑘 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢)))))
11	10	imbi2d 229	. . 3 ⊢ (𝑧 = 𝑤 → ((𝜑 → ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢)))) ↔ (𝜑 → ∃𝑘(𝑘 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢))))))
12		fneq2 5137	. . . . . 6 ⊢ (𝑧 = 𝐶 → (𝑔 Fn 𝑧 ↔ 𝑔 Fn 𝐶))
13		raleq 2576	. . . . . 6 ⊢ (𝑧 = 𝐶 → (∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢)) ↔ ∀𝑢 ∈ 𝐶 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢))))
14	12, 13	anbi12d 458	. . . . 5 ⊢ (𝑧 = 𝐶 → ((𝑔 Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢))) ↔ (𝑔 Fn 𝐶 ∧ ∀𝑢 ∈ 𝐶 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢)))))
15	14	exbidv 1760	. . . 4 ⊢ (𝑧 = 𝐶 → (∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢))) ↔ ∃𝑔(𝑔 Fn 𝐶 ∧ ∀𝑢 ∈ 𝐶 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢)))))
16	15	imbi2d 229	. . 3 ⊢ (𝑧 = 𝐶 → ((𝜑 → ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢)))) ↔ (𝜑 → ∃𝑔(𝑔 Fn 𝐶 ∧ ∀𝑢 ∈ 𝐶 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢))))))
17		r19.21v 2462	. . . 4 ⊢ (∀𝑤 ∈ 𝑧 (𝜑 → ∃𝑘(𝑘 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢)))) ↔ (𝜑 → ∀𝑤 ∈ 𝑧 ∃𝑘(𝑘 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢)))))
18		tfrlemisucfn.1	. . . . . . . . 9 ⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))}
19	18	tfrlem3 6114	. . . . . . . 8 ⊢ 𝐴 = {𝑔 ∣ ∃𝑧 ∈ On (𝑔 Fn 𝑧 ∧ ∀𝑒 ∈ 𝑧 (𝑔‘𝑒) = (𝐹‘(𝑔 ↾ 𝑒)))}
20		tfrlemisucfn.2	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑥(Fun 𝐹 ∧ (𝐹‘𝑥) ∈ V))
21		fveq2 5340	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑧 → (𝐹‘𝑥) = (𝐹‘𝑧))
22	21	eleq1d 2163	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑧 → ((𝐹‘𝑥) ∈ V ↔ (𝐹‘𝑧) ∈ V))
23	22	anbi2d 453	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑧 → ((Fun 𝐹 ∧ (𝐹‘𝑥) ∈ V) ↔ (Fun 𝐹 ∧ (𝐹‘𝑧) ∈ V)))
24	23	cbvalv 1849	. . . . . . . . . 10 ⊢ (∀𝑥(Fun 𝐹 ∧ (𝐹‘𝑥) ∈ V) ↔ ∀𝑧(Fun 𝐹 ∧ (𝐹‘𝑧) ∈ V))
25	20, 24	sylib 121	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑧(Fun 𝐹 ∧ (𝐹‘𝑧) ∈ V))
26	25	adantr 271	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∃𝑘(𝑘 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢))))) → ∀𝑧(Fun 𝐹 ∧ (𝐹‘𝑧) ∈ V))
27		simpr 109	. . . . . . . . . . . . 13 ⊢ (((𝑡 = ℎ ∧ 𝑤 = 𝑣) ∧ 𝑘 = 𝑓) → 𝑘 = 𝑓)
28		simplr 498	. . . . . . . . . . . . 13 ⊢ (((𝑡 = ℎ ∧ 𝑤 = 𝑣) ∧ 𝑘 = 𝑓) → 𝑤 = 𝑣)
29	27, 28	fneq12d 5140	. . . . . . . . . . . 12 ⊢ (((𝑡 = ℎ ∧ 𝑤 = 𝑣) ∧ 𝑘 = 𝑓) → (𝑘 Fn 𝑤 ↔ 𝑓 Fn 𝑣))
30	27	eleq1d 2163	. . . . . . . . . . . 12 ⊢ (((𝑡 = ℎ ∧ 𝑤 = 𝑣) ∧ 𝑘 = 𝑓) → (𝑘 ∈ 𝐴 ↔ 𝑓 ∈ 𝐴))
31		simpll 497	. . . . . . . . . . . . 13 ⊢ (((𝑡 = ℎ ∧ 𝑤 = 𝑣) ∧ 𝑘 = 𝑓) → 𝑡 = ℎ)
32	27	fveq2d 5344	. . . . . . . . . . . . . . . 16 ⊢ (((𝑡 = ℎ ∧ 𝑤 = 𝑣) ∧ 𝑘 = 𝑓) → (𝐹‘𝑘) = (𝐹‘𝑓))
33	28, 32	opeq12d 3652	. . . . . . . . . . . . . . 15 ⊢ (((𝑡 = ℎ ∧ 𝑤 = 𝑣) ∧ 𝑘 = 𝑓) → ⟨𝑤, (𝐹‘𝑘)⟩ = ⟨𝑣, (𝐹‘𝑓)⟩)
34	33	sneqd 3479	. . . . . . . . . . . . . 14 ⊢ (((𝑡 = ℎ ∧ 𝑤 = 𝑣) ∧ 𝑘 = 𝑓) → {⟨𝑤, (𝐹‘𝑘)⟩} = {⟨𝑣, (𝐹‘𝑓)⟩})
35	27, 34	uneq12d 3170	. . . . . . . . . . . . 13 ⊢ (((𝑡 = ℎ ∧ 𝑤 = 𝑣) ∧ 𝑘 = 𝑓) → (𝑘 ∪ {⟨𝑤, (𝐹‘𝑘)⟩}) = (𝑓 ∪ {⟨𝑣, (𝐹‘𝑓)⟩}))
36	31, 35	eqeq12d 2109	. . . . . . . . . . . 12 ⊢ (((𝑡 = ℎ ∧ 𝑤 = 𝑣) ∧ 𝑘 = 𝑓) → (𝑡 = (𝑘 ∪ {⟨𝑤, (𝐹‘𝑘)⟩}) ↔ ℎ = (𝑓 ∪ {⟨𝑣, (𝐹‘𝑓)⟩})))
37	29, 30, 36	3anbi123d 1255	. . . . . . . . . . 11 ⊢ (((𝑡 = ℎ ∧ 𝑤 = 𝑣) ∧ 𝑘 = 𝑓) → ((𝑘 Fn 𝑤 ∧ 𝑘 ∈ 𝐴 ∧ 𝑡 = (𝑘 ∪ {⟨𝑤, (𝐹‘𝑘)⟩})) ↔ (𝑓 Fn 𝑣 ∧ 𝑓 ∈ 𝐴 ∧ ℎ = (𝑓 ∪ {⟨𝑣, (𝐹‘𝑓)⟩}))))
38	37	cbvexdva 1859	. . . . . . . . . 10 ⊢ ((𝑡 = ℎ ∧ 𝑤 = 𝑣) → (∃𝑘(𝑘 Fn 𝑤 ∧ 𝑘 ∈ 𝐴 ∧ 𝑡 = (𝑘 ∪ {⟨𝑤, (𝐹‘𝑘)⟩})) ↔ ∃𝑓(𝑓 Fn 𝑣 ∧ 𝑓 ∈ 𝐴 ∧ ℎ = (𝑓 ∪ {⟨𝑣, (𝐹‘𝑓)⟩}))))
39	38	cbvrexdva 2611	. . . . . . . . 9 ⊢ (𝑡 = ℎ → (∃𝑤 ∈ 𝑧 ∃𝑘(𝑘 Fn 𝑤 ∧ 𝑘 ∈ 𝐴 ∧ 𝑡 = (𝑘 ∪ {⟨𝑤, (𝐹‘𝑘)⟩})) ↔ ∃𝑣 ∈ 𝑧 ∃𝑓(𝑓 Fn 𝑣 ∧ 𝑓 ∈ 𝐴 ∧ ℎ = (𝑓 ∪ {⟨𝑣, (𝐹‘𝑓)⟩}))))
40	39	cbvabv 2218	. . . . . . . 8 ⊢ {𝑡 ∣ ∃𝑤 ∈ 𝑧 ∃𝑘(𝑘 Fn 𝑤 ∧ 𝑘 ∈ 𝐴 ∧ 𝑡 = (𝑘 ∪ {⟨𝑤, (𝐹‘𝑘)⟩}))} = {ℎ ∣ ∃𝑣 ∈ 𝑧 ∃𝑓(𝑓 Fn 𝑣 ∧ 𝑓 ∈ 𝐴 ∧ ℎ = (𝑓 ∪ {⟨𝑣, (𝐹‘𝑓)⟩}))}
41		simpl 108	. . . . . . . . 9 ⊢ ((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∃𝑘(𝑘 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢)))) → 𝑧 ∈ On)
42	41	adantl 272	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∃𝑘(𝑘 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢))))) → 𝑧 ∈ On)
43		simpr 109	. . . . . . . . . 10 ⊢ ((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∃𝑘(𝑘 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢)))) → ∀𝑤 ∈ 𝑧 ∃𝑘(𝑘 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢))))
44		simpr 109	. . . . . . . . . . . . . 14 ⊢ ((𝑤 = 𝑣 ∧ 𝑘 = 𝑓) → 𝑘 = 𝑓)
45		simpl 108	. . . . . . . . . . . . . 14 ⊢ ((𝑤 = 𝑣 ∧ 𝑘 = 𝑓) → 𝑤 = 𝑣)
46	44, 45	fneq12d 5140	. . . . . . . . . . . . 13 ⊢ ((𝑤 = 𝑣 ∧ 𝑘 = 𝑓) → (𝑘 Fn 𝑤 ↔ 𝑓 Fn 𝑣))
47		simplr 498	. . . . . . . . . . . . . . . 16 ⊢ (((𝑤 = 𝑣 ∧ 𝑘 = 𝑓) ∧ 𝑢 = 𝑦) → 𝑘 = 𝑓)
48		simpr 109	. . . . . . . . . . . . . . . 16 ⊢ (((𝑤 = 𝑣 ∧ 𝑘 = 𝑓) ∧ 𝑢 = 𝑦) → 𝑢 = 𝑦)
49	47, 48	fveq12d 5347	. . . . . . . . . . . . . . 15 ⊢ (((𝑤 = 𝑣 ∧ 𝑘 = 𝑓) ∧ 𝑢 = 𝑦) → (𝑘‘𝑢) = (𝑓‘𝑦))
50	47, 48	reseq12d 4746	. . . . . . . . . . . . . . . 16 ⊢ (((𝑤 = 𝑣 ∧ 𝑘 = 𝑓) ∧ 𝑢 = 𝑦) → (𝑘 ↾ 𝑢) = (𝑓 ↾ 𝑦))
51	50	fveq2d 5344	. . . . . . . . . . . . . . 15 ⊢ (((𝑤 = 𝑣 ∧ 𝑘 = 𝑓) ∧ 𝑢 = 𝑦) → (𝐹‘(𝑘 ↾ 𝑢)) = (𝐹‘(𝑓 ↾ 𝑦)))
52	49, 51	eqeq12d 2109	. . . . . . . . . . . . . 14 ⊢ (((𝑤 = 𝑣 ∧ 𝑘 = 𝑓) ∧ 𝑢 = 𝑦) → ((𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢)) ↔ (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))))
53		simpll 497	. . . . . . . . . . . . . 14 ⊢ (((𝑤 = 𝑣 ∧ 𝑘 = 𝑓) ∧ 𝑢 = 𝑦) → 𝑤 = 𝑣)
54	52, 53	cbvraldva2 2608	. . . . . . . . . . . . 13 ⊢ ((𝑤 = 𝑣 ∧ 𝑘 = 𝑓) → (∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢)) ↔ ∀𝑦 ∈ 𝑣 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))))
55	46, 54	anbi12d 458	. . . . . . . . . . . 12 ⊢ ((𝑤 = 𝑣 ∧ 𝑘 = 𝑓) → ((𝑘 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢))) ↔ (𝑓 Fn 𝑣 ∧ ∀𝑦 ∈ 𝑣 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))))
56	55	cbvexdva 1859	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑣 → (∃𝑘(𝑘 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢))) ↔ ∃𝑓(𝑓 Fn 𝑣 ∧ ∀𝑦 ∈ 𝑣 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))))
57	56	cbvralv 2604	. . . . . . . . . 10 ⊢ (∀𝑤 ∈ 𝑧 ∃𝑘(𝑘 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢))) ↔ ∀𝑣 ∈ 𝑧 ∃𝑓(𝑓 Fn 𝑣 ∧ ∀𝑦 ∈ 𝑣 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))))
58	43, 57	sylib 121	. . . . . . . . 9 ⊢ ((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∃𝑘(𝑘 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢)))) → ∀𝑣 ∈ 𝑧 ∃𝑓(𝑓 Fn 𝑣 ∧ ∀𝑦 ∈ 𝑣 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))))
59	58	adantl 272	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∃𝑘(𝑘 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢))))) → ∀𝑣 ∈ 𝑧 ∃𝑓(𝑓 Fn 𝑣 ∧ ∀𝑦 ∈ 𝑣 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))))
60	19, 26, 40, 42, 59	tfrlemiex 6134	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∃𝑘(𝑘 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢))))) → ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢))))
61	60	expr 368	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ On) → (∀𝑤 ∈ 𝑧 ∃𝑘(𝑘 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢))) → ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢)))))
62	61	expcom 115	. . . . 5 ⊢ (𝑧 ∈ On → (𝜑 → (∀𝑤 ∈ 𝑧 ∃𝑘(𝑘 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢))) → ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢))))))
63	62	a2d 26	. . . 4 ⊢ (𝑧 ∈ On → ((𝜑 → ∀𝑤 ∈ 𝑧 ∃𝑘(𝑘 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢)))) → (𝜑 → ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢))))))
64	17, 63	syl5bi 151	. . 3 ⊢ (𝑧 ∈ On → (∀𝑤 ∈ 𝑧 (𝜑 → ∃𝑘(𝑘 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢)))) → (𝜑 → ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢))))))
65	11, 16, 64	tfis3 4429	. 2 ⊢ (𝐶 ∈ On → (𝜑 → ∃𝑔(𝑔 Fn 𝐶 ∧ ∀𝑢 ∈ 𝐶 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢)))))
66	65	impcom 124	1 ⊢ ((𝜑 ∧ 𝐶 ∈ On) → ∃𝑔(𝑔 Fn 𝐶 ∧ ∀𝑢 ∈ 𝐶 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢))))

Syntax hints:   → wi 4   ∧ wa 103   ∧ w3a 927  ∀wal 1294   = wceq 1296  ∃wex 1433   ∈ wcel 1445  {cab 2081  ∀wral 2370  ∃wrex 2371  Vcvv 2633   ∪ cun 3011  {csn 3466  ⟨cop 3469  Oncon0 4214   ↾ cres 4469  Fun wfun 5043   Fn wfn 5044  ‘cfv 5049

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 582  ax-in2 583  ax-io 668  ax-5 1388  ax-7 1389  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-8 1447  ax-10 1448  ax-11 1449  ax-i12 1450  ax-bndl 1451  ax-4 1452  ax-13 1456  ax-14 1457  ax-17 1471  ax-i9 1475  ax-ial 1479  ax-i5r 1480  ax-ext 2077  ax-coll 3975  ax-sep 3978  ax-pow 4030  ax-pr 4060  ax-un 4284  ax-setind 4381

This theorem depends on definitions:  df-bi 116  df-3an 929  df-tru 1299  df-fal 1302  df-nf 1402  df-sb 1700  df-eu 1958  df-mo 1959  df-clab 2082  df-cleq 2088  df-clel 2091  df-nfc 2224  df-ne 2263  df-ral 2375  df-rex 2376  df-reu 2377  df-rab 2379  df-v 2635  df-sbc 2855  df-csb 2948  df-dif 3015  df-un 3017  df-in 3019  df-ss 3026  df-nul 3303  df-pw 3451  df-sn 3472  df-pr 3473  df-op 3475  df-uni 3676  df-iun 3754  df-br 3868  df-opab 3922  df-mpt 3923  df-tr 3959  df-id 4144  df-iord 4217  df-on 4219  df-suc 4222  df-xp 4473  df-rel 4474  df-cnv 4475  df-co 4476  df-dm 4477  df-rn 4478  df-res 4479  df-ima 4480  df-iota 5014  df-fun 5051  df-fn 5052  df-f 5053  df-f1 5054  df-fo 5055  df-f1o 5056  df-fv 5057  df-recs 6108

This theorem is referenced by:  tfrlemi14d  6136  tfrexlem  6137