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

Theorem tfrlem8 6319
Description: Lemma for transfinite recursion. The domain of recs is ordinal. (Contributed by NM, 14-Aug-1994.) (Proof shortened by Alan Sare, 11-Mar-2008.)
Hypothesis
Ref Expression
tfrlem.1 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))}
Assertion
Ref Expression
tfrlem8 Ord dom recs(𝐹)
Distinct variable group:   𝑥,𝑓,𝑦,𝐹
Allowed substitution hints:   𝐴(𝑥,𝑦,𝑓)

Proof of Theorem tfrlem8
Dummy variables 𝑔 𝑧 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 tfrlem.1 . . . . . . . . 9 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))}
21tfrlem3 6312 . . . . . . . 8 𝐴 = {𝑔 ∣ ∃𝑧 ∈ On (𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐹‘(𝑔𝑤)))}
32abeq2i 2288 . . . . . . 7 (𝑔𝐴 ↔ ∃𝑧 ∈ On (𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐹‘(𝑔𝑤))))
4 fndm 5316 . . . . . . . . . . 11 (𝑔 Fn 𝑧 → dom 𝑔 = 𝑧)
54adantr 276 . . . . . . . . . 10 ((𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐹‘(𝑔𝑤))) → dom 𝑔 = 𝑧)
65eleq1d 2246 . . . . . . . . 9 ((𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐹‘(𝑔𝑤))) → (dom 𝑔 ∈ On ↔ 𝑧 ∈ On))
76biimprcd 160 . . . . . . . 8 (𝑧 ∈ On → ((𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐹‘(𝑔𝑤))) → dom 𝑔 ∈ On))
87rexlimiv 2588 . . . . . . 7 (∃𝑧 ∈ On (𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐹‘(𝑔𝑤))) → dom 𝑔 ∈ On)
93, 8sylbi 121 . . . . . 6 (𝑔𝐴 → dom 𝑔 ∈ On)
10 eleq1a 2249 . . . . . 6 (dom 𝑔 ∈ On → (𝑧 = dom 𝑔𝑧 ∈ On))
119, 10syl 14 . . . . 5 (𝑔𝐴 → (𝑧 = dom 𝑔𝑧 ∈ On))
1211rexlimiv 2588 . . . 4 (∃𝑔𝐴 𝑧 = dom 𝑔𝑧 ∈ On)
1312abssi 3231 . . 3 {𝑧 ∣ ∃𝑔𝐴 𝑧 = dom 𝑔} ⊆ On
14 ssorduni 4487 . . 3 ({𝑧 ∣ ∃𝑔𝐴 𝑧 = dom 𝑔} ⊆ On → Ord {𝑧 ∣ ∃𝑔𝐴 𝑧 = dom 𝑔})
1513, 14ax-mp 5 . 2 Ord {𝑧 ∣ ∃𝑔𝐴 𝑧 = dom 𝑔}
161recsfval 6316 . . . . 5 recs(𝐹) = 𝐴
1716dmeqi 4829 . . . 4 dom recs(𝐹) = dom 𝐴
18 dmuni 4838 . . . 4 dom 𝐴 = 𝑔𝐴 dom 𝑔
19 vex 2741 . . . . . 6 𝑔 ∈ V
2019dmex 4894 . . . . 5 dom 𝑔 ∈ V
2120dfiun2 3921 . . . 4 𝑔𝐴 dom 𝑔 = {𝑧 ∣ ∃𝑔𝐴 𝑧 = dom 𝑔}
2217, 18, 213eqtri 2202 . . 3 dom recs(𝐹) = {𝑧 ∣ ∃𝑔𝐴 𝑧 = dom 𝑔}
23 ordeq 4373 . . 3 (dom recs(𝐹) = {𝑧 ∣ ∃𝑔𝐴 𝑧 = dom 𝑔} → (Ord dom recs(𝐹) ↔ Ord {𝑧 ∣ ∃𝑔𝐴 𝑧 = dom 𝑔}))
2422, 23ax-mp 5 . 2 (Ord dom recs(𝐹) ↔ Ord {𝑧 ∣ ∃𝑔𝐴 𝑧 = dom 𝑔})
2515, 24mpbir 146 1 Ord dom recs(𝐹)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wb 105   = wceq 1353  wcel 2148  {cab 2163  wral 2455  wrex 2456  wss 3130   cuni 3810   ciun 3887  Ord word 4363  Oncon0 4364  dom cdm 4627  cres 4629   Fn wfn 5212  cfv 5217  recscrecs 6305
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-13 2150  ax-14 2151  ax-ext 2159  ax-sep 4122  ax-pow 4175  ax-pr 4210  ax-un 4434
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-v 2740  df-un 3134  df-in 3136  df-ss 3143  df-pw 3578  df-sn 3599  df-pr 3600  df-op 3602  df-uni 3811  df-iun 3889  df-br 4005  df-opab 4066  df-tr 4103  df-iord 4367  df-on 4369  df-xp 4633  df-rel 4634  df-cnv 4635  df-co 4636  df-dm 4637  df-rn 4638  df-res 4639  df-iota 5179  df-fun 5219  df-fn 5220  df-fv 5225  df-recs 6306
This theorem is referenced by:  tfrlemi14d  6334  tfri1dALT  6352
  Copyright terms: Public domain W3C validator