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

Theorem frecabcl 6376
Description: The class abstraction from df-frec 6368 exists. Unlike frecabex 6375 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 4576 . . . . . . . . 9 ∅ ∈ ω
4 elex2 2746 . . . . . . . . 9 (∅ ∈ ω → ∃𝑎 𝑎 ∈ ω)
5 r19.9rmv 3505 . . . . . . . . 9 (∃𝑎 𝑎 ∈ ω → (𝑥𝐴 ↔ ∃𝑚 ∈ ω 𝑥𝐴))
63, 4, 5mp2b 8 . . . . . . . 8 (𝑥𝐴 ↔ ∃𝑚 ∈ ω 𝑥𝐴)
7 frecabcl.g . . . . . . . . . . . . . . 15 (𝜑𝐺:𝑁𝑆)
8 fdm 5351 . . . . . . . . . . . . . . 15 (𝐺:𝑁𝑆 → dom 𝐺 = 𝑁)
97, 8syl 14 . . . . . . . . . . . . . 14 (𝜑 → dom 𝐺 = 𝑁)
109adantr 274 . . . . . . . . . . . . 13 ((𝜑𝑁 = ∅) → dom 𝐺 = 𝑁)
11 eqeq2 2180 . . . . . . . . . . . . . 14 (𝑁 = ∅ → (dom 𝐺 = 𝑁 ↔ dom 𝐺 = ∅))
1211adantl 275 . . . . . . . . . . . . 13 ((𝜑𝑁 = ∅) → (dom 𝐺 = 𝑁 ↔ dom 𝐺 = ∅))
1310, 12mpbid 146 . . . . . . . . . . . 12 ((𝜑𝑁 = ∅) → dom 𝐺 = ∅)
1413adantr 274 . . . . . . . . . . 11 (((𝜑𝑁 = ∅) ∧ 𝑚 ∈ ω) → dom 𝐺 = ∅)
1514biantrurd 303 . . . . . . . . . 10 (((𝜑𝑁 = ∅) ∧ 𝑚 ∈ ω) → (𝑥𝐴 ↔ (dom 𝐺 = ∅ ∧ 𝑥𝐴)))
16 peano3 4578 . . . . . . . . . . . . . . . 16 (𝑚 ∈ ω → suc 𝑚 ≠ ∅)
1716adantl 275 . . . . . . . . . . . . . . 15 (((𝜑𝑁 = ∅) ∧ 𝑚 ∈ ω) → suc 𝑚 ≠ ∅)
1817, 14neeqtrrd 2370 . . . . . . . . . . . . . 14 (((𝜑𝑁 = ∅) ∧ 𝑚 ∈ ω) → suc 𝑚 ≠ dom 𝐺)
1918necomd 2426 . . . . . . . . . . . . 13 (((𝜑𝑁 = ∅) ∧ 𝑚 ∈ ω) → dom 𝐺 ≠ suc 𝑚)
2019neneqd 2361 . . . . . . . . . . . 12 (((𝜑𝑁 = ∅) ∧ 𝑚 ∈ ω) → ¬ dom 𝐺 = suc 𝑚)
2120intnanrd 927 . . . . . . . . . . 11 (((𝜑𝑁 = ∅) ∧ 𝑚 ∈ ω) → ¬ (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))))
22 biorf 739 . . . . . . . . . . 11 (¬ (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) → ((dom 𝐺 = ∅ ∧ 𝑥𝐴) ↔ ((dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴))))
2321, 22syl 14 . . . . . . . . . 10 (((𝜑𝑁 = ∅) ∧ 𝑚 ∈ ω) → ((dom 𝐺 = ∅ ∧ 𝑥𝐴) ↔ ((dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴))))
2415, 23bitrd 187 . . . . . . . . 9 (((𝜑𝑁 = ∅) ∧ 𝑚 ∈ ω) → (𝑥𝐴 ↔ ((dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴))))
2524rexbidva 2467 . . . . . . . 8 ((𝜑𝑁 = ∅) → (∃𝑚 ∈ ω 𝑥𝐴 ↔ ∃𝑚 ∈ ω ((dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴))))
266, 25syl5bb 191 . . . . . . 7 ((𝜑𝑁 = ∅) → (𝑥𝐴 ↔ ∃𝑚 ∈ ω ((dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴))))
27 r19.44mv 3508 . . . . . . . 8 (∃𝑎 𝑎 ∈ ω → (∃𝑚 ∈ ω ((dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴)) ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴))))
283, 4, 27mp2b 8 . . . . . . 7 (∃𝑚 ∈ ω ((dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴)) ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴)))
2926, 28bitrdi 195 . . . . . 6 ((𝜑𝑁 = ∅) → (𝑥𝐴 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴))))
3029alrimiv 1867 . . . . 5 ((𝜑𝑁 = ∅) → ∀𝑥(𝑥𝐴 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴))))
312, 30jca 304 . . . 4 ((𝜑𝑁 = ∅) → (𝐴𝑆 ∧ ∀𝑥(𝑥𝐴 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴)))))
32 eleq1 2233 . . . . . 6 (𝑧 = 𝐴 → (𝑧𝑆𝐴𝑆))
33 eleq2 2234 . . . . . . . 8 (𝑧 = 𝐴 → (𝑥𝑧𝑥𝐴))
3433bibi1d 232 . . . . . . 7 (𝑧 = 𝐴 → ((𝑥𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴))) ↔ (𝑥𝐴 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴)))))
3534albidv 1817 . . . . . 6 (𝑧 = 𝐴 → (∀𝑥(𝑥𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴))) ↔ ∀𝑥(𝑥𝐴 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴)))))
3632, 35anbi12d 470 . . . . 5 (𝑧 = 𝐴 → ((𝑧𝑆 ∧ ∀𝑥(𝑥𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴)))) ↔ (𝐴𝑆 ∧ ∀𝑥(𝑥𝐴 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴))))))
3736spcegv 2818 . . . 4 (𝐴𝑆 → ((𝐴𝑆 ∧ ∀𝑥(𝑥𝐴 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴)))) → ∃𝑧(𝑧𝑆 ∧ ∀𝑥(𝑥𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴))))))
382, 31, 37sylc 62 . . 3 ((𝜑𝑁 = ∅) → ∃𝑧(𝑧𝑆 ∧ ∀𝑥(𝑥𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴)))))
39 fveq2 5494 . . . . . . . . 9 (𝑦 = (𝐺𝑘) → (𝐹𝑦) = (𝐹‘(𝐺𝑘)))
4039eleq1d 2239 . . . . . . . 8 (𝑦 = (𝐺𝑘) → ((𝐹𝑦) ∈ 𝑆 ↔ (𝐹‘(𝐺𝑘)) ∈ 𝑆))
41 frecabcl.fs . . . . . . . . 9 (𝜑 → ∀𝑦𝑆 (𝐹𝑦) ∈ 𝑆)
4241ad2antrr 485 . . . . . . . 8 (((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → ∀𝑦𝑆 (𝐹𝑦) ∈ 𝑆)
437ad2antrr 485 . . . . . . . . 9 (((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → 𝐺:𝑁𝑆)
44 vex 2733 . . . . . . . . . . . 12 𝑘 ∈ V
4544sucid 4400 . . . . . . . . . . 11 𝑘 ∈ suc 𝑘
46 eleq2 2234 . . . . . . . . . . 11 (𝑁 = suc 𝑘 → (𝑘𝑁𝑘 ∈ suc 𝑘))
4745, 46mpbiri 167 . . . . . . . . . 10 (𝑁 = suc 𝑘𝑘𝑁)
4847adantl 275 . . . . . . . . 9 (((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → 𝑘𝑁)
4943, 48ffvelrnd 5630 . . . . . . . 8 (((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → (𝐺𝑘) ∈ 𝑆)
5040, 42, 49rspcdva 2839 . . . . . . 7 (((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → (𝐹‘(𝐺𝑘)) ∈ 𝑆)
51 simpllr 529 . . . . . . . . . . . . 13 ((((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑥 ∈ (𝐹‘(𝐺𝑘))) → 𝑘 ∈ ω)
5243, 8syl 14 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → dom 𝐺 = 𝑁)
5352adantr 274 . . . . . . . . . . . . . . 15 ((((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑥 ∈ (𝐹‘(𝐺𝑘))) → dom 𝐺 = 𝑁)
54 simplr 525 . . . . . . . . . . . . . . 15 ((((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑥 ∈ (𝐹‘(𝐺𝑘))) → 𝑁 = suc 𝑘)
5553, 54eqtrd 2203 . . . . . . . . . . . . . 14 ((((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑥 ∈ (𝐹‘(𝐺𝑘))) → dom 𝐺 = suc 𝑘)
56 simpr 109 . . . . . . . . . . . . . 14 ((((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑥 ∈ (𝐹‘(𝐺𝑘))) → 𝑥 ∈ (𝐹‘(𝐺𝑘)))
5755, 56jca 304 . . . . . . . . . . . . 13 ((((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑥 ∈ (𝐹‘(𝐺𝑘))) → (dom 𝐺 = suc 𝑘𝑥 ∈ (𝐹‘(𝐺𝑘))))
58 suceq 4385 . . . . . . . . . . . . . . . 16 (𝑚 = 𝑘 → suc 𝑚 = suc 𝑘)
5958eqeq2d 2182 . . . . . . . . . . . . . . 15 (𝑚 = 𝑘 → (dom 𝐺 = suc 𝑚 ↔ dom 𝐺 = suc 𝑘))
60 fveq2 5494 . . . . . . . . . . . . . . . . 17 (𝑚 = 𝑘 → (𝐺𝑚) = (𝐺𝑘))
6160fveq2d 5498 . . . . . . . . . . . . . . . 16 (𝑚 = 𝑘 → (𝐹‘(𝐺𝑚)) = (𝐹‘(𝐺𝑘)))
6261eleq2d 2240 . . . . . . . . . . . . . . 15 (𝑚 = 𝑘 → (𝑥 ∈ (𝐹‘(𝐺𝑚)) ↔ 𝑥 ∈ (𝐹‘(𝐺𝑘))))
6359, 62anbi12d 470 . . . . . . . . . . . . . 14 (𝑚 = 𝑘 → ((dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ↔ (dom 𝐺 = suc 𝑘𝑥 ∈ (𝐹‘(𝐺𝑘)))))
6463rspcev 2834 . . . . . . . . . . . . 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 485 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚)))) → dom 𝐺 = 𝑁)
70 simprl 526 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚)))) → dom 𝐺 = suc 𝑚)
71 simpllr 529 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚)))) → 𝑁 = suc 𝑘)
7269, 70, 713eqtr3rd 2212 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚)))) → suc 𝑘 = suc 𝑚)
73 simplr 525 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → 𝑘 ∈ ω)
7473ad2antrr 485 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚)))) → 𝑘 ∈ ω)
75 simplr 525 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚)))) → 𝑚 ∈ ω)
76 peano4 4579 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ω ∧ 𝑚 ∈ ω) → (suc 𝑘 = suc 𝑚𝑘 = 𝑚))
7774, 75, 76syl2anc 409 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚)))) → (suc 𝑘 = suc 𝑚𝑘 = 𝑚))
7872, 77mpbid 146 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚)))) → 𝑘 = 𝑚)
7978fveq2d 5498 . . . . . . . . . . . . . . . 16 (((((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚)))) → (𝐺𝑘) = (𝐺𝑚))
8079fveq2d 5498 . . . . . . . . . . . . . . 15 (((((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚)))) → (𝐹‘(𝐺𝑘)) = (𝐹‘(𝐺𝑚)))
8180eleq2d 2240 . . . . . . . . . . . . . 14 (((((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚)))) → (𝑥 ∈ (𝐹‘(𝐺𝑘)) ↔ 𝑥 ∈ (𝐹‘(𝐺𝑚))))
8268, 81mpbird 166 . . . . . . . . . . . . 13 (((((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚)))) → 𝑥 ∈ (𝐹‘(𝐺𝑘)))
8382ex 114 . . . . . . . . . . . 12 ((((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) → ((dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) → 𝑥 ∈ (𝐹‘(𝐺𝑘))))
8483rexlimdva 2587 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) → 𝑥 ∈ (𝐹‘(𝐺𝑘))))
8566, 84impbid 128 . . . . . . . . . 10 (((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → (𝑥 ∈ (𝐹‘(𝐺𝑘)) ↔ ∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚)))))
8685alrimiv 1867 . . . . . . . . 9 (((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → ∀𝑥(𝑥 ∈ (𝐹‘(𝐺𝑘)) ↔ ∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚)))))
87 peano3 4578 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ ω → suc 𝑘 ≠ ∅)
8873, 87syl 14 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → suc 𝑘 ≠ ∅)
89 neeq1 2353 . . . . . . . . . . . . . . . . . 18 (𝑁 = suc 𝑘 → (𝑁 ≠ ∅ ↔ suc 𝑘 ≠ ∅))
9089adantl 275 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → (𝑁 ≠ ∅ ↔ suc 𝑘 ≠ ∅))
9188, 90mpbird 166 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → 𝑁 ≠ ∅)
9252, 91eqnetrd 2364 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → dom 𝐺 ≠ ∅)
9392neneqd 2361 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → ¬ dom 𝐺 = ∅)
9493intnanrd 927 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → ¬ (dom 𝐺 = ∅ ∧ 𝑥𝐴))
95 biorf 739 . . . . . . . . . . . . 13 (¬ (dom 𝐺 = ∅ ∧ 𝑥𝐴) → (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ↔ ((dom 𝐺 = ∅ ∧ 𝑥𝐴) ∨ ∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))))))
9694, 95syl 14 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ↔ ((dom 𝐺 = ∅ ∧ 𝑥𝐴) ∨ ∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))))))
97 orcom 723 . . . . . . . . . . . 12 (((dom 𝐺 = ∅ ∧ 𝑥𝐴) ∨ ∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚)))) ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴)))
9896, 97bitrdi 195 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴))))
9998bibi2d 231 . . . . . . . . . 10 (((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → ((𝑥 ∈ (𝐹‘(𝐺𝑘)) ↔ ∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚)))) ↔ (𝑥 ∈ (𝐹‘(𝐺𝑘)) ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴)))))
10099albidv 1817 . . . . . . . . 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 2233 . . . . . . . . 9 (𝑧 = (𝐹‘(𝐺𝑘)) → (𝑧𝑆 ↔ (𝐹‘(𝐺𝑘)) ∈ 𝑆))
104 eleq2 2234 . . . . . . . . . . 11 (𝑧 = (𝐹‘(𝐺𝑘)) → (𝑥𝑧𝑥 ∈ (𝐹‘(𝐺𝑘))))
105104bibi1d 232 . . . . . . . . . 10 (𝑧 = (𝐹‘(𝐺𝑘)) → ((𝑥𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴))) ↔ (𝑥 ∈ (𝐹‘(𝐺𝑘)) ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴)))))
106105albidv 1817 . . . . . . . . 9 (𝑧 = (𝐹‘(𝐺𝑘)) → (∀𝑥(𝑥𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴))) ↔ ∀𝑥(𝑥 ∈ (𝐹‘(𝐺𝑘)) ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴)))))
107103, 106anbi12d 470 . . . . . . . 8 (𝑧 = (𝐹‘(𝐺𝑘)) → ((𝑧𝑆 ∧ ∀𝑥(𝑥𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴)))) ↔ ((𝐹‘(𝐺𝑘)) ∈ 𝑆 ∧ ∀𝑥(𝑥 ∈ (𝐹‘(𝐺𝑘)) ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴))))))
108107spcegv 2818 . . . . . . 7 ((𝐹‘(𝐺𝑘)) ∈ 𝑆 → (((𝐹‘(𝐺𝑘)) ∈ 𝑆 ∧ ∀𝑥(𝑥 ∈ (𝐹‘(𝐺𝑘)) ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴)))) → ∃𝑧(𝑧𝑆 ∧ ∀𝑥(𝑥𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴))))))
10950, 102, 108sylc 62 . . . . . 6 (((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → ∃𝑧(𝑧𝑆 ∧ ∀𝑥(𝑥𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴)))))
110109ex 114 . . . . 5 ((𝜑𝑘 ∈ ω) → (𝑁 = suc 𝑘 → ∃𝑧(𝑧𝑆 ∧ ∀𝑥(𝑥𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴))))))
111110rexlimdva 2587 . . . 4 (𝜑 → (∃𝑘 ∈ ω 𝑁 = suc 𝑘 → ∃𝑧(𝑧𝑆 ∧ ∀𝑥(𝑥𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴))))))
112111imp 123 . . 3 ((𝜑 ∧ ∃𝑘 ∈ ω 𝑁 = suc 𝑘) → ∃𝑧(𝑧𝑆 ∧ ∀𝑥(𝑥𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴)))))
113 frecabcl.n . . . 4 (𝜑𝑁 ∈ ω)
114 nn0suc 4586 . . . 4 (𝑁 ∈ ω → (𝑁 = ∅ ∨ ∃𝑘 ∈ ω 𝑁 = suc 𝑘))
115113, 114syl 14 . . 3 (𝜑 → (𝑁 = ∅ ∨ ∃𝑘 ∈ ω 𝑁 = suc 𝑘))
11638, 112, 115mpjaodan 793 . 2 (𝜑 → ∃𝑧(𝑧𝑆 ∧ ∀𝑥(𝑥𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴)))))
117 clabel 2297 . 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 703  wal 1346   = wceq 1348  wex 1485  wcel 2141  {cab 2156  wne 2340  wral 2448  wrex 2449  c0 3414  suc csuc 4348  ωcom 4572  dom cdm 4609  wf 5192  cfv 5196
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 609  ax-in2 610  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-13 2143  ax-14 2144  ax-ext 2152  ax-sep 4105  ax-nul 4113  ax-pow 4158  ax-pr 4192  ax-un 4416  ax-setind 4519  ax-iinf 4570
This theorem depends on definitions:  df-bi 116  df-3an 975  df-tru 1351  df-nf 1454  df-sb 1756  df-eu 2022  df-mo 2023  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ne 2341  df-ral 2453  df-rex 2454  df-v 2732  df-sbc 2956  df-dif 3123  df-un 3125  df-in 3127  df-ss 3134  df-nul 3415  df-pw 3566  df-sn 3587  df-pr 3588  df-op 3590  df-uni 3795  df-int 3830  df-br 3988  df-opab 4049  df-id 4276  df-suc 4354  df-iom 4573  df-xp 4615  df-rel 4616  df-cnv 4617  df-co 4618  df-dm 4619  df-rn 4620  df-iota 5158  df-fun 5198  df-fn 5199  df-f 5200  df-fv 5204
This theorem is referenced by:  freccllem  6379  frecfcllem  6381  frecsuclem  6383
  Copyright terms: Public domain W3C validator