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

Theorem rdgon 6289
 Description: Evaluating the recursive definition generator produces an ordinal. There is a hypothesis that the characteristic function produces ordinals on ordinal arguments. (Contributed by Jim Kingdon, 26-Jul-2019.) (Revised by Jim Kingdon, 13-Apr-2022.)
Hypotheses
Ref Expression
rdgon.2 (𝜑𝐴 ∈ On)
rdgon.3 (𝜑 → ∀𝑥 ∈ On (𝐹𝑥) ∈ On)
Assertion
Ref Expression
rdgon ((𝜑𝐵 ∈ On) → (rec(𝐹, 𝐴)‘𝐵) ∈ On)
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝑥,𝐹   𝜑,𝑥

Proof of Theorem rdgon
Dummy variables 𝑓 𝑔 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-irdg 6273 . 2 rec(𝐹, 𝐴) = recs((𝑔 ∈ V ↦ (𝐴 𝑥 ∈ dom 𝑔(𝐹‘(𝑔𝑥)))))
2 funmpt 5167 . . 3 Fun (𝑔 ∈ V ↦ (𝐴 𝑥 ∈ dom 𝑔(𝐹‘(𝑔𝑥))))
32a1i 9 . 2 ((𝜑𝐵 ∈ On) → Fun (𝑔 ∈ V ↦ (𝐴 𝑥 ∈ dom 𝑔(𝐹‘(𝑔𝑥)))))
4 ordon 4408 . . 3 Ord On
54a1i 9 . 2 ((𝜑𝐵 ∈ On) → Ord On)
6 vex 2692 . . . 4 𝑓 ∈ V
7 rdgon.2 . . . . . . 7 (𝜑𝐴 ∈ On)
87adantr 274 . . . . . 6 ((𝜑𝐵 ∈ On) → 𝐴 ∈ On)
983ad2ant1 1003 . . . . 5 (((𝜑𝐵 ∈ On) ∧ 𝑦 ∈ On ∧ 𝑓:𝑦⟶On) → 𝐴 ∈ On)
106dmex 4811 . . . . . 6 dom 𝑓 ∈ V
11 fveq2 5427 . . . . . . . . . 10 (𝑥 = (𝑓𝑧) → (𝐹𝑥) = (𝐹‘(𝑓𝑧)))
1211eleq1d 2209 . . . . . . . . 9 (𝑥 = (𝑓𝑧) → ((𝐹𝑥) ∈ On ↔ (𝐹‘(𝑓𝑧)) ∈ On))
13 rdgon.3 . . . . . . . . . . . 12 (𝜑 → ∀𝑥 ∈ On (𝐹𝑥) ∈ On)
1413adantr 274 . . . . . . . . . . 11 ((𝜑𝐵 ∈ On) → ∀𝑥 ∈ On (𝐹𝑥) ∈ On)
15143ad2ant1 1003 . . . . . . . . . 10 (((𝜑𝐵 ∈ On) ∧ 𝑦 ∈ On ∧ 𝑓:𝑦⟶On) → ∀𝑥 ∈ On (𝐹𝑥) ∈ On)
1615adantr 274 . . . . . . . . 9 ((((𝜑𝐵 ∈ On) ∧ 𝑦 ∈ On ∧ 𝑓:𝑦⟶On) ∧ 𝑧 ∈ dom 𝑓) → ∀𝑥 ∈ On (𝐹𝑥) ∈ On)
17 simpl3 987 . . . . . . . . . 10 ((((𝜑𝐵 ∈ On) ∧ 𝑦 ∈ On ∧ 𝑓:𝑦⟶On) ∧ 𝑧 ∈ dom 𝑓) → 𝑓:𝑦⟶On)
18 simpr 109 . . . . . . . . . . 11 ((((𝜑𝐵 ∈ On) ∧ 𝑦 ∈ On ∧ 𝑓:𝑦⟶On) ∧ 𝑧 ∈ dom 𝑓) → 𝑧 ∈ dom 𝑓)
19 fdm 5284 . . . . . . . . . . . . 13 (𝑓:𝑦⟶On → dom 𝑓 = 𝑦)
2019eleq2d 2210 . . . . . . . . . . . 12 (𝑓:𝑦⟶On → (𝑧 ∈ dom 𝑓𝑧𝑦))
2117, 20syl 14 . . . . . . . . . . 11 ((((𝜑𝐵 ∈ On) ∧ 𝑦 ∈ On ∧ 𝑓:𝑦⟶On) ∧ 𝑧 ∈ dom 𝑓) → (𝑧 ∈ dom 𝑓𝑧𝑦))
2218, 21mpbid 146 . . . . . . . . . 10 ((((𝜑𝐵 ∈ On) ∧ 𝑦 ∈ On ∧ 𝑓:𝑦⟶On) ∧ 𝑧 ∈ dom 𝑓) → 𝑧𝑦)
2317, 22ffvelrnd 5562 . . . . . . . . 9 ((((𝜑𝐵 ∈ On) ∧ 𝑦 ∈ On ∧ 𝑓:𝑦⟶On) ∧ 𝑧 ∈ dom 𝑓) → (𝑓𝑧) ∈ On)
2412, 16, 23rspcdva 2797 . . . . . . . 8 ((((𝜑𝐵 ∈ On) ∧ 𝑦 ∈ On ∧ 𝑓:𝑦⟶On) ∧ 𝑧 ∈ dom 𝑓) → (𝐹‘(𝑓𝑧)) ∈ On)
2524ralrimiva 2508 . . . . . . 7 (((𝜑𝐵 ∈ On) ∧ 𝑦 ∈ On ∧ 𝑓:𝑦⟶On) → ∀𝑧 ∈ dom 𝑓(𝐹‘(𝑓𝑧)) ∈ On)
26 fveq2 5427 . . . . . . . . . 10 (𝑥 = 𝑧 → (𝑓𝑥) = (𝑓𝑧))
2726fveq2d 5431 . . . . . . . . 9 (𝑥 = 𝑧 → (𝐹‘(𝑓𝑥)) = (𝐹‘(𝑓𝑧)))
2827eleq1d 2209 . . . . . . . 8 (𝑥 = 𝑧 → ((𝐹‘(𝑓𝑥)) ∈ On ↔ (𝐹‘(𝑓𝑧)) ∈ On))
2928cbvralv 2657 . . . . . . 7 (∀𝑥 ∈ dom 𝑓(𝐹‘(𝑓𝑥)) ∈ On ↔ ∀𝑧 ∈ dom 𝑓(𝐹‘(𝑓𝑧)) ∈ On)
3025, 29sylibr 133 . . . . . 6 (((𝜑𝐵 ∈ On) ∧ 𝑦 ∈ On ∧ 𝑓:𝑦⟶On) → ∀𝑥 ∈ dom 𝑓(𝐹‘(𝑓𝑥)) ∈ On)
31 iunon 6187 . . . . . 6 ((dom 𝑓 ∈ V ∧ ∀𝑥 ∈ dom 𝑓(𝐹‘(𝑓𝑥)) ∈ On) → 𝑥 ∈ dom 𝑓(𝐹‘(𝑓𝑥)) ∈ On)
3210, 30, 31sylancr 411 . . . . 5 (((𝜑𝐵 ∈ On) ∧ 𝑦 ∈ On ∧ 𝑓:𝑦⟶On) → 𝑥 ∈ dom 𝑓(𝐹‘(𝑓𝑥)) ∈ On)
33 onun2 4412 . . . . 5 ((𝐴 ∈ On ∧ 𝑥 ∈ dom 𝑓(𝐹‘(𝑓𝑥)) ∈ On) → (𝐴 𝑥 ∈ dom 𝑓(𝐹‘(𝑓𝑥))) ∈ On)
349, 32, 33syl2anc 409 . . . 4 (((𝜑𝐵 ∈ On) ∧ 𝑦 ∈ On ∧ 𝑓:𝑦⟶On) → (𝐴 𝑥 ∈ dom 𝑓(𝐹‘(𝑓𝑥))) ∈ On)
35 dmeq 4745 . . . . . . 7 (𝑔 = 𝑓 → dom 𝑔 = dom 𝑓)
36 fveq1 5426 . . . . . . . 8 (𝑔 = 𝑓 → (𝑔𝑥) = (𝑓𝑥))
3736fveq2d 5431 . . . . . . 7 (𝑔 = 𝑓 → (𝐹‘(𝑔𝑥)) = (𝐹‘(𝑓𝑥)))
3835, 37iuneq12d 3843 . . . . . 6 (𝑔 = 𝑓 𝑥 ∈ dom 𝑔(𝐹‘(𝑔𝑥)) = 𝑥 ∈ dom 𝑓(𝐹‘(𝑓𝑥)))
3938uneq2d 3233 . . . . 5 (𝑔 = 𝑓 → (𝐴 𝑥 ∈ dom 𝑔(𝐹‘(𝑔𝑥))) = (𝐴 𝑥 ∈ dom 𝑓(𝐹‘(𝑓𝑥))))
40 eqid 2140 . . . . 5 (𝑔 ∈ V ↦ (𝐴 𝑥 ∈ dom 𝑔(𝐹‘(𝑔𝑥)))) = (𝑔 ∈ V ↦ (𝐴 𝑥 ∈ dom 𝑔(𝐹‘(𝑔𝑥))))
4139, 40fvmptg 5503 . . . 4 ((𝑓 ∈ V ∧ (𝐴 𝑥 ∈ dom 𝑓(𝐹‘(𝑓𝑥))) ∈ On) → ((𝑔 ∈ V ↦ (𝐴 𝑥 ∈ dom 𝑔(𝐹‘(𝑔𝑥))))‘𝑓) = (𝐴 𝑥 ∈ dom 𝑓(𝐹‘(𝑓𝑥))))
426, 34, 41sylancr 411 . . 3 (((𝜑𝐵 ∈ On) ∧ 𝑦 ∈ On ∧ 𝑓:𝑦⟶On) → ((𝑔 ∈ V ↦ (𝐴 𝑥 ∈ dom 𝑔(𝐹‘(𝑔𝑥))))‘𝑓) = (𝐴 𝑥 ∈ dom 𝑓(𝐹‘(𝑓𝑥))))
4342, 34eqeltrd 2217 . 2 (((𝜑𝐵 ∈ On) ∧ 𝑦 ∈ On ∧ 𝑓:𝑦⟶On) → ((𝑔 ∈ V ↦ (𝐴 𝑥 ∈ dom 𝑔(𝐹‘(𝑔𝑥))))‘𝑓) ∈ On)
44 unon 4433 . . . . . 6 On = On
4544eleq2i 2207 . . . . 5 (𝑦 On ↔ 𝑦 ∈ On)
4645biimpi 119 . . . 4 (𝑦 On → 𝑦 ∈ On)
4746adantl 275 . . 3 (((𝜑𝐵 ∈ On) ∧ 𝑦 On) → 𝑦 ∈ On)
48 suceloni 4423 . . 3 (𝑦 ∈ On → suc 𝑦 ∈ On)
4947, 48syl 14 . 2 (((𝜑𝐵 ∈ On) ∧ 𝑦 On) → suc 𝑦 ∈ On)
5044eleq2i 2207 . . . 4 (𝐵 On ↔ 𝐵 ∈ On)
5150biimpri 132 . . 3 (𝐵 ∈ On → 𝐵 On)
5251adantl 275 . 2 ((𝜑𝐵 ∈ On) → 𝐵 On)
531, 3, 5, 43, 49, 52tfrcl 6267 1 ((𝜑𝐵 ∈ On) → (rec(𝐹, 𝐴)‘𝐵) ∈ On)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   ∧ w3a 963   = wceq 1332   ∈ wcel 1481  ∀wral 2417  Vcvv 2689   ∪ cun 3072  ∪ cuni 3742  ∪ ciun 3819   ↦ cmpt 3995  Ord word 4290  Oncon0 4291  suc csuc 4293  dom cdm 4545  Fun wfun 5123  ⟶wf 5125  ‘cfv 5129  reccrdg 6272 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-13 1492  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-coll 4049  ax-sep 4052  ax-pow 4104  ax-pr 4137  ax-un 4361  ax-setind 4458 This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1335  df-fal 1338  df-nf 1438  df-sb 1737  df-eu 2003  df-mo 2004  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ne 2310  df-ral 2422  df-rex 2423  df-reu 2424  df-rab 2426  df-v 2691  df-sbc 2913  df-csb 3007  df-dif 3076  df-un 3078  df-in 3080  df-ss 3087  df-nul 3367  df-pw 3515  df-sn 3536  df-pr 3537  df-op 3539  df-uni 3743  df-iun 3821  df-br 3936  df-opab 3996  df-mpt 3997  df-tr 4033  df-id 4221  df-iord 4294  df-on 4296  df-suc 4299  df-xp 4551  df-rel 4552  df-cnv 4553  df-co 4554  df-dm 4555  df-rn 4556  df-res 4557  df-ima 4558  df-iota 5094  df-fun 5131  df-fn 5132  df-f 5133  df-f1 5134  df-fo 5135  df-f1o 5136  df-fv 5137  df-recs 6208  df-irdg 6273 This theorem is referenced by:  oacl  6362  omcl  6363  oeicl  6364
 Copyright terms: Public domain W3C validator