tfrexlem - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > tfrexlem		GIF version

Theorem tfrexlem 6486

Description: The transfinite recursion function is set-like if the input is. (Contributed by Mario Carneiro, 3-Jul-2019.)

**Hypotheses**
Ref	Expression
tfrexlem.1	⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))}
tfrexlem.2	⊢ (𝜑 → ∀𝑥(Fun 𝐹 ∧ (𝐹‘𝑥) ∈ V))

**Assertion**
Ref	Expression
tfrexlem	⊢ ((𝜑 ∧ 𝐶 ∈ 𝑉) → (recs(𝐹)‘𝐶) ∈ V)

Distinct variable groups: 𝑥,𝑓,𝑦,𝐴 𝑓,𝐹,𝑥,𝑦 Allowed substitution hints: 𝜑(𝑥,𝑦,𝑓) 𝐶(𝑥,𝑦,𝑓) 𝑉(𝑥,𝑦,𝑓)

Proof of Theorem tfrexlem Dummy variables 𝑒 𝑔 ℎ 𝑢 𝑣 𝑡 𝑤 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fveq2 5629	. . . . 5 ⊢ (𝑧 = 𝐶 → (recs(𝐹)‘𝑧) = (recs(𝐹)‘𝐶))
2	1	eleq1d 2298	. . . 4 ⊢ (𝑧 = 𝐶 → ((recs(𝐹)‘𝑧) ∈ V ↔ (recs(𝐹)‘𝐶) ∈ V))
3	2	imbi2d 230	. . 3 ⊢ (𝑧 = 𝐶 → ((𝜑 → (recs(𝐹)‘𝑧) ∈ V) ↔ (𝜑 → (recs(𝐹)‘𝐶) ∈ V)))
4		inss2 3425	. . . . . . 7 ⊢ (suc suc 𝑧 ∩ On) ⊆ On
5		ssorduni 4579	. . . . . . 7 ⊢ ((suc suc 𝑧 ∩ On) ⊆ On → Ord ∪ (suc suc 𝑧 ∩ On))
6	4, 5	ax-mp 5	. . . . . 6 ⊢ Ord ∪ (suc suc 𝑧 ∩ On)
7		vex 2802	. . . . . . . . . 10 ⊢ 𝑧 ∈ V
8	7	sucex 4591	. . . . . . . . 9 ⊢ suc 𝑧 ∈ V
9	8	sucex 4591	. . . . . . . 8 ⊢ suc suc 𝑧 ∈ V
10	9	inex1 4218	. . . . . . 7 ⊢ (suc suc 𝑧 ∩ On) ∈ V
11	10	uniex 4528	. . . . . 6 ⊢ ∪ (suc suc 𝑧 ∩ On) ∈ V
12		elon2 4467	. . . . . 6 ⊢ (∪ (suc suc 𝑧 ∩ On) ∈ On ↔ (Ord ∪ (suc suc 𝑧 ∩ On) ∧ ∪ (suc suc 𝑧 ∩ On) ∈ V))
13	6, 11, 12	mpbir2an 948	. . . . 5 ⊢ ∪ (suc suc 𝑧 ∩ On) ∈ On
14		tfrexlem.1	. . . . . . 7 ⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))}
15	14	tfrlem3 6463	. . . . . 6 ⊢ 𝐴 = {𝑣 ∣ ∃𝑧 ∈ On (𝑣 Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (𝑣‘𝑢) = (𝐹‘(𝑣 ↾ 𝑢)))}
16		tfrexlem.2	. . . . . . 7 ⊢ (𝜑 → ∀𝑥(Fun 𝐹 ∧ (𝐹‘𝑥) ∈ V))
17		fveq2 5629	. . . . . . . . . 10 ⊢ (𝑥 = 𝑧 → (𝐹‘𝑥) = (𝐹‘𝑧))
18	17	eleq1d 2298	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → ((𝐹‘𝑥) ∈ V ↔ (𝐹‘𝑧) ∈ V))
19	18	anbi2d 464	. . . . . . . 8 ⊢ (𝑥 = 𝑧 → ((Fun 𝐹 ∧ (𝐹‘𝑥) ∈ V) ↔ (Fun 𝐹 ∧ (𝐹‘𝑧) ∈ V)))
20	19	cbvalv 1964	. . . . . . 7 ⊢ (∀𝑥(Fun 𝐹 ∧ (𝐹‘𝑥) ∈ V) ↔ ∀𝑧(Fun 𝐹 ∧ (𝐹‘𝑧) ∈ V))
21	16, 20	sylib 122	. . . . . 6 ⊢ (𝜑 → ∀𝑧(Fun 𝐹 ∧ (𝐹‘𝑧) ∈ V))
22	15, 21	tfrlemi1 6484	. . . . 5 ⊢ ((𝜑 ∧ ∪ (suc suc 𝑧 ∩ On) ∈ On) → ∃𝑔(𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))))
23	13, 22	mpan2 425	. . . 4 ⊢ (𝜑 → ∃𝑔(𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))))
24	15	recsfval 6467	. . . . . . . . . . 11 ⊢ recs(𝐹) = ∪ 𝐴
25	24	breqi 4089	. . . . . . . . . 10 ⊢ (𝑧recs(𝐹)𝑦 ↔ 𝑧∪ 𝐴𝑦)
26		df-br 4084	. . . . . . . . . 10 ⊢ (𝑧∪ 𝐴𝑦 ↔ ⟨𝑧, 𝑦⟩ ∈ ∪ 𝐴)
27		eluni 3891	. . . . . . . . . 10 ⊢ (⟨𝑧, 𝑦⟩ ∈ ∪ 𝐴 ↔ ∃ℎ(⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴))
28	25, 26, 27	3bitri 206	. . . . . . . . 9 ⊢ (𝑧recs(𝐹)𝑦 ↔ ∃ℎ(⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴))
29	7	sucid 4508	. . . . . . . . . . . . . . . . 17 ⊢ 𝑧 ∈ suc 𝑧
30		simpr 110	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴) → ℎ ∈ 𝐴)
31		vex 2802	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ℎ ∈ V
32	14, 31	tfrlem3a 6462	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (ℎ ∈ 𝐴 ↔ ∃𝑡 ∈ On (ℎ Fn 𝑡 ∧ ∀𝑒 ∈ 𝑡 (ℎ‘𝑒) = (𝐹‘(ℎ ↾ 𝑒))))
33	30, 32	sylib 122	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴) → ∃𝑡 ∈ On (ℎ Fn 𝑡 ∧ ∀𝑒 ∈ 𝑡 (ℎ‘𝑒) = (𝐹‘(ℎ ↾ 𝑒))))
34		simprl 529	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴) ∧ (𝑡 ∈ On ∧ (ℎ Fn 𝑡 ∧ ∀𝑒 ∈ 𝑡 (ℎ‘𝑒) = (𝐹‘(ℎ ↾ 𝑒))))) → 𝑡 ∈ On)
35		simprrl 539	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴) ∧ (𝑡 ∈ On ∧ (ℎ Fn 𝑡 ∧ ∀𝑒 ∈ 𝑡 (ℎ‘𝑒) = (𝐹‘(ℎ ↾ 𝑒))))) → ℎ Fn 𝑡)
36		simpll 527	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴) ∧ (𝑡 ∈ On ∧ (ℎ Fn 𝑡 ∧ ∀𝑒 ∈ 𝑡 (ℎ‘𝑒) = (𝐹‘(ℎ ↾ 𝑒))))) → ⟨𝑧, 𝑦⟩ ∈ ℎ)
37		fnop 5426	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((ℎ Fn 𝑡 ∧ ⟨𝑧, 𝑦⟩ ∈ ℎ) → 𝑧 ∈ 𝑡)
38	35, 36, 37	syl2anc 411	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴) ∧ (𝑡 ∈ On ∧ (ℎ Fn 𝑡 ∧ ∀𝑒 ∈ 𝑡 (ℎ‘𝑒) = (𝐹‘(ℎ ↾ 𝑒))))) → 𝑧 ∈ 𝑡)
39		onelon 4475	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑡 ∈ On ∧ 𝑧 ∈ 𝑡) → 𝑧 ∈ On)
40	34, 38, 39	syl2anc 411	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴) ∧ (𝑡 ∈ On ∧ (ℎ Fn 𝑡 ∧ ∀𝑒 ∈ 𝑡 (ℎ‘𝑒) = (𝐹‘(ℎ ↾ 𝑒))))) → 𝑧 ∈ On)
41	33, 40	rexlimddv 2653	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴) → 𝑧 ∈ On)
42	41	adantl 277	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) → 𝑧 ∈ On)
43		onsuc 4593	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 ∈ On → suc 𝑧 ∈ On)
44	42, 43	syl 14	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) → suc 𝑧 ∈ On)
45		onsuc 4593	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (suc 𝑧 ∈ On → suc suc 𝑧 ∈ On)
46	44, 45	syl 14	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) → suc suc 𝑧 ∈ On)
47		onss 4585	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (suc suc 𝑧 ∈ On → suc suc 𝑧 ⊆ On)
48	46, 47	syl 14	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) → suc suc 𝑧 ⊆ On)
49		df-ss 3210	. . . . . . . . . . . . . . . . . . . 20 ⊢ (suc suc 𝑧 ⊆ On ↔ (suc suc 𝑧 ∩ On) = suc suc 𝑧)
50	48, 49	sylib 122	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) → (suc suc 𝑧 ∩ On) = suc suc 𝑧)
51	50	unieqd 3899	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) → ∪ (suc suc 𝑧 ∩ On) = ∪ suc suc 𝑧)
52		eloni 4466	. . . . . . . . . . . . . . . . . . . 20 ⊢ (suc 𝑧 ∈ On → Ord suc 𝑧)
53		ordtr 4469	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Ord suc 𝑧 → Tr suc 𝑧)
54	44, 52, 53	3syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) → Tr suc 𝑧)
55	8	unisuc 4504	. . . . . . . . . . . . . . . . . . 19 ⊢ (Tr suc 𝑧 ↔ ∪ suc suc 𝑧 = suc 𝑧)
56	54, 55	sylib 122	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) → ∪ suc suc 𝑧 = suc 𝑧)
57	51, 56	eqtrd 2262	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) → ∪ (suc suc 𝑧 ∩ On) = suc 𝑧)
58	29, 57	eleqtrrid 2319	. . . . . . . . . . . . . . . 16 ⊢ (((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) → 𝑧 ∈ ∪ (suc suc 𝑧 ∩ On))
59		fndm 5420	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 Fn ∪ (suc suc 𝑧 ∩ On) → dom 𝑔 = ∪ (suc suc 𝑧 ∩ On))
60	59	ad2antrr 488	. . . . . . . . . . . . . . . 16 ⊢ (((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) → dom 𝑔 = ∪ (suc suc 𝑧 ∩ On))
61	58, 60	eleqtrrd 2309	. . . . . . . . . . . . . . 15 ⊢ (((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) → 𝑧 ∈ dom 𝑔)
62	7	eldm 4920	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ dom 𝑔 ↔ ∃𝑥 𝑧𝑔𝑥)
63	61, 62	sylib 122	. . . . . . . . . . . . . 14 ⊢ (((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) → ∃𝑥 𝑧𝑔𝑥)
64		simpr 110	. . . . . . . . . . . . . . 15 ⊢ ((((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) ∧ 𝑧𝑔𝑥) → 𝑧𝑔𝑥)
65		fneq2 5410	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 = ∪ (suc suc 𝑧 ∩ On) → (𝑔 Fn 𝑣 ↔ 𝑔 Fn ∪ (suc suc 𝑧 ∩ On)))
66		raleq 2728	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 = ∪ (suc suc 𝑧 ∩ On) → (∀𝑤 ∈ 𝑣 (𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤)) ↔ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))))
67	65, 66	anbi12d 473	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑣 = ∪ (suc suc 𝑧 ∩ On) → ((𝑔 Fn 𝑣 ∧ ∀𝑤 ∈ 𝑣 (𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ↔ (𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤)))))
68	67	rspcev 2907	. . . . . . . . . . . . . . . . . . 19 ⊢ ((∪ (suc suc 𝑧 ∩ On) ∈ On ∧ (𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤)))) → ∃𝑣 ∈ On (𝑔 Fn 𝑣 ∧ ∀𝑤 ∈ 𝑣 (𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))))
69	13, 68	mpan 424	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) → ∃𝑣 ∈ On (𝑔 Fn 𝑣 ∧ ∀𝑤 ∈ 𝑣 (𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))))
70		vex 2802	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑔 ∈ V
71	14, 70	tfrlem3a 6462	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑔 ∈ 𝐴 ↔ ∃𝑣 ∈ On (𝑔 Fn 𝑣 ∧ ∀𝑤 ∈ 𝑣 (𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))))
72	69, 71	sylibr 134	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) → 𝑔 ∈ 𝐴)
73	72	ad2antrr 488	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) ∧ 𝑧𝑔𝑥) → 𝑔 ∈ 𝐴)
74		simplrr 536	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) ∧ 𝑧𝑔𝑥) → ℎ ∈ 𝐴)
75		simplrl 535	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) ∧ 𝑧𝑔𝑥) → ⟨𝑧, 𝑦⟩ ∈ ℎ)
76		df-br 4084	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧ℎ𝑦 ↔ ⟨𝑧, 𝑦⟩ ∈ ℎ)
77	75, 76	sylibr 134	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) ∧ 𝑧𝑔𝑥) → 𝑧ℎ𝑦)
78	15	tfrlem5 6466	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴) → ((𝑧𝑔𝑥 ∧ 𝑧ℎ𝑦) → 𝑥 = 𝑦))
79	78	imp 124	. . . . . . . . . . . . . . . 16 ⊢ (((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴) ∧ (𝑧𝑔𝑥 ∧ 𝑧ℎ𝑦)) → 𝑥 = 𝑦)
80	73, 74, 64, 77, 79	syl22anc 1272	. . . . . . . . . . . . . . 15 ⊢ ((((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) ∧ 𝑧𝑔𝑥) → 𝑥 = 𝑦)
81	64, 80	breqtrd 4109	. . . . . . . . . . . . . 14 ⊢ ((((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) ∧ 𝑧𝑔𝑥) → 𝑧𝑔𝑦)
82	63, 81	exlimddv 1945	. . . . . . . . . . . . 13 ⊢ (((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) → 𝑧𝑔𝑦)
83		vex 2802	. . . . . . . . . . . . . 14 ⊢ 𝑦 ∈ V
84	7, 83	brelrn 4957	. . . . . . . . . . . . 13 ⊢ (𝑧𝑔𝑦 → 𝑦 ∈ ran 𝑔)
85	82, 84	syl 14	. . . . . . . . . . . 12 ⊢ (((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) → 𝑦 ∈ ran 𝑔)
86		elssuni 3916	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ran 𝑔 → 𝑦 ⊆ ∪ ran 𝑔)
87	85, 86	syl 14	. . . . . . . . . . 11 ⊢ (((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) → 𝑦 ⊆ ∪ ran 𝑔)
88	87	ex 115	. . . . . . . . . 10 ⊢ ((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) → ((⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴) → 𝑦 ⊆ ∪ ran 𝑔))
89	88	exlimdv 1865	. . . . . . . . 9 ⊢ ((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) → (∃ℎ(⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴) → 𝑦 ⊆ ∪ ran 𝑔))
90	28, 89	biimtrid 152	. . . . . . . 8 ⊢ ((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) → (𝑧recs(𝐹)𝑦 → 𝑦 ⊆ ∪ ran 𝑔))
91	90	alrimiv 1920	. . . . . . 7 ⊢ ((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) → ∀𝑦(𝑧recs(𝐹)𝑦 → 𝑦 ⊆ ∪ ran 𝑔))
92		fvss 5643	. . . . . . 7 ⊢ (∀𝑦(𝑧recs(𝐹)𝑦 → 𝑦 ⊆ ∪ ran 𝑔) → (recs(𝐹)‘𝑧) ⊆ ∪ ran 𝑔)
93	91, 92	syl 14	. . . . . 6 ⊢ ((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) → (recs(𝐹)‘𝑧) ⊆ ∪ ran 𝑔)
94	70	rnex 4992	. . . . . . . 8 ⊢ ran 𝑔 ∈ V
95	94	uniex 4528	. . . . . . 7 ⊢ ∪ ran 𝑔 ∈ V
96	95	ssex 4221	. . . . . 6 ⊢ ((recs(𝐹)‘𝑧) ⊆ ∪ ran 𝑔 → (recs(𝐹)‘𝑧) ∈ V)
97	93, 96	syl 14	. . . . 5 ⊢ ((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) → (recs(𝐹)‘𝑧) ∈ V)
98	97	exlimiv 1644	. . . 4 ⊢ (∃𝑔(𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) → (recs(𝐹)‘𝑧) ∈ V)
99	23, 98	syl 14	. . 3 ⊢ (𝜑 → (recs(𝐹)‘𝑧) ∈ V)
100	3, 99	vtoclg 2861	. 2 ⊢ (𝐶 ∈ 𝑉 → (𝜑 → (recs(𝐹)‘𝐶) ∈ V))
101	100	impcom 125	1 ⊢ ((𝜑 ∧ 𝐶 ∈ 𝑉) → (recs(𝐹)‘𝐶) ∈ V)

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 104 ∀wal 1393 = wceq 1395 ∃wex 1538 ∈ wcel 2200 {cab 2215 ∀wral 2508 ∃wrex 2509 Vcvv 2799 ∩ cin 3196 ⊆ wss 3197 ⟨cop 3669 ∪ cuni 3888 class class class wbr 4083 Tr wtr 4182 Ord word 4453 Oncon0 4454 suc csuc 4456 dom cdm 4719 ran crn 4720 ↾ cres 4721 Fun wfun 5312 Fn wfn 5313 ‘cfv 5318 recscrecs 6456

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 617 ax-in2 618 ax-io 714 ax-5 1493 ax-7 1494 ax-gen 1495 ax-ie1 1539 ax-ie2 1540 ax-8 1550 ax-10 1551 ax-11 1552 ax-i12 1553 ax-bndl 1555 ax-4 1556 ax-17 1572 ax-i9 1576 ax-ial 1580 ax-i5r 1581 ax-13 2202 ax-14 2203 ax-ext 2211 ax-coll 4199 ax-sep 4202 ax-pow 4258 ax-pr 4293 ax-un 4524 ax-setind 4629

This theorem depends on definitions: df-bi 117 df-3an 1004 df-tru 1398 df-fal 1401 df-nf 1507 df-sb 1809 df-eu 2080 df-mo 2081 df-clab 2216 df-cleq 2222 df-clel 2225 df-nfc 2361 df-ne 2401 df-ral 2513 df-rex 2514 df-reu 2515 df-rab 2517 df-v 2801 df-sbc 3029 df-csb 3125 df-dif 3199 df-un 3201 df-in 3203 df-ss 3210 df-nul 3492 df-pw 3651 df-sn 3672 df-pr 3673 df-op 3675 df-uni 3889 df-iun 3967 df-br 4084 df-opab 4146 df-mpt 4147 df-tr 4183 df-id 4384 df-iord 4457 df-on 4459 df-suc 4462 df-xp 4725 df-rel 4726 df-cnv 4727 df-co 4728 df-dm 4729 df-rn 4730 df-res 4731 df-ima 4732 df-iota 5278 df-fun 5320 df-fn 5321 df-f 5322 df-f1 5323 df-fo 5324 df-f1o 5325 df-fv 5326 df-recs 6457

This theorem is referenced by: tfrex 6520

W3C validator