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

Theorem frecsuclem3 5881
Description: Lemma for frecsuc 5882. (Contributed by Jim Kingdon, 15-Aug-2019.)
Hypothesis
Ref Expression
frecsuclem1.h 𝐺 = (g V ↦ {x ∣ (𝑚 𝜔 (dom g = suc 𝑚 x (𝐹‘(g𝑚))) (dom g = ∅ x A))})
Assertion
Ref Expression
frecsuclem3 ((𝐹 Fn V A 𝑉 B 𝜔) → (frec(𝐹, A)‘suc B) = (𝐹‘(frec(𝐹, A)‘B)))
Distinct variable groups:   g,𝑚,x,A   g,𝐹,x,𝑚   x,B   g,𝑉,𝑚   B,g,𝑚   g,𝐺,𝑚,x   x,𝑉

Proof of Theorem frecsuclem3
Dummy variable y is distinct from all other variables.
StepHypRef Expression
1 eqid 2023 . . . . . . . . . . . . 13 recs(𝐺) = recs(𝐺)
2 frecsuclem1.h . . . . . . . . . . . . . 14 𝐺 = (g V ↦ {x ∣ (𝑚 𝜔 (dom g = suc 𝑚 x (𝐹‘(g𝑚))) (dom g = ∅ x A))})
32frectfr 5875 . . . . . . . . . . . . 13 ((𝐹 Fn V A 𝑉) → y(Fun 𝐺 (𝐺y) V))
41, 3tfri1d 5846 . . . . . . . . . . . 12 ((𝐹 Fn V A 𝑉) → recs(𝐺) Fn On)
5 fnfun 4899 . . . . . . . . . . . 12 (recs(𝐺) Fn On → Fun recs(𝐺))
64, 5syl 14 . . . . . . . . . . 11 ((𝐹 Fn V A 𝑉) → Fun recs(𝐺))
763adant3 915 . . . . . . . . . 10 ((𝐹 Fn V A 𝑉 B 𝜔) → Fun recs(𝐺))
8 peano2 4221 . . . . . . . . . . 11 (B 𝜔 → suc B 𝜔)
983ad2ant3 918 . . . . . . . . . 10 ((𝐹 Fn V A 𝑉 B 𝜔) → suc B 𝜔)
10 resfunexg 5284 . . . . . . . . . 10 ((Fun recs(𝐺) suc B 𝜔) → (recs(𝐺) ↾ suc B) V)
117, 9, 10syl2anc 393 . . . . . . . . 9 ((𝐹 Fn V A 𝑉 B 𝜔) → (recs(𝐺) ↾ suc B) V)
12 simp1 895 . . . . . . . . 9 ((𝐹 Fn V A 𝑉 B 𝜔) → 𝐹 Fn V)
13 simp2 896 . . . . . . . . 9 ((𝐹 Fn V A 𝑉 B 𝜔) → A 𝑉)
1411, 12, 13frecabex 5874 . . . . . . . 8 ((𝐹 Fn V A 𝑉 B 𝜔) → {x ∣ (𝑚 𝜔 (dom (recs(𝐺) ↾ suc B) = suc 𝑚 x (𝐹‘((recs(𝐺) ↾ suc B)‘𝑚))) (dom (recs(𝐺) ↾ suc B) = ∅ x A))} V)
15 dmeq 4438 . . . . . . . . . . . . . . . . 17 (g = (recs(𝐺) ↾ suc B) → dom g = dom (recs(𝐺) ↾ suc B))
1615eqeq1d 2031 . . . . . . . . . . . . . . . 16 (g = (recs(𝐺) ↾ suc B) → (dom g = suc 𝑚 ↔ dom (recs(𝐺) ↾ suc B) = suc 𝑚))
17 fveq1 5079 . . . . . . . . . . . . . . . . . 18 (g = (recs(𝐺) ↾ suc B) → (g𝑚) = ((recs(𝐺) ↾ suc B)‘𝑚))
1817fveq2d 5084 . . . . . . . . . . . . . . . . 17 (g = (recs(𝐺) ↾ suc B) → (𝐹‘(g𝑚)) = (𝐹‘((recs(𝐺) ↾ suc B)‘𝑚)))
1918eleq2d 2090 . . . . . . . . . . . . . . . 16 (g = (recs(𝐺) ↾ suc B) → (x (𝐹‘(g𝑚)) ↔ x (𝐹‘((recs(𝐺) ↾ suc B)‘𝑚))))
2016, 19anbi12d 445 . . . . . . . . . . . . . . 15 (g = (recs(𝐺) ↾ suc B) → ((dom g = suc 𝑚 x (𝐹‘(g𝑚))) ↔ (dom (recs(𝐺) ↾ suc B) = suc 𝑚 x (𝐹‘((recs(𝐺) ↾ suc B)‘𝑚)))))
2120rexbidv 2304 . . . . . . . . . . . . . 14 (g = (recs(𝐺) ↾ suc B) → (𝑚 𝜔 (dom g = suc 𝑚 x (𝐹‘(g𝑚))) ↔ 𝑚 𝜔 (dom (recs(𝐺) ↾ suc B) = suc 𝑚 x (𝐹‘((recs(𝐺) ↾ suc B)‘𝑚)))))
2215eqeq1d 2031 . . . . . . . . . . . . . . 15 (g = (recs(𝐺) ↾ suc B) → (dom g = ∅ ↔ dom (recs(𝐺) ↾ suc B) = ∅))
2322anbi1d 441 . . . . . . . . . . . . . 14 (g = (recs(𝐺) ↾ suc B) → ((dom g = ∅ x A) ↔ (dom (recs(𝐺) ↾ suc B) = ∅ x A)))
2421, 23orbi12d 695 . . . . . . . . . . . . 13 (g = (recs(𝐺) ↾ suc B) → ((𝑚 𝜔 (dom g = suc 𝑚 x (𝐹‘(g𝑚))) (dom g = ∅ x A)) ↔ (𝑚 𝜔 (dom (recs(𝐺) ↾ suc B) = suc 𝑚 x (𝐹‘((recs(𝐺) ↾ suc B)‘𝑚))) (dom (recs(𝐺) ↾ suc B) = ∅ x A))))
2524abbidv 2138 . . . . . . . . . . . 12 (g = (recs(𝐺) ↾ suc B) → {x ∣ (𝑚 𝜔 (dom g = suc 𝑚 x (𝐹‘(g𝑚))) (dom g = ∅ x A))} = {x ∣ (𝑚 𝜔 (dom (recs(𝐺) ↾ suc B) = suc 𝑚 x (𝐹‘((recs(𝐺) ↾ suc B)‘𝑚))) (dom (recs(𝐺) ↾ suc B) = ∅ x A))})
2625, 2fvmptg 5150 . . . . . . . . . . 11 (((recs(𝐺) ↾ suc B) V {x ∣ (𝑚 𝜔 (dom (recs(𝐺) ↾ suc B) = suc 𝑚 x (𝐹‘((recs(𝐺) ↾ suc B)‘𝑚))) (dom (recs(𝐺) ↾ suc B) = ∅ x A))} V) → (𝐺‘(recs(𝐺) ↾ suc B)) = {x ∣ (𝑚 𝜔 (dom (recs(𝐺) ↾ suc B) = suc 𝑚 x (𝐹‘((recs(𝐺) ↾ suc B)‘𝑚))) (dom (recs(𝐺) ↾ suc B) = ∅ x A))})
2726ex 108 . . . . . . . . . 10 ((recs(𝐺) ↾ suc B) V → ({x ∣ (𝑚 𝜔 (dom (recs(𝐺) ↾ suc B) = suc 𝑚 x (𝐹‘((recs(𝐺) ↾ suc B)‘𝑚))) (dom (recs(𝐺) ↾ suc B) = ∅ x A))} V → (𝐺‘(recs(𝐺) ↾ suc B)) = {x ∣ (𝑚 𝜔 (dom (recs(𝐺) ↾ suc B) = suc 𝑚 x (𝐹‘((recs(𝐺) ↾ suc B)‘𝑚))) (dom (recs(𝐺) ↾ suc B) = ∅ x A))}))
2811, 27syl 14 . . . . . . . . 9 ((𝐹 Fn V A 𝑉 B 𝜔) → ({x ∣ (𝑚 𝜔 (dom (recs(𝐺) ↾ suc B) = suc 𝑚 x (𝐹‘((recs(𝐺) ↾ suc B)‘𝑚))) (dom (recs(𝐺) ↾ suc B) = ∅ x A))} V → (𝐺‘(recs(𝐺) ↾ suc B)) = {x ∣ (𝑚 𝜔 (dom (recs(𝐺) ↾ suc B) = suc 𝑚 x (𝐹‘((recs(𝐺) ↾ suc B)‘𝑚))) (dom (recs(𝐺) ↾ suc B) = ∅ x A))}))
292frecsuclem1 5878 . . . . . . . . . 10 ((𝐹 Fn V A 𝑉 B 𝜔) → (frec(𝐹, A)‘suc B) = (𝐺‘(recs(𝐺) ↾ suc B)))
3029eqeq1d 2031 . . . . . . . . 9 ((𝐹 Fn V A 𝑉 B 𝜔) → ((frec(𝐹, A)‘suc B) = {x ∣ (𝑚 𝜔 (dom (recs(𝐺) ↾ suc B) = suc 𝑚 x (𝐹‘((recs(𝐺) ↾ suc B)‘𝑚))) (dom (recs(𝐺) ↾ suc B) = ∅ x A))} ↔ (𝐺‘(recs(𝐺) ↾ suc B)) = {x ∣ (𝑚 𝜔 (dom (recs(𝐺) ↾ suc B) = suc 𝑚 x (𝐹‘((recs(𝐺) ↾ suc B)‘𝑚))) (dom (recs(𝐺) ↾ suc B) = ∅ x A))}))
3128, 30sylibrd 158 . . . . . . . 8 ((𝐹 Fn V A 𝑉 B 𝜔) → ({x ∣ (𝑚 𝜔 (dom (recs(𝐺) ↾ suc B) = suc 𝑚 x (𝐹‘((recs(𝐺) ↾ suc B)‘𝑚))) (dom (recs(𝐺) ↾ suc B) = ∅ x A))} V → (frec(𝐹, A)‘suc B) = {x ∣ (𝑚 𝜔 (dom (recs(𝐺) ↾ suc B) = suc 𝑚 x (𝐹‘((recs(𝐺) ↾ suc B)‘𝑚))) (dom (recs(𝐺) ↾ suc B) = ∅ x A))}))
3214, 31mpd 13 . . . . . . 7 ((𝐹 Fn V A 𝑉 B 𝜔) → (frec(𝐹, A)‘suc B) = {x ∣ (𝑚 𝜔 (dom (recs(𝐺) ↾ suc B) = suc 𝑚 x (𝐹‘((recs(𝐺) ↾ suc B)‘𝑚))) (dom (recs(𝐺) ↾ suc B) = ∅ x A))})
3332abeq2d 2133 . . . . . 6 ((𝐹 Fn V A 𝑉 B 𝜔) → (x (frec(𝐹, A)‘suc B) ↔ (𝑚 𝜔 (dom (recs(𝐺) ↾ suc B) = suc 𝑚 x (𝐹‘((recs(𝐺) ↾ suc B)‘𝑚))) (dom (recs(𝐺) ↾ suc B) = ∅ x A))))
342frecsuclemdm 5879 . . . . . . . . . . 11 ((𝐹 Fn V A 𝑉 B 𝜔) → dom (recs(𝐺) ↾ suc B) = suc B)
35 peano3 4222 . . . . . . . . . . . 12 (B 𝜔 → suc B ≠ ∅)
36353ad2ant3 918 . . . . . . . . . . 11 ((𝐹 Fn V A 𝑉 B 𝜔) → suc B ≠ ∅)
3734, 36eqnetrd 2206 . . . . . . . . . 10 ((𝐹 Fn V A 𝑉 B 𝜔) → dom (recs(𝐺) ↾ suc B) ≠ ∅)
3837neneqd 2204 . . . . . . . . 9 ((𝐹 Fn V A 𝑉 B 𝜔) → ¬ dom (recs(𝐺) ↾ suc B) = ∅)
3938intnanrd 830 . . . . . . . 8 ((𝐹 Fn V A 𝑉 B 𝜔) → ¬ (dom (recs(𝐺) ↾ suc B) = ∅ x A))
40 biorf 650 . . . . . . . 8 (¬ (dom (recs(𝐺) ↾ suc B) = ∅ x A) → (𝑚 𝜔 (dom (recs(𝐺) ↾ suc B) = suc 𝑚 x (𝐹‘((recs(𝐺) ↾ suc B)‘𝑚))) ↔ ((dom (recs(𝐺) ↾ suc B) = ∅ x A) 𝑚 𝜔 (dom (recs(𝐺) ↾ suc B) = suc 𝑚 x (𝐹‘((recs(𝐺) ↾ suc B)‘𝑚))))))
4139, 40syl 14 . . . . . . 7 ((𝐹 Fn V A 𝑉 B 𝜔) → (𝑚 𝜔 (dom (recs(𝐺) ↾ suc B) = suc 𝑚 x (𝐹‘((recs(𝐺) ↾ suc B)‘𝑚))) ↔ ((dom (recs(𝐺) ↾ suc B) = ∅ x A) 𝑚 𝜔 (dom (recs(𝐺) ↾ suc B) = suc 𝑚 x (𝐹‘((recs(𝐺) ↾ suc B)‘𝑚))))))
42 orcom 634 . . . . . . 7 (((dom (recs(𝐺) ↾ suc B) = ∅ x A) 𝑚 𝜔 (dom (recs(𝐺) ↾ suc B) = suc 𝑚 x (𝐹‘((recs(𝐺) ↾ suc B)‘𝑚)))) ↔ (𝑚 𝜔 (dom (recs(𝐺) ↾ suc B) = suc 𝑚 x (𝐹‘((recs(𝐺) ↾ suc B)‘𝑚))) (dom (recs(𝐺) ↾ suc B) = ∅ x A)))
4341, 42syl6bb 185 . . . . . 6 ((𝐹 Fn V A 𝑉 B 𝜔) → (𝑚 𝜔 (dom (recs(𝐺) ↾ suc B) = suc 𝑚 x (𝐹‘((recs(𝐺) ↾ suc B)‘𝑚))) ↔ (𝑚 𝜔 (dom (recs(𝐺) ↾ suc B) = suc 𝑚 x (𝐹‘((recs(𝐺) ↾ suc B)‘𝑚))) (dom (recs(𝐺) ↾ suc B) = ∅ x A))))
4434eqeq1d 2031 . . . . . . . . . 10 ((𝐹 Fn V A 𝑉 B 𝜔) → (dom (recs(𝐺) ↾ suc B) = suc 𝑚 ↔ suc B = suc 𝑚))
45 vex 2537 . . . . . . . . . . . 12 𝑚 V
46 suc11g 4195 . . . . . . . . . . . 12 ((B 𝜔 𝑚 V) → (suc B = suc 𝑚B = 𝑚))
4745, 46mpan2 403 . . . . . . . . . . 11 (B 𝜔 → (suc B = suc 𝑚B = 𝑚))
48473ad2ant3 918 . . . . . . . . . 10 ((𝐹 Fn V A 𝑉 B 𝜔) → (suc B = suc 𝑚B = 𝑚))
4944, 48bitrd 177 . . . . . . . . 9 ((𝐹 Fn V A 𝑉 B 𝜔) → (dom (recs(𝐺) ↾ suc B) = suc 𝑚B = 𝑚))
50 eqcom 2025 . . . . . . . . 9 (B = 𝑚𝑚 = B)
5149, 50syl6bb 185 . . . . . . . 8 ((𝐹 Fn V A 𝑉 B 𝜔) → (dom (recs(𝐺) ↾ suc B) = suc 𝑚𝑚 = B))
5251anbi1d 441 . . . . . . 7 ((𝐹 Fn V A 𝑉 B 𝜔) → ((dom (recs(𝐺) ↾ suc B) = suc 𝑚 x (𝐹‘((recs(𝐺) ↾ suc B)‘𝑚))) ↔ (𝑚 = B x (𝐹‘((recs(𝐺) ↾ suc B)‘𝑚)))))
5352rexbidv 2304 . . . . . 6 ((𝐹 Fn V A 𝑉 B 𝜔) → (𝑚 𝜔 (dom (recs(𝐺) ↾ suc B) = suc 𝑚 x (𝐹‘((recs(𝐺) ↾ suc B)‘𝑚))) ↔ 𝑚 𝜔 (𝑚 = B x (𝐹‘((recs(𝐺) ↾ suc B)‘𝑚)))))
5433, 43, 533bitr2d 205 . . . . 5 ((𝐹 Fn V A 𝑉 B 𝜔) → (x (frec(𝐹, A)‘suc B) ↔ 𝑚 𝜔 (𝑚 = B x (𝐹‘((recs(𝐺) ↾ suc B)‘𝑚)))))
55 fveq2 5080 . . . . . . . 8 (𝑚 = B → ((recs(𝐺) ↾ suc B)‘𝑚) = ((recs(𝐺) ↾ suc B)‘B))
5655fveq2d 5084 . . . . . . 7 (𝑚 = B → (𝐹‘((recs(𝐺) ↾ suc B)‘𝑚)) = (𝐹‘((recs(𝐺) ↾ suc B)‘B)))
5756eleq2d 2090 . . . . . 6 (𝑚 = B → (x (𝐹‘((recs(𝐺) ↾ suc B)‘𝑚)) ↔ x (𝐹‘((recs(𝐺) ↾ suc B)‘B))))
5857ceqsrexbv 2651 . . . . 5 (𝑚 𝜔 (𝑚 = B x (𝐹‘((recs(𝐺) ↾ suc B)‘𝑚))) ↔ (B 𝜔 x (𝐹‘((recs(𝐺) ↾ suc B)‘B))))
5954, 58syl6bb 185 . . . 4 ((𝐹 Fn V A 𝑉 B 𝜔) → (x (frec(𝐹, A)‘suc B) ↔ (B 𝜔 x (𝐹‘((recs(𝐺) ↾ suc B)‘B)))))
60593anibar 1063 . . 3 ((𝐹 Fn V A 𝑉 B 𝜔) → (x (frec(𝐹, A)‘suc B) ↔ x (𝐹‘((recs(𝐺) ↾ suc B)‘B))))
6160eqrdv 2021 . 2 ((𝐹 Fn V A 𝑉 B 𝜔) → (frec(𝐹, A)‘suc B) = (𝐹‘((recs(𝐺) ↾ suc B)‘B)))
622frecsuclem2 5880 . . 3 ((𝐹 Fn V A 𝑉 B 𝜔) → ((recs(𝐺) ↾ suc B)‘B) = (frec(𝐹, A)‘B))
6362fveq2d 5084 . 2 ((𝐹 Fn V A 𝑉 B 𝜔) → (𝐹‘((recs(𝐺) ↾ suc B)‘B)) = (𝐹‘(frec(𝐹, A)‘B)))
6461, 63eqtrd 2055 1 ((𝐹 Fn V A 𝑉 B 𝜔) → (frec(𝐹, A)‘suc B) = (𝐹‘(frec(𝐹, A)‘B)))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4   wa 97  wb 98   wo 616   w3a 876   = wceq 1374   wcel 1376  {cab 2009  wne 2187  wrex 2284  Vcvv 2534  c0 3203   cmpt 3771  Oncon0 4026  suc csuc 4028  𝜔com 4216  dom cdm 4248  cres 4250  Fun wfun 4800   Fn wfn 4801  cfv 4806  recscrecs 5816  freccfrec 5872
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 532  ax-in2 533  ax-io 617  ax-5 1316  ax-7 1317  ax-gen 1318  ax-ie1 1363  ax-ie2 1364  ax-8 1378  ax-10 1379  ax-11 1380  ax-i12 1381  ax-bnd 1382  ax-4 1383  ax-13 1387  ax-14 1388  ax-17 1402  ax-i9 1406  ax-ial 1411  ax-i5r 1412  ax-ext 2005  ax-coll 3825  ax-sep 3828  ax-nul 3836  ax-pow 3880  ax-pr 3897  ax-un 4096  ax-setind 4180  ax-iinf 4214
This theorem depends on definitions:  df-bi 110  df-3an 878  df-tru 1232  df-fal 1233  df-nf 1330  df-sb 1629  df-eu 1885  df-mo 1886  df-clab 2010  df-cleq 2016  df-clel 2019  df-nfc 2150  df-ne 2189  df-ral 2288  df-rex 2289  df-reu 2290  df-rab 2292  df-v 2536  df-sbc 2741  df-csb 2830  df-dif 2899  df-un 2901  df-in 2903  df-ss 2910  df-nul 3204  df-pw 3314  df-sn 3334  df-pr 3335  df-op 3337  df-uni 3534  df-int 3569  df-iun 3612  df-br 3718  df-opab 3772  df-mpt 3773  df-tr 3808  df-id 3984  df-iord 4029  df-on 4030  df-suc 4033  df-iom 4217  df-xp 4254  df-rel 4255  df-cnv 4256  df-co 4257  df-dm 4258  df-rn 4259  df-res 4260  df-ima 4261  df-iota 4771  df-fun 4808  df-fn 4809  df-f 4810  df-f1 4811  df-fo 4812  df-f1o 4813  df-fv 4814  df-recs 5817  df-frec 5873
This theorem is referenced by:  frecsuc  5882
  Copyright terms: Public domain W3C validator