Theorem tfrlemi1 6336

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 110	. . . . . . 7 ⊢ ((𝑧 = 𝑤 ∧ 𝑔 = 𝑘) → 𝑔 = 𝑘)
2		simpl 109	. . . . . . 7 ⊢ ((𝑧 = 𝑤 ∧ 𝑔 = 𝑘) → 𝑧 = 𝑤)
3	1, 2	fneq12d 5310	. . . . . 6 ⊢ ((𝑧 = 𝑤 ∧ 𝑔 = 𝑘) → (𝑔 Fn 𝑧 ↔ 𝑘 Fn 𝑤))
4	1	fveq1d 5519	. . . . . . . 8 ⊢ ((𝑧 = 𝑤 ∧ 𝑔 = 𝑘) → (𝑔‘𝑢) = (𝑘‘𝑢))
5	1	reseq1d 4908	. . . . . . . . 9 ⊢ ((𝑧 = 𝑤 ∧ 𝑔 = 𝑘) → (𝑔 ↾ 𝑢) = (𝑘 ↾ 𝑢))
6	5	fveq2d 5521	. . . . . . . 8 ⊢ ((𝑧 = 𝑤 ∧ 𝑔 = 𝑘) → (𝐹‘(𝑔 ↾ 𝑢)) = (𝐹‘(𝑘 ↾ 𝑢)))
7	4, 6	eqeq12d 2192	. . . . . . 7 ⊢ ((𝑧 = 𝑤 ∧ 𝑔 = 𝑘) → ((𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢)) ↔ (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢))))
8	2, 7	raleqbidv 2685	. . . . . 6 ⊢ ((𝑧 = 𝑤 ∧ 𝑔 = 𝑘) → (∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢)) ↔ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢))))
9	3, 8	anbi12d 473	. . . . 5 ⊢ ((𝑧 = 𝑤 ∧ 𝑔 = 𝑘) → ((𝑔 Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢))) ↔ (𝑘 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢)))))
10	9	cbvexdva 1929	. . . 4 ⊢ (𝑧 = 𝑤 → (∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢))) ↔ ∃𝑘(𝑘 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢)))))
11	10	imbi2d 230	. . 3 ⊢ (𝑧 = 𝑤 → ((𝜑 → ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢)))) ↔ (𝜑 → ∃𝑘(𝑘 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢))))))
12		fneq2 5307	. . . . . 6 ⊢ (𝑧 = 𝐶 → (𝑔 Fn 𝑧 ↔ 𝑔 Fn 𝐶))
13		raleq 2673	. . . . . 6 ⊢ (𝑧 = 𝐶 → (∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢)) ↔ ∀𝑢 ∈ 𝐶 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢))))
14	12, 13	anbi12d 473	. . . . 5 ⊢ (𝑧 = 𝐶 → ((𝑔 Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢))) ↔ (𝑔 Fn 𝐶 ∧ ∀𝑢 ∈ 𝐶 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢)))))
15	14	exbidv 1825	. . . 4 ⊢ (𝑧 = 𝐶 → (∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢))) ↔ ∃𝑔(𝑔 Fn 𝐶 ∧ ∀𝑢 ∈ 𝐶 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢)))))
16	15	imbi2d 230	. . 3 ⊢ (𝑧 = 𝐶 → ((𝜑 → ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢)))) ↔ (𝜑 → ∃𝑔(𝑔 Fn 𝐶 ∧ ∀𝑢 ∈ 𝐶 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢))))))
17		r19.21v 2554	. . . 4 ⊢ (∀𝑤 ∈ 𝑧 (𝜑 → ∃𝑘(𝑘 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢)))) ↔ (𝜑 → ∀𝑤 ∈ 𝑧 ∃𝑘(𝑘 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢)))))
18		tfrlemisucfn.1	. . . . . . . . 9 ⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))}
19	18	tfrlem3 6315	. . . . . . . 8 ⊢ 𝐴 = {𝑔 ∣ ∃𝑧 ∈ On (𝑔 Fn 𝑧 ∧ ∀𝑒 ∈ 𝑧 (𝑔‘𝑒) = (𝐹‘(𝑔 ↾ 𝑒)))}
20		tfrlemisucfn.2	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑥(Fun 𝐹 ∧ (𝐹‘𝑥) ∈ V))
21		fveq2 5517	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑧 → (𝐹‘𝑥) = (𝐹‘𝑧))
22	21	eleq1d 2246	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑧 → ((𝐹‘𝑥) ∈ V ↔ (𝐹‘𝑧) ∈ V))
23	22	anbi2d 464	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑧 → ((Fun 𝐹 ∧ (𝐹‘𝑥) ∈ V) ↔ (Fun 𝐹 ∧ (𝐹‘𝑧) ∈ V)))
24	23	cbvalv 1917	. . . . . . . . . 10 ⊢ (∀𝑥(Fun 𝐹 ∧ (𝐹‘𝑥) ∈ V) ↔ ∀𝑧(Fun 𝐹 ∧ (𝐹‘𝑧) ∈ V))
25	20, 24	sylib 122	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑧(Fun 𝐹 ∧ (𝐹‘𝑧) ∈ V))
26	25	adantr 276	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∃𝑘(𝑘 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢))))) → ∀𝑧(Fun 𝐹 ∧ (𝐹‘𝑧) ∈ V))
27		simpr 110	. . . . . . . . . . . . 13 ⊢ (((𝑡 = ℎ ∧ 𝑤 = 𝑣) ∧ 𝑘 = 𝑓) → 𝑘 = 𝑓)
28		simplr 528	. . . . . . . . . . . . 13 ⊢ (((𝑡 = ℎ ∧ 𝑤 = 𝑣) ∧ 𝑘 = 𝑓) → 𝑤 = 𝑣)
29	27, 28	fneq12d 5310	. . . . . . . . . . . 12 ⊢ (((𝑡 = ℎ ∧ 𝑤 = 𝑣) ∧ 𝑘 = 𝑓) → (𝑘 Fn 𝑤 ↔ 𝑓 Fn 𝑣))
30	27	eleq1d 2246	. . . . . . . . . . . 12 ⊢ (((𝑡 = ℎ ∧ 𝑤 = 𝑣) ∧ 𝑘 = 𝑓) → (𝑘 ∈ 𝐴 ↔ 𝑓 ∈ 𝐴))
31		simpll 527	. . . . . . . . . . . . 13 ⊢ (((𝑡 = ℎ ∧ 𝑤 = 𝑣) ∧ 𝑘 = 𝑓) → 𝑡 = ℎ)
32	27	fveq2d 5521	. . . . . . . . . . . . . . . 16 ⊢ (((𝑡 = ℎ ∧ 𝑤 = 𝑣) ∧ 𝑘 = 𝑓) → (𝐹‘𝑘) = (𝐹‘𝑓))
33	28, 32	opeq12d 3788	. . . . . . . . . . . . . . 15 ⊢ (((𝑡 = ℎ ∧ 𝑤 = 𝑣) ∧ 𝑘 = 𝑓) → ⟨𝑤, (𝐹‘𝑘)⟩ = ⟨𝑣, (𝐹‘𝑓)⟩)
34	33	sneqd 3607	. . . . . . . . . . . . . 14 ⊢ (((𝑡 = ℎ ∧ 𝑤 = 𝑣) ∧ 𝑘 = 𝑓) → {⟨𝑤, (𝐹‘𝑘)⟩} = {⟨𝑣, (𝐹‘𝑓)⟩})
35	27, 34	uneq12d 3292	. . . . . . . . . . . . 13 ⊢ (((𝑡 = ℎ ∧ 𝑤 = 𝑣) ∧ 𝑘 = 𝑓) → (𝑘 ∪ {⟨𝑤, (𝐹‘𝑘)⟩}) = (𝑓 ∪ {⟨𝑣, (𝐹‘𝑓)⟩}))
36	31, 35	eqeq12d 2192	. . . . . . . . . . . 12 ⊢ (((𝑡 = ℎ ∧ 𝑤 = 𝑣) ∧ 𝑘 = 𝑓) → (𝑡 = (𝑘 ∪ {⟨𝑤, (𝐹‘𝑘)⟩}) ↔ ℎ = (𝑓 ∪ {⟨𝑣, (𝐹‘𝑓)⟩})))
37	29, 30, 36	3anbi123d 1312	. . . . . . . . . . 11 ⊢ (((𝑡 = ℎ ∧ 𝑤 = 𝑣) ∧ 𝑘 = 𝑓) → ((𝑘 Fn 𝑤 ∧ 𝑘 ∈ 𝐴 ∧ 𝑡 = (𝑘 ∪ {⟨𝑤, (𝐹‘𝑘)⟩})) ↔ (𝑓 Fn 𝑣 ∧ 𝑓 ∈ 𝐴 ∧ ℎ = (𝑓 ∪ {⟨𝑣, (𝐹‘𝑓)⟩}))))
38	37	cbvexdva 1929	. . . . . . . . . 10 ⊢ ((𝑡 = ℎ ∧ 𝑤 = 𝑣) → (∃𝑘(𝑘 Fn 𝑤 ∧ 𝑘 ∈ 𝐴 ∧ 𝑡 = (𝑘 ∪ {⟨𝑤, (𝐹‘𝑘)⟩})) ↔ ∃𝑓(𝑓 Fn 𝑣 ∧ 𝑓 ∈ 𝐴 ∧ ℎ = (𝑓 ∪ {⟨𝑣, (𝐹‘𝑓)⟩}))))
39	38	cbvrexdva 2715	. . . . . . . . 9 ⊢ (𝑡 = ℎ → (∃𝑤 ∈ 𝑧 ∃𝑘(𝑘 Fn 𝑤 ∧ 𝑘 ∈ 𝐴 ∧ 𝑡 = (𝑘 ∪ {⟨𝑤, (𝐹‘𝑘)⟩})) ↔ ∃𝑣 ∈ 𝑧 ∃𝑓(𝑓 Fn 𝑣 ∧ 𝑓 ∈ 𝐴 ∧ ℎ = (𝑓 ∪ {⟨𝑣, (𝐹‘𝑓)⟩}))))
40	39	cbvabv 2302	. . . . . . . 8 ⊢ {𝑡 ∣ ∃𝑤 ∈ 𝑧 ∃𝑘(𝑘 Fn 𝑤 ∧ 𝑘 ∈ 𝐴 ∧ 𝑡 = (𝑘 ∪ {⟨𝑤, (𝐹‘𝑘)⟩}))} = {ℎ ∣ ∃𝑣 ∈ 𝑧 ∃𝑓(𝑓 Fn 𝑣 ∧ 𝑓 ∈ 𝐴 ∧ ℎ = (𝑓 ∪ {⟨𝑣, (𝐹‘𝑓)⟩}))}
41		simpl 109	. . . . . . . . 9 ⊢ ((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∃𝑘(𝑘 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢)))) → 𝑧 ∈ On)
42	41	adantl 277	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∃𝑘(𝑘 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢))))) → 𝑧 ∈ On)
43		simpr 110	. . . . . . . . . 10 ⊢ ((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∃𝑘(𝑘 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢)))) → ∀𝑤 ∈ 𝑧 ∃𝑘(𝑘 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢))))
44		simpr 110	. . . . . . . . . . . . . 14 ⊢ ((𝑤 = 𝑣 ∧ 𝑘 = 𝑓) → 𝑘 = 𝑓)
45		simpl 109	. . . . . . . . . . . . . 14 ⊢ ((𝑤 = 𝑣 ∧ 𝑘 = 𝑓) → 𝑤 = 𝑣)
46	44, 45	fneq12d 5310	. . . . . . . . . . . . 13 ⊢ ((𝑤 = 𝑣 ∧ 𝑘 = 𝑓) → (𝑘 Fn 𝑤 ↔ 𝑓 Fn 𝑣))
47		simplr 528	. . . . . . . . . . . . . . . 16 ⊢ (((𝑤 = 𝑣 ∧ 𝑘 = 𝑓) ∧ 𝑢 = 𝑦) → 𝑘 = 𝑓)
48		simpr 110	. . . . . . . . . . . . . . . 16 ⊢ (((𝑤 = 𝑣 ∧ 𝑘 = 𝑓) ∧ 𝑢 = 𝑦) → 𝑢 = 𝑦)
49	47, 48	fveq12d 5524	. . . . . . . . . . . . . . 15 ⊢ (((𝑤 = 𝑣 ∧ 𝑘 = 𝑓) ∧ 𝑢 = 𝑦) → (𝑘‘𝑢) = (𝑓‘𝑦))
50	47, 48	reseq12d 4910	. . . . . . . . . . . . . . . 16 ⊢ (((𝑤 = 𝑣 ∧ 𝑘 = 𝑓) ∧ 𝑢 = 𝑦) → (𝑘 ↾ 𝑢) = (𝑓 ↾ 𝑦))
51	50	fveq2d 5521	. . . . . . . . . . . . . . 15 ⊢ (((𝑤 = 𝑣 ∧ 𝑘 = 𝑓) ∧ 𝑢 = 𝑦) → (𝐹‘(𝑘 ↾ 𝑢)) = (𝐹‘(𝑓 ↾ 𝑦)))
52	49, 51	eqeq12d 2192	. . . . . . . . . . . . . 14 ⊢ (((𝑤 = 𝑣 ∧ 𝑘 = 𝑓) ∧ 𝑢 = 𝑦) → ((𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢)) ↔ (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))))
53		simpll 527	. . . . . . . . . . . . . 14 ⊢ (((𝑤 = 𝑣 ∧ 𝑘 = 𝑓) ∧ 𝑢 = 𝑦) → 𝑤 = 𝑣)
54	52, 53	cbvraldva2 2712	. . . . . . . . . . . . 13 ⊢ ((𝑤 = 𝑣 ∧ 𝑘 = 𝑓) → (∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢)) ↔ ∀𝑦 ∈ 𝑣 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))))
55	46, 54	anbi12d 473	. . . . . . . . . . . 12 ⊢ ((𝑤 = 𝑣 ∧ 𝑘 = 𝑓) → ((𝑘 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢))) ↔ (𝑓 Fn 𝑣 ∧ ∀𝑦 ∈ 𝑣 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))))
56	55	cbvexdva 1929	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑣 → (∃𝑘(𝑘 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢))) ↔ ∃𝑓(𝑓 Fn 𝑣 ∧ ∀𝑦 ∈ 𝑣 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))))
57	56	cbvralv 2705	. . . . . . . . . 10 ⊢ (∀𝑤 ∈ 𝑧 ∃𝑘(𝑘 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢))) ↔ ∀𝑣 ∈ 𝑧 ∃𝑓(𝑓 Fn 𝑣 ∧ ∀𝑦 ∈ 𝑣 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))))
58	43, 57	sylib 122	. . . . . . . . 9 ⊢ ((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∃𝑘(𝑘 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢)))) → ∀𝑣 ∈ 𝑧 ∃𝑓(𝑓 Fn 𝑣 ∧ ∀𝑦 ∈ 𝑣 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))))
59	58	adantl 277	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∃𝑘(𝑘 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢))))) → ∀𝑣 ∈ 𝑧 ∃𝑓(𝑓 Fn 𝑣 ∧ ∀𝑦 ∈ 𝑣 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))))
60	19, 26, 40, 42, 59	tfrlemiex 6335	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∃𝑘(𝑘 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢))))) → ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢))))
61	60	expr 375	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ On) → (∀𝑤 ∈ 𝑧 ∃𝑘(𝑘 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢))) → ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢)))))
62	61	expcom 116	. . . . 5 ⊢ (𝑧 ∈ On → (𝜑 → (∀𝑤 ∈ 𝑧 ∃𝑘(𝑘 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢))) → ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢))))))
63	62	a2d 26	. . . 4 ⊢ (𝑧 ∈ On → ((𝜑 → ∀𝑤 ∈ 𝑧 ∃𝑘(𝑘 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢)))) → (𝜑 → ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢))))))
64	17, 63	biimtrid 152	. . 3 ⊢ (𝑧 ∈ On → (∀𝑤 ∈ 𝑧 (𝜑 → ∃𝑘(𝑘 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢)))) → (𝜑 → ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢))))))
65	11, 16, 64	tfis3 4587	. 2 ⊢ (𝐶 ∈ On → (𝜑 → ∃𝑔(𝑔 Fn 𝐶 ∧ ∀𝑢 ∈ 𝐶 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢)))))
66	65	impcom 125	1 ⊢ ((𝜑 ∧ 𝐶 ∈ On) → ∃𝑔(𝑔 Fn 𝐶 ∧ ∀𝑢 ∈ 𝐶 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢))))

Syntax hints:   → wi 4   ∧ wa 104   ∧ w3a 978  ∀wal 1351   = wceq 1353  ∃wex 1492   ∈ wcel 2148  {cab 2163  ∀wral 2455  ∃wrex 2456  Vcvv 2739   ∪ cun 3129  {csn 3594  ⟨cop 3597  Oncon0 4365   ↾ cres 4630  Fun wfun 5212   Fn wfn 5213  ‘cfv 5218

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-coll 4120  ax-sep 4123  ax-pow 4176  ax-pr 4211  ax-un 4435  ax-setind 4538

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-ral 2460  df-rex 2461  df-reu 2462  df-rab 2464  df-v 2741  df-sbc 2965  df-csb 3060  df-dif 3133  df-un 3135  df-in 3137  df-ss 3144  df-nul 3425  df-pw 3579  df-sn 3600  df-pr 3601  df-op 3603  df-uni 3812  df-iun 3890  df-br 4006  df-opab 4067  df-mpt 4068  df-tr 4104  df-id 4295  df-iord 4368  df-on 4370  df-suc 4373  df-xp 4634  df-rel 4635  df-cnv 4636  df-co 4637  df-dm 4638  df-rn 4639  df-res 4640  df-ima 4641  df-iota 5180  df-fun 5220  df-fn 5221  df-f 5222  df-f1 5223  df-fo 5224  df-f1o 5225  df-fv 5226  df-recs 6309

This theorem is referenced by:  tfrlemi14d  6337  tfrexlem  6338