Theorem tfrlemi1 6311

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 5290	. . . . . 6 ⊢ ((𝑧 = 𝑤 ∧ 𝑔 = 𝑘) → (𝑔 Fn 𝑧 ↔ 𝑘 Fn 𝑤))
4	1	fveq1d 5498	. . . . . . . 8 ⊢ ((𝑧 = 𝑤 ∧ 𝑔 = 𝑘) → (𝑔‘𝑢) = (𝑘‘𝑢))
5	1	reseq1d 4890	. . . . . . . . 9 ⊢ ((𝑧 = 𝑤 ∧ 𝑔 = 𝑘) → (𝑔 ↾ 𝑢) = (𝑘 ↾ 𝑢))
6	5	fveq2d 5500	. . . . . . . 8 ⊢ ((𝑧 = 𝑤 ∧ 𝑔 = 𝑘) → (𝐹‘(𝑔 ↾ 𝑢)) = (𝐹‘(𝑘 ↾ 𝑢)))
7	4, 6	eqeq12d 2185	. . . . . . 7 ⊢ ((𝑧 = 𝑤 ∧ 𝑔 = 𝑘) → ((𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢)) ↔ (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢))))
8	2, 7	raleqbidv 2677	. . . . . 6 ⊢ ((𝑧 = 𝑤 ∧ 𝑔 = 𝑘) → (∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢)) ↔ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢))))
9	3, 8	anbi12d 470	. . . . 5 ⊢ ((𝑧 = 𝑤 ∧ 𝑔 = 𝑘) → ((𝑔 Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢))) ↔ (𝑘 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢)))))
10	9	cbvexdva 1922	. . . 4 ⊢ (𝑧 = 𝑤 → (∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢))) ↔ ∃𝑘(𝑘 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢)))))
11	10	imbi2d 229	. . 3 ⊢ (𝑧 = 𝑤 → ((𝜑 → ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢)))) ↔ (𝜑 → ∃𝑘(𝑘 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢))))))
12		fneq2 5287	. . . . . 6 ⊢ (𝑧 = 𝐶 → (𝑔 Fn 𝑧 ↔ 𝑔 Fn 𝐶))
13		raleq 2665	. . . . . 6 ⊢ (𝑧 = 𝐶 → (∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢)) ↔ ∀𝑢 ∈ 𝐶 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢))))
14	12, 13	anbi12d 470	. . . . 5 ⊢ (𝑧 = 𝐶 → ((𝑔 Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢))) ↔ (𝑔 Fn 𝐶 ∧ ∀𝑢 ∈ 𝐶 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢)))))
15	14	exbidv 1818	. . . 4 ⊢ (𝑧 = 𝐶 → (∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢))) ↔ ∃𝑔(𝑔 Fn 𝐶 ∧ ∀𝑢 ∈ 𝐶 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢)))))
16	15	imbi2d 229	. . 3 ⊢ (𝑧 = 𝐶 → ((𝜑 → ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢)))) ↔ (𝜑 → ∃𝑔(𝑔 Fn 𝐶 ∧ ∀𝑢 ∈ 𝐶 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢))))))
17		r19.21v 2547	. . . 4 ⊢ (∀𝑤 ∈ 𝑧 (𝜑 → ∃𝑘(𝑘 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢)))) ↔ (𝜑 → ∀𝑤 ∈ 𝑧 ∃𝑘(𝑘 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢)))))
18		tfrlemisucfn.1	. . . . . . . . 9 ⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))}
19	18	tfrlem3 6290	. . . . . . . 8 ⊢ 𝐴 = {𝑔 ∣ ∃𝑧 ∈ On (𝑔 Fn 𝑧 ∧ ∀𝑒 ∈ 𝑧 (𝑔‘𝑒) = (𝐹‘(𝑔 ↾ 𝑒)))}
20		tfrlemisucfn.2	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑥(Fun 𝐹 ∧ (𝐹‘𝑥) ∈ V))
21		fveq2 5496	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑧 → (𝐹‘𝑥) = (𝐹‘𝑧))
22	21	eleq1d 2239	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑧 → ((𝐹‘𝑥) ∈ V ↔ (𝐹‘𝑧) ∈ V))
23	22	anbi2d 461	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑧 → ((Fun 𝐹 ∧ (𝐹‘𝑥) ∈ V) ↔ (Fun 𝐹 ∧ (𝐹‘𝑧) ∈ V)))
24	23	cbvalv 1910	. . . . . . . . . 10 ⊢ (∀𝑥(Fun 𝐹 ∧ (𝐹‘𝑥) ∈ V) ↔ ∀𝑧(Fun 𝐹 ∧ (𝐹‘𝑧) ∈ V))
25	20, 24	sylib 121	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑧(Fun 𝐹 ∧ (𝐹‘𝑧) ∈ V))
26	25	adantr 274	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∃𝑘(𝑘 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢))))) → ∀𝑧(Fun 𝐹 ∧ (𝐹‘𝑧) ∈ V))
27		simpr 109	. . . . . . . . . . . . 13 ⊢ (((𝑡 = ℎ ∧ 𝑤 = 𝑣) ∧ 𝑘 = 𝑓) → 𝑘 = 𝑓)
28		simplr 525	. . . . . . . . . . . . 13 ⊢ (((𝑡 = ℎ ∧ 𝑤 = 𝑣) ∧ 𝑘 = 𝑓) → 𝑤 = 𝑣)
29	27, 28	fneq12d 5290	. . . . . . . . . . . 12 ⊢ (((𝑡 = ℎ ∧ 𝑤 = 𝑣) ∧ 𝑘 = 𝑓) → (𝑘 Fn 𝑤 ↔ 𝑓 Fn 𝑣))
30	27	eleq1d 2239	. . . . . . . . . . . 12 ⊢ (((𝑡 = ℎ ∧ 𝑤 = 𝑣) ∧ 𝑘 = 𝑓) → (𝑘 ∈ 𝐴 ↔ 𝑓 ∈ 𝐴))
31		simpll 524	. . . . . . . . . . . . 13 ⊢ (((𝑡 = ℎ ∧ 𝑤 = 𝑣) ∧ 𝑘 = 𝑓) → 𝑡 = ℎ)
32	27	fveq2d 5500	. . . . . . . . . . . . . . . 16 ⊢ (((𝑡 = ℎ ∧ 𝑤 = 𝑣) ∧ 𝑘 = 𝑓) → (𝐹‘𝑘) = (𝐹‘𝑓))
33	28, 32	opeq12d 3773	. . . . . . . . . . . . . . 15 ⊢ (((𝑡 = ℎ ∧ 𝑤 = 𝑣) ∧ 𝑘 = 𝑓) → ⟨𝑤, (𝐹‘𝑘)⟩ = ⟨𝑣, (𝐹‘𝑓)⟩)
34	33	sneqd 3596	. . . . . . . . . . . . . 14 ⊢ (((𝑡 = ℎ ∧ 𝑤 = 𝑣) ∧ 𝑘 = 𝑓) → {⟨𝑤, (𝐹‘𝑘)⟩} = {⟨𝑣, (𝐹‘𝑓)⟩})
35	27, 34	uneq12d 3282	. . . . . . . . . . . . 13 ⊢ (((𝑡 = ℎ ∧ 𝑤 = 𝑣) ∧ 𝑘 = 𝑓) → (𝑘 ∪ {⟨𝑤, (𝐹‘𝑘)⟩}) = (𝑓 ∪ {⟨𝑣, (𝐹‘𝑓)⟩}))
36	31, 35	eqeq12d 2185	. . . . . . . . . . . 12 ⊢ (((𝑡 = ℎ ∧ 𝑤 = 𝑣) ∧ 𝑘 = 𝑓) → (𝑡 = (𝑘 ∪ {⟨𝑤, (𝐹‘𝑘)⟩}) ↔ ℎ = (𝑓 ∪ {⟨𝑣, (𝐹‘𝑓)⟩})))
37	29, 30, 36	3anbi123d 1307	. . . . . . . . . . 11 ⊢ (((𝑡 = ℎ ∧ 𝑤 = 𝑣) ∧ 𝑘 = 𝑓) → ((𝑘 Fn 𝑤 ∧ 𝑘 ∈ 𝐴 ∧ 𝑡 = (𝑘 ∪ {⟨𝑤, (𝐹‘𝑘)⟩})) ↔ (𝑓 Fn 𝑣 ∧ 𝑓 ∈ 𝐴 ∧ ℎ = (𝑓 ∪ {⟨𝑣, (𝐹‘𝑓)⟩}))))
38	37	cbvexdva 1922	. . . . . . . . . 10 ⊢ ((𝑡 = ℎ ∧ 𝑤 = 𝑣) → (∃𝑘(𝑘 Fn 𝑤 ∧ 𝑘 ∈ 𝐴 ∧ 𝑡 = (𝑘 ∪ {⟨𝑤, (𝐹‘𝑘)⟩})) ↔ ∃𝑓(𝑓 Fn 𝑣 ∧ 𝑓 ∈ 𝐴 ∧ ℎ = (𝑓 ∪ {⟨𝑣, (𝐹‘𝑓)⟩}))))
39	38	cbvrexdva 2706	. . . . . . . . 9 ⊢ (𝑡 = ℎ → (∃𝑤 ∈ 𝑧 ∃𝑘(𝑘 Fn 𝑤 ∧ 𝑘 ∈ 𝐴 ∧ 𝑡 = (𝑘 ∪ {⟨𝑤, (𝐹‘𝑘)⟩})) ↔ ∃𝑣 ∈ 𝑧 ∃𝑓(𝑓 Fn 𝑣 ∧ 𝑓 ∈ 𝐴 ∧ ℎ = (𝑓 ∪ {⟨𝑣, (𝐹‘𝑓)⟩}))))
40	39	cbvabv 2295	. . . . . . . 8 ⊢ {𝑡 ∣ ∃𝑤 ∈ 𝑧 ∃𝑘(𝑘 Fn 𝑤 ∧ 𝑘 ∈ 𝐴 ∧ 𝑡 = (𝑘 ∪ {⟨𝑤, (𝐹‘𝑘)⟩}))} = {ℎ ∣ ∃𝑣 ∈ 𝑧 ∃𝑓(𝑓 Fn 𝑣 ∧ 𝑓 ∈ 𝐴 ∧ ℎ = (𝑓 ∪ {⟨𝑣, (𝐹‘𝑓)⟩}))}
41		simpl 108	. . . . . . . . 9 ⊢ ((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∃𝑘(𝑘 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢)))) → 𝑧 ∈ On)
42	41	adantl 275	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∃𝑘(𝑘 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢))))) → 𝑧 ∈ On)
43		simpr 109	. . . . . . . . . 10 ⊢ ((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∃𝑘(𝑘 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢)))) → ∀𝑤 ∈ 𝑧 ∃𝑘(𝑘 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢))))
44		simpr 109	. . . . . . . . . . . . . 14 ⊢ ((𝑤 = 𝑣 ∧ 𝑘 = 𝑓) → 𝑘 = 𝑓)
45		simpl 108	. . . . . . . . . . . . . 14 ⊢ ((𝑤 = 𝑣 ∧ 𝑘 = 𝑓) → 𝑤 = 𝑣)
46	44, 45	fneq12d 5290	. . . . . . . . . . . . 13 ⊢ ((𝑤 = 𝑣 ∧ 𝑘 = 𝑓) → (𝑘 Fn 𝑤 ↔ 𝑓 Fn 𝑣))
47		simplr 525	. . . . . . . . . . . . . . . 16 ⊢ (((𝑤 = 𝑣 ∧ 𝑘 = 𝑓) ∧ 𝑢 = 𝑦) → 𝑘 = 𝑓)
48		simpr 109	. . . . . . . . . . . . . . . 16 ⊢ (((𝑤 = 𝑣 ∧ 𝑘 = 𝑓) ∧ 𝑢 = 𝑦) → 𝑢 = 𝑦)
49	47, 48	fveq12d 5503	. . . . . . . . . . . . . . 15 ⊢ (((𝑤 = 𝑣 ∧ 𝑘 = 𝑓) ∧ 𝑢 = 𝑦) → (𝑘‘𝑢) = (𝑓‘𝑦))
50	47, 48	reseq12d 4892	. . . . . . . . . . . . . . . 16 ⊢ (((𝑤 = 𝑣 ∧ 𝑘 = 𝑓) ∧ 𝑢 = 𝑦) → (𝑘 ↾ 𝑢) = (𝑓 ↾ 𝑦))
51	50	fveq2d 5500	. . . . . . . . . . . . . . 15 ⊢ (((𝑤 = 𝑣 ∧ 𝑘 = 𝑓) ∧ 𝑢 = 𝑦) → (𝐹‘(𝑘 ↾ 𝑢)) = (𝐹‘(𝑓 ↾ 𝑦)))
52	49, 51	eqeq12d 2185	. . . . . . . . . . . . . 14 ⊢ (((𝑤 = 𝑣 ∧ 𝑘 = 𝑓) ∧ 𝑢 = 𝑦) → ((𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢)) ↔ (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))))
53		simpll 524	. . . . . . . . . . . . . 14 ⊢ (((𝑤 = 𝑣 ∧ 𝑘 = 𝑓) ∧ 𝑢 = 𝑦) → 𝑤 = 𝑣)
54	52, 53	cbvraldva2 2703	. . . . . . . . . . . . 13 ⊢ ((𝑤 = 𝑣 ∧ 𝑘 = 𝑓) → (∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢)) ↔ ∀𝑦 ∈ 𝑣 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))))
55	46, 54	anbi12d 470	. . . . . . . . . . . 12 ⊢ ((𝑤 = 𝑣 ∧ 𝑘 = 𝑓) → ((𝑘 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢))) ↔ (𝑓 Fn 𝑣 ∧ ∀𝑦 ∈ 𝑣 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))))
56	55	cbvexdva 1922	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑣 → (∃𝑘(𝑘 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢))) ↔ ∃𝑓(𝑓 Fn 𝑣 ∧ ∀𝑦 ∈ 𝑣 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))))
57	56	cbvralv 2696	. . . . . . . . . 10 ⊢ (∀𝑤 ∈ 𝑧 ∃𝑘(𝑘 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢))) ↔ ∀𝑣 ∈ 𝑧 ∃𝑓(𝑓 Fn 𝑣 ∧ ∀𝑦 ∈ 𝑣 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))))
58	43, 57	sylib 121	. . . . . . . . 9 ⊢ ((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∃𝑘(𝑘 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢)))) → ∀𝑣 ∈ 𝑧 ∃𝑓(𝑓 Fn 𝑣 ∧ ∀𝑦 ∈ 𝑣 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))))
59	58	adantl 275	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∃𝑘(𝑘 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢))))) → ∀𝑣 ∈ 𝑧 ∃𝑓(𝑓 Fn 𝑣 ∧ ∀𝑦 ∈ 𝑣 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))))
60	19, 26, 40, 42, 59	tfrlemiex 6310	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∃𝑘(𝑘 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢))))) → ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢))))
61	60	expr 373	. . . . . 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 4570	. 2 ⊢ (𝐶 ∈ On → (𝜑 → ∃𝑔(𝑔 Fn 𝐶 ∧ ∀𝑢 ∈ 𝐶 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢)))))
66	65	impcom 124	1 ⊢ ((𝜑 ∧ 𝐶 ∈ On) → ∃𝑔(𝑔 Fn 𝐶 ∧ ∀𝑢 ∈ 𝐶 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢))))

Syntax hints:   → wi 4   ∧ wa 103   ∧ w3a 973  ∀wal 1346   = wceq 1348  ∃wex 1485   ∈ wcel 2141  {cab 2156  ∀wral 2448  ∃wrex 2449  Vcvv 2730   ∪ cun 3119  {csn 3583  ⟨cop 3586  Oncon0 4348   ↾ cres 4613  Fun wfun 5192   Fn wfn 5193  ‘cfv 5198

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 609  ax-in2 610  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-13 2143  ax-14 2144  ax-ext 2152  ax-coll 4104  ax-sep 4107  ax-pow 4160  ax-pr 4194  ax-un 4418  ax-setind 4521

This theorem depends on definitions:  df-bi 116  df-3an 975  df-tru 1351  df-fal 1354  df-nf 1454  df-sb 1756  df-eu 2022  df-mo 2023  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ne 2341  df-ral 2453  df-rex 2454  df-reu 2455  df-rab 2457  df-v 2732  df-sbc 2956  df-csb 3050  df-dif 3123  df-un 3125  df-in 3127  df-ss 3134  df-nul 3415  df-pw 3568  df-sn 3589  df-pr 3590  df-op 3592  df-uni 3797  df-iun 3875  df-br 3990  df-opab 4051  df-mpt 4052  df-tr 4088  df-id 4278  df-iord 4351  df-on 4353  df-suc 4356  df-xp 4617  df-rel 4618  df-cnv 4619  df-co 4620  df-dm 4621  df-rn 4622  df-res 4623  df-ima 4624  df-iota 5160  df-fun 5200  df-fn 5201  df-f 5202  df-f1 5203  df-fo 5204  df-f1o 5205  df-fv 5206  df-recs 6284

This theorem is referenced by:  tfrlemi14d  6312  tfrexlem  6313