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

Theorem tfrexlem 6183
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 5373 . . . . 5 (𝑧 = 𝐶 → (recs(𝐹)‘𝑧) = (recs(𝐹)‘𝐶))
21eleq1d 2181 . . . 4 (𝑧 = 𝐶 → ((recs(𝐹)‘𝑧) ∈ V ↔ (recs(𝐹)‘𝐶) ∈ V))
32imbi2d 229 . . 3 (𝑧 = 𝐶 → ((𝜑 → (recs(𝐹)‘𝑧) ∈ V) ↔ (𝜑 → (recs(𝐹)‘𝐶) ∈ V)))
4 inss2 3261 . . . . . . 7 (suc suc 𝑧 ∩ On) ⊆ On
5 ssorduni 4361 . . . . . . 7 ((suc suc 𝑧 ∩ On) ⊆ On → Ord (suc suc 𝑧 ∩ On))
64, 5ax-mp 7 . . . . . 6 Ord (suc suc 𝑧 ∩ On)
7 vex 2658 . . . . . . . . . 10 𝑧 ∈ V
87sucex 4373 . . . . . . . . 9 suc 𝑧 ∈ V
98sucex 4373 . . . . . . . 8 suc suc 𝑧 ∈ V
109inex1 4020 . . . . . . 7 (suc suc 𝑧 ∩ On) ∈ V
1110uniex 4317 . . . . . 6 (suc suc 𝑧 ∩ On) ∈ V
12 elon2 4256 . . . . . 6 ( (suc suc 𝑧 ∩ On) ∈ On ↔ (Ord (suc suc 𝑧 ∩ On) ∧ (suc suc 𝑧 ∩ On) ∈ V))
136, 11, 12mpbir2an 907 . . . . 5 (suc suc 𝑧 ∩ On) ∈ On
14 tfrexlem.1 . . . . . . 7 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))}
1514tfrlem3 6160 . . . . . 6 𝐴 = {𝑣 ∣ ∃𝑧 ∈ On (𝑣 Fn 𝑧 ∧ ∀𝑢𝑧 (𝑣𝑢) = (𝐹‘(𝑣𝑢)))}
16 tfrexlem.2 . . . . . . 7 (𝜑 → ∀𝑥(Fun 𝐹 ∧ (𝐹𝑥) ∈ V))
17 fveq2 5373 . . . . . . . . . 10 (𝑥 = 𝑧 → (𝐹𝑥) = (𝐹𝑧))
1817eleq1d 2181 . . . . . . . . 9 (𝑥 = 𝑧 → ((𝐹𝑥) ∈ V ↔ (𝐹𝑧) ∈ V))
1918anbi2d 457 . . . . . . . 8 (𝑥 = 𝑧 → ((Fun 𝐹 ∧ (𝐹𝑥) ∈ V) ↔ (Fun 𝐹 ∧ (𝐹𝑧) ∈ V)))
2019cbvalv 1867 . . . . . . 7 (∀𝑥(Fun 𝐹 ∧ (𝐹𝑥) ∈ V) ↔ ∀𝑧(Fun 𝐹 ∧ (𝐹𝑧) ∈ V))
2116, 20sylib 121 . . . . . 6 (𝜑 → ∀𝑧(Fun 𝐹 ∧ (𝐹𝑧) ∈ V))
2215, 21tfrlemi1 6181 . . . . 5 ((𝜑 (suc suc 𝑧 ∩ On) ∈ On) → ∃𝑔(𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))))
2313, 22mpan2 419 . . . 4 (𝜑 → ∃𝑔(𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))))
2415recsfval 6164 . . . . . . . . . . 11 recs(𝐹) = 𝐴
2524breqi 3899 . . . . . . . . . 10 (𝑧recs(𝐹)𝑦𝑧 𝐴𝑦)
26 df-br 3894 . . . . . . . . . 10 (𝑧 𝐴𝑦 ↔ ⟨𝑧, 𝑦⟩ ∈ 𝐴)
27 eluni 3703 . . . . . . . . . 10 (⟨𝑧, 𝑦⟩ ∈ 𝐴 ↔ ∃(⟨𝑧, 𝑦⟩ ∈ 𝐴))
2825, 26, 273bitri 205 . . . . . . . . 9 (𝑧recs(𝐹)𝑦 ↔ ∃(⟨𝑧, 𝑦⟩ ∈ 𝐴))
297sucid 4297 . . . . . . . . . . . . . . . . 17 𝑧 ∈ suc 𝑧
30 simpr 109 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((⟨𝑧, 𝑦⟩ ∈ 𝐴) → 𝐴)
31 vex 2658 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ∈ V
3214, 31tfrlem3a 6159 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐴 ↔ ∃𝑡 ∈ On ( Fn 𝑡 ∧ ∀𝑒𝑡 (𝑒) = (𝐹‘(𝑒))))
3330, 32sylib 121 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((⟨𝑧, 𝑦⟩ ∈ 𝐴) → ∃𝑡 ∈ On ( Fn 𝑡 ∧ ∀𝑒𝑡 (𝑒) = (𝐹‘(𝑒))))
34 simprl 503 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((⟨𝑧, 𝑦⟩ ∈ 𝐴) ∧ (𝑡 ∈ On ∧ ( Fn 𝑡 ∧ ∀𝑒𝑡 (𝑒) = (𝐹‘(𝑒))))) → 𝑡 ∈ On)
35 simprrl 511 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((⟨𝑧, 𝑦⟩ ∈ 𝐴) ∧ (𝑡 ∈ On ∧ ( Fn 𝑡 ∧ ∀𝑒𝑡 (𝑒) = (𝐹‘(𝑒))))) → Fn 𝑡)
36 simpll 501 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((⟨𝑧, 𝑦⟩ ∈ 𝐴) ∧ (𝑡 ∈ On ∧ ( Fn 𝑡 ∧ ∀𝑒𝑡 (𝑒) = (𝐹‘(𝑒))))) → ⟨𝑧, 𝑦⟩ ∈ )
37 fnop 5182 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (( Fn 𝑡 ∧ ⟨𝑧, 𝑦⟩ ∈ ) → 𝑧𝑡)
3835, 36, 37syl2anc 406 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((⟨𝑧, 𝑦⟩ ∈ 𝐴) ∧ (𝑡 ∈ On ∧ ( Fn 𝑡 ∧ ∀𝑒𝑡 (𝑒) = (𝐹‘(𝑒))))) → 𝑧𝑡)
39 onelon 4264 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑡 ∈ On ∧ 𝑧𝑡) → 𝑧 ∈ On)
4034, 38, 39syl2anc 406 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((⟨𝑧, 𝑦⟩ ∈ 𝐴) ∧ (𝑡 ∈ On ∧ ( Fn 𝑡 ∧ ∀𝑒𝑡 (𝑒) = (𝐹‘(𝑒))))) → 𝑧 ∈ On)
4133, 40rexlimddv 2526 . . . . . . . . . . . . . . . . . . . . . . . 24 ((⟨𝑧, 𝑦⟩ ∈ 𝐴) → 𝑧 ∈ On)
4241adantl 273 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ 𝐴)) → 𝑧 ∈ On)
43 suceloni 4375 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 ∈ On → suc 𝑧 ∈ On)
4442, 43syl 14 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ 𝐴)) → suc 𝑧 ∈ On)
45 suceloni 4375 . . . . . . . . . . . . . . . . . . . . . 22 (suc 𝑧 ∈ On → suc suc 𝑧 ∈ On)
4644, 45syl 14 . . . . . . . . . . . . . . . . . . . . 21 (((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ 𝐴)) → suc suc 𝑧 ∈ On)
47 onss 4367 . . . . . . . . . . . . . . . . . . . . 21 (suc suc 𝑧 ∈ On → suc suc 𝑧 ⊆ On)
4846, 47syl 14 . . . . . . . . . . . . . . . . . . . 20 (((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ 𝐴)) → suc suc 𝑧 ⊆ On)
49 df-ss 3048 . . . . . . . . . . . . . . . . . . . 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 3711 . . . . . . . . . . . . . . . . . 18 (((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ 𝐴)) → (suc suc 𝑧 ∩ On) = suc suc 𝑧)
52 eloni 4255 . . . . . . . . . . . . . . . . . . . 20 (suc 𝑧 ∈ On → Ord suc 𝑧)
53 ordtr 4258 . . . . . . . . . . . . . . . . . . . 20 (Ord suc 𝑧 → Tr suc 𝑧)
5444, 52, 533syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ 𝐴)) → Tr suc 𝑧)
558unisuc 4293 . . . . . . . . . . . . . . . . . . 19 (Tr suc 𝑧 suc suc 𝑧 = suc 𝑧)
5654, 55sylib 121 . . . . . . . . . . . . . . . . . 18 (((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ 𝐴)) → suc suc 𝑧 = suc 𝑧)
5751, 56eqtrd 2145 . . . . . . . . . . . . . . . . 17 (((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ 𝐴)) → (suc suc 𝑧 ∩ On) = suc 𝑧)
5829, 57syl5eleqr 2202 . . . . . . . . . . . . . . . 16 (((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ 𝐴)) → 𝑧 (suc suc 𝑧 ∩ On))
59 fndm 5178 . . . . . . . . . . . . . . . . 17 (𝑔 Fn (suc suc 𝑧 ∩ On) → dom 𝑔 = (suc suc 𝑧 ∩ On))
6059ad2antrr 477 . . . . . . . . . . . . . . . 16 (((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ 𝐴)) → dom 𝑔 = (suc suc 𝑧 ∩ On))
6158, 60eleqtrrd 2192 . . . . . . . . . . . . . . 15 (((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ 𝐴)) → 𝑧 ∈ dom 𝑔)
627eldm 4694 . . . . . . . . . . . . . . 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 5168 . . . . . . . . . . . . . . . . . . . . 21 (𝑣 = (suc suc 𝑧 ∩ On) → (𝑔 Fn 𝑣𝑔 Fn (suc suc 𝑧 ∩ On)))
66 raleq 2598 . . . . . . . . . . . . . . . . . . . . 21 (𝑣 = (suc suc 𝑧 ∩ On) → (∀𝑤𝑣 (𝑔𝑤) = (𝐹‘(𝑔𝑤)) ↔ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))))
6765, 66anbi12d 462 . . . . . . . . . . . . . . . . . . . 20 (𝑣 = (suc suc 𝑧 ∩ On) → ((𝑔 Fn 𝑣 ∧ ∀𝑤𝑣 (𝑔𝑤) = (𝐹‘(𝑔𝑤))) ↔ (𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤)))))
6867rspcev 2758 . . . . . . . . . . . . . . . . . . 19 (( (suc suc 𝑧 ∩ On) ∈ On ∧ (𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤)))) → ∃𝑣 ∈ On (𝑔 Fn 𝑣 ∧ ∀𝑤𝑣 (𝑔𝑤) = (𝐹‘(𝑔𝑤))))
6913, 68mpan 418 . . . . . . . . . . . . . . . . . 18 ((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) → ∃𝑣 ∈ On (𝑔 Fn 𝑣 ∧ ∀𝑤𝑣 (𝑔𝑤) = (𝐹‘(𝑔𝑤))))
70 vex 2658 . . . . . . . . . . . . . . . . . . 19 𝑔 ∈ V
7114, 70tfrlem3a 6159 . . . . . . . . . . . . . . . . . 18 (𝑔𝐴 ↔ ∃𝑣 ∈ On (𝑔 Fn 𝑣 ∧ ∀𝑤𝑣 (𝑔𝑤) = (𝐹‘(𝑔𝑤))))
7269, 71sylibr 133 . . . . . . . . . . . . . . . . 17 ((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) → 𝑔𝐴)
7372ad2antrr 477 . . . . . . . . . . . . . . . 16 ((((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ 𝐴)) ∧ 𝑧𝑔𝑥) → 𝑔𝐴)
74 simplrr 508 . . . . . . . . . . . . . . . 16 ((((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ 𝐴)) ∧ 𝑧𝑔𝑥) → 𝐴)
75 simplrl 507 . . . . . . . . . . . . . . . . 17 ((((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ 𝐴)) ∧ 𝑧𝑔𝑥) → ⟨𝑧, 𝑦⟩ ∈ )
76 df-br 3894 . . . . . . . . . . . . . . . . 17 (𝑧𝑦 ↔ ⟨𝑧, 𝑦⟩ ∈ )
7775, 76sylibr 133 . . . . . . . . . . . . . . . 16 ((((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ 𝐴)) ∧ 𝑧𝑔𝑥) → 𝑧𝑦)
7815tfrlem5 6163 . . . . . . . . . . . . . . . . 17 ((𝑔𝐴𝐴) → ((𝑧𝑔𝑥𝑧𝑦) → 𝑥 = 𝑦))
7978imp 123 . . . . . . . . . . . . . . . 16 (((𝑔𝐴𝐴) ∧ (𝑧𝑔𝑥𝑧𝑦)) → 𝑥 = 𝑦)
8073, 74, 64, 77, 79syl22anc 1198 . . . . . . . . . . . . . . 15 ((((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ 𝐴)) ∧ 𝑧𝑔𝑥) → 𝑥 = 𝑦)
8164, 80breqtrd 3917 . . . . . . . . . . . . . 14 ((((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ 𝐴)) ∧ 𝑧𝑔𝑥) → 𝑧𝑔𝑦)
8263, 81exlimddv 1850 . . . . . . . . . . . . 13 (((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ 𝐴)) → 𝑧𝑔𝑦)
83 vex 2658 . . . . . . . . . . . . . 14 𝑦 ∈ V
847, 83brelrn 4730 . . . . . . . . . . . . 13 (𝑧𝑔𝑦𝑦 ∈ ran 𝑔)
8582, 84syl 14 . . . . . . . . . . . 12 (((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) ∧ (⟨𝑧, 𝑦⟩ ∈ 𝐴)) → 𝑦 ∈ ran 𝑔)
86 elssuni 3728 . . . . . . . . . . . 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 1771 . . . . . . . . 9 ((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) → (∃(⟨𝑧, 𝑦⟩ ∈ 𝐴) → 𝑦 ran 𝑔))
9028, 89syl5bi 151 . . . . . . . 8 ((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) → (𝑧recs(𝐹)𝑦𝑦 ran 𝑔))
9190alrimiv 1826 . . . . . . 7 ((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) → ∀𝑦(𝑧recs(𝐹)𝑦𝑦 ran 𝑔))
92 fvss 5387 . . . . . . 7 (∀𝑦(𝑧recs(𝐹)𝑦𝑦 ran 𝑔) → (recs(𝐹)‘𝑧) ⊆ ran 𝑔)
9391, 92syl 14 . . . . . 6 ((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) → (recs(𝐹)‘𝑧) ⊆ ran 𝑔)
9470rnex 4762 . . . . . . . 8 ran 𝑔 ∈ V
9594uniex 4317 . . . . . . 7 ran 𝑔 ∈ V
9695ssex 4023 . . . . . 6 ((recs(𝐹)‘𝑧) ⊆ ran 𝑔 → (recs(𝐹)‘𝑧) ∈ V)
9793, 96syl 14 . . . . 5 ((𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) → (recs(𝐹)‘𝑧) ∈ V)
9897exlimiv 1558 . . . 4 (∃𝑔(𝑔 Fn (suc suc 𝑧 ∩ On) ∧ ∀𝑤 (suc suc 𝑧 ∩ On)(𝑔𝑤) = (𝐹‘(𝑔𝑤))) → (recs(𝐹)‘𝑧) ∈ V)
9923, 98syl 14 . . 3 (𝜑 → (recs(𝐹)‘𝑧) ∈ V)
1003, 99vtoclg 2715 . 2 (𝐶𝑉 → (𝜑 → (recs(𝐹)‘𝐶) ∈ V))
101100impcom 124 1 ((𝜑𝐶𝑉) → (recs(𝐹)‘𝐶) ∈ V)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wal 1310   = wceq 1312  wex 1449  wcel 1461  {cab 2099  wral 2388  wrex 2389  Vcvv 2655  cin 3034  wss 3035  cop 3494   cuni 3700   class class class wbr 3893  Tr wtr 3984  Ord word 4242  Oncon0 4243  suc csuc 4245  dom cdm 4497  ran crn 4498  cres 4499  Fun wfun 5073   Fn wfn 5074  cfv 5079  recscrecs 6153
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 586  ax-in2 587  ax-io 681  ax-5 1404  ax-7 1405  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-8 1463  ax-10 1464  ax-11 1465  ax-i12 1466  ax-bndl 1467  ax-4 1468  ax-13 1472  ax-14 1473  ax-17 1487  ax-i9 1491  ax-ial 1495  ax-i5r 1496  ax-ext 2095  ax-coll 4001  ax-sep 4004  ax-pow 4056  ax-pr 4089  ax-un 4313  ax-setind 4410
This theorem depends on definitions:  df-bi 116  df-3an 945  df-tru 1315  df-fal 1318  df-nf 1418  df-sb 1717  df-eu 1976  df-mo 1977  df-clab 2100  df-cleq 2106  df-clel 2109  df-nfc 2242  df-ne 2281  df-ral 2393  df-rex 2394  df-reu 2395  df-rab 2397  df-v 2657  df-sbc 2877  df-csb 2970  df-dif 3037  df-un 3039  df-in 3041  df-ss 3048  df-nul 3328  df-pw 3476  df-sn 3497  df-pr 3498  df-op 3500  df-uni 3701  df-iun 3779  df-br 3894  df-opab 3948  df-mpt 3949  df-tr 3985  df-id 4173  df-iord 4246  df-on 4248  df-suc 4251  df-xp 4503  df-rel 4504  df-cnv 4505  df-co 4506  df-dm 4507  df-rn 4508  df-res 4509  df-ima 4510  df-iota 5044  df-fun 5081  df-fn 5082  df-f 5083  df-f1 5084  df-fo 5085  df-f1o 5086  df-fv 5087  df-recs 6154
This theorem is referenced by:  tfrex  6217
  Copyright terms: Public domain W3C validator