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

Theorem rdgivallem 5998
 Description: Value of the recursive definition generator. Lemma for rdgival 5999 which simplifies the value further. (Contributed by Jim Kingdon, 13-Jul-2019.) (New usage is discouraged.)
Assertion
Ref Expression
rdgivallem ((𝐹 Fn V ∧ 𝐴𝑉𝐵 ∈ On) → (rec(𝐹, 𝐴)‘𝐵) = (𝐴 𝑥𝐵 (𝐹‘((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥))))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝑥,𝐹   𝑥,𝑉

Proof of Theorem rdgivallem
Dummy variables 𝑔 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-irdg 5987 . . . 4 rec(𝐹, 𝐴) = recs((𝑔 ∈ V ↦ (𝐴 𝑥 ∈ dom 𝑔(𝐹‘(𝑔𝑥)))))
2 rdgruledefgg 5992 . . . . 5 ((𝐹 Fn V ∧ 𝐴𝑉) → (Fun (𝑔 ∈ V ↦ (𝐴 𝑥 ∈ dom 𝑔(𝐹‘(𝑔𝑥)))) ∧ ((𝑔 ∈ V ↦ (𝐴 𝑥 ∈ dom 𝑔(𝐹‘(𝑔𝑥))))‘𝑦) ∈ V))
32alrimiv 1770 . . . 4 ((𝐹 Fn V ∧ 𝐴𝑉) → ∀𝑦(Fun (𝑔 ∈ V ↦ (𝐴 𝑥 ∈ dom 𝑔(𝐹‘(𝑔𝑥)))) ∧ ((𝑔 ∈ V ↦ (𝐴 𝑥 ∈ dom 𝑔(𝐹‘(𝑔𝑥))))‘𝑦) ∈ V))
41, 3tfri2d 5980 . . 3 (((𝐹 Fn V ∧ 𝐴𝑉) ∧ 𝐵 ∈ On) → (rec(𝐹, 𝐴)‘𝐵) = ((𝑔 ∈ V ↦ (𝐴 𝑥 ∈ dom 𝑔(𝐹‘(𝑔𝑥))))‘(rec(𝐹, 𝐴) ↾ 𝐵)))
543impa 1110 . 2 ((𝐹 Fn V ∧ 𝐴𝑉𝐵 ∈ On) → (rec(𝐹, 𝐴)‘𝐵) = ((𝑔 ∈ V ↦ (𝐴 𝑥 ∈ dom 𝑔(𝐹‘(𝑔𝑥))))‘(rec(𝐹, 𝐴) ↾ 𝐵)))
6 eqidd 2057 . . 3 ((𝐹 Fn V ∧ 𝐴𝑉𝐵 ∈ On) → (𝑔 ∈ V ↦ (𝐴 𝑥 ∈ dom 𝑔(𝐹‘(𝑔𝑥)))) = (𝑔 ∈ V ↦ (𝐴 𝑥 ∈ dom 𝑔(𝐹‘(𝑔𝑥)))))
7 dmeq 4562 . . . . . 6 (𝑔 = (rec(𝐹, 𝐴) ↾ 𝐵) → dom 𝑔 = dom (rec(𝐹, 𝐴) ↾ 𝐵))
8 onss 4246 . . . . . . . . 9 (𝐵 ∈ On → 𝐵 ⊆ On)
983ad2ant3 938 . . . . . . . 8 ((𝐹 Fn V ∧ 𝐴𝑉𝐵 ∈ On) → 𝐵 ⊆ On)
10 rdgifnon 5996 . . . . . . . . . 10 ((𝐹 Fn V ∧ 𝐴𝑉) → rec(𝐹, 𝐴) Fn On)
11 fndm 5025 . . . . . . . . . 10 (rec(𝐹, 𝐴) Fn On → dom rec(𝐹, 𝐴) = On)
1210, 11syl 14 . . . . . . . . 9 ((𝐹 Fn V ∧ 𝐴𝑉) → dom rec(𝐹, 𝐴) = On)
13123adant3 935 . . . . . . . 8 ((𝐹 Fn V ∧ 𝐴𝑉𝐵 ∈ On) → dom rec(𝐹, 𝐴) = On)
149, 13sseqtr4d 3009 . . . . . . 7 ((𝐹 Fn V ∧ 𝐴𝑉𝐵 ∈ On) → 𝐵 ⊆ dom rec(𝐹, 𝐴))
15 ssdmres 4660 . . . . . . 7 (𝐵 ⊆ dom rec(𝐹, 𝐴) ↔ dom (rec(𝐹, 𝐴) ↾ 𝐵) = 𝐵)
1614, 15sylib 131 . . . . . 6 ((𝐹 Fn V ∧ 𝐴𝑉𝐵 ∈ On) → dom (rec(𝐹, 𝐴) ↾ 𝐵) = 𝐵)
177, 16sylan9eqr 2110 . . . . 5 (((𝐹 Fn V ∧ 𝐴𝑉𝐵 ∈ On) ∧ 𝑔 = (rec(𝐹, 𝐴) ↾ 𝐵)) → dom 𝑔 = 𝐵)
18 fveq1 5204 . . . . . . 7 (𝑔 = (rec(𝐹, 𝐴) ↾ 𝐵) → (𝑔𝑥) = ((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥))
1918fveq2d 5209 . . . . . 6 (𝑔 = (rec(𝐹, 𝐴) ↾ 𝐵) → (𝐹‘(𝑔𝑥)) = (𝐹‘((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥)))
2019adantl 266 . . . . 5 (((𝐹 Fn V ∧ 𝐴𝑉𝐵 ∈ On) ∧ 𝑔 = (rec(𝐹, 𝐴) ↾ 𝐵)) → (𝐹‘(𝑔𝑥)) = (𝐹‘((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥)))
2117, 20iuneq12d 3708 . . . 4 (((𝐹 Fn V ∧ 𝐴𝑉𝐵 ∈ On) ∧ 𝑔 = (rec(𝐹, 𝐴) ↾ 𝐵)) → 𝑥 ∈ dom 𝑔(𝐹‘(𝑔𝑥)) = 𝑥𝐵 (𝐹‘((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥)))
2221uneq2d 3124 . . 3 (((𝐹 Fn V ∧ 𝐴𝑉𝐵 ∈ On) ∧ 𝑔 = (rec(𝐹, 𝐴) ↾ 𝐵)) → (𝐴 𝑥 ∈ dom 𝑔(𝐹‘(𝑔𝑥))) = (𝐴 𝑥𝐵 (𝐹‘((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥))))
23 rdgfun 5990 . . . . 5 Fun rec(𝐹, 𝐴)
24 resfunexg 5409 . . . . 5 ((Fun rec(𝐹, 𝐴) ∧ 𝐵 ∈ On) → (rec(𝐹, 𝐴) ↾ 𝐵) ∈ V)
2523, 24mpan 408 . . . 4 (𝐵 ∈ On → (rec(𝐹, 𝐴) ↾ 𝐵) ∈ V)
26253ad2ant3 938 . . 3 ((𝐹 Fn V ∧ 𝐴𝑉𝐵 ∈ On) → (rec(𝐹, 𝐴) ↾ 𝐵) ∈ V)
27 simpr 107 . . . . . 6 ((𝐹 Fn V ∧ 𝐵 ∈ On) → 𝐵 ∈ On)
28 vex 2577 . . . . . . . . . 10 𝑥 ∈ V
29 fvexg 5221 . . . . . . . . . 10 (((rec(𝐹, 𝐴) ↾ 𝐵) ∈ V ∧ 𝑥 ∈ V) → ((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥) ∈ V)
3025, 28, 29sylancl 398 . . . . . . . . 9 (𝐵 ∈ On → ((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥) ∈ V)
3130ralrimivw 2410 . . . . . . . 8 (𝐵 ∈ On → ∀𝑥𝐵 ((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥) ∈ V)
3231adantl 266 . . . . . . 7 ((𝐹 Fn V ∧ 𝐵 ∈ On) → ∀𝑥𝐵 ((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥) ∈ V)
33 funfvex 5219 . . . . . . . . . . 11 ((Fun 𝐹 ∧ ((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥) ∈ dom 𝐹) → (𝐹‘((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥)) ∈ V)
3433funfni 5026 . . . . . . . . . 10 ((𝐹 Fn V ∧ ((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥) ∈ V) → (𝐹‘((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥)) ∈ V)
3534ex 112 . . . . . . . . 9 (𝐹 Fn V → (((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥) ∈ V → (𝐹‘((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥)) ∈ V))
3635ralimdv 2405 . . . . . . . 8 (𝐹 Fn V → (∀𝑥𝐵 ((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥) ∈ V → ∀𝑥𝐵 (𝐹‘((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥)) ∈ V))
3736adantr 265 . . . . . . 7 ((𝐹 Fn V ∧ 𝐵 ∈ On) → (∀𝑥𝐵 ((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥) ∈ V → ∀𝑥𝐵 (𝐹‘((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥)) ∈ V))
3832, 37mpd 13 . . . . . 6 ((𝐹 Fn V ∧ 𝐵 ∈ On) → ∀𝑥𝐵 (𝐹‘((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥)) ∈ V)
39 iunexg 5773 . . . . . 6 ((𝐵 ∈ On ∧ ∀𝑥𝐵 (𝐹‘((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥)) ∈ V) → 𝑥𝐵 (𝐹‘((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥)) ∈ V)
4027, 38, 39syl2anc 397 . . . . 5 ((𝐹 Fn V ∧ 𝐵 ∈ On) → 𝑥𝐵 (𝐹‘((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥)) ∈ V)
41403adant2 934 . . . 4 ((𝐹 Fn V ∧ 𝐴𝑉𝐵 ∈ On) → 𝑥𝐵 (𝐹‘((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥)) ∈ V)
42 unexg 4205 . . . . . 6 ((𝐴𝑉 𝑥𝐵 (𝐹‘((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥)) ∈ V) → (𝐴 𝑥𝐵 (𝐹‘((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥))) ∈ V)
4342ex 112 . . . . 5 (𝐴𝑉 → ( 𝑥𝐵 (𝐹‘((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥)) ∈ V → (𝐴 𝑥𝐵 (𝐹‘((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥))) ∈ V))
44433ad2ant2 937 . . . 4 ((𝐹 Fn V ∧ 𝐴𝑉𝐵 ∈ On) → ( 𝑥𝐵 (𝐹‘((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥)) ∈ V → (𝐴 𝑥𝐵 (𝐹‘((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥))) ∈ V))
4541, 44mpd 13 . . 3 ((𝐹 Fn V ∧ 𝐴𝑉𝐵 ∈ On) → (𝐴 𝑥𝐵 (𝐹‘((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥))) ∈ V)
466, 22, 26, 45fvmptd 5280 . 2 ((𝐹 Fn V ∧ 𝐴𝑉𝐵 ∈ On) → ((𝑔 ∈ V ↦ (𝐴 𝑥 ∈ dom 𝑔(𝐹‘(𝑔𝑥))))‘(rec(𝐹, 𝐴) ↾ 𝐵)) = (𝐴 𝑥𝐵 (𝐹‘((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥))))
475, 46eqtrd 2088 1 ((𝐹 Fn V ∧ 𝐴𝑉𝐵 ∈ On) → (rec(𝐹, 𝐴)‘𝐵) = (𝐴 𝑥𝐵 (𝐹‘((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥))))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 101   ∧ w3a 896   = wceq 1259   ∈ wcel 1409  ∀wral 2323  Vcvv 2574   ∪ cun 2942   ⊆ wss 2944  ∪ ciun 3684   ↦ cmpt 3845  Oncon0 4127  dom cdm 4372   ↾ cres 4374  Fun wfun 4923   Fn wfn 4924  ‘cfv 4929  reccrdg 5986 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-in1 554  ax-in2 555  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-13 1420  ax-14 1421  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038  ax-coll 3899  ax-sep 3902  ax-pow 3954  ax-pr 3971  ax-un 4197  ax-setind 4289 This theorem depends on definitions:  df-bi 114  df-3an 898  df-tru 1262  df-fal 1265  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-ne 2221  df-ral 2328  df-rex 2329  df-reu 2330  df-rab 2332  df-v 2576  df-sbc 2787  df-csb 2880  df-dif 2947  df-un 2949  df-in 2951  df-ss 2958  df-nul 3252  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-suc 4135  df-xp 4378  df-rel 4379  df-cnv 4380  df-co 4381  df-dm 4382  df-rn 4383  df-res 4384  df-ima 4385  df-iota 4894  df-fun 4931  df-fn 4932  df-f 4933  df-f1 4934  df-fo 4935  df-f1o 4936  df-fv 4937  df-recs 5950  df-irdg 5987 This theorem is referenced by:  rdgival  5999  rdgon  6003
 Copyright terms: Public domain W3C validator