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

Theorem tfrcllemres 6109
Description: Lemma for tfr1on 6097. Recursion is defined on an ordinal if the characteristic function is defined up to a suitable point. (Contributed by Jim Kingdon, 18-Mar-2022.)
Hypotheses
Ref Expression
tfrcl.f 𝐹 = recs(𝐺)
tfrcl.g (𝜑 → Fun 𝐺)
tfrcl.x (𝜑 → Ord 𝑋)
tfrcl.ex ((𝜑𝑥𝑋𝑓:𝑥𝑆) → (𝐺𝑓) ∈ 𝑆)
tfrcllemsucfn.1 𝐴 = {𝑓 ∣ ∃𝑥𝑋 (𝑓:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦)))}
tfrcllemres.u ((𝜑𝑥 𝑋) → suc 𝑥𝑋)
tfrcllemres.yx (𝜑𝑌𝑋)
Assertion
Ref Expression
tfrcllemres (𝜑𝑌 ⊆ dom 𝐹)
Distinct variable groups:   𝑥,𝐴,𝑦   𝑓,𝐺,𝑥,𝑦   𝑆,𝑓,𝑥,𝑦   𝑓,𝑋,𝑥,𝑦   𝑓,𝑌,𝑥,𝑦   𝜑,𝑓,𝑥,𝑦
Allowed substitution hints:   𝐴(𝑓)   𝐹(𝑥,𝑦,𝑓)

Proof of Theorem tfrcllemres
Dummy variables 𝑔 𝑧 𝑢 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 tfrcl.x . . . . . . . . . 10 (𝜑 → Ord 𝑋)
21adantr 270 . . . . . . . . 9 ((𝜑𝑧𝑌) → Ord 𝑋)
3 simpr 108 . . . . . . . . . 10 ((𝜑𝑧𝑌) → 𝑧𝑌)
4 tfrcllemres.yx . . . . . . . . . . 11 (𝜑𝑌𝑋)
54adantr 270 . . . . . . . . . 10 ((𝜑𝑧𝑌) → 𝑌𝑋)
63, 5jca 300 . . . . . . . . 9 ((𝜑𝑧𝑌) → (𝑧𝑌𝑌𝑋))
7 ordtr1 4206 . . . . . . . . 9 (Ord 𝑋 → ((𝑧𝑌𝑌𝑋) → 𝑧𝑋))
82, 6, 7sylc 61 . . . . . . . 8 ((𝜑𝑧𝑌) → 𝑧𝑋)
9 tfrcl.f . . . . . . . . 9 𝐹 = recs(𝐺)
10 tfrcl.g . . . . . . . . 9 (𝜑 → Fun 𝐺)
11 tfrcl.ex . . . . . . . . 9 ((𝜑𝑥𝑋𝑓:𝑥𝑆) → (𝐺𝑓) ∈ 𝑆)
12 tfrcllemsucfn.1 . . . . . . . . 9 𝐴 = {𝑓 ∣ ∃𝑥𝑋 (𝑓:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦)))}
13 tfrcllemres.u . . . . . . . . 9 ((𝜑𝑥 𝑋) → suc 𝑥𝑋)
149, 10, 1, 11, 12, 13tfrcllemaccex 6108 . . . . . . . 8 ((𝜑𝑧𝑋) → ∃𝑔(𝑔:𝑧𝑆 ∧ ∀𝑢𝑧 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))
158, 14syldan 276 . . . . . . 7 ((𝜑𝑧𝑌) → ∃𝑔(𝑔:𝑧𝑆 ∧ ∀𝑢𝑧 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))
1610ad2antrr 472 . . . . . . . . 9 (((𝜑𝑧𝑌) ∧ (𝑔:𝑧𝑆 ∧ ∀𝑢𝑧 (𝑔𝑢) = (𝐺‘(𝑔𝑢)))) → Fun 𝐺)
171ad2antrr 472 . . . . . . . . 9 (((𝜑𝑧𝑌) ∧ (𝑔:𝑧𝑆 ∧ ∀𝑢𝑧 (𝑔𝑢) = (𝐺‘(𝑔𝑢)))) → Ord 𝑋)
18113adant1r 1167 . . . . . . . . . 10 (((𝜑𝑧𝑌) ∧ 𝑥𝑋𝑓:𝑥𝑆) → (𝐺𝑓) ∈ 𝑆)
19183adant1r 1167 . . . . . . . . 9 ((((𝜑𝑧𝑌) ∧ (𝑔:𝑧𝑆 ∧ ∀𝑢𝑧 (𝑔𝑢) = (𝐺‘(𝑔𝑢)))) ∧ 𝑥𝑋𝑓:𝑥𝑆) → (𝐺𝑓) ∈ 𝑆)
204ad2antrr 472 . . . . . . . . 9 (((𝜑𝑧𝑌) ∧ (𝑔:𝑧𝑆 ∧ ∀𝑢𝑧 (𝑔𝑢) = (𝐺‘(𝑔𝑢)))) → 𝑌𝑋)
213adantr 270 . . . . . . . . 9 (((𝜑𝑧𝑌) ∧ (𝑔:𝑧𝑆 ∧ ∀𝑢𝑧 (𝑔𝑢) = (𝐺‘(𝑔𝑢)))) → 𝑧𝑌)
2213adantlr 461 . . . . . . . . . 10 (((𝜑𝑧𝑌) ∧ 𝑥 𝑋) → suc 𝑥𝑋)
2322adantlr 461 . . . . . . . . 9 ((((𝜑𝑧𝑌) ∧ (𝑔:𝑧𝑆 ∧ ∀𝑢𝑧 (𝑔𝑢) = (𝐺‘(𝑔𝑢)))) ∧ 𝑥 𝑋) → suc 𝑥𝑋)
24 simprl 498 . . . . . . . . 9 (((𝜑𝑧𝑌) ∧ (𝑔:𝑧𝑆 ∧ ∀𝑢𝑧 (𝑔𝑢) = (𝐺‘(𝑔𝑢)))) → 𝑔:𝑧𝑆)
25 feq2 5132 . . . . . . . . . . . . . 14 (𝑥 = 𝑧 → (𝑔:𝑥𝑆𝑔:𝑧𝑆))
26 raleq 2562 . . . . . . . . . . . . . 14 (𝑥 = 𝑧 → (∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦)) ↔ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))
2725, 26anbi12d 457 . . . . . . . . . . . . 13 (𝑥 = 𝑧 → ((𝑔:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦))) ↔ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))))
28 fveq2 5289 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑢 → (𝑔𝑦) = (𝑔𝑢))
29 reseq2 4696 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑢 → (𝑔𝑦) = (𝑔𝑢))
3029fveq2d 5293 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑢 → (𝐺‘(𝑔𝑦)) = (𝐺‘(𝑔𝑢)))
3128, 30eqeq12d 2102 . . . . . . . . . . . . . . 15 (𝑦 = 𝑢 → ((𝑔𝑦) = (𝐺‘(𝑔𝑦)) ↔ (𝑔𝑢) = (𝐺‘(𝑔𝑢))))
3231cbvralv 2590 . . . . . . . . . . . . . 14 (∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)) ↔ ∀𝑢𝑧 (𝑔𝑢) = (𝐺‘(𝑔𝑢)))
3332anbi2i 445 . . . . . . . . . . . . 13 ((𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦))) ↔ (𝑔:𝑧𝑆 ∧ ∀𝑢𝑧 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))
3427, 33syl6bb 194 . . . . . . . . . . . 12 (𝑥 = 𝑧 → ((𝑔:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦))) ↔ (𝑔:𝑧𝑆 ∧ ∀𝑢𝑧 (𝑔𝑢) = (𝐺‘(𝑔𝑢)))))
3534rspcev 2722 . . . . . . . . . . 11 ((𝑧𝑋 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑢𝑧 (𝑔𝑢) = (𝐺‘(𝑔𝑢)))) → ∃𝑥𝑋 (𝑔:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))
368, 35sylan 277 . . . . . . . . . 10 (((𝜑𝑧𝑌) ∧ (𝑔:𝑧𝑆 ∧ ∀𝑢𝑧 (𝑔𝑢) = (𝐺‘(𝑔𝑢)))) → ∃𝑥𝑋 (𝑔:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))
37 vex 2622 . . . . . . . . . . 11 𝑔 ∈ V
38 feq1 5131 . . . . . . . . . . . . 13 (𝑓 = 𝑔 → (𝑓:𝑥𝑆𝑔:𝑥𝑆))
39 fveq1 5288 . . . . . . . . . . . . . . 15 (𝑓 = 𝑔 → (𝑓𝑦) = (𝑔𝑦))
40 reseq1 4695 . . . . . . . . . . . . . . . 16 (𝑓 = 𝑔 → (𝑓𝑦) = (𝑔𝑦))
4140fveq2d 5293 . . . . . . . . . . . . . . 15 (𝑓 = 𝑔 → (𝐺‘(𝑓𝑦)) = (𝐺‘(𝑔𝑦)))
4239, 41eqeq12d 2102 . . . . . . . . . . . . . 14 (𝑓 = 𝑔 → ((𝑓𝑦) = (𝐺‘(𝑓𝑦)) ↔ (𝑔𝑦) = (𝐺‘(𝑔𝑦))))
4342ralbidv 2380 . . . . . . . . . . . . 13 (𝑓 = 𝑔 → (∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦)) ↔ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))
4438, 43anbi12d 457 . . . . . . . . . . . 12 (𝑓 = 𝑔 → ((𝑓:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦))) ↔ (𝑔:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))))
4544rexbidv 2381 . . . . . . . . . . 11 (𝑓 = 𝑔 → (∃𝑥𝑋 (𝑓:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦))) ↔ ∃𝑥𝑋 (𝑔:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))))
4637, 45, 12elab2 2761 . . . . . . . . . 10 (𝑔𝐴 ↔ ∃𝑥𝑋 (𝑔:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))
4736, 46sylibr 132 . . . . . . . . 9 (((𝜑𝑧𝑌) ∧ (𝑔:𝑧𝑆 ∧ ∀𝑢𝑧 (𝑔𝑢) = (𝐺‘(𝑔𝑢)))) → 𝑔𝐴)
489, 16, 17, 19, 12, 20, 21, 23, 24, 47tfrcllemsucaccv 6101 . . . . . . . 8 (((𝜑𝑧𝑌) ∧ (𝑔:𝑧𝑆 ∧ ∀𝑢𝑧 (𝑔𝑢) = (𝐺‘(𝑔𝑢)))) → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ 𝐴)
49 vex 2622 . . . . . . . . . . 11 𝑧 ∈ V
5025imbi1d 229 . . . . . . . . . . . . . 14 (𝑥 = 𝑧 → ((𝑔:𝑥𝑆 → (𝐺𝑔) ∈ 𝑆) ↔ (𝑔:𝑧𝑆 → (𝐺𝑔) ∈ 𝑆)))
51113expia 1145 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝑋) → (𝑓:𝑥𝑆 → (𝐺𝑓) ∈ 𝑆))
5251alrimiv 1802 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝑋) → ∀𝑓(𝑓:𝑥𝑆 → (𝐺𝑓) ∈ 𝑆))
53 fveq2 5289 . . . . . . . . . . . . . . . . . . . 20 (𝑓 = 𝑔 → (𝐺𝑓) = (𝐺𝑔))
5453eleq1d 2156 . . . . . . . . . . . . . . . . . . 19 (𝑓 = 𝑔 → ((𝐺𝑓) ∈ 𝑆 ↔ (𝐺𝑔) ∈ 𝑆))
5538, 54imbi12d 232 . . . . . . . . . . . . . . . . . 18 (𝑓 = 𝑔 → ((𝑓:𝑥𝑆 → (𝐺𝑓) ∈ 𝑆) ↔ (𝑔:𝑥𝑆 → (𝐺𝑔) ∈ 𝑆)))
5655spv 1788 . . . . . . . . . . . . . . . . 17 (∀𝑓(𝑓:𝑥𝑆 → (𝐺𝑓) ∈ 𝑆) → (𝑔:𝑥𝑆 → (𝐺𝑔) ∈ 𝑆))
5752, 56syl 14 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝑋) → (𝑔:𝑥𝑆 → (𝐺𝑔) ∈ 𝑆))
5857ralrimiva 2446 . . . . . . . . . . . . . . 15 (𝜑 → ∀𝑥𝑋 (𝑔:𝑥𝑆 → (𝐺𝑔) ∈ 𝑆))
5958adantr 270 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑌) → ∀𝑥𝑋 (𝑔:𝑥𝑆 → (𝐺𝑔) ∈ 𝑆))
6050, 59, 8rspcdva 2727 . . . . . . . . . . . . 13 ((𝜑𝑧𝑌) → (𝑔:𝑧𝑆 → (𝐺𝑔) ∈ 𝑆))
6160imp 122 . . . . . . . . . . . 12 (((𝜑𝑧𝑌) ∧ 𝑔:𝑧𝑆) → (𝐺𝑔) ∈ 𝑆)
6224, 61syldan 276 . . . . . . . . . . 11 (((𝜑𝑧𝑌) ∧ (𝑔:𝑧𝑆 ∧ ∀𝑢𝑧 (𝑔𝑢) = (𝐺‘(𝑔𝑢)))) → (𝐺𝑔) ∈ 𝑆)
63 opexg 4046 . . . . . . . . . . 11 ((𝑧 ∈ V ∧ (𝐺𝑔) ∈ 𝑆) → ⟨𝑧, (𝐺𝑔)⟩ ∈ V)
6449, 62, 63sylancr 405 . . . . . . . . . 10 (((𝜑𝑧𝑌) ∧ (𝑔:𝑧𝑆 ∧ ∀𝑢𝑧 (𝑔𝑢) = (𝐺‘(𝑔𝑢)))) → ⟨𝑧, (𝐺𝑔)⟩ ∈ V)
65 snidg 3468 . . . . . . . . . 10 (⟨𝑧, (𝐺𝑔)⟩ ∈ V → ⟨𝑧, (𝐺𝑔)⟩ ∈ {⟨𝑧, (𝐺𝑔)⟩})
66 elun2 3166 . . . . . . . . . 10 (⟨𝑧, (𝐺𝑔)⟩ ∈ {⟨𝑧, (𝐺𝑔)⟩} → ⟨𝑧, (𝐺𝑔)⟩ ∈ (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))
6764, 65, 663syl 17 . . . . . . . . 9 (((𝜑𝑧𝑌) ∧ (𝑔:𝑧𝑆 ∧ ∀𝑢𝑧 (𝑔𝑢) = (𝐺‘(𝑔𝑢)))) → ⟨𝑧, (𝐺𝑔)⟩ ∈ (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))
68 opeldmg 4629 . . . . . . . . . 10 ((𝑧 ∈ V ∧ (𝐺𝑔) ∈ 𝑆) → (⟨𝑧, (𝐺𝑔)⟩ ∈ (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) → 𝑧 ∈ dom (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})))
6949, 62, 68sylancr 405 . . . . . . . . 9 (((𝜑𝑧𝑌) ∧ (𝑔:𝑧𝑆 ∧ ∀𝑢𝑧 (𝑔𝑢) = (𝐺‘(𝑔𝑢)))) → (⟨𝑧, (𝐺𝑔)⟩ ∈ (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) → 𝑧 ∈ dom (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})))
7067, 69mpd 13 . . . . . . . 8 (((𝜑𝑧𝑌) ∧ (𝑔:𝑧𝑆 ∧ ∀𝑢𝑧 (𝑔𝑢) = (𝐺‘(𝑔𝑢)))) → 𝑧 ∈ dom (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))
71 dmeq 4624 . . . . . . . . . 10 ( = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) → dom = dom (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))
7271eleq2d 2157 . . . . . . . . 9 ( = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) → (𝑧 ∈ dom 𝑧 ∈ dom (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})))
7372rspcev 2722 . . . . . . . 8 (((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ 𝐴𝑧 ∈ dom (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})) → ∃𝐴 𝑧 ∈ dom )
7448, 70, 73syl2anc 403 . . . . . . 7 (((𝜑𝑧𝑌) ∧ (𝑔:𝑧𝑆 ∧ ∀𝑢𝑧 (𝑔𝑢) = (𝐺‘(𝑔𝑢)))) → ∃𝐴 𝑧 ∈ dom )
7515, 74exlimddv 1826 . . . . . 6 ((𝜑𝑧𝑌) → ∃𝐴 𝑧 ∈ dom )
76 eliun 3729 . . . . . 6 (𝑧 𝐴 dom ↔ ∃𝐴 𝑧 ∈ dom )
7775, 76sylibr 132 . . . . 5 ((𝜑𝑧𝑌) → 𝑧 𝐴 dom )
7877ex 113 . . . 4 (𝜑 → (𝑧𝑌𝑧 𝐴 dom ))
7978ssrdv 3029 . . 3 (𝜑𝑌 𝐴 dom )
80 dmuni 4634 . . . 4 dom 𝐴 = 𝐴 dom
8112, 1tfrcllemssrecs 6099 . . . . 5 (𝜑 𝐴 ⊆ recs(𝐺))
82 dmss 4623 . . . . 5 ( 𝐴 ⊆ recs(𝐺) → dom 𝐴 ⊆ dom recs(𝐺))
8381, 82syl 14 . . . 4 (𝜑 → dom 𝐴 ⊆ dom recs(𝐺))
8480, 83syl5eqssr 3069 . . 3 (𝜑 𝐴 dom ⊆ dom recs(𝐺))
8579, 84sstrd 3033 . 2 (𝜑𝑌 ⊆ dom recs(𝐺))
869dmeqi 4625 . 2 dom 𝐹 = dom recs(𝐺)
8785, 86syl6sseqr 3071 1 (𝜑𝑌 ⊆ dom 𝐹)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  w3a 924  wal 1287   = wceq 1289  wex 1426  wcel 1438  {cab 2074  wral 2359  wrex 2360  Vcvv 2619  cun 2995  wss 2997  {csn 3441  cop 3444   cuni 3648   ciun 3725  Ord word 4180  suc csuc 4183  dom cdm 4428  cres 4430  Fun wfun 4996  wf 4998  cfv 5002  recscrecs 6051
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 579  ax-in2 580  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-13 1449  ax-14 1450  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070  ax-coll 3946  ax-sep 3949  ax-pow 4001  ax-pr 4027  ax-un 4251  ax-setind 4343
This theorem depends on definitions:  df-bi 115  df-3an 926  df-tru 1292  df-fal 1295  df-nf 1395  df-sb 1693  df-eu 1951  df-mo 1952  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-ne 2256  df-ral 2364  df-rex 2365  df-reu 2366  df-rab 2368  df-v 2621  df-sbc 2839  df-csb 2932  df-dif 2999  df-un 3001  df-in 3003  df-ss 3010  df-nul 3285  df-pw 3427  df-sn 3447  df-pr 3448  df-op 3450  df-uni 3649  df-iun 3727  df-br 3838  df-opab 3892  df-mpt 3893  df-tr 3929  df-id 4111  df-iord 4184  df-on 4186  df-suc 4189  df-xp 4434  df-rel 4435  df-cnv 4436  df-co 4437  df-dm 4438  df-rn 4439  df-res 4440  df-ima 4441  df-iota 4967  df-fun 5004  df-fn 5005  df-f 5006  df-f1 5007  df-fo 5008  df-f1o 5009  df-fv 5010  df-recs 6052
This theorem is referenced by:  tfrcldm  6110
  Copyright terms: Public domain W3C validator