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

Theorem tfrcllemssrecs 6352
Description: Lemma for tfrcl 6364. The union of functions acceptable for tfrcl 6364 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 4491 . . . . . 6 (Ord 𝑋𝑋 ⊆ On)
4 ssrexv 3220 . . . . . 6 (𝑋 ⊆ On → (∃𝑥𝑋 (𝑓:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦))) → ∃𝑥 ∈ On (𝑓:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦)))))
52, 3, 43syl 17 . . . . 5 (𝜑 → (∃𝑥𝑋 (𝑓:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦))) → ∃𝑥 ∈ On (𝑓:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦)))))
65ss2abdv 3228 . . . 4 (𝜑 → {𝑓 ∣ ∃𝑥𝑋 (𝑓:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦)))} ⊆ {𝑓 ∣ ∃𝑥 ∈ On (𝑓:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦)))})
71, 6eqsstrid 3201 . . 3 (𝜑𝐴 ⊆ {𝑓 ∣ ∃𝑥 ∈ On (𝑓:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦)))})
87unissd 3833 . 2 (𝜑 𝐴 {𝑓 ∣ ∃𝑥 ∈ On (𝑓:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦)))})
9 ffn 5365 . . . . . . 7 (𝑓:𝑥𝑆𝑓 Fn 𝑥)
109anim1i 340 . . . . . 6 ((𝑓:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦))) → (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦))))
1110reximi 2574 . . . . 5 (∃𝑥 ∈ On (𝑓:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦))) → ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦))))
1211ss2abi 3227 . . . 4 {𝑓 ∣ ∃𝑥 ∈ On (𝑓:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦)))} ⊆ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦)))}
1312unissi 3832 . . 3 {𝑓 ∣ ∃𝑥 ∈ On (𝑓:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦)))} ⊆ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦)))}
14 df-recs 6305 . . 3 recs(𝐺) = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦)))}
1513, 14sseqtrri 3190 . 2 {𝑓 ∣ ∃𝑥 ∈ On (𝑓:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦)))} ⊆ recs(𝐺)
168, 15sstrdi 3167 1 (𝜑 𝐴 ⊆ recs(𝐺))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104   = wceq 1353  {cab 2163  wral 2455  wrex 2456  wss 3129   cuni 3809  Ord word 4362  Oncon0 4363  cres 4628   Fn wfn 5211  wf 5212  cfv 5216  recscrecs 6304
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-v 2739  df-in 3135  df-ss 3142  df-uni 3810  df-tr 4102  df-iord 4366  df-on 4368  df-f 5220  df-recs 6305
This theorem is referenced by:  tfrcllembfn  6357  tfrcllemubacc  6359  tfrcllemres  6362
  Copyright terms: Public domain W3C validator