tfrexlem - Intuitionistic Logic Explorer

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

Theorem tfrexlem 6302

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 5486	. . . . 5 ⊢ (𝑧 = 𝐶 → (recs(𝐹)‘𝑧) = (recs(𝐹)‘𝐶))
2	1	eleq1d 2235	. . . 4 ⊢ (𝑧 = 𝐶 → ((recs(𝐹)‘𝑧) ∈ V ↔ (recs(𝐹)‘𝐶) ∈ V))
3	2	imbi2d 229	. . 3 ⊢ (𝑧 = 𝐶 → ((𝜑 → (recs(𝐹)‘𝑧) ∈ V) ↔ (𝜑 → (recs(𝐹)‘𝐶) ∈ V)))
4		inss2 3343	. . . . . . 7 ⊢ (suc suc 𝑧 ∩ On) ⊆ On
5		ssorduni 4464	. . . . . . 7 ⊢ ((suc suc 𝑧 ∩ On) ⊆ On → Ord ∪ (suc suc 𝑧 ∩ On))
6	4, 5	ax-mp 5	. . . . . 6 ⊢ Ord ∪ (suc suc 𝑧 ∩ On)
7		vex 2729	. . . . . . . . . 10 ⊢ 𝑧 ∈ V
8	7	sucex 4476	. . . . . . . . 9 ⊢ suc 𝑧 ∈ V
9	8	sucex 4476	. . . . . . . 8 ⊢ suc suc 𝑧 ∈ V
10	9	inex1 4116	. . . . . . 7 ⊢ (suc suc 𝑧 ∩ On) ∈ V
11	10	uniex 4415	. . . . . 6 ⊢ ∪ (suc suc 𝑧 ∩ On) ∈ V
12		elon2 4354	. . . . . 6 ⊢ (∪ (suc suc 𝑧 ∩ On) ∈ On ↔ (Ord ∪ (suc suc 𝑧 ∩ On) ∧ ∪ (suc suc 𝑧 ∩ On) ∈ V))
13	6, 11, 12	mpbir2an 932	. . . . 5 ⊢ ∪ (suc suc 𝑧 ∩ On) ∈ On
14		tfrexlem.1	. . . . . . 7 ⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))}
15	14	tfrlem3 6279	. . . . . 6 ⊢ 𝐴 = {𝑣 ∣ ∃𝑧 ∈ On (𝑣 Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (𝑣‘𝑢) = (𝐹‘(𝑣 ↾ 𝑢)))}
16		tfrexlem.2	. . . . . . 7 ⊢ (𝜑 → ∀𝑥(Fun 𝐹 ∧ (𝐹‘𝑥) ∈ V))
17		fveq2 5486	. . . . . . . . . 10 ⊢ (𝑥 = 𝑧 → (𝐹‘𝑥) = (𝐹‘𝑧))
18	17	eleq1d 2235	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → ((𝐹‘𝑥) ∈ V ↔ (𝐹‘𝑧) ∈ V))
19	18	anbi2d 460	. . . . . . . 8 ⊢ (𝑥 = 𝑧 → ((Fun 𝐹 ∧ (𝐹‘𝑥) ∈ V) ↔ (Fun 𝐹 ∧ (𝐹‘𝑧) ∈ V)))
20	19	cbvalv 1905	. . . . . . 7 ⊢ (∀𝑥(Fun 𝐹 ∧ (𝐹‘𝑥) ∈ V) ↔ ∀𝑧(Fun 𝐹 ∧ (𝐹‘𝑧) ∈ V))
21	16, 20	sylib 121	. . . . . 6 ⊢ (𝜑 → ∀𝑧(Fun 𝐹 ∧ (𝐹‘𝑧) ∈ V))
22	15, 21	tfrlemi1 6300	. . . . 5 ⊢ ((𝜑 ∧ ∪ (suc suc 𝑧 ∩ On) ∈ On) → ∃𝑔(𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))))
23	13, 22	mpan2 422	. . . 4 ⊢ (𝜑 → ∃𝑔(𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))))
24	15	recsfval 6283	. . . . . . . . . . 11 ⊢ recs(𝐹) = ∪ 𝐴
25	24	breqi 3988	. . . . . . . . . 10 ⊢ (𝑧recs(𝐹)𝑦 ↔ 𝑧∪ 𝐴𝑦)
26		df-br 3983	. . . . . . . . . 10 ⊢ (𝑧∪ 𝐴𝑦 ↔ ⟨𝑧, 𝑦⟩ ∈ ∪ 𝐴)
27		eluni 3792	. . . . . . . . . 10 ⊢ (⟨𝑧, 𝑦⟩ ∈ ∪ 𝐴 ↔ ∃ℎ(⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴))
28	25, 26, 27	3bitri 205	. . . . . . . . 9 ⊢ (𝑧recs(𝐹)𝑦 ↔ ∃ℎ(⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴))
29	7	sucid 4395	. . . . . . . . . . . . . . . . 17 ⊢ 𝑧 ∈ suc 𝑧
30		simpr 109	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴) → ℎ ∈ 𝐴)
31		vex 2729	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ℎ ∈ V
32	14, 31	tfrlem3a 6278	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (ℎ ∈ 𝐴 ↔ ∃𝑡 ∈ On (ℎ Fn 𝑡 ∧ ∀𝑒 ∈ 𝑡 (ℎ‘𝑒) = (𝐹‘(ℎ ↾ 𝑒))))
33	30, 32	sylib 121	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴) → ∃𝑡 ∈ On (ℎ Fn 𝑡 ∧ ∀𝑒 ∈ 𝑡 (ℎ‘𝑒) = (𝐹‘(ℎ ↾ 𝑒))))
34		simprl 521	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴) ∧ (𝑡 ∈ On ∧ (ℎ Fn 𝑡 ∧ ∀𝑒 ∈ 𝑡 (ℎ‘𝑒) = (𝐹‘(ℎ ↾ 𝑒))))) → 𝑡 ∈ On)
35		simprrl 529	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴) ∧ (𝑡 ∈ On ∧ (ℎ Fn 𝑡 ∧ ∀𝑒 ∈ 𝑡 (ℎ‘𝑒) = (𝐹‘(ℎ ↾ 𝑒))))) → ℎ Fn 𝑡)
36		simpll 519	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴) ∧ (𝑡 ∈ On ∧ (ℎ Fn 𝑡 ∧ ∀𝑒 ∈ 𝑡 (ℎ‘𝑒) = (𝐹‘(ℎ ↾ 𝑒))))) → ⟨𝑧, 𝑦⟩ ∈ ℎ)
37		fnop 5291	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((ℎ Fn 𝑡 ∧ ⟨𝑧, 𝑦⟩ ∈ ℎ) → 𝑧 ∈ 𝑡)
38	35, 36, 37	syl2anc 409	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴) ∧ (𝑡 ∈ On ∧ (ℎ Fn 𝑡 ∧ ∀𝑒 ∈ 𝑡 (ℎ‘𝑒) = (𝐹‘(ℎ ↾ 𝑒))))) → 𝑧 ∈ 𝑡)
39		onelon 4362	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑡 ∈ On ∧ 𝑧 ∈ 𝑡) → 𝑧 ∈ On)
40	34, 38, 39	syl2anc 409	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴) ∧ (𝑡 ∈ On ∧ (ℎ Fn 𝑡 ∧ ∀𝑒 ∈ 𝑡 (ℎ‘𝑒) = (𝐹‘(ℎ ↾ 𝑒))))) → 𝑧 ∈ On)
41	33, 40	rexlimddv 2588	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴) → 𝑧 ∈ On)
42	41	adantl 275	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) → 𝑧 ∈ On)
43		suceloni 4478	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 ∈ On → suc 𝑧 ∈ On)
44	42, 43	syl 14	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) → suc 𝑧 ∈ On)
45		suceloni 4478	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (suc 𝑧 ∈ On → suc suc 𝑧 ∈ On)
46	44, 45	syl 14	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) → suc suc 𝑧 ∈ On)
47		onss 4470	. . . . . . . . . . . . . . . . . . . . 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 3129	. . . . . . . . . . . . . . . . . . . 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 3800	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) → ∪ (suc suc 𝑧 ∩ On) = ∪ suc suc 𝑧)
52		eloni 4353	. . . . . . . . . . . . . . . . . . . 20 ⊢ (suc 𝑧 ∈ On → Ord suc 𝑧)
53		ordtr 4356	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Ord suc 𝑧 → Tr suc 𝑧)
54	44, 52, 53	3syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) → Tr suc 𝑧)
55	8	unisuc 4391	. . . . . . . . . . . . . . . . . . 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 2198	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) → ∪ (suc suc 𝑧 ∩ On) = suc 𝑧)
58	29, 57	eleqtrrid 2256	. . . . . . . . . . . . . . . 16 ⊢ (((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) → 𝑧 ∈ ∪ (suc suc 𝑧 ∩ On))
59		fndm 5287	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 Fn ∪ (suc suc 𝑧 ∩ On) → dom 𝑔 = ∪ (suc suc 𝑧 ∩ On))
60	59	ad2antrr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) → dom 𝑔 = ∪ (suc suc 𝑧 ∩ On))
61	58, 60	eleqtrrd 2246	. . . . . . . . . . . . . . 15 ⊢ (((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) → 𝑧 ∈ dom 𝑔)
62	7	eldm 4801	. . . . . . . . . . . . . . 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 5277	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 = ∪ (suc suc 𝑧 ∩ On) → (𝑔 Fn 𝑣 ↔ 𝑔 Fn ∪ (suc suc 𝑧 ∩ On)))
66		raleq 2661	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 = ∪ (suc suc 𝑧 ∩ On) → (∀𝑤 ∈ 𝑣 (𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤)) ↔ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))))
67	65, 66	anbi12d 465	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑣 = ∪ (suc suc 𝑧 ∩ On) → ((𝑔 Fn 𝑣 ∧ ∀𝑤 ∈ 𝑣 (𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ↔ (𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤)))))
68	67	rspcev 2830	. . . . . . . . . . . . . . . . . . 19 ⊢ ((∪ (suc suc 𝑧 ∩ On) ∈ On ∧ (𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤)))) → ∃𝑣 ∈ On (𝑔 Fn 𝑣 ∧ ∀𝑤 ∈ 𝑣 (𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))))
69	13, 68	mpan 421	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) → ∃𝑣 ∈ On (𝑔 Fn 𝑣 ∧ ∀𝑤 ∈ 𝑣 (𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))))
70		vex 2729	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑔 ∈ V
71	14, 70	tfrlem3a 6278	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑔 ∈ 𝐴 ↔ ∃𝑣 ∈ On (𝑔 Fn 𝑣 ∧ ∀𝑤 ∈ 𝑣 (𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))))
72	69, 71	sylibr 133	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) → 𝑔 ∈ 𝐴)
73	72	ad2antrr 480	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) ∧ 𝑧𝑔𝑥) → 𝑔 ∈ 𝐴)
74		simplrr 526	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) ∧ 𝑧𝑔𝑥) → ℎ ∈ 𝐴)
75		simplrl 525	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) ∧ 𝑧𝑔𝑥) → ⟨𝑧, 𝑦⟩ ∈ ℎ)
76		df-br 3983	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧ℎ𝑦 ↔ ⟨𝑧, 𝑦⟩ ∈ ℎ)
77	75, 76	sylibr 133	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) ∧ 𝑧𝑔𝑥) → 𝑧ℎ𝑦)
78	15	tfrlem5 6282	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴) → ((𝑧𝑔𝑥 ∧ 𝑧ℎ𝑦) → 𝑥 = 𝑦))
79	78	imp 123	. . . . . . . . . . . . . . . 16 ⊢ (((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴) ∧ (𝑧𝑔𝑥 ∧ 𝑧ℎ𝑦)) → 𝑥 = 𝑦)
80	73, 74, 64, 77, 79	syl22anc 1229	. . . . . . . . . . . . . . 15 ⊢ ((((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) ∧ 𝑧𝑔𝑥) → 𝑥 = 𝑦)
81	64, 80	breqtrd 4008	. . . . . . . . . . . . . 14 ⊢ ((((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) ∧ 𝑧𝑔𝑥) → 𝑧𝑔𝑦)
82	63, 81	exlimddv 1886	. . . . . . . . . . . . 13 ⊢ (((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) → 𝑧𝑔𝑦)
83		vex 2729	. . . . . . . . . . . . . 14 ⊢ 𝑦 ∈ V
84	7, 83	brelrn 4837	. . . . . . . . . . . . 13 ⊢ (𝑧𝑔𝑦 → 𝑦 ∈ ran 𝑔)
85	82, 84	syl 14	. . . . . . . . . . . 12 ⊢ (((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) → 𝑦 ∈ ran 𝑔)
86		elssuni 3817	. . . . . . . . . . . 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 1807	. . . . . . . . 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 1862	. . . . . . 7 ⊢ ((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) → ∀𝑦(𝑧recs(𝐹)𝑦 → 𝑦 ⊆ ∪ ran 𝑔))
92		fvss 5500	. . . . . . 7 ⊢ (∀𝑦(𝑧recs(𝐹)𝑦 → 𝑦 ⊆ ∪ ran 𝑔) → (recs(𝐹)‘𝑧) ⊆ ∪ ran 𝑔)
93	91, 92	syl 14	. . . . . 6 ⊢ ((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) → (recs(𝐹)‘𝑧) ⊆ ∪ ran 𝑔)
94	70	rnex 4871	. . . . . . . 8 ⊢ ran 𝑔 ∈ V
95	94	uniex 4415	. . . . . . 7 ⊢ ∪ ran 𝑔 ∈ V
96	95	ssex 4119	. . . . . 6 ⊢ ((recs(𝐹)‘𝑧) ⊆ ∪ ran 𝑔 → (recs(𝐹)‘𝑧) ∈ V)
97	93, 96	syl 14	. . . . 5 ⊢ ((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) → (recs(𝐹)‘𝑧) ∈ V)
98	97	exlimiv 1586	. . . 4 ⊢ (∃𝑔(𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) → (recs(𝐹)‘𝑧) ∈ V)
99	23, 98	syl 14	. . 3 ⊢ (𝜑 → (recs(𝐹)‘𝑧) ∈ V)
100	3, 99	vtoclg 2786	. 2 ⊢ (𝐶 ∈ 𝑉 → (𝜑 → (recs(𝐹)‘𝐶) ∈ V))
101	100	impcom 124	1 ⊢ ((𝜑 ∧ 𝐶 ∈ 𝑉) → (recs(𝐹)‘𝐶) ∈ V)

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 103 ∀wal 1341 = wceq 1343 ∃wex 1480 ∈ wcel 2136 {cab 2151 ∀wral 2444 ∃wrex 2445 Vcvv 2726 ∩ cin 3115 ⊆ wss 3116 ⟨cop 3579 ∪ cuni 3789 class class class wbr 3982 Tr wtr 4080 Ord word 4340 Oncon0 4341 suc csuc 4343 dom cdm 4604 ran crn 4605 ↾ cres 4606 Fun wfun 5182 Fn wfn 5183 ‘cfv 5188 recscrecs 6272

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 604 ax-in2 605 ax-io 699 ax-5 1435 ax-7 1436 ax-gen 1437 ax-ie1 1481 ax-ie2 1482 ax-8 1492 ax-10 1493 ax-11 1494 ax-i12 1495 ax-bndl 1497 ax-4 1498 ax-17 1514 ax-i9 1518 ax-ial 1522 ax-i5r 1523 ax-13 2138 ax-14 2139 ax-ext 2147 ax-coll 4097 ax-sep 4100 ax-pow 4153 ax-pr 4187 ax-un 4411 ax-setind 4514

This theorem depends on definitions: df-bi 116 df-3an 970 df-tru 1346 df-fal 1349 df-nf 1449 df-sb 1751 df-eu 2017 df-mo 2018 df-clab 2152 df-cleq 2158 df-clel 2161 df-nfc 2297 df-ne 2337 df-ral 2449 df-rex 2450 df-reu 2451 df-rab 2453 df-v 2728 df-sbc 2952 df-csb 3046 df-dif 3118 df-un 3120 df-in 3122 df-ss 3129 df-nul 3410 df-pw 3561 df-sn 3582 df-pr 3583 df-op 3585 df-uni 3790 df-iun 3868 df-br 3983 df-opab 4044 df-mpt 4045 df-tr 4081 df-id 4271 df-iord 4344 df-on 4346 df-suc 4349 df-xp 4610 df-rel 4611 df-cnv 4612 df-co 4613 df-dm 4614 df-rn 4615 df-res 4616 df-ima 4617 df-iota 5153 df-fun 5190 df-fn 5191 df-f 5192 df-f1 5193 df-fo 5194 df-f1o 5195 df-fv 5196 df-recs 6273

This theorem is referenced by: tfrex 6336

W3C validator