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

Theorem rdgivallem 5946
Description: Value of the recursive definition generator. Lemma for rdgival 5947 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 5935 . . . 4 rec(𝐹, 𝐴) = recs((𝑔 ∈ V ↦ (𝐴 𝑥 ∈ dom 𝑔(𝐹‘(𝑔𝑥)))))
2 rdgruledefgg 5940 . . . . 5 ((𝐹 Fn V ∧ 𝐴𝑉) → (Fun (𝑔 ∈ V ↦ (𝐴 𝑥 ∈ dom 𝑔(𝐹‘(𝑔𝑥)))) ∧ ((𝑔 ∈ V ↦ (𝐴 𝑥 ∈ dom 𝑔(𝐹‘(𝑔𝑥))))‘𝑦) ∈ V))
32alrimiv 1754 . . . 4 ((𝐹 Fn V ∧ 𝐴𝑉) → ∀𝑦(Fun (𝑔 ∈ V ↦ (𝐴 𝑥 ∈ dom 𝑔(𝐹‘(𝑔𝑥)))) ∧ ((𝑔 ∈ V ↦ (𝐴 𝑥 ∈ dom 𝑔(𝐹‘(𝑔𝑥))))‘𝑦) ∈ V))
41, 3tfri2d 5928 . . 3 (((𝐹 Fn V ∧ 𝐴𝑉) ∧ 𝐵 ∈ On) → (rec(𝐹, 𝐴)‘𝐵) = ((𝑔 ∈ V ↦ (𝐴 𝑥 ∈ dom 𝑔(𝐹‘(𝑔𝑥))))‘(rec(𝐹, 𝐴) ↾ 𝐵)))
543impa 1099 . 2 ((𝐹 Fn V ∧ 𝐴𝑉𝐵 ∈ On) → (rec(𝐹, 𝐴)‘𝐵) = ((𝑔 ∈ V ↦ (𝐴 𝑥 ∈ dom 𝑔(𝐹‘(𝑔𝑥))))‘(rec(𝐹, 𝐴) ↾ 𝐵)))
6 eqidd 2041 . . 3 ((𝐹 Fn V ∧ 𝐴𝑉𝐵 ∈ On) → (𝑔 ∈ V ↦ (𝐴 𝑥 ∈ dom 𝑔(𝐹‘(𝑔𝑥)))) = (𝑔 ∈ V ↦ (𝐴 𝑥 ∈ dom 𝑔(𝐹‘(𝑔𝑥)))))
7 dmeq 4513 . . . . . 6 (𝑔 = (rec(𝐹, 𝐴) ↾ 𝐵) → dom 𝑔 = dom (rec(𝐹, 𝐴) ↾ 𝐵))
8 onss 4206 . . . . . . . . 9 (𝐵 ∈ On → 𝐵 ⊆ On)
983ad2ant3 927 . . . . . . . 8 ((𝐹 Fn V ∧ 𝐴𝑉𝐵 ∈ On) → 𝐵 ⊆ On)
10 rdgifnon 5944 . . . . . . . . . 10 ((𝐹 Fn V ∧ 𝐴𝑉) → rec(𝐹, 𝐴) Fn On)
11 fndm 4976 . . . . . . . . . 10 (rec(𝐹, 𝐴) Fn On → dom rec(𝐹, 𝐴) = On)
1210, 11syl 14 . . . . . . . . 9 ((𝐹 Fn V ∧ 𝐴𝑉) → dom rec(𝐹, 𝐴) = On)
13123adant3 924 . . . . . . . 8 ((𝐹 Fn V ∧ 𝐴𝑉𝐵 ∈ On) → dom rec(𝐹, 𝐴) = On)
149, 13sseqtr4d 2979 . . . . . . 7 ((𝐹 Fn V ∧ 𝐴𝑉𝐵 ∈ On) → 𝐵 ⊆ dom rec(𝐹, 𝐴))
15 ssdmres 4611 . . . . . . 7 (𝐵 ⊆ dom rec(𝐹, 𝐴) ↔ dom (rec(𝐹, 𝐴) ↾ 𝐵) = 𝐵)
1614, 15sylib 127 . . . . . 6 ((𝐹 Fn V ∧ 𝐴𝑉𝐵 ∈ On) → dom (rec(𝐹, 𝐴) ↾ 𝐵) = 𝐵)
177, 16sylan9eqr 2094 . . . . 5 (((𝐹 Fn V ∧ 𝐴𝑉𝐵 ∈ On) ∧ 𝑔 = (rec(𝐹, 𝐴) ↾ 𝐵)) → dom 𝑔 = 𝐵)
18 fveq1 5155 . . . . . . 7 (𝑔 = (rec(𝐹, 𝐴) ↾ 𝐵) → (𝑔𝑥) = ((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥))
1918fveq2d 5160 . . . . . 6 (𝑔 = (rec(𝐹, 𝐴) ↾ 𝐵) → (𝐹‘(𝑔𝑥)) = (𝐹‘((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥)))
2019adantl 262 . . . . 5 (((𝐹 Fn V ∧ 𝐴𝑉𝐵 ∈ On) ∧ 𝑔 = (rec(𝐹, 𝐴) ↾ 𝐵)) → (𝐹‘(𝑔𝑥)) = (𝐹‘((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥)))
2117, 20iuneq12d 3678 . . . 4 (((𝐹 Fn V ∧ 𝐴𝑉𝐵 ∈ On) ∧ 𝑔 = (rec(𝐹, 𝐴) ↾ 𝐵)) → 𝑥 ∈ dom 𝑔(𝐹‘(𝑔𝑥)) = 𝑥𝐵 (𝐹‘((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥)))
2221uneq2d 3094 . . 3 (((𝐹 Fn V ∧ 𝐴𝑉𝐵 ∈ On) ∧ 𝑔 = (rec(𝐹, 𝐴) ↾ 𝐵)) → (𝐴 𝑥 ∈ dom 𝑔(𝐹‘(𝑔𝑥))) = (𝐴 𝑥𝐵 (𝐹‘((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥))))
23 rdgfun 5938 . . . . 5 Fun rec(𝐹, 𝐴)
24 resfunexg 5360 . . . . 5 ((Fun rec(𝐹, 𝐴) ∧ 𝐵 ∈ On) → (rec(𝐹, 𝐴) ↾ 𝐵) ∈ V)
2523, 24mpan 400 . . . 4 (𝐵 ∈ On → (rec(𝐹, 𝐴) ↾ 𝐵) ∈ V)
26253ad2ant3 927 . . 3 ((𝐹 Fn V ∧ 𝐴𝑉𝐵 ∈ On) → (rec(𝐹, 𝐴) ↾ 𝐵) ∈ V)
27 simpr 103 . . . . . 6 ((𝐹 Fn V ∧ 𝐵 ∈ On) → 𝐵 ∈ On)
28 vex 2557 . . . . . . . . . 10 𝑥 ∈ V
29 fvexg 5172 . . . . . . . . . 10 (((rec(𝐹, 𝐴) ↾ 𝐵) ∈ V ∧ 𝑥 ∈ V) → ((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥) ∈ V)
3025, 28, 29sylancl 392 . . . . . . . . 9 (𝐵 ∈ On → ((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥) ∈ V)
3130ralrimivw 2390 . . . . . . . 8 (𝐵 ∈ On → ∀𝑥𝐵 ((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥) ∈ V)
3231adantl 262 . . . . . . 7 ((𝐹 Fn V ∧ 𝐵 ∈ On) → ∀𝑥𝐵 ((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥) ∈ V)
33 funfvex 5170 . . . . . . . . . . 11 ((Fun 𝐹 ∧ ((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥) ∈ dom 𝐹) → (𝐹‘((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥)) ∈ V)
3433funfni 4977 . . . . . . . . . 10 ((𝐹 Fn V ∧ ((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥) ∈ V) → (𝐹‘((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥)) ∈ V)
3534ex 108 . . . . . . . . 9 (𝐹 Fn V → (((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥) ∈ V → (𝐹‘((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥)) ∈ V))
3635ralimdv 2385 . . . . . . . 8 (𝐹 Fn V → (∀𝑥𝐵 ((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥) ∈ V → ∀𝑥𝐵 (𝐹‘((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥)) ∈ V))
3736adantr 261 . . . . . . 7 ((𝐹 Fn V ∧ 𝐵 ∈ On) → (∀𝑥𝐵 ((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥) ∈ V → ∀𝑥𝐵 (𝐹‘((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥)) ∈ V))
3832, 37mpd 13 . . . . . 6 ((𝐹 Fn V ∧ 𝐵 ∈ On) → ∀𝑥𝐵 (𝐹‘((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥)) ∈ V)
39 iunexg 5724 . . . . . 6 ((𝐵 ∈ On ∧ ∀𝑥𝐵 (𝐹‘((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥)) ∈ V) → 𝑥𝐵 (𝐹‘((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥)) ∈ V)
4027, 38, 39syl2anc 391 . . . . 5 ((𝐹 Fn V ∧ 𝐵 ∈ On) → 𝑥𝐵 (𝐹‘((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥)) ∈ V)
41403adant2 923 . . . 4 ((𝐹 Fn V ∧ 𝐴𝑉𝐵 ∈ On) → 𝑥𝐵 (𝐹‘((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥)) ∈ V)
42 unexg 4165 . . . . . 6 ((𝐴𝑉 𝑥𝐵 (𝐹‘((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥)) ∈ V) → (𝐴 𝑥𝐵 (𝐹‘((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥))) ∈ V)
4342ex 108 . . . . 5 (𝐴𝑉 → ( 𝑥𝐵 (𝐹‘((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥)) ∈ V → (𝐴 𝑥𝐵 (𝐹‘((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥))) ∈ V))
44433ad2ant2 926 . . . 4 ((𝐹 Fn V ∧ 𝐴𝑉𝐵 ∈ On) → ( 𝑥𝐵 (𝐹‘((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥)) ∈ V → (𝐴 𝑥𝐵 (𝐹‘((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥))) ∈ V))
4541, 44mpd 13 . . 3 ((𝐹 Fn V ∧ 𝐴𝑉𝐵 ∈ On) → (𝐴 𝑥𝐵 (𝐹‘((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥))) ∈ V)
466, 22, 26, 45fvmptd 5231 . 2 ((𝐹 Fn V ∧ 𝐴𝑉𝐵 ∈ On) → ((𝑔 ∈ V ↦ (𝐴 𝑥 ∈ dom 𝑔(𝐹‘(𝑔𝑥))))‘(rec(𝐹, 𝐴) ↾ 𝐵)) = (𝐴 𝑥𝐵 (𝐹‘((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥))))
475, 46eqtrd 2072 1 ((𝐹 Fn V ∧ 𝐴𝑉𝐵 ∈ On) → (rec(𝐹, 𝐴)‘𝐵) = (𝐴 𝑥𝐵 (𝐹‘((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥))))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 97  w3a 885   = wceq 1243  wcel 1393  wral 2303  Vcvv 2554  cun 2912  wss 2914   ciun 3654  cmpt 3815  Oncon0 4087  dom cdm 4323  cres 4325  Fun wfun 4874   Fn wfn 4875  cfv 4880  reccrdg 5934
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-13 1404  ax-14 1405  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022  ax-coll 3869  ax-sep 3872  ax-pow 3924  ax-pr 3941  ax-un 4157  ax-setind 4247
This theorem depends on definitions:  df-bi 110  df-3an 887  df-tru 1246  df-fal 1249  df-nf 1350  df-sb 1646  df-eu 1903  df-mo 1904  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-ne 2206  df-ral 2308  df-rex 2309  df-reu 2310  df-rab 2312  df-v 2556  df-sbc 2762  df-csb 2850  df-dif 2917  df-un 2919  df-in 2921  df-ss 2928  df-nul 3222  df-pw 3358  df-sn 3378  df-pr 3379  df-op 3381  df-uni 3578  df-iun 3656  df-br 3762  df-opab 3816  df-mpt 3817  df-tr 3852  df-id 4027  df-iord 4090  df-on 4092  df-suc 4095  df-xp 4329  df-rel 4330  df-cnv 4331  df-co 4332  df-dm 4333  df-rn 4334  df-res 4335  df-ima 4336  df-iota 4845  df-fun 4882  df-fn 4883  df-f 4884  df-f1 4885  df-fo 4886  df-f1o 4887  df-fv 4888  df-recs 5898  df-irdg 5935
This theorem is referenced by:  rdgival  5947  rdgon  5951
  Copyright terms: Public domain W3C validator