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

Theorem tfrexlem 6329
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 5511 . . . . 5 (𝑧 = 𝐶 → (recs(𝐹)‘𝑧) = (recs(𝐹)‘𝐶))
21eleq1d 2246 . . . 4 (𝑧 = 𝐶 → ((recs(𝐹)‘𝑧) ∈ V ↔ (recs(𝐹)‘𝐶) ∈ V))
32imbi2d 230 . . 3 (𝑧 = 𝐶 → ((𝜑 → (recs(𝐹)‘𝑧) ∈ V) ↔ (𝜑 → (recs(𝐹)‘𝐶) ∈ V)))
4 inss2 3356 . . . . . . 7 (suc suc 𝑧 ∩ On) ⊆ On
5 ssorduni 4483 . . . . . . 7 ((suc suc 𝑧 ∩ On) ⊆ On → Ord (suc suc 𝑧 ∩ On))
64, 5ax-mp 5 . . . . . 6 Ord (suc suc 𝑧 ∩ On)
7 vex 2740 . . . . . . . . . 10 𝑧 ∈ V
87sucex 4495 . . . . . . . . 9 suc 𝑧 ∈ V
98sucex 4495 . . . . . . . 8 suc suc 𝑧 ∈ V
109inex1 4134 . . . . . . 7 (suc suc 𝑧 ∩ On) ∈ V
1110uniex 4434 . . . . . 6 (suc suc 𝑧 ∩ On) ∈ V
12 elon2 4373 . . . . . 6 ( (suc suc 𝑧 ∩ On) ∈ On ↔ (Ord (suc suc 𝑧 ∩ On) ∧ (suc suc 𝑧 ∩ On) ∈ V))
136, 11, 12mpbir2an 942 . . . . 5 (suc suc 𝑧 ∩ On) ∈ On
14 tfrexlem.1 . . . . . . 7 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))}
1514tfrlem3 6306 . . . . . 6 𝐴 = {𝑣 ∣ ∃𝑧 ∈ On (𝑣 Fn 𝑧 ∧ ∀𝑢𝑧 (𝑣𝑢) = (𝐹‘(𝑣𝑢)))}
16 tfrexlem.2 . . . . . . 7 (𝜑 → ∀𝑥(Fun 𝐹 ∧ (𝐹𝑥) ∈ V))
17 fveq2 5511 . . . . . . . . . 10 (𝑥 = 𝑧 → (𝐹𝑥) = (𝐹𝑧))
1817eleq1d 2246 . . . . . . . . 9 (𝑥 = 𝑧 → ((𝐹𝑥) ∈ V ↔ (𝐹𝑧) ∈ V))
1918anbi2d 464 . . . . . . . 8 (𝑥 = 𝑧 → ((Fun 𝐹 ∧ (𝐹𝑥) ∈ V) ↔ (Fun 𝐹 ∧ (𝐹𝑧) ∈ V)))
2019cbvalv 1917 . . . . . . 7 (∀𝑥(Fun 𝐹 ∧ (𝐹𝑥) ∈ V) ↔ ∀𝑧(Fun 𝐹 ∧ (𝐹𝑧) ∈ V))
2116, 20sylib 122 . . . . . 6 (𝜑 → ∀𝑧(Fun 𝐹 ∧ (𝐹𝑧) ∈ V))
2215, 21tfrlemi1 6327 . . . . 5 ((𝜑 (suc suc 𝑧 ∩ On) ∈ On) → ∃𝑔(𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))))
2313, 22mpan2 425 . . . 4 (𝜑 → ∃𝑔(𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))))
2415recsfval 6310 . . . . . . . . . . 11 recs(𝐹) = 𝐴
2524breqi 4006 . . . . . . . . . 10 (𝑧recs(𝐹)𝑦𝑧 𝐴𝑦)
26 df-br 4001 . . . . . . . . . 10 (𝑧 𝐴𝑦 ↔ ⟨𝑧, 𝑦⟩ ∈ 𝐴)
27 eluni 3810 . . . . . . . . . 10 (⟨𝑧, 𝑦⟩ ∈ 𝐴 ↔ ∃(⟨𝑧, 𝑦⟩ ∈ 𝐴))
2825, 26, 273bitri 206 . . . . . . . . 9 (𝑧recs(𝐹)𝑦 ↔ ∃(⟨𝑧, 𝑦⟩ ∈ 𝐴))
297sucid 4414 . . . . . . . . . . . . . . . . 17 𝑧 ∈ suc 𝑧
30 simpr 110 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((⟨𝑧, 𝑦⟩ ∈ 𝐴) → 𝐴)
31 vex 2740 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ∈ V
3214, 31tfrlem3a 6305 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐴 ↔ ∃𝑡 ∈ On ( Fn 𝑡 ∧ ∀𝑒𝑡 (𝑒) = (𝐹‘(𝑒))))
3330, 32sylib 122 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((⟨𝑧, 𝑦⟩ ∈ 𝐴) → ∃𝑡 ∈ On ( Fn 𝑡 ∧ ∀𝑒𝑡 (𝑒) = (𝐹‘(𝑒))))
34 simprl 529 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((⟨𝑧, 𝑦⟩ ∈ 𝐴) ∧ (𝑡 ∈ On ∧ ( Fn 𝑡 ∧ ∀𝑒𝑡 (𝑒) = (𝐹‘(𝑒))))) → 𝑡 ∈ On)
35 simprrl 539 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((⟨𝑧, 𝑦⟩ ∈ 𝐴) ∧ (𝑡 ∈ On ∧ ( Fn 𝑡 ∧ ∀𝑒𝑡 (𝑒) = (𝐹‘(𝑒))))) → Fn 𝑡)
36 simpll 527 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((⟨𝑧, 𝑦⟩ ∈ 𝐴) ∧ (𝑡 ∈ On ∧ ( Fn 𝑡 ∧ ∀𝑒𝑡 (𝑒) = (𝐹‘(𝑒))))) → ⟨𝑧, 𝑦⟩ ∈ )
37 fnop 5315 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (( Fn 𝑡 ∧ ⟨𝑧, 𝑦⟩ ∈ ) → 𝑧𝑡)
3835, 36, 37syl2anc 411 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((⟨𝑧, 𝑦⟩ ∈ 𝐴) ∧ (𝑡 ∈ On ∧ ( Fn 𝑡 ∧ ∀𝑒𝑡 (𝑒) = (𝐹‘(𝑒))))) → 𝑧𝑡)
39 onelon 4381 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑡 ∈ On ∧ 𝑧𝑡) → 𝑧 ∈ On)
4034, 38, 39syl2anc 411 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((⟨𝑧, 𝑦⟩ ∈ 𝐴) ∧ (𝑡 ∈ On ∧ ( Fn 𝑡 ∧ ∀𝑒𝑡 (𝑒) = (𝐹‘(𝑒))))) → 𝑧 ∈ On)
4133, 40rexlimddv 2599 . . . . . . . . . . . . . . . . . . . . . . . 24 ((⟨𝑧, 𝑦⟩ ∈ 𝐴) → 𝑧 ∈ On)
4241adantl 277 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ 𝐴)) → 𝑧 ∈ On)
43 onsuc 4497 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 ∈ On → suc 𝑧 ∈ On)
4442, 43syl 14 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ 𝐴)) → suc 𝑧 ∈ On)
45 onsuc 4497 . . . . . . . . . . . . . . . . . . . . . 22 (suc 𝑧 ∈ On → suc suc 𝑧 ∈ On)
4644, 45syl 14 . . . . . . . . . . . . . . . . . . . . 21 (((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ 𝐴)) → suc suc 𝑧 ∈ On)
47 onss 4489 . . . . . . . . . . . . . . . . . . . . 21 (suc suc 𝑧 ∈ On → suc suc 𝑧 ⊆ On)
4846, 47syl 14 . . . . . . . . . . . . . . . . . . . 20 (((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ 𝐴)) → suc suc 𝑧 ⊆ On)
49 df-ss 3142 . . . . . . . . . . . . . . . . . . . 20 (suc suc 𝑧 ⊆ On ↔ (suc suc 𝑧 ∩ On) = suc suc 𝑧)
5048, 49sylib 122 . . . . . . . . . . . . . . . . . . 19 (((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ 𝐴)) → (suc suc 𝑧 ∩ On) = suc suc 𝑧)
5150unieqd 3818 . . . . . . . . . . . . . . . . . 18 (((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ 𝐴)) → (suc suc 𝑧 ∩ On) = suc suc 𝑧)
52 eloni 4372 . . . . . . . . . . . . . . . . . . . 20 (suc 𝑧 ∈ On → Ord suc 𝑧)
53 ordtr 4375 . . . . . . . . . . . . . . . . . . . 20 (Ord suc 𝑧 → Tr suc 𝑧)
5444, 52, 533syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ 𝐴)) → Tr suc 𝑧)
558unisuc 4410 . . . . . . . . . . . . . . . . . . 19 (Tr suc 𝑧 suc suc 𝑧 = suc 𝑧)
5654, 55sylib 122 . . . . . . . . . . . . . . . . . 18 (((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ 𝐴)) → suc suc 𝑧 = suc 𝑧)
5751, 56eqtrd 2210 . . . . . . . . . . . . . . . . 17 (((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ 𝐴)) → (suc suc 𝑧 ∩ On) = suc 𝑧)
5829, 57eleqtrrid 2267 . . . . . . . . . . . . . . . 16 (((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ 𝐴)) → 𝑧 (suc suc 𝑧 ∩ On))
59 fndm 5311 . . . . . . . . . . . . . . . . 17 (𝑔 Fn (suc suc 𝑧 ∩ On) → dom 𝑔 = (suc suc 𝑧 ∩ On))
6059ad2antrr 488 . . . . . . . . . . . . . . . 16 (((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ 𝐴)) → dom 𝑔 = (suc suc 𝑧 ∩ On))
6158, 60eleqtrrd 2257 . . . . . . . . . . . . . . 15 (((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ 𝐴)) → 𝑧 ∈ dom 𝑔)
627eldm 4820 . . . . . . . . . . . . . . 15 (𝑧 ∈ dom 𝑔 ↔ ∃𝑥 𝑧𝑔𝑥)
6361, 62sylib 122 . . . . . . . . . . . . . 14 (((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ 𝐴)) → ∃𝑥 𝑧𝑔𝑥)
64 simpr 110 . . . . . . . . . . . . . . 15 ((((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ 𝐴)) ∧ 𝑧𝑔𝑥) → 𝑧𝑔𝑥)
65 fneq2 5301 . . . . . . . . . . . . . . . . . . . . 21 (𝑣 = (suc suc 𝑧 ∩ On) → (𝑔 Fn 𝑣𝑔 Fn (suc suc 𝑧 ∩ On)))
66 raleq 2672 . . . . . . . . . . . . . . . . . . . . 21 (𝑣 = (suc suc 𝑧 ∩ On) → (∀𝑤𝑣 (𝑔𝑤) = (𝐹‘(𝑔𝑤)) ↔ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))))
6765, 66anbi12d 473 . . . . . . . . . . . . . . . . . . . 20 (𝑣 = (suc suc 𝑧 ∩ On) → ((𝑔 Fn 𝑣 ∧ ∀𝑤𝑣 (𝑔𝑤) = (𝐹‘(𝑔𝑤))) ↔ (𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤)))))
6867rspcev 2841 . . . . . . . . . . . . . . . . . . 19 (( (suc suc 𝑧 ∩ On) ∈ On ∧ (𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤)))) → ∃𝑣 ∈ On (𝑔 Fn 𝑣 ∧ ∀𝑤𝑣 (𝑔𝑤) = (𝐹‘(𝑔𝑤))))
6913, 68mpan 424 . . . . . . . . . . . . . . . . . 18 ((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) → ∃𝑣 ∈ On (𝑔 Fn 𝑣 ∧ ∀𝑤𝑣 (𝑔𝑤) = (𝐹‘(𝑔𝑤))))
70 vex 2740 . . . . . . . . . . . . . . . . . . 19 𝑔 ∈ V
7114, 70tfrlem3a 6305 . . . . . . . . . . . . . . . . . 18 (𝑔𝐴 ↔ ∃𝑣 ∈ On (𝑔 Fn 𝑣 ∧ ∀𝑤𝑣 (𝑔𝑤) = (𝐹‘(𝑔𝑤))))
7269, 71sylibr 134 . . . . . . . . . . . . . . . . 17 ((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) → 𝑔𝐴)
7372ad2antrr 488 . . . . . . . . . . . . . . . 16 ((((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ 𝐴)) ∧ 𝑧𝑔𝑥) → 𝑔𝐴)
74 simplrr 536 . . . . . . . . . . . . . . . 16 ((((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ 𝐴)) ∧ 𝑧𝑔𝑥) → 𝐴)
75 simplrl 535 . . . . . . . . . . . . . . . . 17 ((((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ 𝐴)) ∧ 𝑧𝑔𝑥) → ⟨𝑧, 𝑦⟩ ∈ )
76 df-br 4001 . . . . . . . . . . . . . . . . 17 (𝑧𝑦 ↔ ⟨𝑧, 𝑦⟩ ∈ )
7775, 76sylibr 134 . . . . . . . . . . . . . . . 16 ((((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ 𝐴)) ∧ 𝑧𝑔𝑥) → 𝑧𝑦)
7815tfrlem5 6309 . . . . . . . . . . . . . . . . 17 ((𝑔𝐴𝐴) → ((𝑧𝑔𝑥𝑧𝑦) → 𝑥 = 𝑦))
7978imp 124 . . . . . . . . . . . . . . . 16 (((𝑔𝐴𝐴) ∧ (𝑧𝑔𝑥𝑧𝑦)) → 𝑥 = 𝑦)
8073, 74, 64, 77, 79syl22anc 1239 . . . . . . . . . . . . . . 15 ((((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ 𝐴)) ∧ 𝑧𝑔𝑥) → 𝑥 = 𝑦)
8164, 80breqtrd 4026 . . . . . . . . . . . . . 14 ((((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ 𝐴)) ∧ 𝑧𝑔𝑥) → 𝑧𝑔𝑦)
8263, 81exlimddv 1898 . . . . . . . . . . . . 13 (((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ 𝐴)) → 𝑧𝑔𝑦)
83 vex 2740 . . . . . . . . . . . . . 14 𝑦 ∈ V
847, 83brelrn 4856 . . . . . . . . . . . . 13 (𝑧𝑔𝑦𝑦 ∈ ran 𝑔)
8582, 84syl 14 . . . . . . . . . . . 12 (((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ 𝐴)) → 𝑦 ∈ ran 𝑔)
86 elssuni 3835 . . . . . . . . . . . 12 (𝑦 ∈ ran 𝑔𝑦 ran 𝑔)
8785, 86syl 14 . . . . . . . . . . 11 (((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ 𝐴)) → 𝑦 ran 𝑔)
8887ex 115 . . . . . . . . . 10 ((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) → ((⟨𝑧, 𝑦⟩ ∈ 𝐴) → 𝑦 ran 𝑔))
8988exlimdv 1819 . . . . . . . . 9 ((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) → (∃(⟨𝑧, 𝑦⟩ ∈ 𝐴) → 𝑦 ran 𝑔))
9028, 89biimtrid 152 . . . . . . . 8 ((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) → (𝑧recs(𝐹)𝑦𝑦 ran 𝑔))
9190alrimiv 1874 . . . . . . 7 ((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) → ∀𝑦(𝑧recs(𝐹)𝑦𝑦 ran 𝑔))
92 fvss 5525 . . . . . . 7 (∀𝑦(𝑧recs(𝐹)𝑦𝑦 ran 𝑔) → (recs(𝐹)‘𝑧) ⊆ ran 𝑔)
9391, 92syl 14 . . . . . 6 ((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) → (recs(𝐹)‘𝑧) ⊆ ran 𝑔)
9470rnex 4890 . . . . . . . 8 ran 𝑔 ∈ V
9594uniex 4434 . . . . . . 7 ran 𝑔 ∈ V
9695ssex 4137 . . . . . 6 ((recs(𝐹)‘𝑧) ⊆ ran 𝑔 → (recs(𝐹)‘𝑧) ∈ V)
9793, 96syl 14 . . . . 5 ((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) → (recs(𝐹)‘𝑧) ∈ V)
9897exlimiv 1598 . . . 4 (∃𝑔(𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) → (recs(𝐹)‘𝑧) ∈ V)
9923, 98syl 14 . . 3 (𝜑 → (recs(𝐹)‘𝑧) ∈ V)
1003, 99vtoclg 2797 . 2 (𝐶𝑉 → (𝜑 → (recs(𝐹)‘𝐶) ∈ V))
101100impcom 125 1 ((𝜑𝐶𝑉) → (recs(𝐹)‘𝐶) ∈ V)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wal 1351   = wceq 1353  wex 1492  wcel 2148  {cab 2163  wral 2455  wrex 2456  Vcvv 2737  cin 3128  wss 3129  cop 3594   cuni 3807   class class class wbr 4000  Tr wtr 4098  Ord word 4359  Oncon0 4360  suc csuc 4362  dom cdm 4623  ran crn 4624  cres 4625  Fun wfun 5206   Fn wfn 5207  cfv 5212  recscrecs 6299
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 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-coll 4115  ax-sep 4118  ax-pow 4171  ax-pr 4206  ax-un 4430  ax-setind 4533
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-ral 2460  df-rex 2461  df-reu 2462  df-rab 2464  df-v 2739  df-sbc 2963  df-csb 3058  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-nul 3423  df-pw 3576  df-sn 3597  df-pr 3598  df-op 3600  df-uni 3808  df-iun 3886  df-br 4001  df-opab 4062  df-mpt 4063  df-tr 4099  df-id 4290  df-iord 4363  df-on 4365  df-suc 4368  df-xp 4629  df-rel 4630  df-cnv 4631  df-co 4632  df-dm 4633  df-rn 4634  df-res 4635  df-ima 4636  df-iota 5174  df-fun 5214  df-fn 5215  df-f 5216  df-f1 5217  df-fo 5218  df-f1o 5219  df-fv 5220  df-recs 6300
This theorem is referenced by:  tfrex  6363
  Copyright terms: Public domain W3C validator