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

Theorem tfrlemi14d 6336
Description: The domain of recs is all ordinals (lemma for transfinite recursion). (Contributed by Jim Kingdon, 9-Jul-2019.)
Hypotheses
Ref Expression
tfrlemi14d.1 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))}
tfrlemi14d.2 (𝜑 → ∀𝑥(Fun 𝐹 ∧ (𝐹𝑥) ∈ V))
Assertion
Ref Expression
tfrlemi14d (𝜑 → dom recs(𝐹) = On)
Distinct variable groups:   𝑥,𝑓,𝑦,𝐴   𝑓,𝐹,𝑥,𝑦   𝜑,𝑓,𝑦
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem tfrlemi14d
Dummy variables 𝑔 𝑢 𝑤 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 tfrlemi14d.1 . . . 4 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))}
21tfrlem8 6321 . . 3 Ord dom recs(𝐹)
3 ordsson 4493 . . 3 (Ord dom recs(𝐹) → dom recs(𝐹) ⊆ On)
42, 3mp1i 10 . 2 (𝜑 → dom recs(𝐹) ⊆ On)
5 tfrlemi14d.2 . . . . . . . 8 (𝜑 → ∀𝑥(Fun 𝐹 ∧ (𝐹𝑥) ∈ V))
61, 5tfrlemi1 6335 . . . . . . 7 ((𝜑𝑧 ∈ On) → ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑢𝑧 (𝑔𝑢) = (𝐹‘(𝑔𝑢))))
75ad2antrr 488 . . . . . . . . 9 (((𝜑𝑧 ∈ On) ∧ (𝑔 Fn 𝑧 ∧ ∀𝑢𝑧 (𝑔𝑢) = (𝐹‘(𝑔𝑢)))) → ∀𝑥(Fun 𝐹 ∧ (𝐹𝑥) ∈ V))
8 simplr 528 . . . . . . . . 9 (((𝜑𝑧 ∈ On) ∧ (𝑔 Fn 𝑧 ∧ ∀𝑢𝑧 (𝑔𝑢) = (𝐹‘(𝑔𝑢)))) → 𝑧 ∈ On)
9 simprl 529 . . . . . . . . 9 (((𝜑𝑧 ∈ On) ∧ (𝑔 Fn 𝑧 ∧ ∀𝑢𝑧 (𝑔𝑢) = (𝐹‘(𝑔𝑢)))) → 𝑔 Fn 𝑧)
10 fneq2 5307 . . . . . . . . . . . . 13 (𝑤 = 𝑧 → (𝑔 Fn 𝑤𝑔 Fn 𝑧))
11 raleq 2673 . . . . . . . . . . . . 13 (𝑤 = 𝑧 → (∀𝑢𝑤 (𝑔𝑢) = (𝐹‘(𝑔𝑢)) ↔ ∀𝑢𝑧 (𝑔𝑢) = (𝐹‘(𝑔𝑢))))
1210, 11anbi12d 473 . . . . . . . . . . . 12 (𝑤 = 𝑧 → ((𝑔 Fn 𝑤 ∧ ∀𝑢𝑤 (𝑔𝑢) = (𝐹‘(𝑔𝑢))) ↔ (𝑔 Fn 𝑧 ∧ ∀𝑢𝑧 (𝑔𝑢) = (𝐹‘(𝑔𝑢)))))
1312rspcev 2843 . . . . . . . . . . 11 ((𝑧 ∈ On ∧ (𝑔 Fn 𝑧 ∧ ∀𝑢𝑧 (𝑔𝑢) = (𝐹‘(𝑔𝑢)))) → ∃𝑤 ∈ On (𝑔 Fn 𝑤 ∧ ∀𝑢𝑤 (𝑔𝑢) = (𝐹‘(𝑔𝑢))))
1413adantll 476 . . . . . . . . . 10 (((𝜑𝑧 ∈ On) ∧ (𝑔 Fn 𝑧 ∧ ∀𝑢𝑧 (𝑔𝑢) = (𝐹‘(𝑔𝑢)))) → ∃𝑤 ∈ On (𝑔 Fn 𝑤 ∧ ∀𝑢𝑤 (𝑔𝑢) = (𝐹‘(𝑔𝑢))))
15 vex 2742 . . . . . . . . . . 11 𝑔 ∈ V
161, 15tfrlem3a 6313 . . . . . . . . . 10 (𝑔𝐴 ↔ ∃𝑤 ∈ On (𝑔 Fn 𝑤 ∧ ∀𝑢𝑤 (𝑔𝑢) = (𝐹‘(𝑔𝑢))))
1714, 16sylibr 134 . . . . . . . . 9 (((𝜑𝑧 ∈ On) ∧ (𝑔 Fn 𝑧 ∧ ∀𝑢𝑧 (𝑔𝑢) = (𝐹‘(𝑔𝑢)))) → 𝑔𝐴)
181, 7, 8, 9, 17tfrlemisucaccv 6328 . . . . . . . 8 (((𝜑𝑧 ∈ On) ∧ (𝑔 Fn 𝑧 ∧ ∀𝑢𝑧 (𝑔𝑢) = (𝐹‘(𝑔𝑢)))) → (𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ∈ 𝐴)
19 vex 2742 . . . . . . . . . . . 12 𝑧 ∈ V
205tfrlem3-2d 6315 . . . . . . . . . . . . 13 (𝜑 → (Fun 𝐹 ∧ (𝐹𝑔) ∈ V))
2120simprd 114 . . . . . . . . . . . 12 (𝜑 → (𝐹𝑔) ∈ V)
22 opexg 4230 . . . . . . . . . . . 12 ((𝑧 ∈ V ∧ (𝐹𝑔) ∈ V) → ⟨𝑧, (𝐹𝑔)⟩ ∈ V)
2319, 21, 22sylancr 414 . . . . . . . . . . 11 (𝜑 → ⟨𝑧, (𝐹𝑔)⟩ ∈ V)
24 snidg 3623 . . . . . . . . . . 11 (⟨𝑧, (𝐹𝑔)⟩ ∈ V → ⟨𝑧, (𝐹𝑔)⟩ ∈ {⟨𝑧, (𝐹𝑔)⟩})
25 elun2 3305 . . . . . . . . . . 11 (⟨𝑧, (𝐹𝑔)⟩ ∈ {⟨𝑧, (𝐹𝑔)⟩} → ⟨𝑧, (𝐹𝑔)⟩ ∈ (𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}))
2623, 24, 253syl 17 . . . . . . . . . 10 (𝜑 → ⟨𝑧, (𝐹𝑔)⟩ ∈ (𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}))
2726ad2antrr 488 . . . . . . . . 9 (((𝜑𝑧 ∈ On) ∧ (𝑔 Fn 𝑧 ∧ ∀𝑢𝑧 (𝑔𝑢) = (𝐹‘(𝑔𝑢)))) → ⟨𝑧, (𝐹𝑔)⟩ ∈ (𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}))
28 opeldmg 4834 . . . . . . . . . . 11 ((𝑧 ∈ V ∧ (𝐹𝑔) ∈ V) → (⟨𝑧, (𝐹𝑔)⟩ ∈ (𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) → 𝑧 ∈ dom (𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩})))
2919, 21, 28sylancr 414 . . . . . . . . . 10 (𝜑 → (⟨𝑧, (𝐹𝑔)⟩ ∈ (𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) → 𝑧 ∈ dom (𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩})))
3029ad2antrr 488 . . . . . . . . 9 (((𝜑𝑧 ∈ On) ∧ (𝑔 Fn 𝑧 ∧ ∀𝑢𝑧 (𝑔𝑢) = (𝐹‘(𝑔𝑢)))) → (⟨𝑧, (𝐹𝑔)⟩ ∈ (𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) → 𝑧 ∈ dom (𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩})))
3127, 30mpd 13 . . . . . . . 8 (((𝜑𝑧 ∈ On) ∧ (𝑔 Fn 𝑧 ∧ ∀𝑢𝑧 (𝑔𝑢) = (𝐹‘(𝑔𝑢)))) → 𝑧 ∈ dom (𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}))
32 dmeq 4829 . . . . . . . . . 10 ( = (𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) → dom = dom (𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}))
3332eleq2d 2247 . . . . . . . . 9 ( = (𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) → (𝑧 ∈ dom 𝑧 ∈ dom (𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩})))
3433rspcev 2843 . . . . . . . 8 (((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ∈ 𝐴𝑧 ∈ dom (𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩})) → ∃𝐴 𝑧 ∈ dom )
3518, 31, 34syl2anc 411 . . . . . . 7 (((𝜑𝑧 ∈ On) ∧ (𝑔 Fn 𝑧 ∧ ∀𝑢𝑧 (𝑔𝑢) = (𝐹‘(𝑔𝑢)))) → ∃𝐴 𝑧 ∈ dom )
366, 35exlimddv 1898 . . . . . 6 ((𝜑𝑧 ∈ On) → ∃𝐴 𝑧 ∈ dom )
37 eliun 3892 . . . . . 6 (𝑧 𝐴 dom ↔ ∃𝐴 𝑧 ∈ dom )
3836, 37sylibr 134 . . . . 5 ((𝜑𝑧 ∈ On) → 𝑧 𝐴 dom )
3938ex 115 . . . 4 (𝜑 → (𝑧 ∈ On → 𝑧 𝐴 dom ))
4039ssrdv 3163 . . 3 (𝜑 → On ⊆ 𝐴 dom )
411recsfval 6318 . . . . 5 recs(𝐹) = 𝐴
4241dmeqi 4830 . . . 4 dom recs(𝐹) = dom 𝐴
43 dmuni 4839 . . . 4 dom 𝐴 = 𝐴 dom
4442, 43eqtri 2198 . . 3 dom recs(𝐹) = 𝐴 dom
4540, 44sseqtrrdi 3206 . 2 (𝜑 → On ⊆ dom recs(𝐹))
464, 45eqssd 3174 1 (𝜑 → dom recs(𝐹) = On)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wal 1351   = wceq 1353  wcel 2148  {cab 2163  wral 2455  wrex 2456  Vcvv 2739  cun 3129  wss 3131  {csn 3594  cop 3597   cuni 3811   ciun 3888  Ord word 4364  Oncon0 4365  dom cdm 4628  cres 4630  Fun wfun 5212   Fn wfn 5213  cfv 5218  recscrecs 6307
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 614  ax-in2 615  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-coll 4120  ax-sep 4123  ax-pow 4176  ax-pr 4211  ax-un 4435  ax-setind 4538
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-fal 1359  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-ne 2348  df-ral 2460  df-rex 2461  df-reu 2462  df-rab 2464  df-v 2741  df-sbc 2965  df-csb 3060  df-dif 3133  df-un 3135  df-in 3137  df-ss 3144  df-nul 3425  df-pw 3579  df-sn 3600  df-pr 3601  df-op 3603  df-uni 3812  df-iun 3890  df-br 4006  df-opab 4067  df-mpt 4068  df-tr 4104  df-id 4295  df-iord 4368  df-on 4370  df-suc 4373  df-xp 4634  df-rel 4635  df-cnv 4636  df-co 4637  df-dm 4638  df-rn 4639  df-res 4640  df-ima 4641  df-iota 5180  df-fun 5220  df-fn 5221  df-f 5222  df-f1 5223  df-fo 5224  df-f1o 5225  df-fv 5226  df-recs 6308
This theorem is referenced by:  tfri1d  6338
  Copyright terms: Public domain W3C validator