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

Theorem frecsuclem3 5990
 Description: Lemma for frecsuc 5991. (Contributed by Jim Kingdon, 15-Aug-2019.)
Hypothesis
Ref Expression
frecsuclem1.h
Assertion
Ref Expression
frecsuclem3 frec frec
Distinct variable groups:   ,,,,   ,,,,   ,,,,   ,,,,   ,,,
Allowed substitution hint:   ()

Proof of Theorem frecsuclem3
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 eqid 2040 . . . . . . . . . . . . 13 recs recs
2 frecsuclem1.h . . . . . . . . . . . . . 14
32frectfr 5985 . . . . . . . . . . . . 13
41, 3tfri1d 5949 . . . . . . . . . . . 12 recs
5 fnfun 4996 . . . . . . . . . . . 12 recs recs
64, 5syl 14 . . . . . . . . . . 11 recs
763adant3 924 . . . . . . . . . 10 recs
8 peano2 4318 . . . . . . . . . . 11
983ad2ant3 927 . . . . . . . . . 10
10 resfunexg 5382 . . . . . . . . . 10 recs recs
117, 9, 10syl2anc 391 . . . . . . . . 9 recs
12 simp1 904 . . . . . . . . 9
13 simp2 905 . . . . . . . . 9
1411, 12, 13frecabex 5984 . . . . . . . 8 recs recs recs
15 dmeq 4535 . . . . . . . . . . . . . . . . 17 recs recs
1615eqeq1d 2048 . . . . . . . . . . . . . . . 16 recs recs
17 fveq1 5177 . . . . . . . . . . . . . . . . . 18 recs recs
1817fveq2d 5182 . . . . . . . . . . . . . . . . 17 recs recs
1918eleq2d 2107 . . . . . . . . . . . . . . . 16 recs recs
2016, 19anbi12d 442 . . . . . . . . . . . . . . 15 recs recs recs
2120rexbidv 2327 . . . . . . . . . . . . . 14 recs recs recs
2215eqeq1d 2048 . . . . . . . . . . . . . . 15 recs recs
2322anbi1d 438 . . . . . . . . . . . . . 14 recs recs
2421, 23orbi12d 707 . . . . . . . . . . . . 13 recs recs recs recs
2524abbidv 2155 . . . . . . . . . . . 12 recs recs recs recs
2625, 2fvmptg 5248 . . . . . . . . . . 11 recs recs recs recs recs recs recs recs
2726ex 108 . . . . . . . . . 10 recs recs recs recs recs recs recs recs
2811, 27syl 14 . . . . . . . . 9 recs recs recs recs recs recs recs
292frecsuclem1 5987 . . . . . . . . . 10 frec recs
3029eqeq1d 2048 . . . . . . . . 9 frec recs recs recs recs recs recs recs
3128, 30sylibrd 158 . . . . . . . 8 recs recs recs frec recs recs recs
3214, 31mpd 13 . . . . . . 7 frec recs recs recs
3332abeq2d 2150 . . . . . 6 frec recs recs recs
342frecsuclemdm 5988 . . . . . . . . . . 11 recs
35 peano3 4319 . . . . . . . . . . . 12
36353ad2ant3 927 . . . . . . . . . . 11
3734, 36eqnetrd 2229 . . . . . . . . . 10 recs
3837neneqd 2226 . . . . . . . . 9 recs
3938intnanrd 841 . . . . . . . 8 recs
40 biorf 663 . . . . . . . 8 recs recs recs recs recs recs
4139, 40syl 14 . . . . . . 7 recs recs recs recs recs
42 orcom 647 . . . . . . 7 recs recs recs recs recs recs
4341, 42syl6bb 185 . . . . . 6 recs recs recs recs recs
4434eqeq1d 2048 . . . . . . . . . 10 recs
45 vex 2560 . . . . . . . . . . . 12
46 suc11g 4281 . . . . . . . . . . . 12
4745, 46mpan2 401 . . . . . . . . . . 11
48473ad2ant3 927 . . . . . . . . . 10
4944, 48bitrd 177 . . . . . . . . 9 recs
50 eqcom 2042 . . . . . . . . 9
5149, 50syl6bb 185 . . . . . . . 8 recs
5251anbi1d 438 . . . . . . 7 recs recs recs
5352rexbidv 2327 . . . . . 6 recs recs recs
5433, 43, 533bitr2d 205 . . . . 5 frec recs
55 fveq2 5178 . . . . . . . 8 recs recs
5655fveq2d 5182 . . . . . . 7 recs recs
5756eleq2d 2107 . . . . . 6 recs recs
5857ceqsrexbv 2675 . . . . 5 recs recs
5954, 58syl6bb 185 . . . 4 frec recs
60593anibar 1072 . . 3 frec recs
6160eqrdv 2038 . 2 frec recs
622frecsuclem2 5989 . . 3 recs frec
6362fveq2d 5182 . 2 recs frec
6461, 63eqtrd 2072 1 frec frec
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wa 97   wb 98   wo 629   w3a 885  wal 1241   wceq 1243   wcel 1393  cab 2026   wne 2204  wrex 2307  cvv 2557  c0 3224   cmpt 3818  con0 4100   csuc 4102  com 4313   cdm 4345   cres 4347   wfun 4896   wfn 4897  cfv 4902  recscrecs 5919  freccfrec 5977 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 3872  ax-sep 3875  ax-nul 3883  ax-pow 3927  ax-pr 3944  ax-un 4170  ax-setind 4262  ax-iinf 4311 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 2311  df-rex 2312  df-reu 2313  df-rab 2315  df-v 2559  df-sbc 2765  df-csb 2853  df-dif 2920  df-un 2922  df-in 2924  df-ss 2931  df-nul 3225  df-pw 3361  df-sn 3381  df-pr 3382  df-op 3384  df-uni 3581  df-int 3616  df-iun 3659  df-br 3765  df-opab 3819  df-mpt 3820  df-tr 3855  df-id 4030  df-iord 4103  df-on 4105  df-suc 4108  df-iom 4314  df-xp 4351  df-rel 4352  df-cnv 4353  df-co 4354  df-dm 4355  df-rn 4356  df-res 4357  df-ima 4358  df-iota 4867  df-fun 4904  df-fn 4905  df-f 4906  df-f1 4907  df-fo 4908  df-f1o 4909  df-fv 4910  df-recs 5920  df-frec 5978 This theorem is referenced by:  frecsuc  5991
 Copyright terms: Public domain W3C validator