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

Theorem frecabcl 6069
Description: The class abstraction from df-frec 6061 exists. Unlike frecabex 6068 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 270 . . . 4 ((𝜑𝑁 = ∅) → 𝐴𝑆)
3 peano1 4363 . . . . . . . . 9 ∅ ∈ ω
4 elex2 2624 . . . . . . . . 9 (∅ ∈ ω → ∃𝑎 𝑎 ∈ ω)
5 r19.9rmv 3349 . . . . . . . . 9 (∃𝑎 𝑎 ∈ ω → (𝑥𝐴 ↔ ∃𝑚 ∈ ω 𝑥𝐴))
63, 4, 5mp2b 8 . . . . . . . 8 (𝑥𝐴 ↔ ∃𝑚 ∈ ω 𝑥𝐴)
7 frecabcl.g . . . . . . . . . . . . . . 15 (𝜑𝐺:𝑁𝑆)
8 fdm 5101 . . . . . . . . . . . . . . 15 (𝐺:𝑁𝑆 → dom 𝐺 = 𝑁)
97, 8syl 14 . . . . . . . . . . . . . 14 (𝜑 → dom 𝐺 = 𝑁)
109adantr 270 . . . . . . . . . . . . 13 ((𝜑𝑁 = ∅) → dom 𝐺 = 𝑁)
11 eqeq2 2092 . . . . . . . . . . . . . 14 (𝑁 = ∅ → (dom 𝐺 = 𝑁 ↔ dom 𝐺 = ∅))
1211adantl 271 . . . . . . . . . . . . 13 ((𝜑𝑁 = ∅) → (dom 𝐺 = 𝑁 ↔ dom 𝐺 = ∅))
1310, 12mpbid 145 . . . . . . . . . . . 12 ((𝜑𝑁 = ∅) → dom 𝐺 = ∅)
1413adantr 270 . . . . . . . . . . 11 (((𝜑𝑁 = ∅) ∧ 𝑚 ∈ ω) → dom 𝐺 = ∅)
1514biantrurd 299 . . . . . . . . . 10 (((𝜑𝑁 = ∅) ∧ 𝑚 ∈ ω) → (𝑥𝐴 ↔ (dom 𝐺 = ∅ ∧ 𝑥𝐴)))
16 peano3 4365 . . . . . . . . . . . . . . . 16 (𝑚 ∈ ω → suc 𝑚 ≠ ∅)
1716adantl 271 . . . . . . . . . . . . . . 15 (((𝜑𝑁 = ∅) ∧ 𝑚 ∈ ω) → suc 𝑚 ≠ ∅)
1817, 14neeqtrrd 2279 . . . . . . . . . . . . . 14 (((𝜑𝑁 = ∅) ∧ 𝑚 ∈ ω) → suc 𝑚 ≠ dom 𝐺)
1918necomd 2335 . . . . . . . . . . . . 13 (((𝜑𝑁 = ∅) ∧ 𝑚 ∈ ω) → dom 𝐺 ≠ suc 𝑚)
2019neneqd 2270 . . . . . . . . . . . 12 (((𝜑𝑁 = ∅) ∧ 𝑚 ∈ ω) → ¬ dom 𝐺 = suc 𝑚)
2120intnanrd 875 . . . . . . . . . . 11 (((𝜑𝑁 = ∅) ∧ 𝑚 ∈ ω) → ¬ (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))))
22 biorf 696 . . . . . . . . . . 11 (¬ (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) → ((dom 𝐺 = ∅ ∧ 𝑥𝐴) ↔ ((dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴))))
2321, 22syl 14 . . . . . . . . . 10 (((𝜑𝑁 = ∅) ∧ 𝑚 ∈ ω) → ((dom 𝐺 = ∅ ∧ 𝑥𝐴) ↔ ((dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴))))
2415, 23bitrd 186 . . . . . . . . 9 (((𝜑𝑁 = ∅) ∧ 𝑚 ∈ ω) → (𝑥𝐴 ↔ ((dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴))))
2524rexbidva 2370 . . . . . . . 8 ((𝜑𝑁 = ∅) → (∃𝑚 ∈ ω 𝑥𝐴 ↔ ∃𝑚 ∈ ω ((dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴))))
266, 25syl5bb 190 . . . . . . 7 ((𝜑𝑁 = ∅) → (𝑥𝐴 ↔ ∃𝑚 ∈ ω ((dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴))))
27 r19.44mv 3352 . . . . . . . 8 (∃𝑎 𝑎 ∈ ω → (∃𝑚 ∈ ω ((dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴)) ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴))))
283, 4, 27mp2b 8 . . . . . . 7 (∃𝑚 ∈ ω ((dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴)) ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴)))
2926, 28syl6bb 194 . . . . . 6 ((𝜑𝑁 = ∅) → (𝑥𝐴 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴))))
3029alrimiv 1797 . . . . 5 ((𝜑𝑁 = ∅) → ∀𝑥(𝑥𝐴 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴))))
312, 30jca 300 . . . 4 ((𝜑𝑁 = ∅) → (𝐴𝑆 ∧ ∀𝑥(𝑥𝐴 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴)))))
32 eleq1 2145 . . . . . 6 (𝑧 = 𝐴 → (𝑧𝑆𝐴𝑆))
33 eleq2 2146 . . . . . . . 8 (𝑧 = 𝐴 → (𝑥𝑧𝑥𝐴))
3433bibi1d 231 . . . . . . 7 (𝑧 = 𝐴 → ((𝑥𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴))) ↔ (𝑥𝐴 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴)))))
3534albidv 1747 . . . . . 6 (𝑧 = 𝐴 → (∀𝑥(𝑥𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴))) ↔ ∀𝑥(𝑥𝐴 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴)))))
3632, 35anbi12d 457 . . . . 5 (𝑧 = 𝐴 → ((𝑧𝑆 ∧ ∀𝑥(𝑥𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴)))) ↔ (𝐴𝑆 ∧ ∀𝑥(𝑥𝐴 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴))))))
3736spcegv 2695 . . . 4 (𝐴𝑆 → ((𝐴𝑆 ∧ ∀𝑥(𝑥𝐴 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴)))) → ∃𝑧(𝑧𝑆 ∧ ∀𝑥(𝑥𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴))))))
382, 31, 37sylc 61 . . 3 ((𝜑𝑁 = ∅) → ∃𝑧(𝑧𝑆 ∧ ∀𝑥(𝑥𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴)))))
39 fveq2 5230 . . . . . . . . 9 (𝑦 = (𝐺𝑘) → (𝐹𝑦) = (𝐹‘(𝐺𝑘)))
4039eleq1d 2151 . . . . . . . 8 (𝑦 = (𝐺𝑘) → ((𝐹𝑦) ∈ 𝑆 ↔ (𝐹‘(𝐺𝑘)) ∈ 𝑆))
41 frecabcl.fs . . . . . . . . 9 (𝜑 → ∀𝑦𝑆 (𝐹𝑦) ∈ 𝑆)
4241ad2antrr 472 . . . . . . . 8 (((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → ∀𝑦𝑆 (𝐹𝑦) ∈ 𝑆)
437ad2antrr 472 . . . . . . . . 9 (((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → 𝐺:𝑁𝑆)
44 vex 2613 . . . . . . . . . . . 12 𝑘 ∈ V
4544sucid 4200 . . . . . . . . . . 11 𝑘 ∈ suc 𝑘
46 eleq2 2146 . . . . . . . . . . 11 (𝑁 = suc 𝑘 → (𝑘𝑁𝑘 ∈ suc 𝑘))
4745, 46mpbiri 166 . . . . . . . . . 10 (𝑁 = suc 𝑘𝑘𝑁)
4847adantl 271 . . . . . . . . 9 (((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → 𝑘𝑁)
4943, 48ffvelrnd 5356 . . . . . . . 8 (((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → (𝐺𝑘) ∈ 𝑆)
5040, 42, 49rspcdva 2715 . . . . . . 7 (((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → (𝐹‘(𝐺𝑘)) ∈ 𝑆)
51 simpllr 501 . . . . . . . . . . . . 13 ((((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑥 ∈ (𝐹‘(𝐺𝑘))) → 𝑘 ∈ ω)
5243, 8syl 14 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → dom 𝐺 = 𝑁)
5352adantr 270 . . . . . . . . . . . . . . 15 ((((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑥 ∈ (𝐹‘(𝐺𝑘))) → dom 𝐺 = 𝑁)
54 simplr 497 . . . . . . . . . . . . . . 15 ((((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑥 ∈ (𝐹‘(𝐺𝑘))) → 𝑁 = suc 𝑘)
5553, 54eqtrd 2115 . . . . . . . . . . . . . 14 ((((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑥 ∈ (𝐹‘(𝐺𝑘))) → dom 𝐺 = suc 𝑘)
56 simpr 108 . . . . . . . . . . . . . 14 ((((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑥 ∈ (𝐹‘(𝐺𝑘))) → 𝑥 ∈ (𝐹‘(𝐺𝑘)))
5755, 56jca 300 . . . . . . . . . . . . 13 ((((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑥 ∈ (𝐹‘(𝐺𝑘))) → (dom 𝐺 = suc 𝑘𝑥 ∈ (𝐹‘(𝐺𝑘))))
58 suceq 4185 . . . . . . . . . . . . . . . 16 (𝑚 = 𝑘 → suc 𝑚 = suc 𝑘)
5958eqeq2d 2094 . . . . . . . . . . . . . . 15 (𝑚 = 𝑘 → (dom 𝐺 = suc 𝑚 ↔ dom 𝐺 = suc 𝑘))
60 fveq2 5230 . . . . . . . . . . . . . . . . 17 (𝑚 = 𝑘 → (𝐺𝑚) = (𝐺𝑘))
6160fveq2d 5234 . . . . . . . . . . . . . . . 16 (𝑚 = 𝑘 → (𝐹‘(𝐺𝑚)) = (𝐹‘(𝐺𝑘)))
6261eleq2d 2152 . . . . . . . . . . . . . . 15 (𝑚 = 𝑘 → (𝑥 ∈ (𝐹‘(𝐺𝑚)) ↔ 𝑥 ∈ (𝐹‘(𝐺𝑘))))
6359, 62anbi12d 457 . . . . . . . . . . . . . 14 (𝑚 = 𝑘 → ((dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ↔ (dom 𝐺 = suc 𝑘𝑥 ∈ (𝐹‘(𝐺𝑘)))))
6463rspcev 2710 . . . . . . . . . . . . 13 ((𝑘 ∈ ω ∧ (dom 𝐺 = suc 𝑘𝑥 ∈ (𝐹‘(𝐺𝑘)))) → ∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))))
6551, 57, 64syl2anc 403 . . . . . . . . . . . 12 ((((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑥 ∈ (𝐹‘(𝐺𝑘))) → ∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))))
6665ex 113 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → (𝑥 ∈ (𝐹‘(𝐺𝑘)) → ∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚)))))
67 simpr 108 . . . . . . . . . . . . . . 15 ((dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) → 𝑥 ∈ (𝐹‘(𝐺𝑚)))
6867adantl 271 . . . . . . . . . . . . . 14 (((((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚)))) → 𝑥 ∈ (𝐹‘(𝐺𝑚)))
6952ad2antrr 472 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚)))) → dom 𝐺 = 𝑁)
70 simprl 498 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚)))) → dom 𝐺 = suc 𝑚)
71 simpllr 501 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚)))) → 𝑁 = suc 𝑘)
7269, 70, 713eqtr3rd 2124 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚)))) → suc 𝑘 = suc 𝑚)
73 simplr 497 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → 𝑘 ∈ ω)
7473ad2antrr 472 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚)))) → 𝑘 ∈ ω)
75 simplr 497 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚)))) → 𝑚 ∈ ω)
76 peano4 4366 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ω ∧ 𝑚 ∈ ω) → (suc 𝑘 = suc 𝑚𝑘 = 𝑚))
7774, 75, 76syl2anc 403 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚)))) → (suc 𝑘 = suc 𝑚𝑘 = 𝑚))
7872, 77mpbid 145 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚)))) → 𝑘 = 𝑚)
7978fveq2d 5234 . . . . . . . . . . . . . . . 16 (((((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚)))) → (𝐺𝑘) = (𝐺𝑚))
8079fveq2d 5234 . . . . . . . . . . . . . . 15 (((((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚)))) → (𝐹‘(𝐺𝑘)) = (𝐹‘(𝐺𝑚)))
8180eleq2d 2152 . . . . . . . . . . . . . 14 (((((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚)))) → (𝑥 ∈ (𝐹‘(𝐺𝑘)) ↔ 𝑥 ∈ (𝐹‘(𝐺𝑚))))
8268, 81mpbird 165 . . . . . . . . . . . . 13 (((((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚)))) → 𝑥 ∈ (𝐹‘(𝐺𝑘)))
8382ex 113 . . . . . . . . . . . 12 ((((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) → ((dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) → 𝑥 ∈ (𝐹‘(𝐺𝑘))))
8483rexlimdva 2482 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) → 𝑥 ∈ (𝐹‘(𝐺𝑘))))
8566, 84impbid 127 . . . . . . . . . 10 (((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → (𝑥 ∈ (𝐹‘(𝐺𝑘)) ↔ ∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚)))))
8685alrimiv 1797 . . . . . . . . 9 (((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → ∀𝑥(𝑥 ∈ (𝐹‘(𝐺𝑘)) ↔ ∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚)))))
87 peano3 4365 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ ω → suc 𝑘 ≠ ∅)
8873, 87syl 14 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → suc 𝑘 ≠ ∅)
89 neeq1 2262 . . . . . . . . . . . . . . . . . 18 (𝑁 = suc 𝑘 → (𝑁 ≠ ∅ ↔ suc 𝑘 ≠ ∅))
9089adantl 271 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → (𝑁 ≠ ∅ ↔ suc 𝑘 ≠ ∅))
9188, 90mpbird 165 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → 𝑁 ≠ ∅)
9252, 91eqnetrd 2273 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → dom 𝐺 ≠ ∅)
9392neneqd 2270 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → ¬ dom 𝐺 = ∅)
9493intnanrd 875 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → ¬ (dom 𝐺 = ∅ ∧ 𝑥𝐴))
95 biorf 696 . . . . . . . . . . . . 13 (¬ (dom 𝐺 = ∅ ∧ 𝑥𝐴) → (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ↔ ((dom 𝐺 = ∅ ∧ 𝑥𝐴) ∨ ∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))))))
9694, 95syl 14 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ↔ ((dom 𝐺 = ∅ ∧ 𝑥𝐴) ∨ ∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))))))
97 orcom 680 . . . . . . . . . . . 12 (((dom 𝐺 = ∅ ∧ 𝑥𝐴) ∨ ∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚)))) ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴)))
9896, 97syl6bb 194 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴))))
9998bibi2d 230 . . . . . . . . . 10 (((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → ((𝑥 ∈ (𝐹‘(𝐺𝑘)) ↔ ∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚)))) ↔ (𝑥 ∈ (𝐹‘(𝐺𝑘)) ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴)))))
10099albidv 1747 . . . . . . . . 9 (((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → (∀𝑥(𝑥 ∈ (𝐹‘(𝐺𝑘)) ↔ ∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚)))) ↔ ∀𝑥(𝑥 ∈ (𝐹‘(𝐺𝑘)) ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴)))))
10186, 100mpbid 145 . . . . . . . 8 (((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → ∀𝑥(𝑥 ∈ (𝐹‘(𝐺𝑘)) ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴))))
10250, 101jca 300 . . . . . . 7 (((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → ((𝐹‘(𝐺𝑘)) ∈ 𝑆 ∧ ∀𝑥(𝑥 ∈ (𝐹‘(𝐺𝑘)) ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴)))))
103 eleq1 2145 . . . . . . . . 9 (𝑧 = (𝐹‘(𝐺𝑘)) → (𝑧𝑆 ↔ (𝐹‘(𝐺𝑘)) ∈ 𝑆))
104 eleq2 2146 . . . . . . . . . . 11 (𝑧 = (𝐹‘(𝐺𝑘)) → (𝑥𝑧𝑥 ∈ (𝐹‘(𝐺𝑘))))
105104bibi1d 231 . . . . . . . . . 10 (𝑧 = (𝐹‘(𝐺𝑘)) → ((𝑥𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴))) ↔ (𝑥 ∈ (𝐹‘(𝐺𝑘)) ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴)))))
106105albidv 1747 . . . . . . . . 9 (𝑧 = (𝐹‘(𝐺𝑘)) → (∀𝑥(𝑥𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴))) ↔ ∀𝑥(𝑥 ∈ (𝐹‘(𝐺𝑘)) ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴)))))
107103, 106anbi12d 457 . . . . . . . 8 (𝑧 = (𝐹‘(𝐺𝑘)) → ((𝑧𝑆 ∧ ∀𝑥(𝑥𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴)))) ↔ ((𝐹‘(𝐺𝑘)) ∈ 𝑆 ∧ ∀𝑥(𝑥 ∈ (𝐹‘(𝐺𝑘)) ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴))))))
108107spcegv 2695 . . . . . . 7 ((𝐹‘(𝐺𝑘)) ∈ 𝑆 → (((𝐹‘(𝐺𝑘)) ∈ 𝑆 ∧ ∀𝑥(𝑥 ∈ (𝐹‘(𝐺𝑘)) ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴)))) → ∃𝑧(𝑧𝑆 ∧ ∀𝑥(𝑥𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴))))))
10950, 102, 108sylc 61 . . . . . 6 (((𝜑𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → ∃𝑧(𝑧𝑆 ∧ ∀𝑥(𝑥𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴)))))
110109ex 113 . . . . 5 ((𝜑𝑘 ∈ ω) → (𝑁 = suc 𝑘 → ∃𝑧(𝑧𝑆 ∧ ∀𝑥(𝑥𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴))))))
111110rexlimdva 2482 . . . 4 (𝜑 → (∃𝑘 ∈ ω 𝑁 = suc 𝑘 → ∃𝑧(𝑧𝑆 ∧ ∀𝑥(𝑥𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴))))))
112111imp 122 . . 3 ((𝜑 ∧ ∃𝑘 ∈ ω 𝑁 = suc 𝑘) → ∃𝑧(𝑧𝑆 ∧ ∀𝑥(𝑥𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴)))))
113 frecabcl.n . . . 4 (𝜑𝑁 ∈ ω)
114 nn0suc 4373 . . . 4 (𝑁 ∈ ω → (𝑁 = ∅ ∨ ∃𝑘 ∈ ω 𝑁 = suc 𝑘))
115113, 114syl 14 . . 3 (𝜑 → (𝑁 = ∅ ∨ ∃𝑘 ∈ ω 𝑁 = suc 𝑘))
11638, 112, 115mpjaodan 745 . 2 (𝜑 → ∃𝑧(𝑧𝑆 ∧ ∀𝑥(𝑥𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴)))))
117 clabel 2208 . 2 ({𝑥 ∣ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴))} ∈ 𝑆 ↔ ∃𝑧(𝑧𝑆 ∧ ∀𝑥(𝑥𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴)))))
118116, 117sylibr 132 1 (𝜑 → {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚𝑥 ∈ (𝐹‘(𝐺𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥𝐴))} ∈ 𝑆)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 102  wb 103  wo 662  wal 1283   = wceq 1285  wex 1422  wcel 1434  {cab 2069  wne 2249  wral 2353  wrex 2354  c0 3267  suc csuc 4148  ωcom 4359  dom cdm 4391  wf 4948  cfv 4952
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-13 1445  ax-14 1446  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065  ax-sep 3916  ax-nul 3924  ax-pow 3968  ax-pr 3992  ax-un 4216  ax-setind 4308  ax-iinf 4357
This theorem depends on definitions:  df-bi 115  df-3an 922  df-tru 1288  df-nf 1391  df-sb 1688  df-eu 1946  df-mo 1947  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-ne 2250  df-ral 2358  df-rex 2359  df-v 2612  df-sbc 2825  df-dif 2984  df-un 2986  df-in 2988  df-ss 2995  df-nul 3268  df-pw 3402  df-sn 3422  df-pr 3423  df-op 3425  df-uni 3622  df-int 3657  df-br 3806  df-opab 3860  df-id 4076  df-suc 4154  df-iom 4360  df-xp 4397  df-rel 4398  df-cnv 4399  df-co 4400  df-dm 4401  df-rn 4402  df-iota 4917  df-fun 4954  df-fn 4955  df-f 4956  df-fv 4960
This theorem is referenced by:  freccllem  6072  frecfcllem  6074  frecsuclem  6076
  Copyright terms: Public domain W3C validator