tfrexlem - Intuitionistic Logic Explorer

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

Theorem tfrexlem 6543

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 5648	. . . . 5 ⊢ (𝑧 = 𝐶 → (recs(𝐹)‘𝑧) = (recs(𝐹)‘𝐶))
2	1	eleq1d 2300	. . . 4 ⊢ (𝑧 = 𝐶 → ((recs(𝐹)‘𝑧) ∈ V ↔ (recs(𝐹)‘𝐶) ∈ V))
3	2	imbi2d 230	. . 3 ⊢ (𝑧 = 𝐶 → ((𝜑 → (recs(𝐹)‘𝑧) ∈ V) ↔ (𝜑 → (recs(𝐹)‘𝐶) ∈ V)))
4		inss2 3430	. . . . . . 7 ⊢ (suc suc 𝑧 ∩ On) ⊆ On
5		ssorduni 4591	. . . . . . 7 ⊢ ((suc suc 𝑧 ∩ On) ⊆ On → Ord ∪ (suc suc 𝑧 ∩ On))
6	4, 5	ax-mp 5	. . . . . 6 ⊢ Ord ∪ (suc suc 𝑧 ∩ On)
7		vex 2806	. . . . . . . . . 10 ⊢ 𝑧 ∈ V
8	7	sucex 4603	. . . . . . . . 9 ⊢ suc 𝑧 ∈ V
9	8	sucex 4603	. . . . . . . 8 ⊢ suc suc 𝑧 ∈ V
10	9	inex1 4228	. . . . . . 7 ⊢ (suc suc 𝑧 ∩ On) ∈ V
11	10	uniex 4540	. . . . . 6 ⊢ ∪ (suc suc 𝑧 ∩ On) ∈ V
12		elon2 4479	. . . . . 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 6520	. . . . . 6 ⊢ 𝐴 = {𝑣 ∣ ∃𝑧 ∈ On (𝑣 Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (𝑣‘𝑢) = (𝐹‘(𝑣 ↾ 𝑢)))}
16		tfrexlem.2	. . . . . . 7 ⊢ (𝜑 → ∀𝑥(Fun 𝐹 ∧ (𝐹‘𝑥) ∈ V))
17		fveq2 5648	. . . . . . . . . 10 ⊢ (𝑥 = 𝑧 → (𝐹‘𝑥) = (𝐹‘𝑧))
18	17	eleq1d 2300	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → ((𝐹‘𝑥) ∈ V ↔ (𝐹‘𝑧) ∈ V))
19	18	anbi2d 464	. . . . . . . 8 ⊢ (𝑥 = 𝑧 → ((Fun 𝐹 ∧ (𝐹‘𝑥) ∈ V) ↔ (Fun 𝐹 ∧ (𝐹‘𝑧) ∈ V)))
20	19	cbvalv 1966	. . . . . . 7 ⊢ (∀𝑥(Fun 𝐹 ∧ (𝐹‘𝑥) ∈ V) ↔ ∀𝑧(Fun 𝐹 ∧ (𝐹‘𝑧) ∈ V))
21	16, 20	sylib 122	. . . . . 6 ⊢ (𝜑 → ∀𝑧(Fun 𝐹 ∧ (𝐹‘𝑧) ∈ V))
22	15, 21	tfrlemi1 6541	. . . . 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 6524	. . . . . . . . . . 11 ⊢ recs(𝐹) = ∪ 𝐴
25	24	breqi 4099	. . . . . . . . . 10 ⊢ (𝑧recs(𝐹)𝑦 ↔ 𝑧∪ 𝐴𝑦)
26		df-br 4094	. . . . . . . . . 10 ⊢ (𝑧∪ 𝐴𝑦 ↔ ⟨𝑧, 𝑦⟩ ∈ ∪ 𝐴)
27		eluni 3901	. . . . . . . . . 10 ⊢ (⟨𝑧, 𝑦⟩ ∈ ∪ 𝐴 ↔ ∃ℎ(⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴))
28	25, 26, 27	3bitri 206	. . . . . . . . 9 ⊢ (𝑧recs(𝐹)𝑦 ↔ ∃ℎ(⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴))
29	7	sucid 4520	. . . . . . . . . . . . . . . . 17 ⊢ 𝑧 ∈ suc 𝑧
30		simpr 110	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴) → ℎ ∈ 𝐴)
31		vex 2806	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ℎ ∈ V
32	14, 31	tfrlem3a 6519	. . . . . . . . . . . . . . . . . . . . . . . . . 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 5442	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((ℎ Fn 𝑡 ∧ ⟨𝑧, 𝑦⟩ ∈ ℎ) → 𝑧 ∈ 𝑡)
38	35, 36, 37	syl2anc 411	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴) ∧ (𝑡 ∈ On ∧ (ℎ Fn 𝑡 ∧ ∀𝑒 ∈ 𝑡 (ℎ‘𝑒) = (𝐹‘(ℎ ↾ 𝑒))))) → 𝑧 ∈ 𝑡)
39		onelon 4487	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑡 ∈ On ∧ 𝑧 ∈ 𝑡) → 𝑧 ∈ On)
40	34, 38, 39	syl2anc 411	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴) ∧ (𝑡 ∈ On ∧ (ℎ Fn 𝑡 ∧ ∀𝑒 ∈ 𝑡 (ℎ‘𝑒) = (𝐹‘(ℎ ↾ 𝑒))))) → 𝑧 ∈ On)
41	33, 40	rexlimddv 2656	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴) → 𝑧 ∈ On)
42	41	adantl 277	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) → 𝑧 ∈ On)
43		onsuc 4605	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 ∈ On → suc 𝑧 ∈ On)
44	42, 43	syl 14	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) → suc 𝑧 ∈ On)
45		onsuc 4605	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (suc 𝑧 ∈ On → suc suc 𝑧 ∈ On)
46	44, 45	syl 14	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) → suc suc 𝑧 ∈ On)
47		onss 4597	. . . . . . . . . . . . . . . . . . . . 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 3214	. . . . . . . . . . . . . . . . . . . 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 3909	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) → ∪ (suc suc 𝑧 ∩ On) = ∪ suc suc 𝑧)
52		eloni 4478	. . . . . . . . . . . . . . . . . . . 20 ⊢ (suc 𝑧 ∈ On → Ord suc 𝑧)
53		ordtr 4481	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Ord suc 𝑧 → Tr suc 𝑧)
54	44, 52, 53	3syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) → Tr suc 𝑧)
55	8	unisuc 4516	. . . . . . . . . . . . . . . . . . 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 2264	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) → ∪ (suc suc 𝑧 ∩ On) = suc 𝑧)
58	29, 57	eleqtrrid 2321	. . . . . . . . . . . . . . . 16 ⊢ (((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) → 𝑧 ∈ ∪ (suc suc 𝑧 ∩ On))
59		fndm 5436	. . . . . . . . . . . . . . . . 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 2311	. . . . . . . . . . . . . . 15 ⊢ (((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) → 𝑧 ∈ dom 𝑔)
62	7	eldm 4934	. . . . . . . . . . . . . . 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 5426	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 = ∪ (suc suc 𝑧 ∩ On) → (𝑔 Fn 𝑣 ↔ 𝑔 Fn ∪ (suc suc 𝑧 ∩ On)))
66		raleq 2731	. . . . . . . . . . . . . . . . . . . . 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 2911	. . . . . . . . . . . . . . . . . . 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 2806	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑔 ∈ V
71	14, 70	tfrlem3a 6519	. . . . . . . . . . . . . . . . . 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 4094	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧ℎ𝑦 ↔ ⟨𝑧, 𝑦⟩ ∈ ℎ)
77	75, 76	sylibr 134	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) ∧ 𝑧𝑔𝑥) → 𝑧ℎ𝑦)
78	15	tfrlem5 6523	. . . . . . . . . . . . . . . . 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 4119	. . . . . . . . . . . . . 14 ⊢ ((((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) ∧ 𝑧𝑔𝑥) → 𝑧𝑔𝑦)
82	63, 81	exlimddv 1947	. . . . . . . . . . . . 13 ⊢ (((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) → 𝑧𝑔𝑦)
83		vex 2806	. . . . . . . . . . . . . 14 ⊢ 𝑦 ∈ V
84	7, 83	brelrn 4971	. . . . . . . . . . . . 13 ⊢ (𝑧𝑔𝑦 → 𝑦 ∈ ran 𝑔)
85	82, 84	syl 14	. . . . . . . . . . . 12 ⊢ (((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ ℎ ∧ ℎ ∈ 𝐴)) → 𝑦 ∈ ran 𝑔)
86		elssuni 3926	. . . . . . . . . . . 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 1867	. . . . . . . . 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 1922	. . . . . . 7 ⊢ ((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) → ∀𝑦(𝑧recs(𝐹)𝑦 → 𝑦 ⊆ ∪ ran 𝑔))
92		fvss 5662	. . . . . . 7 ⊢ (∀𝑦(𝑧recs(𝐹)𝑦 → 𝑦 ⊆ ∪ ran 𝑔) → (recs(𝐹)‘𝑧) ⊆ ∪ ran 𝑔)
93	91, 92	syl 14	. . . . . 6 ⊢ ((𝑔 Fn ∪ (suc suc 𝑧 ∩ On) ∧ ∀𝑤 ∈ ∪ (suc suc 𝑧 ∩ On)(𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) → (recs(𝐹)‘𝑧) ⊆ ∪ ran 𝑔)
94	70	rnex 5006	. . . . . . . 8 ⊢ ran 𝑔 ∈ V
95	94	uniex 4540	. . . . . . 7 ⊢ ∪ ran 𝑔 ∈ V
96	95	ssex 4231	. . . . . 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 2865	. 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 2202 {cab 2217 ∀wral 2511 ∃wrex 2512 Vcvv 2803 ∩ cin 3200 ⊆ wss 3201 ⟨cop 3676 ∪ cuni 3898 class class class wbr 4093 Tr wtr 4192 Ord word 4465 Oncon0 4466 suc csuc 4468 dom cdm 4731 ran crn 4732 ↾ cres 4733 Fun wfun 5327 Fn wfn 5328 ‘cfv 5333 recscrecs 6513

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 2204 ax-14 2205 ax-ext 2213 ax-coll 4209 ax-sep 4212 ax-pow 4270 ax-pr 4305 ax-un 4536 ax-setind 4641

This theorem depends on definitions: df-bi 117 df-3an 1007 df-tru 1401 df-fal 1404 df-nf 1510 df-sb 1811 df-eu 2082 df-mo 2083 df-clab 2218 df-cleq 2224 df-clel 2227 df-nfc 2364 df-ne 2404 df-ral 2516 df-rex 2517 df-reu 2518 df-rab 2520 df-v 2805 df-sbc 3033 df-csb 3129 df-dif 3203 df-un 3205 df-in 3207 df-ss 3214 df-nul 3497 df-pw 3658 df-sn 3679 df-pr 3680 df-op 3682 df-uni 3899 df-iun 3977 df-br 4094 df-opab 4156 df-mpt 4157 df-tr 4193 df-id 4396 df-iord 4469 df-on 4471 df-suc 4474 df-xp 4737 df-rel 4738 df-cnv 4739 df-co 4740 df-dm 4741 df-rn 4742 df-res 4743 df-ima 4744 df-iota 5293 df-fun 5335 df-fn 5336 df-f 5337 df-f1 5338 df-fo 5339 df-f1o 5340 df-fv 5341 df-recs 6514

This theorem is referenced by: tfrex 6577

W3C validator