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

Theorem frecsuclem3 5906
Description: Lemma for frecsuc 5907. (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 2022 . . . . . . . . . . . . 13 recs(𝐺) = recs(𝐺)
2 frecsuclem1.h . . . . . . . . . . . . . 14 𝐺 = (g V ↦ {x ∣ (𝑚 𝜔 (dom g = suc 𝑚 x (𝐹‘(g𝑚))) (dom g = ∅ x A))})
32frectfr 5900 . . . . . . . . . . . . 13 ((𝐹 Fn V A 𝑉) → y(Fun 𝐺 (𝐺y) V))
41, 3tfri1d 5871 . . . . . . . . . . . 12 ((𝐹 Fn V A 𝑉) → recs(𝐺) Fn On)
5 fnfun 4922 . . . . . . . . . . . 12 (recs(𝐺) Fn On → Fun recs(𝐺))
64, 5syl 14 . . . . . . . . . . 11 ((𝐹 Fn V A 𝑉) → Fun recs(𝐺))
763adant3 912 . . . . . . . . . 10 ((𝐹 Fn V A 𝑉 B 𝜔) → Fun recs(𝐺))
8 peano2 4245 . . . . . . . . . . 11 (B 𝜔 → suc B 𝜔)
983ad2ant3 915 . . . . . . . . . 10 ((𝐹 Fn V A 𝑉 B 𝜔) → suc B 𝜔)
10 resfunexg 5307 . . . . . . . . . 10 ((Fun recs(𝐺) suc B 𝜔) → (recs(𝐺) ↾ suc B) V)
117, 9, 10syl2anc 393 . . . . . . . . 9 ((𝐹 Fn V A 𝑉 B 𝜔) → (recs(𝐺) ↾ suc B) V)
12 simp1 892 . . . . . . . . 9 ((𝐹 Fn V A 𝑉 B 𝜔) → 𝐹 Fn V)
13 simp2 893 . . . . . . . . 9 ((𝐹 Fn V A 𝑉 B 𝜔) → A 𝑉)
1411, 12, 13frecabex 5899 . . . . . . . 8 ((𝐹 Fn V A 𝑉 B 𝜔) → {x ∣ (𝑚 𝜔 (dom (recs(𝐺) ↾ suc B) = suc 𝑚 x (𝐹‘((recs(𝐺) ↾ suc B)‘𝑚))) (dom (recs(𝐺) ↾ suc B) = ∅ x A))} V)
15 dmeq 4462 . . . . . . . . . . . . . . . . 17 (g = (recs(𝐺) ↾ suc B) → dom g = dom (recs(𝐺) ↾ suc B))
1615eqeq1d 2030 . . . . . . . . . . . . . . . 16 (g = (recs(𝐺) ↾ suc B) → (dom g = suc 𝑚 ↔ dom (recs(𝐺) ↾ suc B) = suc 𝑚))
17 fveq1 5102 . . . . . . . . . . . . . . . . . 18 (g = (recs(𝐺) ↾ suc B) → (g𝑚) = ((recs(𝐺) ↾ suc B)‘𝑚))
1817fveq2d 5107 . . . . . . . . . . . . . . . . 17 (g = (recs(𝐺) ↾ suc B) → (𝐹‘(g𝑚)) = (𝐹‘((recs(𝐺) ↾ suc B)‘𝑚)))
1918eleq2d 2089 . . . . . . . . . . . . . . . 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 2305 . . . . . . . . . . . . . 14 (g = (recs(𝐺) ↾ suc B) → (𝑚 𝜔 (dom g = suc 𝑚 x (𝐹‘(g𝑚))) ↔ 𝑚 𝜔 (dom (recs(𝐺) ↾ suc B) = suc 𝑚 x (𝐹‘((recs(𝐺) ↾ suc B)‘𝑚)))))
2215eqeq1d 2030 . . . . . . . . . . . . . . 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 694 . . . . . . . . . . . . 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 2137 . . . . . . . . . . . 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 5173 . . . . . . . . . . 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 5903 . . . . . . . . . 10 ((𝐹 Fn V A 𝑉 B 𝜔) → (frec(𝐹, A)‘suc B) = (𝐺‘(recs(𝐺) ↾ suc B)))
3029eqeq1d 2030 . . . . . . . . 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 2132 . . . . . 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 5904 . . . . . . . . . . 11 ((𝐹 Fn V A 𝑉 B 𝜔) → dom (recs(𝐺) ↾ suc B) = suc B)
35 peano3 4246 . . . . . . . . . . . 12 (B 𝜔 → suc B ≠ ∅)
36353ad2ant3 915 . . . . . . . . . . 11 ((𝐹 Fn V A 𝑉 B 𝜔) → suc B ≠ ∅)
3734, 36eqnetrd 2207 . . . . . . . . . 10 ((𝐹 Fn V A 𝑉 B 𝜔) → dom (recs(𝐺) ↾ suc B) ≠ ∅)
3837neneqd 2205 . . . . . . . . 9 ((𝐹 Fn V A 𝑉 B 𝜔) → ¬ dom (recs(𝐺) ↾ suc B) = ∅)
3938intnanrd 829 . . . . . . . 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 2030 . . . . . . . . . 10 ((𝐹 Fn V A 𝑉 B 𝜔) → (dom (recs(𝐺) ↾ suc B) = suc 𝑚 ↔ suc B = suc 𝑚))
45 vex 2538 . . . . . . . . . . . 12 𝑚 V
46 suc11g 4219 . . . . . . . . . . . 12 ((B 𝜔 𝑚 V) → (suc B = suc 𝑚B = 𝑚))
4745, 46mpan2 403 . . . . . . . . . . 11 (B 𝜔 → (suc B = suc 𝑚B = 𝑚))
48473ad2ant3 915 . . . . . . . . . 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 2024 . . . . . . . . 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 2305 . . . . . 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 5103 . . . . . . . 8 (𝑚 = B → ((recs(𝐺) ↾ suc B)‘𝑚) = ((recs(𝐺) ↾ suc B)‘B))
5655fveq2d 5107 . . . . . . 7 (𝑚 = B → (𝐹‘((recs(𝐺) ↾ suc B)‘𝑚)) = (𝐹‘((recs(𝐺) ↾ suc B)‘B)))
5756eleq2d 2089 . . . . . 6 (𝑚 = B → (x (𝐹‘((recs(𝐺) ↾ suc B)‘𝑚)) ↔ x (𝐹‘((recs(𝐺) ↾ suc B)‘B))))
5857ceqsrexbv 2652 . . . . 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 1060 . . 3 ((𝐹 Fn V A 𝑉 B 𝜔) → (x (frec(𝐹, A)‘suc B) ↔ x (𝐹‘((recs(𝐺) ↾ suc B)‘B))))
6160eqrdv 2020 . 2 ((𝐹 Fn V A 𝑉 B 𝜔) → (frec(𝐹, A)‘suc B) = (𝐹‘((recs(𝐺) ↾ suc B)‘B)))
622frecsuclem2 5905 . . 3 ((𝐹 Fn V A 𝑉 B 𝜔) → ((recs(𝐺) ↾ suc B)‘B) = (frec(𝐹, A)‘B))
6362fveq2d 5107 . 2 ((𝐹 Fn V A 𝑉 B 𝜔) → (𝐹‘((recs(𝐺) ↾ suc B)‘B)) = (𝐹‘(frec(𝐹, A)‘B)))
6461, 63eqtrd 2054 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 873   = wceq 1228   wcel 1374  {cab 2008  wne 2186  wrex 2285  Vcvv 2535  c0 3201  cmpt 3792  Oncon0 4049  suc csuc 4051  𝜔com 4240  dom cdm 4272  cres 4274  Fun wfun 4823   Fn wfn 4824  cfv 4829  recscrecs 5841  freccfrec 5897
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 1376  ax-10 1377  ax-11 1378  ax-i12 1379  ax-bnd 1380  ax-4 1381  ax-13 1385  ax-14 1386  ax-17 1400  ax-i9 1404  ax-ial 1409  ax-i5r 1410  ax-ext 2004  ax-coll 3846  ax-sep 3849  ax-nul 3857  ax-pow 3901  ax-pr 3918  ax-un 4120  ax-setind 4204  ax-iinf 4238
This theorem depends on definitions:  df-bi 110  df-3an 875  df-tru 1231  df-fal 1234  df-nf 1330  df-sb 1628  df-eu 1885  df-mo 1886  df-clab 2009  df-cleq 2015  df-clel 2018  df-nfc 2149  df-ne 2188  df-ral 2289  df-rex 2290  df-reu 2291  df-rab 2293  df-v 2537  df-sbc 2742  df-csb 2830  df-dif 2897  df-un 2899  df-in 2901  df-ss 2908  df-nul 3202  df-pw 3336  df-sn 3356  df-pr 3357  df-op 3359  df-uni 3555  df-int 3590  df-iun 3633  df-br 3739  df-opab 3793  df-mpt 3794  df-tr 3829  df-id 4004  df-iord 4052  df-on 4054  df-suc 4057  df-iom 4241  df-xp 4278  df-rel 4279  df-cnv 4280  df-co 4281  df-dm 4282  df-rn 4283  df-res 4284  df-ima 4285  df-iota 4794  df-fun 4831  df-fn 4832  df-f 4833  df-f1 4834  df-fo 4835  df-f1o 4836  df-fv 4837  df-recs 5842  df-frec 5898
This theorem is referenced by:  frecsuc  5907
  Copyright terms: Public domain W3C validator