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

Theorem tfrlem7 5963
 Description: Lemma for transfinite recursion. The union of all acceptable functions is a function. (Contributed by NM, 9-Aug-1994.) (Revised by Mario Carneiro, 24-May-2019.)
Hypothesis
Ref Expression
tfrlem.1 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))}
Assertion
Ref Expression
tfrlem7 Fun recs(𝐹)
Distinct variable group:   𝑥,𝑓,𝑦,𝐹
Allowed substitution hints:   𝐴(𝑥,𝑦,𝑓)

Proof of Theorem tfrlem7
Dummy variables 𝑔 𝑢 𝑣 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 tfrlem.1 . . 3 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))}
21tfrlem6 5962 . 2 Rel recs(𝐹)
31recsfval 5961 . . . . . . . . 9 recs(𝐹) = 𝐴
43eleq2i 2120 . . . . . . . 8 (⟨𝑥, 𝑢⟩ ∈ recs(𝐹) ↔ ⟨𝑥, 𝑢⟩ ∈ 𝐴)
5 eluni 3610 . . . . . . . 8 (⟨𝑥, 𝑢⟩ ∈ 𝐴 ↔ ∃𝑔(⟨𝑥, 𝑢⟩ ∈ 𝑔𝑔𝐴))
64, 5bitri 177 . . . . . . 7 (⟨𝑥, 𝑢⟩ ∈ recs(𝐹) ↔ ∃𝑔(⟨𝑥, 𝑢⟩ ∈ 𝑔𝑔𝐴))
73eleq2i 2120 . . . . . . . 8 (⟨𝑥, 𝑣⟩ ∈ recs(𝐹) ↔ ⟨𝑥, 𝑣⟩ ∈ 𝐴)
8 eluni 3610 . . . . . . . 8 (⟨𝑥, 𝑣⟩ ∈ 𝐴 ↔ ∃(⟨𝑥, 𝑣⟩ ∈ 𝐴))
97, 8bitri 177 . . . . . . 7 (⟨𝑥, 𝑣⟩ ∈ recs(𝐹) ↔ ∃(⟨𝑥, 𝑣⟩ ∈ 𝐴))
106, 9anbi12i 441 . . . . . 6 ((⟨𝑥, 𝑢⟩ ∈ recs(𝐹) ∧ ⟨𝑥, 𝑣⟩ ∈ recs(𝐹)) ↔ (∃𝑔(⟨𝑥, 𝑢⟩ ∈ 𝑔𝑔𝐴) ∧ ∃(⟨𝑥, 𝑣⟩ ∈ 𝐴)))
11 eeanv 1823 . . . . . 6 (∃𝑔((⟨𝑥, 𝑢⟩ ∈ 𝑔𝑔𝐴) ∧ (⟨𝑥, 𝑣⟩ ∈ 𝐴)) ↔ (∃𝑔(⟨𝑥, 𝑢⟩ ∈ 𝑔𝑔𝐴) ∧ ∃(⟨𝑥, 𝑣⟩ ∈ 𝐴)))
1210, 11bitr4i 180 . . . . 5 ((⟨𝑥, 𝑢⟩ ∈ recs(𝐹) ∧ ⟨𝑥, 𝑣⟩ ∈ recs(𝐹)) ↔ ∃𝑔((⟨𝑥, 𝑢⟩ ∈ 𝑔𝑔𝐴) ∧ (⟨𝑥, 𝑣⟩ ∈ 𝐴)))
13 df-br 3792 . . . . . . . . 9 (𝑥𝑔𝑢 ↔ ⟨𝑥, 𝑢⟩ ∈ 𝑔)
14 df-br 3792 . . . . . . . . 9 (𝑥𝑣 ↔ ⟨𝑥, 𝑣⟩ ∈ )
1513, 14anbi12i 441 . . . . . . . 8 ((𝑥𝑔𝑢𝑥𝑣) ↔ (⟨𝑥, 𝑢⟩ ∈ 𝑔 ∧ ⟨𝑥, 𝑣⟩ ∈ ))
161tfrlem5 5960 . . . . . . . . 9 ((𝑔𝐴𝐴) → ((𝑥𝑔𝑢𝑥𝑣) → 𝑢 = 𝑣))
1716impcom 120 . . . . . . . 8 (((𝑥𝑔𝑢𝑥𝑣) ∧ (𝑔𝐴𝐴)) → 𝑢 = 𝑣)
1815, 17sylanbr 273 . . . . . . 7 (((⟨𝑥, 𝑢⟩ ∈ 𝑔 ∧ ⟨𝑥, 𝑣⟩ ∈ ) ∧ (𝑔𝐴𝐴)) → 𝑢 = 𝑣)
1918an4s 530 . . . . . 6 (((⟨𝑥, 𝑢⟩ ∈ 𝑔𝑔𝐴) ∧ (⟨𝑥, 𝑣⟩ ∈ 𝐴)) → 𝑢 = 𝑣)
2019exlimivv 1792 . . . . 5 (∃𝑔((⟨𝑥, 𝑢⟩ ∈ 𝑔𝑔𝐴) ∧ (⟨𝑥, 𝑣⟩ ∈ 𝐴)) → 𝑢 = 𝑣)
2112, 20sylbi 118 . . . 4 ((⟨𝑥, 𝑢⟩ ∈ recs(𝐹) ∧ ⟨𝑥, 𝑣⟩ ∈ recs(𝐹)) → 𝑢 = 𝑣)
2221ax-gen 1354 . . 3 𝑣((⟨𝑥, 𝑢⟩ ∈ recs(𝐹) ∧ ⟨𝑥, 𝑣⟩ ∈ recs(𝐹)) → 𝑢 = 𝑣)
2322gen2 1355 . 2 𝑥𝑢𝑣((⟨𝑥, 𝑢⟩ ∈ recs(𝐹) ∧ ⟨𝑥, 𝑣⟩ ∈ recs(𝐹)) → 𝑢 = 𝑣)
24 dffun4 4940 . 2 (Fun recs(𝐹) ↔ (Rel recs(𝐹) ∧ ∀𝑥𝑢𝑣((⟨𝑥, 𝑢⟩ ∈ recs(𝐹) ∧ ⟨𝑥, 𝑣⟩ ∈ recs(𝐹)) → 𝑢 = 𝑣)))
252, 23, 24mpbir2an 860 1 Fun recs(𝐹)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 101  ∀wal 1257   = wceq 1259  ∃wex 1397   ∈ wcel 1409  {cab 2042  ∀wral 2323  ∃wrex 2324  ⟨cop 3405  ∪ cuni 3607   class class class wbr 3791  Oncon0 4127   ↾ cres 4374  Rel wrel 4377  Fun wfun 4923   Fn wfn 4924  ‘cfv 4929  recscrecs 5949 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-io 640  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-10 1412  ax-11 1413  ax-i12 1414  ax-bndl 1415  ax-4 1416  ax-14 1421  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038  ax-sep 3902  ax-pow 3954  ax-pr 3971  ax-setind 4289 This theorem depends on definitions:  df-bi 114  df-3an 898  df-tru 1262  df-nf 1366  df-sb 1662  df-eu 1919  df-mo 1920  df-clab 2043  df-cleq 2049  df-clel 2052  df-nfc 2183  df-ral 2328  df-rex 2329  df-rab 2332  df-v 2576  df-sbc 2787  df-csb 2880  df-un 2949  df-in 2951  df-ss 2958  df-pw 3388  df-sn 3408  df-pr 3409  df-op 3411  df-uni 3608  df-iun 3686  df-br 3792  df-opab 3846  df-mpt 3847  df-tr 3882  df-id 4057  df-iord 4130  df-on 4132  df-xp 4378  df-rel 4379  df-cnv 4380  df-co 4381  df-dm 4382  df-res 4384  df-iota 4894  df-fun 4931  df-fn 4932  df-fv 4937  df-recs 5950 This theorem is referenced by:  tfrlem9  5965  tfrlemibfn  5972  tfrlemiubacc  5974  tfri1d  5979  tfrfun  5985  rdgfun  5990
 Copyright terms: Public domain W3C validator