Theorem tfrlemi1 5969

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 108	. . . . . . 7 ⊢ ((𝑧 = 𝑤 ∧ 𝑔 = 𝑘) → 𝑔 = 𝑘)
2		simpl 107	. . . . . . 7 ⊢ ((𝑧 = 𝑤 ∧ 𝑔 = 𝑘) → 𝑧 = 𝑤)
3	1, 2	fneq12d 5011	. . . . . 6 ⊢ ((𝑧 = 𝑤 ∧ 𝑔 = 𝑘) → (𝑔 Fn 𝑧 ↔ 𝑘 Fn 𝑤))
4	1	fveq1d 5200	. . . . . . . 8 ⊢ ((𝑧 = 𝑤 ∧ 𝑔 = 𝑘) → (𝑔‘𝑢) = (𝑘‘𝑢))
5	1	reseq1d 4629	. . . . . . . . 9 ⊢ ((𝑧 = 𝑤 ∧ 𝑔 = 𝑘) → (𝑔 ↾ 𝑢) = (𝑘 ↾ 𝑢))
6	5	fveq2d 5202	. . . . . . . 8 ⊢ ((𝑧 = 𝑤 ∧ 𝑔 = 𝑘) → (𝐹‘(𝑔 ↾ 𝑢)) = (𝐹‘(𝑘 ↾ 𝑢)))
7	4, 6	eqeq12d 2095	. . . . . . 7 ⊢ ((𝑧 = 𝑤 ∧ 𝑔 = 𝑘) → ((𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢)) ↔ (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢))))
8	2, 7	raleqbidv 2561	. . . . . 6 ⊢ ((𝑧 = 𝑤 ∧ 𝑔 = 𝑘) → (∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢)) ↔ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢))))
9	3, 8	anbi12d 456	. . . . 5 ⊢ ((𝑧 = 𝑤 ∧ 𝑔 = 𝑘) → ((𝑔 Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢))) ↔ (𝑘 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢)))))
10	9	cbvexdva 1845	. . . 4 ⊢ (𝑧 = 𝑤 → (∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢))) ↔ ∃𝑘(𝑘 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢)))))
11	10	imbi2d 228	. . 3 ⊢ (𝑧 = 𝑤 → ((𝜑 → ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢)))) ↔ (𝜑 → ∃𝑘(𝑘 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢))))))
12		fneq2 5008	. . . . . 6 ⊢ (𝑧 = 𝐶 → (𝑔 Fn 𝑧 ↔ 𝑔 Fn 𝐶))
13		raleq 2549	. . . . . 6 ⊢ (𝑧 = 𝐶 → (∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢)) ↔ ∀𝑢 ∈ 𝐶 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢))))
14	12, 13	anbi12d 456	. . . . 5 ⊢ (𝑧 = 𝐶 → ((𝑔 Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢))) ↔ (𝑔 Fn 𝐶 ∧ ∀𝑢 ∈ 𝐶 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢)))))
15	14	exbidv 1746	. . . 4 ⊢ (𝑧 = 𝐶 → (∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢))) ↔ ∃𝑔(𝑔 Fn 𝐶 ∧ ∀𝑢 ∈ 𝐶 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢)))))
16	15	imbi2d 228	. . 3 ⊢ (𝑧 = 𝐶 → ((𝜑 → ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢)))) ↔ (𝜑 → ∃𝑔(𝑔 Fn 𝐶 ∧ ∀𝑢 ∈ 𝐶 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢))))))
17		r19.21v 2438	. . . 4 ⊢ (∀𝑤 ∈ 𝑧 (𝜑 → ∃𝑘(𝑘 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢)))) ↔ (𝜑 → ∀𝑤 ∈ 𝑧 ∃𝑘(𝑘 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢)))))
18		tfrlemisucfn.1	. . . . . . . . 9 ⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))}
19	18	tfrlem3 5949	. . . . . . . 8 ⊢ 𝐴 = {𝑔 ∣ ∃𝑧 ∈ On (𝑔 Fn 𝑧 ∧ ∀𝑒 ∈ 𝑧 (𝑔‘𝑒) = (𝐹‘(𝑔 ↾ 𝑒)))}
20		tfrlemisucfn.2	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑥(Fun 𝐹 ∧ (𝐹‘𝑥) ∈ V))
21		fveq2 5198	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑧 → (𝐹‘𝑥) = (𝐹‘𝑧))
22	21	eleq1d 2147	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑧 → ((𝐹‘𝑥) ∈ V ↔ (𝐹‘𝑧) ∈ V))
23	22	anbi2d 451	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑧 → ((Fun 𝐹 ∧ (𝐹‘𝑥) ∈ V) ↔ (Fun 𝐹 ∧ (𝐹‘𝑧) ∈ V)))
24	23	cbvalv 1835	. . . . . . . . . 10 ⊢ (∀𝑥(Fun 𝐹 ∧ (𝐹‘𝑥) ∈ V) ↔ ∀𝑧(Fun 𝐹 ∧ (𝐹‘𝑧) ∈ V))
25	20, 24	sylib 120	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑧(Fun 𝐹 ∧ (𝐹‘𝑧) ∈ V))
26	25	adantr 270	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∃𝑘(𝑘 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢))))) → ∀𝑧(Fun 𝐹 ∧ (𝐹‘𝑧) ∈ V))
27		simpr 108	. . . . . . . . . . . . 13 ⊢ (((𝑡 = ℎ ∧ 𝑤 = 𝑣) ∧ 𝑘 = 𝑓) → 𝑘 = 𝑓)
28		simplr 496	. . . . . . . . . . . . 13 ⊢ (((𝑡 = ℎ ∧ 𝑤 = 𝑣) ∧ 𝑘 = 𝑓) → 𝑤 = 𝑣)
29	27, 28	fneq12d 5011	. . . . . . . . . . . 12 ⊢ (((𝑡 = ℎ ∧ 𝑤 = 𝑣) ∧ 𝑘 = 𝑓) → (𝑘 Fn 𝑤 ↔ 𝑓 Fn 𝑣))
30	27	eleq1d 2147	. . . . . . . . . . . 12 ⊢ (((𝑡 = ℎ ∧ 𝑤 = 𝑣) ∧ 𝑘 = 𝑓) → (𝑘 ∈ 𝐴 ↔ 𝑓 ∈ 𝐴))
31		simpll 495	. . . . . . . . . . . . 13 ⊢ (((𝑡 = ℎ ∧ 𝑤 = 𝑣) ∧ 𝑘 = 𝑓) → 𝑡 = ℎ)
32	27	fveq2d 5202	. . . . . . . . . . . . . . . 16 ⊢ (((𝑡 = ℎ ∧ 𝑤 = 𝑣) ∧ 𝑘 = 𝑓) → (𝐹‘𝑘) = (𝐹‘𝑓))
33	28, 32	opeq12d 3578	. . . . . . . . . . . . . . 15 ⊢ (((𝑡 = ℎ ∧ 𝑤 = 𝑣) ∧ 𝑘 = 𝑓) → ⟨𝑤, (𝐹‘𝑘)⟩ = ⟨𝑣, (𝐹‘𝑓)⟩)
34	33	sneqd 3411	. . . . . . . . . . . . . 14 ⊢ (((𝑡 = ℎ ∧ 𝑤 = 𝑣) ∧ 𝑘 = 𝑓) → {⟨𝑤, (𝐹‘𝑘)⟩} = {⟨𝑣, (𝐹‘𝑓)⟩})
35	27, 34	uneq12d 3127	. . . . . . . . . . . . 13 ⊢ (((𝑡 = ℎ ∧ 𝑤 = 𝑣) ∧ 𝑘 = 𝑓) → (𝑘 ∪ {⟨𝑤, (𝐹‘𝑘)⟩}) = (𝑓 ∪ {⟨𝑣, (𝐹‘𝑓)⟩}))
36	31, 35	eqeq12d 2095	. . . . . . . . . . . 12 ⊢ (((𝑡 = ℎ ∧ 𝑤 = 𝑣) ∧ 𝑘 = 𝑓) → (𝑡 = (𝑘 ∪ {⟨𝑤, (𝐹‘𝑘)⟩}) ↔ ℎ = (𝑓 ∪ {⟨𝑣, (𝐹‘𝑓)⟩})))
37	29, 30, 36	3anbi123d 1243	. . . . . . . . . . 11 ⊢ (((𝑡 = ℎ ∧ 𝑤 = 𝑣) ∧ 𝑘 = 𝑓) → ((𝑘 Fn 𝑤 ∧ 𝑘 ∈ 𝐴 ∧ 𝑡 = (𝑘 ∪ {⟨𝑤, (𝐹‘𝑘)⟩})) ↔ (𝑓 Fn 𝑣 ∧ 𝑓 ∈ 𝐴 ∧ ℎ = (𝑓 ∪ {⟨𝑣, (𝐹‘𝑓)⟩}))))
38	37	cbvexdva 1845	. . . . . . . . . 10 ⊢ ((𝑡 = ℎ ∧ 𝑤 = 𝑣) → (∃𝑘(𝑘 Fn 𝑤 ∧ 𝑘 ∈ 𝐴 ∧ 𝑡 = (𝑘 ∪ {⟨𝑤, (𝐹‘𝑘)⟩})) ↔ ∃𝑓(𝑓 Fn 𝑣 ∧ 𝑓 ∈ 𝐴 ∧ ℎ = (𝑓 ∪ {⟨𝑣, (𝐹‘𝑓)⟩}))))
39	38	cbvrexdva 2584	. . . . . . . . 9 ⊢ (𝑡 = ℎ → (∃𝑤 ∈ 𝑧 ∃𝑘(𝑘 Fn 𝑤 ∧ 𝑘 ∈ 𝐴 ∧ 𝑡 = (𝑘 ∪ {⟨𝑤, (𝐹‘𝑘)⟩})) ↔ ∃𝑣 ∈ 𝑧 ∃𝑓(𝑓 Fn 𝑣 ∧ 𝑓 ∈ 𝐴 ∧ ℎ = (𝑓 ∪ {⟨𝑣, (𝐹‘𝑓)⟩}))))
40	39	cbvabv 2202	. . . . . . . 8 ⊢ {𝑡 ∣ ∃𝑤 ∈ 𝑧 ∃𝑘(𝑘 Fn 𝑤 ∧ 𝑘 ∈ 𝐴 ∧ 𝑡 = (𝑘 ∪ {⟨𝑤, (𝐹‘𝑘)⟩}))} = {ℎ ∣ ∃𝑣 ∈ 𝑧 ∃𝑓(𝑓 Fn 𝑣 ∧ 𝑓 ∈ 𝐴 ∧ ℎ = (𝑓 ∪ {⟨𝑣, (𝐹‘𝑓)⟩}))}
41		simpl 107	. . . . . . . . 9 ⊢ ((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∃𝑘(𝑘 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢)))) → 𝑧 ∈ On)
42	41	adantl 271	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∃𝑘(𝑘 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢))))) → 𝑧 ∈ On)
43		simpr 108	. . . . . . . . . 10 ⊢ ((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∃𝑘(𝑘 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢)))) → ∀𝑤 ∈ 𝑧 ∃𝑘(𝑘 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢))))
44		simpr 108	. . . . . . . . . . . . . 14 ⊢ ((𝑤 = 𝑣 ∧ 𝑘 = 𝑓) → 𝑘 = 𝑓)
45		simpl 107	. . . . . . . . . . . . . 14 ⊢ ((𝑤 = 𝑣 ∧ 𝑘 = 𝑓) → 𝑤 = 𝑣)
46	44, 45	fneq12d 5011	. . . . . . . . . . . . 13 ⊢ ((𝑤 = 𝑣 ∧ 𝑘 = 𝑓) → (𝑘 Fn 𝑤 ↔ 𝑓 Fn 𝑣))
47		simplr 496	. . . . . . . . . . . . . . . 16 ⊢ (((𝑤 = 𝑣 ∧ 𝑘 = 𝑓) ∧ 𝑢 = 𝑦) → 𝑘 = 𝑓)
48		simpr 108	. . . . . . . . . . . . . . . 16 ⊢ (((𝑤 = 𝑣 ∧ 𝑘 = 𝑓) ∧ 𝑢 = 𝑦) → 𝑢 = 𝑦)
49	47, 48	fveq12d 5204	. . . . . . . . . . . . . . 15 ⊢ (((𝑤 = 𝑣 ∧ 𝑘 = 𝑓) ∧ 𝑢 = 𝑦) → (𝑘‘𝑢) = (𝑓‘𝑦))
50	47, 48	reseq12d 4631	. . . . . . . . . . . . . . . 16 ⊢ (((𝑤 = 𝑣 ∧ 𝑘 = 𝑓) ∧ 𝑢 = 𝑦) → (𝑘 ↾ 𝑢) = (𝑓 ↾ 𝑦))
51	50	fveq2d 5202	. . . . . . . . . . . . . . 15 ⊢ (((𝑤 = 𝑣 ∧ 𝑘 = 𝑓) ∧ 𝑢 = 𝑦) → (𝐹‘(𝑘 ↾ 𝑢)) = (𝐹‘(𝑓 ↾ 𝑦)))
52	49, 51	eqeq12d 2095	. . . . . . . . . . . . . 14 ⊢ (((𝑤 = 𝑣 ∧ 𝑘 = 𝑓) ∧ 𝑢 = 𝑦) → ((𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢)) ↔ (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))))
53		simpll 495	. . . . . . . . . . . . . 14 ⊢ (((𝑤 = 𝑣 ∧ 𝑘 = 𝑓) ∧ 𝑢 = 𝑦) → 𝑤 = 𝑣)
54	52, 53	cbvraldva2 2581	. . . . . . . . . . . . 13 ⊢ ((𝑤 = 𝑣 ∧ 𝑘 = 𝑓) → (∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢)) ↔ ∀𝑦 ∈ 𝑣 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))))
55	46, 54	anbi12d 456	. . . . . . . . . . . 12 ⊢ ((𝑤 = 𝑣 ∧ 𝑘 = 𝑓) → ((𝑘 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢))) ↔ (𝑓 Fn 𝑣 ∧ ∀𝑦 ∈ 𝑣 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))))
56	55	cbvexdva 1845	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑣 → (∃𝑘(𝑘 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢))) ↔ ∃𝑓(𝑓 Fn 𝑣 ∧ ∀𝑦 ∈ 𝑣 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))))
57	56	cbvralv 2577	. . . . . . . . . 10 ⊢ (∀𝑤 ∈ 𝑧 ∃𝑘(𝑘 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢))) ↔ ∀𝑣 ∈ 𝑧 ∃𝑓(𝑓 Fn 𝑣 ∧ ∀𝑦 ∈ 𝑣 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))))
58	43, 57	sylib 120	. . . . . . . . 9 ⊢ ((𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∃𝑘(𝑘 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢)))) → ∀𝑣 ∈ 𝑧 ∃𝑓(𝑓 Fn 𝑣 ∧ ∀𝑦 ∈ 𝑣 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))))
59	58	adantl 271	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∃𝑘(𝑘 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢))))) → ∀𝑣 ∈ 𝑧 ∃𝑓(𝑓 Fn 𝑣 ∧ ∀𝑦 ∈ 𝑣 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))))
60	19, 26, 40, 42, 59	tfrlemiex 5968	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ On ∧ ∀𝑤 ∈ 𝑧 ∃𝑘(𝑘 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢))))) → ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢))))
61	60	expr 367	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ On) → (∀𝑤 ∈ 𝑧 ∃𝑘(𝑘 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢))) → ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢)))))
62	61	expcom 114	. . . . 5 ⊢ (𝑧 ∈ On → (𝜑 → (∀𝑤 ∈ 𝑧 ∃𝑘(𝑘 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢))) → ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢))))))
63	62	a2d 26	. . . 4 ⊢ (𝑧 ∈ On → ((𝜑 → ∀𝑤 ∈ 𝑧 ∃𝑘(𝑘 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢)))) → (𝜑 → ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢))))))
64	17, 63	syl5bi 150	. . 3 ⊢ (𝑧 ∈ On → (∀𝑤 ∈ 𝑧 (𝜑 → ∃𝑘(𝑘 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑘‘𝑢) = (𝐹‘(𝑘 ↾ 𝑢)))) → (𝜑 → ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢))))))
65	11, 16, 64	tfis3 4327	. 2 ⊢ (𝐶 ∈ On → (𝜑 → ∃𝑔(𝑔 Fn 𝐶 ∧ ∀𝑢 ∈ 𝐶 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢)))))
66	65	impcom 123	1 ⊢ ((𝜑 ∧ 𝐶 ∈ On) → ∃𝑔(𝑔 Fn 𝐶 ∧ ∀𝑢 ∈ 𝐶 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢))))

Syntax hints:   → wi 4   ∧ wa 102   ∧ w3a 919  ∀wal 1282   = wceq 1284  ∃wex 1421   ∈ wcel 1433  {cab 2067  ∀wral 2348  ∃wrex 2349  Vcvv 2601   ∪ cun 2971  {csn 3398  ⟨cop 3401  Oncon0 4118   ↾ cres 4365  Fun wfun 4916   Fn wfn 4917  ‘cfv 4922

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 576  ax-in2 577  ax-io 662  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-10 1436  ax-11 1437  ax-i12 1438  ax-bndl 1439  ax-4 1440  ax-13 1444  ax-14 1445  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468  ax-ext 2063  ax-coll 3893  ax-sep 3896  ax-pow 3948  ax-pr 3964  ax-un 4188  ax-setind 4280

This theorem depends on definitions:  df-bi 115  df-3an 921  df-tru 1287  df-fal 1290  df-nf 1390  df-sb 1686  df-eu 1944  df-mo 1945  df-clab 2068  df-cleq 2074  df-clel 2077  df-nfc 2208  df-ne 2246  df-ral 2353  df-rex 2354  df-reu 2355  df-rab 2357  df-v 2603  df-sbc 2816  df-csb 2909  df-dif 2975  df-un 2977  df-in 2979  df-ss 2986  df-nul 3252  df-pw 3384  df-sn 3404  df-pr 3405  df-op 3407  df-uni 3602  df-iun 3680  df-br 3786  df-opab 3840  df-mpt 3841  df-tr 3876  df-id 4048  df-iord 4121  df-on 4123  df-suc 4126  df-xp 4369  df-rel 4370  df-cnv 4371  df-co 4372  df-dm 4373  df-rn 4374  df-res 4375  df-ima 4376  df-iota 4887  df-fun 4924  df-fn 4925  df-f 4926  df-f1 4927  df-fo 4928  df-f1o 4929  df-fv 4930  df-recs 5943

This theorem is referenced by:  tfrlemi14d  5970  tfrexlem  5971