tfrexlem - Intuitionistic Logic Explorer

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

Theorem tfrexlem 6565

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 5670	. . . . 5 ⊢ (𝑧 = 𝐶 → (recs(𝐹)‘𝑧) = (recs(𝐹)‘𝐶))
2	1	eleq1d 2301	. . . 4 ⊢ (𝑧 = 𝐶 → ((recs(𝐹)‘𝑧) ∈ V ↔ (recs(𝐹)‘𝐶) ∈ V))
3	2	imbi2d 230	. . 3 ⊢ (𝑧 = 𝐶 → ((𝜑 → (recs(𝐹)‘𝑧) ∈ V) ↔ (𝜑 → (recs(𝐹)‘𝐶) ∈ V)))
4		inss2 3442	. . . . . . 7 ⊢ (suc suc 𝑧 ∩ On) ⊆ On
5		ssorduni 4609	. . . . . . 7 ⊢ ((suc suc 𝑧 ∩ On) ⊆ On → Ord ∪ (suc suc 𝑧 ∩ On))
6	4, 5	ax-mp 5	. . . . . 6 ⊢ Ord ∪ (suc suc 𝑧 ∩ On)
7		vex 2816	. . . . . . . . . 10 ⊢ 𝑧 ∈ V
8	7	sucex 4621	. . . . . . . . 9 ⊢ suc 𝑧 ∈ V
9	8	sucex 4621	. . . . . . . 8 ⊢ suc suc 𝑧 ∈ V
10	9	inex1 4244	. . . . . . 7 ⊢ (suc suc 𝑧 ∩ On) ∈ V
11	10	uniex 4558	. . . . . 6 ⊢ ∪ (suc suc 𝑧 ∩ On) ∈ V
12		elon2 4497	. . . . . 6 ⊢ (∪ (suc suc 𝑧 ∩ On) ∈ On ↔ (Ord ∪ (suc suc 𝑧 ∩ On) ∧ ∪ (suc suc 𝑧 ∩ On) ∈ V))
13	6, 11, 12	mpbir2an 951	. . . . 5 ⊢ ∪ (suc suc 𝑧 ∩ On) ∈ On
14		tfrexlem.1	. . . . . . 7 ⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))}
15	14	tfrlem3 6542	. . . . . 6 ⊢ 𝐴 = {𝑣 ∣ ∃𝑧 ∈ On (𝑣 Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (𝑣‘𝑢) = (𝐹‘(𝑣 ↾ 𝑢)))}
16		tfrexlem.2	. . . . . . 7 ⊢ (𝜑 → ∀𝑥(Fun 𝐹 ∧ (𝐹‘𝑥) ∈ V))
17		fveq2 5670	. . . . . . . . . 10 ⊢ (𝑥 = 𝑧 → (𝐹‘𝑥) = (𝐹‘𝑧))
18	17	eleq1d 2301	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → ((𝐹‘𝑥) ∈ V ↔ (𝐹‘𝑧) ∈ V))
19	18	anbi2d 464	. . . . . . . 8 ⊢ (𝑥 = 𝑧 → ((Fun 𝐹 ∧ (𝐹‘𝑥) ∈ V) ↔ (Fun 𝐹 ∧ (𝐹‘𝑧) ∈ V)))
20	19	cbvalv 1967	. . . . . . 7 ⊢ (∀𝑥(Fun 𝐹 ∧ (𝐹‘𝑥) ∈ V) ↔ ∀𝑧(Fun 𝐹 ∧ (𝐹‘𝑧) ∈ V))
21	16, 20	sylib 122	. . . . . 6 ⊢ (𝜑 → ∀𝑧(Fun 𝐹 ∧ (𝐹‘𝑧) ∈ V))
22	15, 21	tfrlemi1 6563	. . . . 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 6546	. . . . . . . . . . 11 ⊢ recs(𝐹) = ∪ 𝐴
25	24	breqi 4115	. . . . . . . . . 10 ⊢ (𝑧recs(𝐹)𝑦 ↔ 𝑧∪ 𝐴𝑦)
26		df-br 4110	. . . . . . . . . 10 ⊢ (𝑧∪ 𝐴𝑦 ↔ ⟨𝑧, 𝑦⟩ ∈ ∪ 𝐴)
27		eluni 3917	. . . . . . . . . 10 ⊢ (⟨𝑧, 𝑦⟩ ∈ ∪ 𝐴 ↔ ∃ℎ(⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴))
28	25, 26, 27	3bitri 206	. . . . . . . . 9 ⊢ (𝑧recs(𝐹)𝑦 ↔ ∃ℎ(⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴))
29	7	sucid 4538	. . . . . . . . . . . . . . . . 17 ⊢ 𝑧 ∈ suc 𝑧
30		simpr 110	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴) → ℎ ∈ 𝐴)
31		vex 2816	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ℎ ∈ V
32	14, 31	tfrlem3a 6541	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (ℎ ∈ 𝐴 ↔ ∃𝑡 ∈ On (ℎ Fn 𝑡 ∧ ∀𝑒 ∈ 𝑡 (ℎ‘𝑒) = (𝐹‘(ℎ ↾ 𝑒))))
33	30, 32	sylib 122	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴) → ∃𝑡 ∈ On (ℎ Fn 𝑡 ∧ ∀𝑒 ∈ 𝑡 (ℎ‘𝑒) = (𝐹‘(ℎ ↾ 𝑒))))
34		simprl 531	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴) ∧ (𝑡 ∈ On ∧ (ℎ Fn 𝑡 ∧ ∀𝑒 ∈ 𝑡 (ℎ‘𝑒) = (𝐹‘(ℎ ↾ 𝑒))))) → 𝑡 ∈ On)
35		simprrl 541	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴) ∧ (𝑡 ∈ On ∧ (ℎ Fn 𝑡 ∧ ∀𝑒 ∈ 𝑡 (ℎ‘𝑒) = (𝐹‘(ℎ ↾ 𝑒))))) → ℎ Fn 𝑡)
36		simpll 527	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴) ∧ (𝑡 ∈ On ∧ (ℎ Fn 𝑡 ∧ ∀𝑒 ∈ 𝑡 (ℎ‘𝑒) = (𝐹‘(ℎ ↾ 𝑒))))) → ⟨𝑧, 𝑦⟩ ∈ ℎ)
37		fnop 5461	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((ℎ Fn 𝑡 ∧ ⟨𝑧, 𝑦⟩ ∈ ℎ) → 𝑧 ∈ 𝑡)
38	35, 36, 37	syl2anc 411	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴) ∧ (𝑡 ∈ On ∧ (ℎ Fn 𝑡 ∧ ∀𝑒 ∈ 𝑡 (ℎ‘𝑒) = (𝐹‘(ℎ ↾ 𝑒))))) → 𝑧 ∈ 𝑡)
39		onelon 4505	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑡 ∈ On ∧ 𝑧 ∈ 𝑡) → 𝑧 ∈ On)
40	34, 38, 39	syl2anc 411	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴) ∧ (𝑡 ∈ On ∧ (ℎ Fn 𝑡 ∧ ∀𝑒 ∈ 𝑡 (ℎ‘𝑒) = (𝐹‘(ℎ ↾ 𝑒))))) → 𝑧 ∈ On)
41	33, 40	rexlimddv 2665	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴) → 𝑧 ∈ On)
42	41	adantl 277	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) → 𝑧 ∈ On)
43		onsuc 4623	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 ∈ On → suc 𝑧 ∈ On)
44	42, 43	syl 14	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) → suc 𝑧 ∈ On)
45		onsuc 4623	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (suc 𝑧 ∈ On → suc suc 𝑧 ∈ On)
46	44, 45	syl 14	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) → suc suc 𝑧 ∈ On)
47		onss 4615	. . . . . . . . . . . . . . . . . . . . 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 3224	. . . . . . . . . . . . . . . . . . . 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 3925	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) → ∪ (suc suc 𝑧 ∩ On) = ∪ suc suc 𝑧)
52		eloni 4496	. . . . . . . . . . . . . . . . . . . 20 ⊢ (suc 𝑧 ∈ On → Ord suc 𝑧)
53		ordtr 4499	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Ord suc 𝑧 → Tr suc 𝑧)
54	44, 52, 53	3syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) → Tr suc 𝑧)
55	8	unisuc 4534	. . . . . . . . . . . . . . . . . . 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 2265	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) → ∪ (suc suc 𝑧 ∩ On) = suc 𝑧)
58	29, 57	eleqtrrid 2322	. . . . . . . . . . . . . . . 16 ⊢ (((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) → 𝑧 ∈ ∪ (suc suc 𝑧 ∩ On))
59		fndm 5455	. . . . . . . . . . . . . . . . 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 2312	. . . . . . . . . . . . . . 15 ⊢ (((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) → 𝑧 ∈ dom 𝑔)
62	7	eldm 4953	. . . . . . . . . . . . . . 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 5445	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 = ∪ (suc suc 𝑧 ∩ On) → (𝑔 Fn 𝑣 ↔ 𝑔 Fn ∪ (suc suc 𝑧 ∩ On)))
66		raleq 2741	. . . . . . . . . . . . . . . . . . . . 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 2921	. . . . . . . . . . . . . . . . . . 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 2816	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑔 ∈ V
71	14, 70	tfrlem3a 6541	. . . . . . . . . . . . . . . . . 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 538	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) ∧ 𝑧𝑔𝑥) → ℎ ∈ 𝐴)
75		simplrl 537	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) ∧ 𝑧𝑔𝑥) → ⟨𝑧, 𝑦⟩ ∈ ℎ)
76		df-br 4110	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧ℎ𝑦 ↔ ⟨𝑧, 𝑦⟩ ∈ ℎ)
77	75, 76	sylibr 134	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) ∧ 𝑧𝑔𝑥) → 𝑧ℎ𝑦)
78	15	tfrlem5 6545	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴) → ((𝑧𝑔𝑥 ∧ 𝑧ℎ𝑦) → 𝑥 = 𝑦))
79	78	imp 124	. . . . . . . . . . . . . . . 16 ⊢ (((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴) ∧ (𝑧𝑔𝑥 ∧ 𝑧ℎ𝑦)) → 𝑥 = 𝑦)
80	73, 74, 64, 77, 79	syl22anc 1275	. . . . . . . . . . . . . . 15 ⊢ ((((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) ∧ 𝑧𝑔𝑥) → 𝑥 = 𝑦)
81	64, 80	breqtrd 4135	. . . . . . . . . . . . . 14 ⊢ ((((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) ∧ 𝑧𝑔𝑥) → 𝑧𝑔𝑦)
82	63, 81	exlimddv 1948	. . . . . . . . . . . . 13 ⊢ (((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) → 𝑧𝑔𝑦)
83		vex 2816	. . . . . . . . . . . . . 14 ⊢ 𝑦 ∈ V
84	7, 83	brelrn 4990	. . . . . . . . . . . . 13 ⊢ (𝑧𝑔𝑦 → 𝑦 ∈ ran 𝑔)
85	82, 84	syl 14	. . . . . . . . . . . 12 ⊢ (((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) → 𝑦 ∈ ran 𝑔)
86		elssuni 3942	. . . . . . . . . . . 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 1868	. . . . . . . . 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 1923	. . . . . . 7 ⊢ ((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) → ∀𝑦(𝑧recs(𝐹)𝑦 → 𝑦 ⊆ ∪ ran 𝑔))
92		fvss 5684	. . . . . . 7 ⊢ (∀𝑦(𝑧recs(𝐹)𝑦 → 𝑦 ⊆ ∪ ran 𝑔) → (recs(𝐹)‘𝑧) ⊆ ∪ ran 𝑔)
93	91, 92	syl 14	. . . . . 6 ⊢ ((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) → (recs(𝐹)‘𝑧) ⊆ ∪ ran 𝑔)
94	70	rnex 5025	. . . . . . . 8 ⊢ ran 𝑔 ∈ V
95	94	uniex 4558	. . . . . . 7 ⊢ ∪ ran 𝑔 ∈ V
96	95	ssex 4247	. . . . . 6 ⊢ ((recs(𝐹)‘𝑧) ⊆ ∪ ran 𝑔 → (recs(𝐹)‘𝑧) ∈ V)
97	93, 96	syl 14	. . . . 5 ⊢ ((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) → (recs(𝐹)‘𝑧) ∈ V)
98	97	exlimiv 1647	. . . 4 ⊢ (∃𝑔(𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) → (recs(𝐹)‘𝑧) ∈ V)
99	23, 98	syl 14	. . 3 ⊢ (𝜑 → (recs(𝐹)‘𝑧) ∈ V)
100	3, 99	vtoclg 2875	. 2 ⊢ (𝐶 ∈ 𝑉 → (𝜑 → (recs(𝐹)‘𝐶) ∈ V))
101	100	impcom 125	1 ⊢ ((𝜑 ∧ 𝐶 ∈ 𝑉) → (recs(𝐹)‘𝐶) ∈ V)

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 104 ∀wal 1396 = wceq 1398 ∃wex 1541 ∈ wcel 2203 {cab 2218 ∀wral 2520 ∃wrex 2521 Vcvv 2813 ∩ cin 3210 ⊆ wss 3211 ⟨cop 3692 ∪ cuni 3914 class class class wbr 4109 Tr wtr 4208 Ord word 4483 Oncon0 4484 suc csuc 4486 dom cdm 4749 ran crn 4750 ↾ cres 4751 Fun wfun 5346 Fn wfn 5347 ‘cfv 5352 recscrecs 6535

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 619 ax-in2 620 ax-io 717 ax-5 1496 ax-7 1497 ax-gen 1498 ax-ie1 1542 ax-ie2 1543 ax-8 1553 ax-10 1554 ax-11 1555 ax-i12 1556 ax-bndl 1558 ax-4 1559 ax-17 1575 ax-i9 1579 ax-ial 1583 ax-i5r 1584 ax-13 2205 ax-14 2206 ax-ext 2214 ax-coll 4225 ax-sep 4228 ax-pow 4287 ax-pr 4322 ax-un 4554 ax-setind 4659

This theorem depends on definitions: df-bi 117 df-3an 1007 df-tru 1401 df-fal 1404 df-nf 1510 df-sb 1812 df-eu 2083 df-mo 2084 df-clab 2219 df-cleq 2225 df-clel 2228 df-nfc 2373 df-ne 2413 df-ral 2525 df-rex 2526 df-reu 2527 df-rab 2529 df-v 2815 df-sbc 3043 df-csb 3139 df-dif 3213 df-un 3215 df-in 3217 df-ss 3224 df-nul 3509 df-pw 3671 df-sn 3695 df-pr 3696 df-op 3698 df-uni 3915 df-iun 3993 df-br 4110 df-opab 4172 df-mpt 4173 df-tr 4209 df-id 4414 df-iord 4487 df-on 4489 df-suc 4492 df-xp 4755 df-rel 4756 df-cnv 4757 df-co 4758 df-dm 4759 df-rn 4760 df-res 4761 df-ima 4762 df-iota 5312 df-fun 5354 df-fn 5355 df-f 5356 df-f1 5357 df-fo 5358 df-f1o 5359 df-fv 5360 df-recs 6536

This theorem is referenced by: tfrex 6599

W3C validator