tfrexlem - Intuitionistic Logic Explorer

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

Theorem tfrexlem 6313

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 5496	. . . . 5 ⊢ (𝑧 = 𝐶 → (recs(𝐹)‘𝑧) = (recs(𝐹)‘𝐶))
2	1	eleq1d 2239	. . . 4 ⊢ (𝑧 = 𝐶 → ((recs(𝐹)‘𝑧) ∈ V ↔ (recs(𝐹)‘𝐶) ∈ V))
3	2	imbi2d 229	. . 3 ⊢ (𝑧 = 𝐶 → ((𝜑 → (recs(𝐹)‘𝑧) ∈ V) ↔ (𝜑 → (recs(𝐹)‘𝐶) ∈ V)))
4		inss2 3348	. . . . . . 7 ⊢ (suc suc 𝑧 ∩ On) ⊆ On
5		ssorduni 4471	. . . . . . 7 ⊢ ((suc suc 𝑧 ∩ On) ⊆ On → Ord ∪ (suc suc 𝑧 ∩ On))
6	4, 5	ax-mp 5	. . . . . 6 ⊢ Ord ∪ (suc suc 𝑧 ∩ On)
7		vex 2733	. . . . . . . . . 10 ⊢ 𝑧 ∈ V
8	7	sucex 4483	. . . . . . . . 9 ⊢ suc 𝑧 ∈ V
9	8	sucex 4483	. . . . . . . 8 ⊢ suc suc 𝑧 ∈ V
10	9	inex1 4123	. . . . . . 7 ⊢ (suc suc 𝑧 ∩ On) ∈ V
11	10	uniex 4422	. . . . . 6 ⊢ ∪ (suc suc 𝑧 ∩ On) ∈ V
12		elon2 4361	. . . . . 6 ⊢ (∪ (suc suc 𝑧 ∩ On) ∈ On ↔ (Ord ∪ (suc suc 𝑧 ∩ On) ∧ ∪ (suc suc 𝑧 ∩ On) ∈ V))
13	6, 11, 12	mpbir2an 937	. . . . 5 ⊢ ∪ (suc suc 𝑧 ∩ On) ∈ On
14		tfrexlem.1	. . . . . . 7 ⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))}
15	14	tfrlem3 6290	. . . . . 6 ⊢ 𝐴 = {𝑣 ∣ ∃𝑧 ∈ On (𝑣 Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (𝑣‘𝑢) = (𝐹‘(𝑣 ↾ 𝑢)))}
16		tfrexlem.2	. . . . . . 7 ⊢ (𝜑 → ∀𝑥(Fun 𝐹 ∧ (𝐹‘𝑥) ∈ V))
17		fveq2 5496	. . . . . . . . . 10 ⊢ (𝑥 = 𝑧 → (𝐹‘𝑥) = (𝐹‘𝑧))
18	17	eleq1d 2239	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → ((𝐹‘𝑥) ∈ V ↔ (𝐹‘𝑧) ∈ V))
19	18	anbi2d 461	. . . . . . . 8 ⊢ (𝑥 = 𝑧 → ((Fun 𝐹 ∧ (𝐹‘𝑥) ∈ V) ↔ (Fun 𝐹 ∧ (𝐹‘𝑧) ∈ V)))
20	19	cbvalv 1910	. . . . . . 7 ⊢ (∀𝑥(Fun 𝐹 ∧ (𝐹‘𝑥) ∈ V) ↔ ∀𝑧(Fun 𝐹 ∧ (𝐹‘𝑧) ∈ V))
21	16, 20	sylib 121	. . . . . 6 ⊢ (𝜑 → ∀𝑧(Fun 𝐹 ∧ (𝐹‘𝑧) ∈ V))
22	15, 21	tfrlemi1 6311	. . . . 5 ⊢ ((𝜑 ∧ ∪ (suc suc 𝑧 ∩ On) ∈ On) → ∃𝑔(𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))))
23	13, 22	mpan2 423	. . . 4 ⊢ (𝜑 → ∃𝑔(𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))))
24	15	recsfval 6294	. . . . . . . . . . 11 ⊢ recs(𝐹) = ∪ 𝐴
25	24	breqi 3995	. . . . . . . . . 10 ⊢ (𝑧recs(𝐹)𝑦 ↔ 𝑧∪ 𝐴𝑦)
26		df-br 3990	. . . . . . . . . 10 ⊢ (𝑧∪ 𝐴𝑦 ↔ ⟨𝑧, 𝑦⟩ ∈ ∪ 𝐴)
27		eluni 3799	. . . . . . . . . 10 ⊢ (⟨𝑧, 𝑦⟩ ∈ ∪ 𝐴 ↔ ∃ℎ(⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴))
28	25, 26, 27	3bitri 205	. . . . . . . . 9 ⊢ (𝑧recs(𝐹)𝑦 ↔ ∃ℎ(⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴))
29	7	sucid 4402	. . . . . . . . . . . . . . . . 17 ⊢ 𝑧 ∈ suc 𝑧
30		simpr 109	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴) → ℎ ∈ 𝐴)
31		vex 2733	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ℎ ∈ V
32	14, 31	tfrlem3a 6289	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (ℎ ∈ 𝐴 ↔ ∃𝑡 ∈ On (ℎ Fn 𝑡 ∧ ∀𝑒 ∈ 𝑡 (ℎ‘𝑒) = (𝐹‘(ℎ ↾ 𝑒))))
33	30, 32	sylib 121	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴) → ∃𝑡 ∈ On (ℎ Fn 𝑡 ∧ ∀𝑒 ∈ 𝑡 (ℎ‘𝑒) = (𝐹‘(ℎ ↾ 𝑒))))
34		simprl 526	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴) ∧ (𝑡 ∈ On ∧ (ℎ Fn 𝑡 ∧ ∀𝑒 ∈ 𝑡 (ℎ‘𝑒) = (𝐹‘(ℎ ↾ 𝑒))))) → 𝑡 ∈ On)
35		simprrl 534	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴) ∧ (𝑡 ∈ On ∧ (ℎ Fn 𝑡 ∧ ∀𝑒 ∈ 𝑡 (ℎ‘𝑒) = (𝐹‘(ℎ ↾ 𝑒))))) → ℎ Fn 𝑡)
36		simpll 524	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴) ∧ (𝑡 ∈ On ∧ (ℎ Fn 𝑡 ∧ ∀𝑒 ∈ 𝑡 (ℎ‘𝑒) = (𝐹‘(ℎ ↾ 𝑒))))) → ⟨𝑧, 𝑦⟩ ∈ ℎ)
37		fnop 5301	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((ℎ Fn 𝑡 ∧ ⟨𝑧, 𝑦⟩ ∈ ℎ) → 𝑧 ∈ 𝑡)
38	35, 36, 37	syl2anc 409	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴) ∧ (𝑡 ∈ On ∧ (ℎ Fn 𝑡 ∧ ∀𝑒 ∈ 𝑡 (ℎ‘𝑒) = (𝐹‘(ℎ ↾ 𝑒))))) → 𝑧 ∈ 𝑡)
39		onelon 4369	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑡 ∈ On ∧ 𝑧 ∈ 𝑡) → 𝑧 ∈ On)
40	34, 38, 39	syl2anc 409	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴) ∧ (𝑡 ∈ On ∧ (ℎ Fn 𝑡 ∧ ∀𝑒 ∈ 𝑡 (ℎ‘𝑒) = (𝐹‘(ℎ ↾ 𝑒))))) → 𝑧 ∈ On)
41	33, 40	rexlimddv 2592	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴) → 𝑧 ∈ On)
42	41	adantl 275	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) → 𝑧 ∈ On)
43		suceloni 4485	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 ∈ On → suc 𝑧 ∈ On)
44	42, 43	syl 14	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) → suc 𝑧 ∈ On)
45		suceloni 4485	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (suc 𝑧 ∈ On → suc suc 𝑧 ∈ On)
46	44, 45	syl 14	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) → suc suc 𝑧 ∈ On)
47		onss 4477	. . . . . . . . . . . . . . . . . . . . 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 3134	. . . . . . . . . . . . . . . . . . . 20 ⊢ (suc suc 𝑧 ⊆ On ↔ (suc suc 𝑧 ∩ On) = suc suc 𝑧)
50	48, 49	sylib 121	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) → (suc suc 𝑧 ∩ On) = suc suc 𝑧)
51	50	unieqd 3807	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) → ∪ (suc suc 𝑧 ∩ On) = ∪ suc suc 𝑧)
52		eloni 4360	. . . . . . . . . . . . . . . . . . . 20 ⊢ (suc 𝑧 ∈ On → Ord suc 𝑧)
53		ordtr 4363	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Ord suc 𝑧 → Tr suc 𝑧)
54	44, 52, 53	3syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) → Tr suc 𝑧)
55	8	unisuc 4398	. . . . . . . . . . . . . . . . . . 19 ⊢ (Tr suc 𝑧 ↔ ∪ suc suc 𝑧 = suc 𝑧)
56	54, 55	sylib 121	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) → ∪ suc suc 𝑧 = suc 𝑧)
57	51, 56	eqtrd 2203	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) → ∪ (suc suc 𝑧 ∩ On) = suc 𝑧)
58	29, 57	eleqtrrid 2260	. . . . . . . . . . . . . . . 16 ⊢ (((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) → 𝑧 ∈ ∪ (suc suc 𝑧 ∩ On))
59		fndm 5297	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 Fn ∪ (suc suc 𝑧 ∩ On) → dom 𝑔 = ∪ (suc suc 𝑧 ∩ On))
60	59	ad2antrr 485	. . . . . . . . . . . . . . . 16 ⊢ (((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) → dom 𝑔 = ∪ (suc suc 𝑧 ∩ On))
61	58, 60	eleqtrrd 2250	. . . . . . . . . . . . . . 15 ⊢ (((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) → 𝑧 ∈ dom 𝑔)
62	7	eldm 4808	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ dom 𝑔 ↔ ∃𝑥 𝑧𝑔𝑥)
63	61, 62	sylib 121	. . . . . . . . . . . . . 14 ⊢ (((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) → ∃𝑥 𝑧𝑔𝑥)
64		simpr 109	. . . . . . . . . . . . . . 15 ⊢ ((((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) ∧ 𝑧𝑔𝑥) → 𝑧𝑔𝑥)
65		fneq2 5287	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 = ∪ (suc suc 𝑧 ∩ On) → (𝑔 Fn 𝑣 ↔ 𝑔 Fn ∪ (suc suc 𝑧 ∩ On)))
66		raleq 2665	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 = ∪ (suc suc 𝑧 ∩ On) → (∀𝑤 ∈ 𝑣 (𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤)) ↔ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))))
67	65, 66	anbi12d 470	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑣 = ∪ (suc suc 𝑧 ∩ On) → ((𝑔 Fn 𝑣 ∧ ∀𝑤 ∈ 𝑣 (𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ↔ (𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤)))))
68	67	rspcev 2834	. . . . . . . . . . . . . . . . . . 19 ⊢ ((∪ (suc suc 𝑧 ∩ On) ∈ On ∧ (𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤)))) → ∃𝑣 ∈ On (𝑔 Fn 𝑣 ∧ ∀𝑤 ∈ 𝑣 (𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))))
69	13, 68	mpan 422	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) → ∃𝑣 ∈ On (𝑔 Fn 𝑣 ∧ ∀𝑤 ∈ 𝑣 (𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))))
70		vex 2733	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑔 ∈ V
71	14, 70	tfrlem3a 6289	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑔 ∈ 𝐴 ↔ ∃𝑣 ∈ On (𝑔 Fn 𝑣 ∧ ∀𝑤 ∈ 𝑣 (𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))))
72	69, 71	sylibr 133	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) → 𝑔 ∈ 𝐴)
73	72	ad2antrr 485	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) ∧ 𝑧𝑔𝑥) → 𝑔 ∈ 𝐴)
74		simplrr 531	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) ∧ 𝑧𝑔𝑥) → ℎ ∈ 𝐴)
75		simplrl 530	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) ∧ 𝑧𝑔𝑥) → ⟨𝑧, 𝑦⟩ ∈ ℎ)
76		df-br 3990	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧ℎ𝑦 ↔ ⟨𝑧, 𝑦⟩ ∈ ℎ)
77	75, 76	sylibr 133	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) ∧ 𝑧𝑔𝑥) → 𝑧ℎ𝑦)
78	15	tfrlem5 6293	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴) → ((𝑧𝑔𝑥 ∧ 𝑧ℎ𝑦) → 𝑥 = 𝑦))
79	78	imp 123	. . . . . . . . . . . . . . . 16 ⊢ (((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴) ∧ (𝑧𝑔𝑥 ∧ 𝑧ℎ𝑦)) → 𝑥 = 𝑦)
80	73, 74, 64, 77, 79	syl22anc 1234	. . . . . . . . . . . . . . 15 ⊢ ((((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) ∧ 𝑧𝑔𝑥) → 𝑥 = 𝑦)
81	64, 80	breqtrd 4015	. . . . . . . . . . . . . 14 ⊢ ((((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) ∧ 𝑧𝑔𝑥) → 𝑧𝑔𝑦)
82	63, 81	exlimddv 1891	. . . . . . . . . . . . 13 ⊢ (((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) → 𝑧𝑔𝑦)
83		vex 2733	. . . . . . . . . . . . . 14 ⊢ 𝑦 ∈ V
84	7, 83	brelrn 4844	. . . . . . . . . . . . 13 ⊢ (𝑧𝑔𝑦 → 𝑦 ∈ ran 𝑔)
85	82, 84	syl 14	. . . . . . . . . . . 12 ⊢ (((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) → 𝑦 ∈ ran 𝑔)
86		elssuni 3824	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ran 𝑔 → 𝑦 ⊆ ∪ ran 𝑔)
87	85, 86	syl 14	. . . . . . . . . . 11 ⊢ (((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) → 𝑦 ⊆ ∪ ran 𝑔)
88	87	ex 114	. . . . . . . . . 10 ⊢ ((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) → ((⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴) → 𝑦 ⊆ ∪ ran 𝑔))
89	88	exlimdv 1812	. . . . . . . . 9 ⊢ ((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) → (∃ℎ(⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴) → 𝑦 ⊆ ∪ ran 𝑔))
90	28, 89	syl5bi 151	. . . . . . . 8 ⊢ ((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) → (𝑧recs(𝐹)𝑦 → 𝑦 ⊆ ∪ ran 𝑔))
91	90	alrimiv 1867	. . . . . . 7 ⊢ ((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) → ∀𝑦(𝑧recs(𝐹)𝑦 → 𝑦 ⊆ ∪ ran 𝑔))
92		fvss 5510	. . . . . . 7 ⊢ (∀𝑦(𝑧recs(𝐹)𝑦 → 𝑦 ⊆ ∪ ran 𝑔) → (recs(𝐹)‘𝑧) ⊆ ∪ ran 𝑔)
93	91, 92	syl 14	. . . . . 6 ⊢ ((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) → (recs(𝐹)‘𝑧) ⊆ ∪ ran 𝑔)
94	70	rnex 4878	. . . . . . . 8 ⊢ ran 𝑔 ∈ V
95	94	uniex 4422	. . . . . . 7 ⊢ ∪ ran 𝑔 ∈ V
96	95	ssex 4126	. . . . . 6 ⊢ ((recs(𝐹)‘𝑧) ⊆ ∪ ran 𝑔 → (recs(𝐹)‘𝑧) ∈ V)
97	93, 96	syl 14	. . . . 5 ⊢ ((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) → (recs(𝐹)‘𝑧) ∈ V)
98	97	exlimiv 1591	. . . 4 ⊢ (∃𝑔(𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) → (recs(𝐹)‘𝑧) ∈ V)
99	23, 98	syl 14	. . 3 ⊢ (𝜑 → (recs(𝐹)‘𝑧) ∈ V)
100	3, 99	vtoclg 2790	. 2 ⊢ (𝐶 ∈ 𝑉 → (𝜑 → (recs(𝐹)‘𝐶) ∈ V))
101	100	impcom 124	1 ⊢ ((𝜑 ∧ 𝐶 ∈ 𝑉) → (recs(𝐹)‘𝐶) ∈ V)

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 103 ∀wal 1346 = wceq 1348 ∃wex 1485 ∈ wcel 2141 {cab 2156 ∀wral 2448 ∃wrex 2449 Vcvv 2730 ∩ cin 3120 ⊆ wss 3121 ⟨cop 3586 ∪ cuni 3796 class class class wbr 3989 Tr wtr 4087 Ord word 4347 Oncon0 4348 suc csuc 4350 dom cdm 4611 ran crn 4612 ↾ cres 4613 Fun wfun 5192 Fn wfn 5193 ‘cfv 5198 recscrecs 6283

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: tfrex 6347

W3C validator