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

Theorem tfrcllemssrecs 6249
 Description: Lemma for tfrcl 6261. The union of functions acceptable for tfrcl 6261 is a subset of recs. (Contributed by Jim Kingdon, 25-Mar-2022.)
Hypotheses
Ref Expression
tfrcllemssrecs.1 𝐴 = {𝑓 ∣ ∃𝑥𝑋 (𝑓:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦)))}
tfrcllemssrecs.x (𝜑 → Ord 𝑋)
Assertion
Ref Expression
tfrcllemssrecs (𝜑 𝐴 ⊆ recs(𝐺))
Distinct variable groups:   𝑓,𝐺,𝑥,𝑦   𝑥,𝑋   𝜑,𝑓
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝐴(𝑥,𝑦,𝑓)   𝑆(𝑥,𝑦,𝑓)   𝑋(𝑦,𝑓)

Proof of Theorem tfrcllemssrecs
StepHypRef Expression
1 tfrcllemssrecs.1 . . . 4 𝐴 = {𝑓 ∣ ∃𝑥𝑋 (𝑓:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦)))}
2 tfrcllemssrecs.x . . . . . 6 (𝜑 → Ord 𝑋)
3 ordsson 4408 . . . . . 6 (Ord 𝑋𝑋 ⊆ On)
4 ssrexv 3162 . . . . . 6 (𝑋 ⊆ On → (∃𝑥𝑋 (𝑓:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦))) → ∃𝑥 ∈ On (𝑓:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦)))))
52, 3, 43syl 17 . . . . 5 (𝜑 → (∃𝑥𝑋 (𝑓:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦))) → ∃𝑥 ∈ On (𝑓:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦)))))
65ss2abdv 3170 . . . 4 (𝜑 → {𝑓 ∣ ∃𝑥𝑋 (𝑓:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦)))} ⊆ {𝑓 ∣ ∃𝑥 ∈ On (𝑓:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦)))})
71, 6eqsstrid 3143 . . 3 (𝜑𝐴 ⊆ {𝑓 ∣ ∃𝑥 ∈ On (𝑓:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦)))})
87unissd 3760 . 2 (𝜑 𝐴 {𝑓 ∣ ∃𝑥 ∈ On (𝑓:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦)))})
9 ffn 5272 . . . . . . 7 (𝑓:𝑥𝑆𝑓 Fn 𝑥)
109anim1i 338 . . . . . 6 ((𝑓:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦))) → (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦))))
1110reximi 2529 . . . . 5 (∃𝑥 ∈ On (𝑓:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦))) → ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦))))
1211ss2abi 3169 . . . 4 {𝑓 ∣ ∃𝑥 ∈ On (𝑓:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦)))} ⊆ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦)))}
1312unissi 3759 . . 3 {𝑓 ∣ ∃𝑥 ∈ On (𝑓:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦)))} ⊆ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦)))}
14 df-recs 6202 . . 3 recs(𝐺) = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦)))}
1513, 14sseqtrri 3132 . 2 {𝑓 ∣ ∃𝑥 ∈ On (𝑓:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦)))} ⊆ recs(𝐺)
168, 15sstrdi 3109 1 (𝜑 𝐴 ⊆ recs(𝐺))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   = wceq 1331  {cab 2125  ∀wral 2416  ∃wrex 2417   ⊆ wss 3071  ∪ cuni 3736  Ord word 4284  Oncon0 4285   ↾ cres 4541   Fn wfn 5118  ⟶wf 5119  ‘cfv 5123  recscrecs 6201 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-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121 This theorem depends on definitions:  df-bi 116  df-3an 964  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-ral 2421  df-rex 2422  df-v 2688  df-in 3077  df-ss 3084  df-uni 3737  df-tr 4027  df-iord 4288  df-on 4290  df-f 5127  df-recs 6202 This theorem is referenced by:  tfrcllembfn  6254  tfrcllemubacc  6256  tfrcllemres  6259
 Copyright terms: Public domain W3C validator