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

Theorem tfrexlem 6325
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 5507 . . . . 5 (𝑧 = 𝐶 → (recs(𝐹)‘𝑧) = (recs(𝐹)‘𝐶))
21eleq1d 2244 . . . 4 (𝑧 = 𝐶 → ((recs(𝐹)‘𝑧) ∈ V ↔ (recs(𝐹)‘𝐶) ∈ V))
32imbi2d 230 . . 3 (𝑧 = 𝐶 → ((𝜑 → (recs(𝐹)‘𝑧) ∈ V) ↔ (𝜑 → (recs(𝐹)‘𝐶) ∈ V)))
4 inss2 3354 . . . . . . 7 (suc suc 𝑧 ∩ On) ⊆ On
5 ssorduni 4480 . . . . . . 7 ((suc suc 𝑧 ∩ On) ⊆ On → Ord (suc suc 𝑧 ∩ On))
64, 5ax-mp 5 . . . . . 6 Ord (suc suc 𝑧 ∩ On)
7 vex 2738 . . . . . . . . . 10 𝑧 ∈ V
87sucex 4492 . . . . . . . . 9 suc 𝑧 ∈ V
98sucex 4492 . . . . . . . 8 suc suc 𝑧 ∈ V
109inex1 4132 . . . . . . 7 (suc suc 𝑧 ∩ On) ∈ V
1110uniex 4431 . . . . . 6 (suc suc 𝑧 ∩ On) ∈ V
12 elon2 4370 . . . . . 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 6302 . . . . . 6 𝐴 = {𝑣 ∣ ∃𝑧 ∈ On (𝑣 Fn 𝑧 ∧ ∀𝑢𝑧 (𝑣𝑢) = (𝐹‘(𝑣𝑢)))}
16 tfrexlem.2 . . . . . . 7 (𝜑 → ∀𝑥(Fun 𝐹 ∧ (𝐹𝑥) ∈ V))
17 fveq2 5507 . . . . . . . . . 10 (𝑥 = 𝑧 → (𝐹𝑥) = (𝐹𝑧))
1817eleq1d 2244 . . . . . . . . 9 (𝑥 = 𝑧 → ((𝐹𝑥) ∈ V ↔ (𝐹𝑧) ∈ V))
1918anbi2d 464 . . . . . . . 8 (𝑥 = 𝑧 → ((Fun 𝐹 ∧ (𝐹𝑥) ∈ V) ↔ (Fun 𝐹 ∧ (𝐹𝑧) ∈ V)))
2019cbvalv 1915 . . . . . . 7 (∀𝑥(Fun 𝐹 ∧ (𝐹𝑥) ∈ V) ↔ ∀𝑧(Fun 𝐹 ∧ (𝐹𝑧) ∈ V))
2116, 20sylib 122 . . . . . 6 (𝜑 → ∀𝑧(Fun 𝐹 ∧ (𝐹𝑧) ∈ V))
2215, 21tfrlemi1 6323 . . . . 5 ((𝜑 (suc suc 𝑧 ∩ On) ∈ On) → ∃𝑔(𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))))
2313, 22mpan2 425 . . . 4 (𝜑 → ∃𝑔(𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))))
2415recsfval 6306 . . . . . . . . . . 11 recs(𝐹) = 𝐴
2524breqi 4004 . . . . . . . . . 10 (𝑧recs(𝐹)𝑦𝑧 𝐴𝑦)
26 df-br 3999 . . . . . . . . . 10 (𝑧 𝐴𝑦 ↔ ⟨𝑧, 𝑦⟩ ∈ 𝐴)
27 eluni 3808 . . . . . . . . . 10 (⟨𝑧, 𝑦⟩ ∈ 𝐴 ↔ ∃(⟨𝑧, 𝑦⟩ ∈ 𝐴))
2825, 26, 273bitri 206 . . . . . . . . 9 (𝑧recs(𝐹)𝑦 ↔ ∃(⟨𝑧, 𝑦⟩ ∈ 𝐴))
297sucid 4411 . . . . . . . . . . . . . . . . 17 𝑧 ∈ suc 𝑧
30 simpr 110 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((⟨𝑧, 𝑦⟩ ∈ 𝐴) → 𝐴)
31 vex 2738 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ∈ V
3214, 31tfrlem3a 6301 . . . . . . . . . . . . . . . . . . . . . . . . . 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 5311 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (( Fn 𝑡 ∧ ⟨𝑧, 𝑦⟩ ∈ ) → 𝑧𝑡)
3835, 36, 37syl2anc 411 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((⟨𝑧, 𝑦⟩ ∈ 𝐴) ∧ (𝑡 ∈ On ∧ ( Fn 𝑡 ∧ ∀𝑒𝑡 (𝑒) = (𝐹‘(𝑒))))) → 𝑧𝑡)
39 onelon 4378 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑡 ∈ On ∧ 𝑧𝑡) → 𝑧 ∈ On)
4034, 38, 39syl2anc 411 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((⟨𝑧, 𝑦⟩ ∈ 𝐴) ∧ (𝑡 ∈ On ∧ ( Fn 𝑡 ∧ ∀𝑒𝑡 (𝑒) = (𝐹‘(𝑒))))) → 𝑧 ∈ On)
4133, 40rexlimddv 2597 . . . . . . . . . . . . . . . . . . . . . . . 24 ((⟨𝑧, 𝑦⟩ ∈ 𝐴) → 𝑧 ∈ On)
4241adantl 277 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ 𝐴)) → 𝑧 ∈ On)
43 suceloni 4494 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 ∈ On → suc 𝑧 ∈ On)
4442, 43syl 14 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ 𝐴)) → suc 𝑧 ∈ On)
45 suceloni 4494 . . . . . . . . . . . . . . . . . . . . . 22 (suc 𝑧 ∈ On → suc suc 𝑧 ∈ On)
4644, 45syl 14 . . . . . . . . . . . . . . . . . . . . 21 (((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ 𝐴)) → suc suc 𝑧 ∈ On)
47 onss 4486 . . . . . . . . . . . . . . . . . . . . 21 (suc suc 𝑧 ∈ On → suc suc 𝑧 ⊆ On)
4846, 47syl 14 . . . . . . . . . . . . . . . . . . . 20 (((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ 𝐴)) → suc suc 𝑧 ⊆ On)
49 df-ss 3140 . . . . . . . . . . . . . . . . . . . 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 3816 . . . . . . . . . . . . . . . . . 18 (((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ 𝐴)) → (suc suc 𝑧 ∩ On) = suc suc 𝑧)
52 eloni 4369 . . . . . . . . . . . . . . . . . . . 20 (suc 𝑧 ∈ On → Ord suc 𝑧)
53 ordtr 4372 . . . . . . . . . . . . . . . . . . . 20 (Ord suc 𝑧 → Tr suc 𝑧)
5444, 52, 533syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ 𝐴)) → Tr suc 𝑧)
558unisuc 4407 . . . . . . . . . . . . . . . . . . 19 (Tr suc 𝑧 suc suc 𝑧 = suc 𝑧)
5654, 55sylib 122 . . . . . . . . . . . . . . . . . 18 (((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ 𝐴)) → suc suc 𝑧 = suc 𝑧)
5751, 56eqtrd 2208 . . . . . . . . . . . . . . . . 17 (((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ 𝐴)) → (suc suc 𝑧 ∩ On) = suc 𝑧)
5829, 57eleqtrrid 2265 . . . . . . . . . . . . . . . 16 (((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ 𝐴)) → 𝑧 (suc suc 𝑧 ∩ On))
59 fndm 5307 . . . . . . . . . . . . . . . . 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 2255 . . . . . . . . . . . . . . 15 (((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ 𝐴)) → 𝑧 ∈ dom 𝑔)
627eldm 4817 . . . . . . . . . . . . . . 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 5297 . . . . . . . . . . . . . . . . . . . . 21 (𝑣 = (suc suc 𝑧 ∩ On) → (𝑔 Fn 𝑣𝑔 Fn (suc suc 𝑧 ∩ On)))
66 raleq 2670 . . . . . . . . . . . . . . . . . . . . 21 (𝑣 = (suc suc 𝑧 ∩ On) → (∀𝑤𝑣 (𝑔𝑤) = (𝐹‘(𝑔𝑤)) ↔ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))))
6765, 66anbi12d 473 . . . . . . . . . . . . . . . . . . . 20 (𝑣 = (suc suc 𝑧 ∩ On) → ((𝑔 Fn 𝑣 ∧ ∀𝑤𝑣 (𝑔𝑤) = (𝐹‘(𝑔𝑤))) ↔ (𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤)))))
6867rspcev 2839 . . . . . . . . . . . . . . . . . . 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 2738 . . . . . . . . . . . . . . . . . . 19 𝑔 ∈ V
7114, 70tfrlem3a 6301 . . . . . . . . . . . . . . . . . 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 3999 . . . . . . . . . . . . . . . . 17 (𝑧𝑦 ↔ ⟨𝑧, 𝑦⟩ ∈ )
7775, 76sylibr 134 . . . . . . . . . . . . . . . 16 ((((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ 𝐴)) ∧ 𝑧𝑔𝑥) → 𝑧𝑦)
7815tfrlem5 6305 . . . . . . . . . . . . . . . . 17 ((𝑔𝐴𝐴) → ((𝑧𝑔𝑥𝑧𝑦) → 𝑥 = 𝑦))
7978imp 124 . . . . . . . . . . . . . . . 16 (((𝑔𝐴𝐴) ∧ (𝑧𝑔𝑥𝑧𝑦)) → 𝑥 = 𝑦)
8073, 74, 64, 77, 79syl22anc 1239 . . . . . . . . . . . . . . 15 ((((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ 𝐴)) ∧ 𝑧𝑔𝑥) → 𝑥 = 𝑦)
8164, 80breqtrd 4024 . . . . . . . . . . . . . 14 ((((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ 𝐴)) ∧ 𝑧𝑔𝑥) → 𝑧𝑔𝑦)
8263, 81exlimddv 1896 . . . . . . . . . . . . 13 (((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ 𝐴)) → 𝑧𝑔𝑦)
83 vex 2738 . . . . . . . . . . . . . 14 𝑦 ∈ V
847, 83brelrn 4853 . . . . . . . . . . . . 13 (𝑧𝑔𝑦𝑦 ∈ ran 𝑔)
8582, 84syl 14 . . . . . . . . . . . 12 (((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ 𝐴)) → 𝑦 ∈ ran 𝑔)
86 elssuni 3833 . . . . . . . . . . . 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 1817 . . . . . . . . 9 ((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) → (∃(⟨𝑧, 𝑦⟩ ∈ 𝐴) → 𝑦 ran 𝑔))
9028, 89biimtrid 152 . . . . . . . 8 ((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) → (𝑧recs(𝐹)𝑦𝑦 ran 𝑔))
9190alrimiv 1872 . . . . . . 7 ((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) → ∀𝑦(𝑧recs(𝐹)𝑦𝑦 ran 𝑔))
92 fvss 5521 . . . . . . 7 (∀𝑦(𝑧recs(𝐹)𝑦𝑦 ran 𝑔) → (recs(𝐹)‘𝑧) ⊆ ran 𝑔)
9391, 92syl 14 . . . . . 6 ((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) → (recs(𝐹)‘𝑧) ⊆ ran 𝑔)
9470rnex 4887 . . . . . . . 8 ran 𝑔 ∈ V
9594uniex 4431 . . . . . . 7 ran 𝑔 ∈ V
9695ssex 4135 . . . . . 6 ((recs(𝐹)‘𝑧) ⊆ ran 𝑔 → (recs(𝐹)‘𝑧) ∈ V)
9793, 96syl 14 . . . . 5 ((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) → (recs(𝐹)‘𝑧) ∈ V)
9897exlimiv 1596 . . . 4 (∃𝑔(𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) → (recs(𝐹)‘𝑧) ∈ V)
9923, 98syl 14 . . 3 (𝜑 → (recs(𝐹)‘𝑧) ∈ V)
1003, 99vtoclg 2795 . 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 1490  wcel 2146  {cab 2161  wral 2453  wrex 2454  Vcvv 2735  cin 3126  wss 3127  cop 3592   cuni 3805   class class class wbr 3998  Tr wtr 4096  Ord word 4356  Oncon0 4357  suc csuc 4359  dom cdm 4620  ran crn 4621  cres 4622  Fun wfun 5202   Fn wfn 5203  cfv 5208  recscrecs 6295
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 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-13 2148  ax-14 2149  ax-ext 2157  ax-coll 4113  ax-sep 4116  ax-pow 4169  ax-pr 4203  ax-un 4427  ax-setind 4530
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1459  df-sb 1761  df-eu 2027  df-mo 2028  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-ne 2346  df-ral 2458  df-rex 2459  df-reu 2460  df-rab 2462  df-v 2737  df-sbc 2961  df-csb 3056  df-dif 3129  df-un 3131  df-in 3133  df-ss 3140  df-nul 3421  df-pw 3574  df-sn 3595  df-pr 3596  df-op 3598  df-uni 3806  df-iun 3884  df-br 3999  df-opab 4060  df-mpt 4061  df-tr 4097  df-id 4287  df-iord 4360  df-on 4362  df-suc 4365  df-xp 4626  df-rel 4627  df-cnv 4628  df-co 4629  df-dm 4630  df-rn 4631  df-res 4632  df-ima 4633  df-iota 5170  df-fun 5210  df-fn 5211  df-f 5212  df-f1 5213  df-fo 5214  df-f1o 5215  df-fv 5216  df-recs 6296
This theorem is referenced by:  tfrex  6359
  Copyright terms: Public domain W3C validator