Theorem tfrlemi1 6351

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 5323	. . . . . 6 ⊢ ((𝑧 = 𝑤 ∧ 𝑔 = 𝑘) → (𝑔 Fn 𝑧 ↔ 𝑘 Fn 𝑤))
4	1	fveq1d 5532	. . . . . . . 8 ⊢ ((𝑧 = 𝑤 ∧ 𝑔 = 𝑘) → (𝑔‘𝑢) = (𝑘‘𝑢))
5	1	reseq1d 4921	. . . . . . . . 9 ⊢ ((𝑧 = 𝑤 ∧ 𝑔 = 𝑘) → (𝑔 ↾ 𝑢) = (𝑘 ↾ 𝑢))
6	5	fveq2d 5534	. . . . . . . 8 ⊢ ((𝑧 = 𝑤 ∧ 𝑔 = 𝑘) → (𝐹‘(𝑔 ↾ 𝑢)) = (𝐹‘(𝑘 ↾ 𝑢)))
7	4, 6	eqeq12d 2204	. . . . . . 7 ⊢ ((𝑧 = 𝑤 ∧ 𝑔 = 𝑘) → ((𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢)) ↔ (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢))))
8	2, 7	raleqbidv 2698	. . . . . 6 ⊢ ((𝑧 = 𝑤 ∧ 𝑔 = 𝑘) → (∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢)) ↔ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢))))
9	3, 8	anbi12d 473	. . . . 5 ⊢ ((𝑧 = 𝑤 ∧ 𝑔 = 𝑘) → ((𝑔 Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢))) ↔ (𝑘 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢)))))
10	9	cbvexdva 1941	. . . 4 ⊢ (𝑧 = 𝑤 → (∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢))) ↔ ∃𝑘(𝑘 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢)))))
11	10	imbi2d 230	. . 3 ⊢ (𝑧 = 𝑤 → ((𝜑 → ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢)))) ↔ (𝜑 → ∃𝑘(𝑘 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢))))))
12		fneq2 5320	. . . . . 6 ⊢ (𝑧 = 𝐶 → (𝑔 Fn 𝑧 ↔ 𝑔 Fn 𝐶))
13		raleq 2686	. . . . . 6 ⊢ (𝑧 = 𝐶 → (∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢)) ↔ ∀𝑢 ∈ 𝐶 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢))))
14	12, 13	anbi12d 473	. . . . 5 ⊢ (𝑧 = 𝐶 → ((𝑔 Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢))) ↔ (𝑔 Fn 𝐶 ∧ ∀𝑢 ∈ 𝐶 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢)))))
15	14	exbidv 1836	. . . 4 ⊢ (𝑧 = 𝐶 → (∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢))) ↔ ∃𝑔(𝑔 Fn 𝐶 ∧ ∀𝑢 ∈ 𝐶 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢)))))
16	15	imbi2d 230	. . 3 ⊢ (𝑧 = 𝐶 → ((𝜑 → ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢)))) ↔ (𝜑 → ∃𝑔(𝑔 Fn 𝐶 ∧ ∀𝑢 ∈ 𝐶 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢))))))
17		r19.21v 2567	. . . 4 ⊢ (∀𝑤 ∈ 𝑧 (𝜑 → ∃𝑘(𝑘 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢)))) ↔ (𝜑 → ∀𝑤 ∈ 𝑧 ∃𝑘(𝑘 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢)))))
18		tfrlemisucfn.1	. . . . . . . . 9 ⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))}
19	18	tfrlem3 6330	. . . . . . . 8 ⊢ 𝐴 = {𝑔 ∣ ∃𝑧 ∈ On (𝑔 Fn 𝑧 ∧ ∀𝑒 ∈ 𝑧 (𝑔‘𝑒) = (𝐹‘(𝑔 ↾ 𝑒)))}
20		tfrlemisucfn.2	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑥(Fun 𝐹 ∧ (𝐹‘𝑥) ∈ V))
21		fveq2 5530	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑧 → (𝐹‘𝑥) = (𝐹‘𝑧))
22	21	eleq1d 2258	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑧 → ((𝐹‘𝑥) ∈ V ↔ (𝐹‘𝑧) ∈ V))
23	22	anbi2d 464	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑧 → ((Fun 𝐹 ∧ (𝐹‘𝑥) ∈ V) ↔ (Fun 𝐹 ∧ (𝐹‘𝑧) ∈ V)))
24	23	cbvalv 1929	. . . . . . . . . 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 5323	. . . . . . . . . . . 12 ⊢ (((𝑡 = ℎ ∧ 𝑤 = 𝑣) ∧ 𝑘 = 𝑓) → (𝑘 Fn 𝑤 ↔ 𝑓 Fn 𝑣))
30	27	eleq1d 2258	. . . . . . . . . . . 12 ⊢ (((𝑡 = ℎ ∧ 𝑤 = 𝑣) ∧ 𝑘 = 𝑓) → (𝑘 ∈ 𝐴 ↔ 𝑓 ∈ 𝐴))
31		simpll 527	. . . . . . . . . . . . 13 ⊢ (((𝑡 = ℎ ∧ 𝑤 = 𝑣) ∧ 𝑘 = 𝑓) → 𝑡 = ℎ)
32	27	fveq2d 5534	. . . . . . . . . . . . . . . 16 ⊢ (((𝑡 = ℎ ∧ 𝑤 = 𝑣) ∧ 𝑘 = 𝑓) → (𝐹‘𝑘) = (𝐹‘𝑓))
33	28, 32	opeq12d 3801	. . . . . . . . . . . . . . 15 ⊢ (((𝑡 = ℎ ∧ 𝑤 = 𝑣) ∧ 𝑘 = 𝑓) → ⟨𝑤, (𝐹‘𝑘)⟩ = ⟨𝑣, (𝐹‘𝑓)⟩)
34	33	sneqd 3620	. . . . . . . . . . . . . 14 ⊢ (((𝑡 = ℎ ∧ 𝑤 = 𝑣) ∧ 𝑘 = 𝑓) → {⟨𝑤, (𝐹‘𝑘)⟩} = {⟨𝑣, (𝐹‘𝑓)⟩})
35	27, 34	uneq12d 3305	. . . . . . . . . . . . 13 ⊢ (((𝑡 = ℎ ∧ 𝑤 = 𝑣) ∧ 𝑘 = 𝑓) → (𝑘 ∪ {⟨𝑤, (𝐹‘𝑘)⟩}) = (𝑓 ∪ {⟨𝑣, (𝐹‘𝑓)⟩}))
36	31, 35	eqeq12d 2204	. . . . . . . . . . . 12 ⊢ (((𝑡 = ℎ ∧ 𝑤 = 𝑣) ∧ 𝑘 = 𝑓) → (𝑡 = (𝑘 ∪ {⟨𝑤, (𝐹‘𝑘)⟩}) ↔ ℎ = (𝑓 ∪ {⟨𝑣, (𝐹‘𝑓)⟩})))
37	29, 30, 36	3anbi123d 1323	. . . . . . . . . . 11 ⊢ (((𝑡 = ℎ ∧ 𝑤 = 𝑣) ∧ 𝑘 = 𝑓) → ((𝑘 Fn 𝑤 ∧ 𝑘 ∈ 𝐴 ∧ 𝑡 = (𝑘 ∪ {⟨𝑤, (𝐹‘𝑘)⟩})) ↔ (𝑓 Fn 𝑣 ∧ 𝑓 ∈ 𝐴 ∧ ℎ = (𝑓 ∪ {⟨𝑣, (𝐹‘𝑓)⟩}))))
38	37	cbvexdva 1941	. . . . . . . . . 10 ⊢ ((𝑡 = ℎ ∧ 𝑤 = 𝑣) → (∃𝑘(𝑘 Fn 𝑤 ∧ 𝑘 ∈ 𝐴 ∧ 𝑡 = (𝑘 ∪ {⟨𝑤, (𝐹‘𝑘)⟩})) ↔ ∃𝑓(𝑓 Fn 𝑣 ∧ 𝑓 ∈ 𝐴 ∧ ℎ = (𝑓 ∪ {⟨𝑣, (𝐹‘𝑓)⟩}))))
39	38	cbvrexdva 2728	. . . . . . . . 9 ⊢ (𝑡 = ℎ → (∃𝑤 ∈ 𝑧 ∃𝑘(𝑘 Fn 𝑤 ∧ 𝑘 ∈ 𝐴 ∧ 𝑡 = (𝑘 ∪ {⟨𝑤, (𝐹‘𝑘)⟩})) ↔ ∃𝑣 ∈ 𝑧 ∃𝑓(𝑓 Fn 𝑣 ∧ 𝑓 ∈ 𝐴 ∧ ℎ = (𝑓 ∪ {⟨𝑣, (𝐹‘𝑓)⟩}))))
40	39	cbvabv 2314	. . . . . . . 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 5323	. . . . . . . . . . . . 13 ⊢ ((𝑤 = 𝑣 ∧ 𝑘 = 𝑓) → (𝑘 Fn 𝑤 ↔ 𝑓 Fn 𝑣))
47		simplr 528	. . . . . . . . . . . . . . . 16 ⊢ (((𝑤 = 𝑣 ∧ 𝑘 = 𝑓) ∧ 𝑢 = 𝑦) → 𝑘 = 𝑓)
48		simpr 110	. . . . . . . . . . . . . . . 16 ⊢ (((𝑤 = 𝑣 ∧ 𝑘 = 𝑓) ∧ 𝑢 = 𝑦) → 𝑢 = 𝑦)
49	47, 48	fveq12d 5537	. . . . . . . . . . . . . . 15 ⊢ (((𝑤 = 𝑣 ∧ 𝑘 = 𝑓) ∧ 𝑢 = 𝑦) → (𝑘‘𝑢) = (𝑓‘𝑦))
50	47, 48	reseq12d 4923	. . . . . . . . . . . . . . . 16 ⊢ (((𝑤 = 𝑣 ∧ 𝑘 = 𝑓) ∧ 𝑢 = 𝑦) → (𝑘 ↾ 𝑢) = (𝑓 ↾ 𝑦))
51	50	fveq2d 5534	. . . . . . . . . . . . . . 15 ⊢ (((𝑤 = 𝑣 ∧ 𝑘 = 𝑓) ∧ 𝑢 = 𝑦) → (𝐹‘(𝑘 ↾ 𝑢)) = (𝐹‘(𝑓 ↾ 𝑦)))
52	49, 51	eqeq12d 2204	. . . . . . . . . . . . . 14 ⊢ (((𝑤 = 𝑣 ∧ 𝑘 = 𝑓) ∧ 𝑢 = 𝑦) → ((𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢)) ↔ (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))))
53		simpll 527	. . . . . . . . . . . . . 14 ⊢ (((𝑤 = 𝑣 ∧ 𝑘 = 𝑓) ∧ 𝑢 = 𝑦) → 𝑤 = 𝑣)
54	52, 53	cbvraldva2 2725	. . . . . . . . . . . . 13 ⊢ ((𝑤 = 𝑣 ∧ 𝑘 = 𝑓) → (∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢)) ↔ ∀𝑦 ∈ 𝑣 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))))
55	46, 54	anbi12d 473	. . . . . . . . . . . 12 ⊢ ((𝑤 = 𝑣 ∧ 𝑘 = 𝑓) → ((𝑘 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢))) ↔ (𝑓 Fn 𝑣 ∧ ∀𝑦 ∈ 𝑣 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))))
56	55	cbvexdva 1941	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑣 → (∃𝑘(𝑘 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢))) ↔ ∃𝑓(𝑓 Fn 𝑣 ∧ ∀𝑦 ∈ 𝑣 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))))
57	56	cbvralv 2718	. . . . . . . . . 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 6350	. . . . . . 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 4600	. 2 ⊢ (𝐶 ∈ On → (𝜑 → ∃𝑔(𝑔 Fn 𝐶 ∧ ∀𝑢 ∈ 𝐶 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢)))))
66	65	impcom 125	1 ⊢ ((𝜑 ∧ 𝐶 ∈ On) → ∃𝑔(𝑔 Fn 𝐶 ∧ ∀𝑢 ∈ 𝐶 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢))))

Syntax hints:   → wi 4   ∧ wa 104   ∧ w3a 980  ∀wal 1362   = wceq 1364  ∃wex 1503   ∈ wcel 2160  {cab 2175  ∀wral 2468  ∃wrex 2469  Vcvv 2752   ∪ cun 3142  {csn 3607  ⟨cop 3610  Oncon0 4378   ↾ cres 4643  Fun wfun 5225   Fn wfn 5226  ‘cfv 5231

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 615  ax-in2 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2162  ax-14 2163  ax-ext 2171  ax-coll 4133  ax-sep 4136  ax-pow 4189  ax-pr 4224  ax-un 4448  ax-setind 4551

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1472  df-sb 1774  df-eu 2041  df-mo 2042  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-ne 2361  df-ral 2473  df-rex 2474  df-reu 2475  df-rab 2477  df-v 2754  df-sbc 2978  df-csb 3073  df-dif 3146  df-un 3148  df-in 3150  df-ss 3157  df-nul 3438  df-pw 3592  df-sn 3613  df-pr 3614  df-op 3616  df-uni 3825  df-iun 3903  df-br 4019  df-opab 4080  df-mpt 4081  df-tr 4117  df-id 4308  df-iord 4381  df-on 4383  df-suc 4386  df-xp 4647  df-rel 4648  df-cnv 4649  df-co 4650  df-dm 4651  df-rn 4652  df-res 4653  df-ima 4654  df-iota 5193  df-fun 5233  df-fn 5234  df-f 5235  df-f1 5236  df-fo 5237  df-f1o 5238  df-fv 5239  df-recs 6324

This theorem is referenced by:  tfrlemi14d  6352  tfrexlem  6353