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

Theorem tfrexlem 6238
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.
StepHypRef Expression
1 fveq2 5428 . . . . 5 (𝑧 = 𝐶 → (recs(𝐹)‘𝑧) = (recs(𝐹)‘𝐶))
21eleq1d 2209 . . . 4 (𝑧 = 𝐶 → ((recs(𝐹)‘𝑧) ∈ V ↔ (recs(𝐹)‘𝐶) ∈ V))
32imbi2d 229 . . 3 (𝑧 = 𝐶 → ((𝜑 → (recs(𝐹)‘𝑧) ∈ V) ↔ (𝜑 → (recs(𝐹)‘𝐶) ∈ V)))
4 inss2 3301 . . . . . . 7 (suc suc 𝑧 ∩ On) ⊆ On
5 ssorduni 4410 . . . . . . 7 ((suc suc 𝑧 ∩ On) ⊆ On → Ord (suc suc 𝑧 ∩ On))
64, 5ax-mp 5 . . . . . 6 Ord (suc suc 𝑧 ∩ On)
7 vex 2692 . . . . . . . . . 10 𝑧 ∈ V
87sucex 4422 . . . . . . . . 9 suc 𝑧 ∈ V
98sucex 4422 . . . . . . . 8 suc suc 𝑧 ∈ V
109inex1 4069 . . . . . . 7 (suc suc 𝑧 ∩ On) ∈ V
1110uniex 4366 . . . . . 6 (suc suc 𝑧 ∩ On) ∈ V
12 elon2 4305 . . . . . 6 ( (suc suc 𝑧 ∩ On) ∈ On ↔ (Ord (suc suc 𝑧 ∩ On) ∧ (suc suc 𝑧 ∩ On) ∈ V))
136, 11, 12mpbir2an 927 . . . . 5 (suc suc 𝑧 ∩ On) ∈ On
14 tfrexlem.1 . . . . . . 7 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))}
1514tfrlem3 6215 . . . . . 6 𝐴 = {𝑣 ∣ ∃𝑧 ∈ On (𝑣 Fn 𝑧 ∧ ∀𝑢𝑧 (𝑣𝑢) = (𝐹‘(𝑣𝑢)))}
16 tfrexlem.2 . . . . . . 7 (𝜑 → ∀𝑥(Fun 𝐹 ∧ (𝐹𝑥) ∈ V))
17 fveq2 5428 . . . . . . . . . 10 (𝑥 = 𝑧 → (𝐹𝑥) = (𝐹𝑧))
1817eleq1d 2209 . . . . . . . . 9 (𝑥 = 𝑧 → ((𝐹𝑥) ∈ V ↔ (𝐹𝑧) ∈ V))
1918anbi2d 460 . . . . . . . 8 (𝑥 = 𝑧 → ((Fun 𝐹 ∧ (𝐹𝑥) ∈ V) ↔ (Fun 𝐹 ∧ (𝐹𝑧) ∈ V)))
2019cbvalv 1890 . . . . . . 7 (∀𝑥(Fun 𝐹 ∧ (𝐹𝑥) ∈ V) ↔ ∀𝑧(Fun 𝐹 ∧ (𝐹𝑧) ∈ V))
2116, 20sylib 121 . . . . . 6 (𝜑 → ∀𝑧(Fun 𝐹 ∧ (𝐹𝑧) ∈ V))
2215, 21tfrlemi1 6236 . . . . 5 ((𝜑 (suc suc 𝑧 ∩ On) ∈ On) → ∃𝑔(𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))))
2313, 22mpan2 422 . . . 4 (𝜑 → ∃𝑔(𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))))
2415recsfval 6219 . . . . . . . . . . 11 recs(𝐹) = 𝐴
2524breqi 3942 . . . . . . . . . 10 (𝑧recs(𝐹)𝑦𝑧 𝐴𝑦)
26 df-br 3937 . . . . . . . . . 10 (𝑧 𝐴𝑦 ↔ ⟨𝑧, 𝑦⟩ ∈ 𝐴)
27 eluni 3746 . . . . . . . . . 10 (⟨𝑧, 𝑦⟩ ∈ 𝐴 ↔ ∃(⟨𝑧, 𝑦⟩ ∈ 𝐴))
2825, 26, 273bitri 205 . . . . . . . . 9 (𝑧recs(𝐹)𝑦 ↔ ∃(⟨𝑧, 𝑦⟩ ∈ 𝐴))
297sucid 4346 . . . . . . . . . . . . . . . . 17 𝑧 ∈ suc 𝑧
30 simpr 109 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((⟨𝑧, 𝑦⟩ ∈ 𝐴) → 𝐴)
31 vex 2692 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ∈ V
3214, 31tfrlem3a 6214 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐴 ↔ ∃𝑡 ∈ On ( Fn 𝑡 ∧ ∀𝑒𝑡 (𝑒) = (𝐹‘(𝑒))))
3330, 32sylib 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 5233 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (( Fn 𝑡 ∧ ⟨𝑧, 𝑦⟩ ∈ ) → 𝑧𝑡)
3835, 36, 37syl2anc 409 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((⟨𝑧, 𝑦⟩ ∈ 𝐴) ∧ (𝑡 ∈ On ∧ ( Fn 𝑡 ∧ ∀𝑒𝑡 (𝑒) = (𝐹‘(𝑒))))) → 𝑧𝑡)
39 onelon 4313 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑡 ∈ On ∧ 𝑧𝑡) → 𝑧 ∈ On)
4034, 38, 39syl2anc 409 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((⟨𝑧, 𝑦⟩ ∈ 𝐴) ∧ (𝑡 ∈ On ∧ ( Fn 𝑡 ∧ ∀𝑒𝑡 (𝑒) = (𝐹‘(𝑒))))) → 𝑧 ∈ On)
4133, 40rexlimddv 2557 . . . . . . . . . . . . . . . . . . . . . . . 24 ((⟨𝑧, 𝑦⟩ ∈ 𝐴) → 𝑧 ∈ On)
4241adantl 275 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ 𝐴)) → 𝑧 ∈ On)
43 suceloni 4424 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 ∈ On → suc 𝑧 ∈ On)
4442, 43syl 14 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ 𝐴)) → suc 𝑧 ∈ On)
45 suceloni 4424 . . . . . . . . . . . . . . . . . . . . . 22 (suc 𝑧 ∈ On → suc suc 𝑧 ∈ On)
4644, 45syl 14 . . . . . . . . . . . . . . . . . . . . 21 (((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ 𝐴)) → suc suc 𝑧 ∈ On)
47 onss 4416 . . . . . . . . . . . . . . . . . . . . 21 (suc suc 𝑧 ∈ On → suc suc 𝑧 ⊆ On)
4846, 47syl 14 . . . . . . . . . . . . . . . . . . . 20 (((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ 𝐴)) → suc suc 𝑧 ⊆ On)
49 df-ss 3088 . . . . . . . . . . . . . . . . . . . 20 (suc suc 𝑧 ⊆ On ↔ (suc suc 𝑧 ∩ On) = suc suc 𝑧)
5048, 49sylib 121 . . . . . . . . . . . . . . . . . . 19 (((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ 𝐴)) → (suc suc 𝑧 ∩ On) = suc suc 𝑧)
5150unieqd 3754 . . . . . . . . . . . . . . . . . 18 (((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ 𝐴)) → (suc suc 𝑧 ∩ On) = suc suc 𝑧)
52 eloni 4304 . . . . . . . . . . . . . . . . . . . 20 (suc 𝑧 ∈ On → Ord suc 𝑧)
53 ordtr 4307 . . . . . . . . . . . . . . . . . . . 20 (Ord suc 𝑧 → Tr suc 𝑧)
5444, 52, 533syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ 𝐴)) → Tr suc 𝑧)
558unisuc 4342 . . . . . . . . . . . . . . . . . . 19 (Tr suc 𝑧 suc suc 𝑧 = suc 𝑧)
5654, 55sylib 121 . . . . . . . . . . . . . . . . . 18 (((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ 𝐴)) → suc suc 𝑧 = suc 𝑧)
5751, 56eqtrd 2173 . . . . . . . . . . . . . . . . 17 (((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ 𝐴)) → (suc suc 𝑧 ∩ On) = suc 𝑧)
5829, 57eleqtrrid 2230 . . . . . . . . . . . . . . . 16 (((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ 𝐴)) → 𝑧 (suc suc 𝑧 ∩ On))
59 fndm 5229 . . . . . . . . . . . . . . . . 17 (𝑔 Fn (suc suc 𝑧 ∩ On) → dom 𝑔 = (suc suc 𝑧 ∩ On))
6059ad2antrr 480 . . . . . . . . . . . . . . . 16 (((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ 𝐴)) → dom 𝑔 = (suc suc 𝑧 ∩ On))
6158, 60eleqtrrd 2220 . . . . . . . . . . . . . . 15 (((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ 𝐴)) → 𝑧 ∈ dom 𝑔)
627eldm 4743 . . . . . . . . . . . . . . 15 (𝑧 ∈ dom 𝑔 ↔ ∃𝑥 𝑧𝑔𝑥)
6361, 62sylib 121 . . . . . . . . . . . . . 14 (((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ 𝐴)) → ∃𝑥 𝑧𝑔𝑥)
64 simpr 109 . . . . . . . . . . . . . . 15 ((((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ 𝐴)) ∧ 𝑧𝑔𝑥) → 𝑧𝑔𝑥)
65 fneq2 5219 . . . . . . . . . . . . . . . . . . . . 21 (𝑣 = (suc suc 𝑧 ∩ On) → (𝑔 Fn 𝑣𝑔 Fn (suc suc 𝑧 ∩ On)))
66 raleq 2629 . . . . . . . . . . . . . . . . . . . . 21 (𝑣 = (suc suc 𝑧 ∩ On) → (∀𝑤𝑣 (𝑔𝑤) = (𝐹‘(𝑔𝑤)) ↔ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))))
6765, 66anbi12d 465 . . . . . . . . . . . . . . . . . . . 20 (𝑣 = (suc suc 𝑧 ∩ On) → ((𝑔 Fn 𝑣 ∧ ∀𝑤𝑣 (𝑔𝑤) = (𝐹‘(𝑔𝑤))) ↔ (𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤)))))
6867rspcev 2792 . . . . . . . . . . . . . . . . . . 19 (( (suc suc 𝑧 ∩ On) ∈ On ∧ (𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤)))) → ∃𝑣 ∈ On (𝑔 Fn 𝑣 ∧ ∀𝑤𝑣 (𝑔𝑤) = (𝐹‘(𝑔𝑤))))
6913, 68mpan 421 . . . . . . . . . . . . . . . . . 18 ((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) → ∃𝑣 ∈ On (𝑔 Fn 𝑣 ∧ ∀𝑤𝑣 (𝑔𝑤) = (𝐹‘(𝑔𝑤))))
70 vex 2692 . . . . . . . . . . . . . . . . . . 19 𝑔 ∈ V
7114, 70tfrlem3a 6214 . . . . . . . . . . . . . . . . . 18 (𝑔𝐴 ↔ ∃𝑣 ∈ On (𝑔 Fn 𝑣 ∧ ∀𝑤𝑣 (𝑔𝑤) = (𝐹‘(𝑔𝑤))))
7269, 71sylibr 133 . . . . . . . . . . . . . . . . 17 ((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) → 𝑔𝐴)
7372ad2antrr 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 3937 . . . . . . . . . . . . . . . . 17 (𝑧𝑦 ↔ ⟨𝑧, 𝑦⟩ ∈ )
7775, 76sylibr 133 . . . . . . . . . . . . . . . 16 ((((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ 𝐴)) ∧ 𝑧𝑔𝑥) → 𝑧𝑦)
7815tfrlem5 6218 . . . . . . . . . . . . . . . . 17 ((𝑔𝐴𝐴) → ((𝑧𝑔𝑥𝑧𝑦) → 𝑥 = 𝑦))
7978imp 123 . . . . . . . . . . . . . . . 16 (((𝑔𝐴𝐴) ∧ (𝑧𝑔𝑥𝑧𝑦)) → 𝑥 = 𝑦)
8073, 74, 64, 77, 79syl22anc 1218 . . . . . . . . . . . . . . 15 ((((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ 𝐴)) ∧ 𝑧𝑔𝑥) → 𝑥 = 𝑦)
8164, 80breqtrd 3961 . . . . . . . . . . . . . 14 ((((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ 𝐴)) ∧ 𝑧𝑔𝑥) → 𝑧𝑔𝑦)
8263, 81exlimddv 1871 . . . . . . . . . . . . 13 (((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ 𝐴)) → 𝑧𝑔𝑦)
83 vex 2692 . . . . . . . . . . . . . 14 𝑦 ∈ V
847, 83brelrn 4779 . . . . . . . . . . . . 13 (𝑧𝑔𝑦𝑦 ∈ ran 𝑔)
8582, 84syl 14 . . . . . . . . . . . 12 (((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ 𝐴)) → 𝑦 ∈ ran 𝑔)
86 elssuni 3771 . . . . . . . . . . . 12 (𝑦 ∈ ran 𝑔𝑦 ran 𝑔)
8785, 86syl 14 . . . . . . . . . . 11 (((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ 𝐴)) → 𝑦 ran 𝑔)
8887ex 114 . . . . . . . . . 10 ((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) → ((⟨𝑧, 𝑦⟩ ∈ 𝐴) → 𝑦 ran 𝑔))
8988exlimdv 1792 . . . . . . . . 9 ((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) → (∃(⟨𝑧, 𝑦⟩ ∈ 𝐴) → 𝑦 ran 𝑔))
9028, 89syl5bi 151 . . . . . . . 8 ((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) → (𝑧recs(𝐹)𝑦𝑦 ran 𝑔))
9190alrimiv 1847 . . . . . . 7 ((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) → ∀𝑦(𝑧recs(𝐹)𝑦𝑦 ran 𝑔))
92 fvss 5442 . . . . . . 7 (∀𝑦(𝑧recs(𝐹)𝑦𝑦 ran 𝑔) → (recs(𝐹)‘𝑧) ⊆ ran 𝑔)
9391, 92syl 14 . . . . . 6 ((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) → (recs(𝐹)‘𝑧) ⊆ ran 𝑔)
9470rnex 4813 . . . . . . . 8 ran 𝑔 ∈ V
9594uniex 4366 . . . . . . 7 ran 𝑔 ∈ V
9695ssex 4072 . . . . . 6 ((recs(𝐹)‘𝑧) ⊆ ran 𝑔 → (recs(𝐹)‘𝑧) ∈ V)
9793, 96syl 14 . . . . 5 ((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) → (recs(𝐹)‘𝑧) ∈ V)
9897exlimiv 1578 . . . 4 (∃𝑔(𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) → (recs(𝐹)‘𝑧) ∈ V)
9923, 98syl 14 . . 3 (𝜑 → (recs(𝐹)‘𝑧) ∈ V)
1003, 99vtoclg 2749 . 2 (𝐶𝑉 → (𝜑 → (recs(𝐹)‘𝐶) ∈ V))
101100impcom 124 1 ((𝜑𝐶𝑉) → (recs(𝐹)‘𝐶) ∈ V)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wal 1330   = wceq 1332  wex 1469  wcel 1481  {cab 2126  wral 2417  wrex 2418  Vcvv 2689  cin 3074  wss 3075  cop 3534   cuni 3743   class class class wbr 3936  Tr wtr 4033  Ord word 4291  Oncon0 4292  suc csuc 4294  dom cdm 4546  ran crn 4547  cres 4548  Fun wfun 5124   Fn wfn 5125  cfv 5130  recscrecs 6208
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 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-13 1492  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-coll 4050  ax-sep 4053  ax-pow 4105  ax-pr 4138  ax-un 4362  ax-setind 4459
This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1335  df-fal 1338  df-nf 1438  df-sb 1737  df-eu 2003  df-mo 2004  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ne 2310  df-ral 2422  df-rex 2423  df-reu 2424  df-rab 2426  df-v 2691  df-sbc 2913  df-csb 3007  df-dif 3077  df-un 3079  df-in 3081  df-ss 3088  df-nul 3368  df-pw 3516  df-sn 3537  df-pr 3538  df-op 3540  df-uni 3744  df-iun 3822  df-br 3937  df-opab 3997  df-mpt 3998  df-tr 4034  df-id 4222  df-iord 4295  df-on 4297  df-suc 4300  df-xp 4552  df-rel 4553  df-cnv 4554  df-co 4555  df-dm 4556  df-rn 4557  df-res 4558  df-ima 4559  df-iota 5095  df-fun 5132  df-fn 5133  df-f 5134  df-f1 5135  df-fo 5136  df-f1o 5137  df-fv 5138  df-recs 6209
This theorem is referenced by:  tfrex  6272
  Copyright terms: Public domain W3C validator