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

Theorem tfr1onlemex 6376
Description: Lemma for tfr1on 6379. (Contributed by Jim Kingdon, 16-Mar-2022.)
Hypotheses
Ref Expression
tfr1on.f 𝐹 = recs(𝐺)
tfr1on.g (𝜑 → Fun 𝐺)
tfr1on.x (𝜑 → Ord 𝑋)
tfr1on.ex ((𝜑𝑥𝑋𝑓 Fn 𝑥) → (𝐺𝑓) ∈ V)
tfr1onlemsucfn.1 𝐴 = {𝑓 ∣ ∃𝑥𝑋 (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦)))}
tfr1onlembacc.3 𝐵 = { ∣ ∃𝑧𝐷𝑔(𝑔 Fn 𝑧𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))}
tfr1onlembacc.u ((𝜑𝑥 𝑋) → suc 𝑥𝑋)
tfr1onlembacc.4 (𝜑𝐷𝑋)
tfr1onlembacc.5 (𝜑 → ∀𝑧𝐷𝑔(𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤))))
Assertion
Ref Expression
tfr1onlemex (𝜑 → ∃𝑓(𝑓 Fn 𝐷 ∧ ∀𝑢𝐷 (𝑓𝑢) = (𝐺‘(𝑓𝑢))))
Distinct variable groups:   𝐴,𝑓,𝑔,,𝑥,𝑧   𝐷,𝑓,𝑔,𝑥   𝑓,𝐺,𝑥,𝑦   𝑓,𝑋,𝑥   𝜑,𝑓,𝑔,,𝑥,𝑧   𝑦,𝑔,𝑧   𝐵,𝑓,𝑔,,𝑤,𝑧   𝑢,𝐵,𝑓,𝑤   𝐷,,𝑤,𝑧,𝑥   𝑢,𝐷   ,𝐺,𝑧,𝑦   𝑢,𝐺,𝑤   𝑔,𝑋,𝑧   𝜑,𝑤   𝑦,𝑤
Allowed substitution hints:   𝜑(𝑦,𝑢)   𝐴(𝑦,𝑤,𝑢)   𝐵(𝑥,𝑦)   𝐷(𝑦)   𝐹(𝑥,𝑦,𝑧,𝑤,𝑢,𝑓,𝑔,)   𝐺(𝑔)   𝑋(𝑦,𝑤,𝑢,)

Proof of Theorem tfr1onlemex
StepHypRef Expression
1 tfr1on.f . . . 4 𝐹 = recs(𝐺)
2 tfr1on.g . . . 4 (𝜑 → Fun 𝐺)
3 tfr1on.x . . . 4 (𝜑 → Ord 𝑋)
4 tfr1on.ex . . . 4 ((𝜑𝑥𝑋𝑓 Fn 𝑥) → (𝐺𝑓) ∈ V)
5 tfr1onlemsucfn.1 . . . 4 𝐴 = {𝑓 ∣ ∃𝑥𝑋 (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦)))}
6 tfr1onlembacc.3 . . . 4 𝐵 = { ∣ ∃𝑧𝐷𝑔(𝑔 Fn 𝑧𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))}
7 tfr1onlembacc.u . . . 4 ((𝜑𝑥 𝑋) → suc 𝑥𝑋)
8 tfr1onlembacc.4 . . . 4 (𝜑𝐷𝑋)
9 tfr1onlembacc.5 . . . 4 (𝜑 → ∀𝑧𝐷𝑔(𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤))))
101, 2, 3, 4, 5, 6, 7, 8, 9tfr1onlembex 6374 . . 3 (𝜑𝐵 ∈ V)
11 uniexg 4460 . . 3 (𝐵 ∈ V → 𝐵 ∈ V)
1210, 11syl 14 . 2 (𝜑 𝐵 ∈ V)
131, 2, 3, 4, 5, 6, 7, 8, 9tfr1onlembfn 6373 . . 3 (𝜑 𝐵 Fn 𝐷)
141, 2, 3, 4, 5, 6, 7, 8, 9tfr1onlemubacc 6375 . . 3 (𝜑 → ∀𝑢𝐷 ( 𝐵𝑢) = (𝐺‘( 𝐵𝑢)))
1513, 14jca 306 . 2 (𝜑 → ( 𝐵 Fn 𝐷 ∧ ∀𝑢𝐷 ( 𝐵𝑢) = (𝐺‘( 𝐵𝑢))))
16 fneq1 5326 . . . 4 (𝑓 = 𝐵 → (𝑓 Fn 𝐷 𝐵 Fn 𝐷))
17 fveq1 5536 . . . . . 6 (𝑓 = 𝐵 → (𝑓𝑢) = ( 𝐵𝑢))
18 reseq1 4922 . . . . . . 7 (𝑓 = 𝐵 → (𝑓𝑢) = ( 𝐵𝑢))
1918fveq2d 5541 . . . . . 6 (𝑓 = 𝐵 → (𝐺‘(𝑓𝑢)) = (𝐺‘( 𝐵𝑢)))
2017, 19eqeq12d 2204 . . . . 5 (𝑓 = 𝐵 → ((𝑓𝑢) = (𝐺‘(𝑓𝑢)) ↔ ( 𝐵𝑢) = (𝐺‘( 𝐵𝑢))))
2120ralbidv 2490 . . . 4 (𝑓 = 𝐵 → (∀𝑢𝐷 (𝑓𝑢) = (𝐺‘(𝑓𝑢)) ↔ ∀𝑢𝐷 ( 𝐵𝑢) = (𝐺‘( 𝐵𝑢))))
2216, 21anbi12d 473 . . 3 (𝑓 = 𝐵 → ((𝑓 Fn 𝐷 ∧ ∀𝑢𝐷 (𝑓𝑢) = (𝐺‘(𝑓𝑢))) ↔ ( 𝐵 Fn 𝐷 ∧ ∀𝑢𝐷 ( 𝐵𝑢) = (𝐺‘( 𝐵𝑢)))))
2322spcegv 2840 . 2 ( 𝐵 ∈ V → (( 𝐵 Fn 𝐷 ∧ ∀𝑢𝐷 ( 𝐵𝑢) = (𝐺‘( 𝐵𝑢))) → ∃𝑓(𝑓 Fn 𝐷 ∧ ∀𝑢𝐷 (𝑓𝑢) = (𝐺‘(𝑓𝑢)))))
2412, 15, 23sylc 62 1 (𝜑 → ∃𝑓(𝑓 Fn 𝐷 ∧ ∀𝑢𝐷 (𝑓𝑢) = (𝐺‘(𝑓𝑢))))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  w3a 980   = wceq 1364  wex 1503  wcel 2160  {cab 2175  wral 2468  wrex 2469  Vcvv 2752  cun 3142  {csn 3610  cop 3613   cuni 3827  Ord word 4383  suc csuc 4386  cres 4649  Fun wfun 5232   Fn wfn 5233  cfv 5238  recscrecs 6333
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-in1 615  ax-in2 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2162  ax-14 2163  ax-ext 2171  ax-coll 4136  ax-sep 4139  ax-pow 4195  ax-pr 4230  ax-un 4454  ax-setind 4557
This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1472  df-sb 1774  df-eu 2041  df-mo 2042  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-ne 2361  df-ral 2473  df-rex 2474  df-reu 2475  df-rab 2477  df-v 2754  df-sbc 2978  df-csb 3073  df-dif 3146  df-un 3148  df-in 3150  df-ss 3157  df-nul 3438  df-pw 3595  df-sn 3616  df-pr 3617  df-op 3619  df-uni 3828  df-iun 3906  df-br 4022  df-opab 4083  df-mpt 4084  df-tr 4120  df-id 4314  df-iord 4387  df-on 4389  df-suc 4392  df-xp 4653  df-rel 4654  df-cnv 4655  df-co 4656  df-dm 4657  df-rn 4658  df-res 4659  df-ima 4660  df-iota 5199  df-fun 5240  df-fn 5241  df-f 5242  df-f1 5243  df-fo 5244  df-f1o 5245  df-fv 5246  df-recs 6334
This theorem is referenced by:  tfr1onlemaccex  6377
  Copyright terms: Public domain W3C validator