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

Theorem frecabcl 6303
Description: The class abstraction from df-frec 6295 exists. Unlike frecabex 6302 the function 𝐹 only needs to be defined on 𝑆, not all sets. This is a lemma for other finite recursion proofs. (Contributed by Jim Kingdon, 21-Mar-2022.)
Hypotheses
Ref Expression
frecabcl.n (𝜑𝑁 ∈ ω)
frecabcl.g (𝜑𝐺:𝑁𝑆)
frecabcl.fs (𝜑 → ∀𝑦𝑆 (𝐹𝑦) ∈ 𝑆)
frecabcl.as (𝜑𝐴𝑆)
Assertion
Ref Expression
frecabcl (𝜑 → {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴))} ∈ 𝑆)
Distinct variable groups:   𝐴,𝑚,𝑥   𝑚,𝐹,𝑥,𝑦   𝑚,𝐺,𝑥,𝑦   𝑚,𝑁,𝑥,𝑦   𝑥,𝑆,𝑦   𝜑,𝑚,𝑥,𝑦
Allowed substitution hints:   𝐴(𝑦)   𝑆(𝑚)

Proof of Theorem frecabcl
Dummy variables 𝑘 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 frecabcl.as . . . . 5 (𝜑𝐴𝑆)
21adantr 274 . . . 4 ((𝜑𝑁 = ∅) → 𝐴𝑆)
3 peano1 4515 . . . . . . . . 9 ∅ ∈ ω
4 elex2 2705 . . . . . . . . 9 (∅ ∈ ω → ∃𝑎 𝑎 ∈ ω)
5 r19.9rmv 3458 . . . . . . . . 9 (∃𝑎 𝑎 ∈ ω → (𝑥𝐴 ↔ ∃𝑚 ∈ ω 𝑥𝐴))
63, 4, 5mp2b 8 . . . . . . . 8 (𝑥𝐴 ↔ ∃𝑚 ∈ ω 𝑥𝐴)
7 frecabcl.g . . . . . . . . . . . . . . 15 (𝜑𝐺:𝑁𝑆)
8 fdm 5285 . . . . . . . . . . . . . . 15 (𝐺:𝑁𝑆 → dom 𝐺 = 𝑁)
97, 8syl 14 . . . . . . . . . . . . . 14 (𝜑 → dom 𝐺 = 𝑁)
109adantr 274 . . . . . . . . . . . . 13 ((𝜑𝑁 = ∅) → dom 𝐺 = 𝑁)
11 eqeq2 2150 . . . . . . . . . . . . . 14 (𝑁 = ∅ → (dom 𝐺 = 𝑁 ↔ dom 𝐺 = ∅))
1211adantl 275 . . . . . . . . . . . . 13 ((𝜑𝑁 = ∅) → (dom 𝐺 = 𝑁 ↔ dom 𝐺 = ∅))
1310, 12mpbid 146 . . . . . . . . . . . 12 ((𝜑𝑁 = ∅) → dom 𝐺 = ∅)
1413adantr 274 . . . . . . . . . . 11 (((𝜑𝑁 = ∅) ∧ 𝑚 ∈ ω) → dom 𝐺 = ∅)
1514biantrurd 303 . . . . . . . . . 10 (((𝜑𝑁 = ∅) ∧ 𝑚 ∈ ω) → (𝑥𝐴 ↔ (dom 𝐺 = ∅ ∧ 𝑥𝐴)))
16 peano3 4517 . . . . . . . . . . . . . . . 16 (𝑚 ∈ ω → suc 𝑚 ≠ ∅)
1716adantl 275 . . . . . . . . . . . . . . 15 (((𝜑𝑁 = ∅) ∧ 𝑚 ∈ ω) → suc 𝑚 ≠ ∅)
1817, 14neeqtrrd 2339 . . . . . . . . . . . . . 14 (((𝜑𝑁 = ∅) ∧ 𝑚 ∈ ω) → suc 𝑚 ≠ dom 𝐺)
1918necomd 2395 . . . . . . . . . . . . 13 (((𝜑𝑁 = ∅) ∧ 𝑚 ∈ ω) → dom 𝐺 ≠ suc 𝑚)
2019neneqd 2330 . . . . . . . . . . . 12 (((𝜑𝑁 = ∅) ∧ 𝑚 ∈ ω) → ¬ dom 𝐺 = suc 𝑚)
2120intnanrd 918 . . . . . . . . . . 11 (((𝜑𝑁 = ∅) ∧ 𝑚 ∈ ω) → ¬ (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))))
22 biorf 734 . . . . . . . . . . 11 (¬ (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) → ((dom 𝐺 = ∅ ∧ 𝑥𝐴) ↔ ((dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴))))
2321, 22syl 14 . . . . . . . . . 10 (((𝜑𝑁 = ∅) ∧ 𝑚 ∈ ω) → ((dom 𝐺 = ∅ ∧ 𝑥𝐴) ↔ ((dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴))))
2415, 23bitrd 187 . . . . . . . . 9 (((𝜑𝑁 = ∅) ∧ 𝑚 ∈ ω) → (𝑥𝐴 ↔ ((dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴))))
2524rexbidva 2435 . . . . . . . 8 ((𝜑𝑁 = ∅) → (∃𝑚 ∈ ω 𝑥𝐴 ↔ ∃𝑚 ∈ ω ((dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴))))
266, 25syl5bb 191 . . . . . . 7 ((𝜑𝑁 = ∅) → (𝑥𝐴 ↔ ∃𝑚 ∈ ω ((dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴))))
27 r19.44mv 3461 . . . . . . . 8 (∃𝑎 𝑎 ∈ ω → (∃𝑚 ∈ ω ((dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴)) ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴))))
283, 4, 27mp2b 8 . . . . . . 7 (∃𝑚 ∈ ω ((dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴)) ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴)))
2926, 28syl6bb 195 . . . . . 6 ((𝜑𝑁 = ∅) → (𝑥𝐴 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴))))
3029alrimiv 1847 . . . . 5 ((𝜑𝑁 = ∅) → ∀𝑥(𝑥𝐴 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴))))
312, 30jca 304 . . . 4 ((𝜑𝑁 = ∅) → (𝐴𝑆 ∧ ∀𝑥(𝑥𝐴 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴)))))
32 eleq1 2203 . . . . . 6 (𝑧 = 𝐴 → (𝑧𝑆𝐴𝑆))
33 eleq2 2204 . . . . . . . 8 (𝑧 = 𝐴 → (𝑥𝑧𝑥𝐴))
3433bibi1d 232 . . . . . . 7 (𝑧 = 𝐴 → ((𝑥𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴))) ↔ (𝑥𝐴 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴)))))
3534albidv 1797 . . . . . 6 (𝑧 = 𝐴 → (∀𝑥(𝑥𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴))) ↔ ∀𝑥(𝑥𝐴 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴)))))
3632, 35anbi12d 465 . . . . 5 (𝑧 = 𝐴 → ((𝑧𝑆 ∧ ∀𝑥(𝑥𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴)))) ↔ (𝐴𝑆 ∧ ∀𝑥(𝑥𝐴 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴))))))
3736spcegv 2777 . . . 4 (𝐴𝑆 → ((𝐴𝑆 ∧ ∀𝑥(𝑥𝐴 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴)))) → ∃𝑧(𝑧𝑆 ∧ ∀𝑥(𝑥𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴))))))
382, 31, 37sylc 62 . . 3 ((𝜑𝑁 = ∅) → ∃𝑧(𝑧𝑆 ∧ ∀𝑥(𝑥𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴)))))
39 fveq2 5428 . . . . . . . . 9 (𝑦 = (𝐺𝑘) → (𝐹𝑦) = (𝐹‘(𝐺𝑘)))
4039eleq1d 2209 . . . . . . . 8 (𝑦 = (𝐺𝑘) → ((𝐹𝑦) ∈ 𝑆 ↔ (𝐹‘(𝐺𝑘)) ∈ 𝑆))
41 frecabcl.fs . . . . . . . . 9 (𝜑 → ∀𝑦𝑆 (𝐹𝑦) ∈ 𝑆)
4241ad2antrr 480 . . . . . . . 8 (((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → ∀𝑦𝑆 (𝐹𝑦) ∈ 𝑆)
437ad2antrr 480 . . . . . . . . 9 (((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → 𝐺:𝑁𝑆)
44 vex 2692 . . . . . . . . . . . 12 𝑘 ∈ V
4544sucid 4346 . . . . . . . . . . 11 𝑘 ∈ suc 𝑘
46 eleq2 2204 . . . . . . . . . . 11 (𝑁 = suc 𝑘 → (𝑘𝑁𝑘 ∈ suc 𝑘))
4745, 46mpbiri 167 . . . . . . . . . 10 (𝑁 = suc 𝑘𝑘𝑁)
4847adantl 275 . . . . . . . . 9 (((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → 𝑘𝑁)
4943, 48ffvelrnd 5563 . . . . . . . 8 (((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → (𝐺𝑘) ∈ 𝑆)
5040, 42, 49rspcdva 2797 . . . . . . 7 (((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → (𝐹‘(𝐺𝑘)) ∈ 𝑆)
51 simpllr 524 . . . . . . . . . . . . 13 ((((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑥 ∈ (𝐹‘(𝐺𝑘))) → 𝑘 ∈ ω)
5243, 8syl 14 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → dom 𝐺 = 𝑁)
5352adantr 274 . . . . . . . . . . . . . . 15 ((((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑥 ∈ (𝐹‘(𝐺𝑘))) → dom 𝐺 = 𝑁)
54 simplr 520 . . . . . . . . . . . . . . 15 ((((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑥 ∈ (𝐹‘(𝐺𝑘))) → 𝑁 = suc 𝑘)
5553, 54eqtrd 2173 . . . . . . . . . . . . . 14 ((((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑥 ∈ (𝐹‘(𝐺𝑘))) → dom 𝐺 = suc 𝑘)
56 simpr 109 . . . . . . . . . . . . . 14 ((((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑥 ∈ (𝐹‘(𝐺𝑘))) → 𝑥 ∈ (𝐹‘(𝐺𝑘)))
5755, 56jca 304 . . . . . . . . . . . . 13 ((((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑥 ∈ (𝐹‘(𝐺𝑘))) → (dom 𝐺 = suc 𝑘𝑥 ∈ (𝐹‘(𝐺𝑘))))
58 suceq 4331 . . . . . . . . . . . . . . . 16 (𝑚 = 𝑘 → suc 𝑚 = suc 𝑘)
5958eqeq2d 2152 . . . . . . . . . . . . . . 15 (𝑚 = 𝑘 → (dom 𝐺 = suc 𝑚 ↔ dom 𝐺 = suc 𝑘))
60 fveq2 5428 . . . . . . . . . . . . . . . . 17 (𝑚 = 𝑘 → (𝐺𝑚) = (𝐺𝑘))
6160fveq2d 5432 . . . . . . . . . . . . . . . 16 (𝑚 = 𝑘 → (𝐹‘(𝐺𝑚)) = (𝐹‘(𝐺𝑘)))
6261eleq2d 2210 . . . . . . . . . . . . . . 15 (𝑚 = 𝑘 → (𝑥 ∈ (𝐹‘(𝐺𝑚)) ↔ 𝑥 ∈ (𝐹‘(𝐺𝑘))))
6359, 62anbi12d 465 . . . . . . . . . . . . . 14 (𝑚 = 𝑘 → ((dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ↔ (dom 𝐺 = suc 𝑘𝑥 ∈ (𝐹‘(𝐺𝑘)))))
6463rspcev 2792 . . . . . . . . . . . . 13 ((𝑘 ∈ ω ∧ (dom 𝐺 = suc 𝑘𝑥 ∈ (𝐹‘(𝐺𝑘)))) → ∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))))
6551, 57, 64syl2anc 409 . . . . . . . . . . . 12 ((((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑥 ∈ (𝐹‘(𝐺𝑘))) → ∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))))
6665ex 114 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → (𝑥 ∈ (𝐹‘(𝐺𝑘)) → ∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚)))))
67 simpr 109 . . . . . . . . . . . . . . 15 ((dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) → 𝑥 ∈ (𝐹‘(𝐺𝑚)))
6867adantl 275 . . . . . . . . . . . . . 14 (((((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚)))) → 𝑥 ∈ (𝐹‘(𝐺𝑚)))
6952ad2antrr 480 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚)))) → dom 𝐺 = 𝑁)
70 simprl 521 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚)))) → dom 𝐺 = suc 𝑚)
71 simpllr 524 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚)))) → 𝑁 = suc 𝑘)
7269, 70, 713eqtr3rd 2182 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚)))) → suc 𝑘 = suc 𝑚)
73 simplr 520 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → 𝑘 ∈ ω)
7473ad2antrr 480 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚)))) → 𝑘 ∈ ω)
75 simplr 520 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚)))) → 𝑚 ∈ ω)
76 peano4 4518 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ω ∧ 𝑚 ∈ ω) → (suc 𝑘 = suc 𝑚𝑘 = 𝑚))
7774, 75, 76syl2anc 409 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚)))) → (suc 𝑘 = suc 𝑚𝑘 = 𝑚))
7872, 77mpbid 146 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚)))) → 𝑘 = 𝑚)
7978fveq2d 5432 . . . . . . . . . . . . . . . 16 (((((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚)))) → (𝐺𝑘) = (𝐺𝑚))
8079fveq2d 5432 . . . . . . . . . . . . . . 15 (((((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚)))) → (𝐹‘(𝐺𝑘)) = (𝐹‘(𝐺𝑚)))
8180eleq2d 2210 . . . . . . . . . . . . . 14 (((((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚)))) → (𝑥 ∈ (𝐹‘(𝐺𝑘)) ↔ 𝑥 ∈ (𝐹‘(𝐺𝑚))))
8268, 81mpbird 166 . . . . . . . . . . . . 13 (((((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚)))) → 𝑥 ∈ (𝐹‘(𝐺𝑘)))
8382ex 114 . . . . . . . . . . . 12 ((((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) → ((dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) → 𝑥 ∈ (𝐹‘(𝐺𝑘))))
8483rexlimdva 2552 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) → 𝑥 ∈ (𝐹‘(𝐺𝑘))))
8566, 84impbid 128 . . . . . . . . . 10 (((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → (𝑥 ∈ (𝐹‘(𝐺𝑘)) ↔ ∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚)))))
8685alrimiv 1847 . . . . . . . . 9 (((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → ∀𝑥(𝑥 ∈ (𝐹‘(𝐺𝑘)) ↔ ∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚)))))
87 peano3 4517 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ ω → suc 𝑘 ≠ ∅)
8873, 87syl 14 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → suc 𝑘 ≠ ∅)
89 neeq1 2322 . . . . . . . . . . . . . . . . . 18 (𝑁 = suc 𝑘 → (𝑁 ≠ ∅ ↔ suc 𝑘 ≠ ∅))
9089adantl 275 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → (𝑁 ≠ ∅ ↔ suc 𝑘 ≠ ∅))
9188, 90mpbird 166 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → 𝑁 ≠ ∅)
9252, 91eqnetrd 2333 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → dom 𝐺 ≠ ∅)
9392neneqd 2330 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → ¬ dom 𝐺 = ∅)
9493intnanrd 918 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → ¬ (dom 𝐺 = ∅ ∧ 𝑥𝐴))
95 biorf 734 . . . . . . . . . . . . 13 (¬ (dom 𝐺 = ∅ ∧ 𝑥𝐴) → (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ↔ ((dom 𝐺 = ∅ ∧ 𝑥𝐴) ∨ ∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))))))
9694, 95syl 14 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ↔ ((dom 𝐺 = ∅ ∧ 𝑥𝐴) ∨ ∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))))))
97 orcom 718 . . . . . . . . . . . 12 (((dom 𝐺 = ∅ ∧ 𝑥𝐴) ∨ ∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚)))) ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴)))
9896, 97syl6bb 195 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴))))
9998bibi2d 231 . . . . . . . . . 10 (((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → ((𝑥 ∈ (𝐹‘(𝐺𝑘)) ↔ ∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚)))) ↔ (𝑥 ∈ (𝐹‘(𝐺𝑘)) ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴)))))
10099albidv 1797 . . . . . . . . 9 (((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → (∀𝑥(𝑥 ∈ (𝐹‘(𝐺𝑘)) ↔ ∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚)))) ↔ ∀𝑥(𝑥 ∈ (𝐹‘(𝐺𝑘)) ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴)))))
10186, 100mpbid 146 . . . . . . . 8 (((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → ∀𝑥(𝑥 ∈ (𝐹‘(𝐺𝑘)) ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴))))
10250, 101jca 304 . . . . . . 7 (((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → ((𝐹‘(𝐺𝑘)) ∈ 𝑆 ∧ ∀𝑥(𝑥 ∈ (𝐹‘(𝐺𝑘)) ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴)))))
103 eleq1 2203 . . . . . . . . 9 (𝑧 = (𝐹‘(𝐺𝑘)) → (𝑧𝑆 ↔ (𝐹‘(𝐺𝑘)) ∈ 𝑆))
104 eleq2 2204 . . . . . . . . . . 11 (𝑧 = (𝐹‘(𝐺𝑘)) → (𝑥𝑧𝑥 ∈ (𝐹‘(𝐺𝑘))))
105104bibi1d 232 . . . . . . . . . 10 (𝑧 = (𝐹‘(𝐺𝑘)) → ((𝑥𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴))) ↔ (𝑥 ∈ (𝐹‘(𝐺𝑘)) ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴)))))
106105albidv 1797 . . . . . . . . 9 (𝑧 = (𝐹‘(𝐺𝑘)) → (∀𝑥(𝑥𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴))) ↔ ∀𝑥(𝑥 ∈ (𝐹‘(𝐺𝑘)) ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴)))))
107103, 106anbi12d 465 . . . . . . . 8 (𝑧 = (𝐹‘(𝐺𝑘)) → ((𝑧𝑆 ∧ ∀𝑥(𝑥𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴)))) ↔ ((𝐹‘(𝐺𝑘)) ∈ 𝑆 ∧ ∀𝑥(𝑥 ∈ (𝐹‘(𝐺𝑘)) ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴))))))
108107spcegv 2777 . . . . . . 7 ((𝐹‘(𝐺𝑘)) ∈ 𝑆 → (((𝐹‘(𝐺𝑘)) ∈ 𝑆 ∧ ∀𝑥(𝑥 ∈ (𝐹‘(𝐺𝑘)) ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴)))) → ∃𝑧(𝑧𝑆 ∧ ∀𝑥(𝑥𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴))))))
10950, 102, 108sylc 62 . . . . . 6 (((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → ∃𝑧(𝑧𝑆 ∧ ∀𝑥(𝑥𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴)))))
110109ex 114 . . . . 5 ((𝜑𝑘 ∈ ω) → (𝑁 = suc 𝑘 → ∃𝑧(𝑧𝑆 ∧ ∀𝑥(𝑥𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴))))))
111110rexlimdva 2552 . . . 4 (𝜑 → (∃𝑘 ∈ ω 𝑁 = suc 𝑘 → ∃𝑧(𝑧𝑆 ∧ ∀𝑥(𝑥𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴))))))
112111imp 123 . . 3 ((𝜑 ∧ ∃𝑘 ∈ ω 𝑁 = suc 𝑘) → ∃𝑧(𝑧𝑆 ∧ ∀𝑥(𝑥𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴)))))
113 frecabcl.n . . . 4 (𝜑𝑁 ∈ ω)
114 nn0suc 4525 . . . 4 (𝑁 ∈ ω → (𝑁 = ∅ ∨ ∃𝑘 ∈ ω 𝑁 = suc 𝑘))
115113, 114syl 14 . . 3 (𝜑 → (𝑁 = ∅ ∨ ∃𝑘 ∈ ω 𝑁 = suc 𝑘))
11638, 112, 115mpjaodan 788 . 2 (𝜑 → ∃𝑧(𝑧𝑆 ∧ ∀𝑥(𝑥𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴)))))
117 clabel 2267 . 2 ({𝑥 ∣ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴))} ∈ 𝑆 ↔ ∃𝑧(𝑧𝑆 ∧ ∀𝑥(𝑥𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴)))))
118116, 117sylibr 133 1 (𝜑 → {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴))} ∈ 𝑆)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 103  wb 104  wo 698  wal 1330   = wceq 1332  wex 1469  wcel 1481  {cab 2126  wne 2309  wral 2417  wrex 2418  c0 3367  suc csuc 4294  ωcom 4511  dom cdm 4546  wf 5126  cfv 5130
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-sep 4053  ax-nul 4061  ax-pow 4105  ax-pr 4138  ax-un 4362  ax-setind 4459  ax-iinf 4509
This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1335  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-v 2691  df-sbc 2913  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-int 3779  df-br 3937  df-opab 3997  df-id 4222  df-suc 4300  df-iom 4512  df-xp 4552  df-rel 4553  df-cnv 4554  df-co 4555  df-dm 4556  df-rn 4557  df-iota 5095  df-fun 5132  df-fn 5133  df-f 5134  df-fv 5138
This theorem is referenced by:  freccllem  6306  frecfcllem  6308  frecsuclem  6310
  Copyright terms: Public domain W3C validator