![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > axcaucvglemf | GIF version |
Description: Lemma for axcaucvg 7918. Mapping to N and R yields a sequence. (Contributed by Jim Kingdon, 9-Jul-2021.) |
Ref | Expression |
---|---|
axcaucvg.n | β’ π = β© {π₯ β£ (1 β π₯ β§ βπ¦ β π₯ (π¦ + 1) β π₯)} |
axcaucvg.f | β’ (π β πΉ:πβΆβ) |
axcaucvg.cau | β’ (π β βπ β π βπ β π (π <β π β ((πΉβπ) <β ((πΉβπ) + (β©π β β (π Β· π) = 1)) β§ (πΉβπ) <β ((πΉβπ) + (β©π β β (π Β· π) = 1))))) |
axcaucvg.g | β’ πΊ = (π β N β¦ (β©π§ β R (πΉββ¨[β¨(β¨{π β£ π <Q [β¨π, 1oβ©] ~Q }, {π’ β£ [β¨π, 1oβ©] ~Q <Q π’}β© +P 1P), 1Pβ©] ~R , 0Rβ©) = β¨π§, 0Rβ©)) |
Ref | Expression |
---|---|
axcaucvglemf | β’ (π β πΊ:NβΆR) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | axcaucvg.n | . . 3 β’ π = β© {π₯ β£ (1 β π₯ β§ βπ¦ β π₯ (π¦ + 1) β π₯)} | |
2 | axcaucvg.f | . . 3 β’ (π β πΉ:πβΆβ) | |
3 | 1, 2 | axcaucvglemcl 7913 | . 2 β’ ((π β§ π β N) β (β©π§ β R (πΉββ¨[β¨(β¨{π β£ π <Q [β¨π, 1oβ©] ~Q }, {π’ β£ [β¨π, 1oβ©] ~Q <Q π’}β© +P 1P), 1Pβ©] ~R , 0Rβ©) = β¨π§, 0Rβ©) β R) |
4 | axcaucvg.g | . 2 β’ πΊ = (π β N β¦ (β©π§ β R (πΉββ¨[β¨(β¨{π β£ π <Q [β¨π, 1oβ©] ~Q }, {π’ β£ [β¨π, 1oβ©] ~Q <Q π’}β© +P 1P), 1Pβ©] ~R , 0Rβ©) = β¨π§, 0Rβ©)) | |
5 | 3, 4 | fmptd 5686 | 1 β’ (π β πΊ:NβΆR) |
Colors of variables: wff set class |
Syntax hints: β wi 4 β§ wa 104 = wceq 1364 β wcel 2160 {cab 2175 βwral 2468 β¨cop 3610 β© cint 3859 class class class wbr 4018 β¦ cmpt 4079 βΆwf 5227 βcfv 5231 β©crio 5846 (class class class)co 5891 1oc1o 6428 [cec 6551 Ncnpi 7290 ~Q ceq 7297 <Q cltq 7303 1Pc1p 7310 +P cpp 7311 ~R cer 7314 Rcnr 7315 0Rc0r 7316 βcr 7829 1c1 7831 + caddc 7833 <β cltrr 7834 Β· cmul 7835 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 615 ax-in2 616 ax-io 710 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-13 2162 ax-14 2163 ax-ext 2171 ax-coll 4133 ax-sep 4136 ax-nul 4144 ax-pow 4189 ax-pr 4224 ax-un 4448 ax-setind 4551 ax-iinf 4602 |
This theorem depends on definitions: df-bi 117 df-dc 836 df-3or 981 df-3an 982 df-tru 1367 df-fal 1370 df-nf 1472 df-sb 1774 df-eu 2041 df-mo 2042 df-clab 2176 df-cleq 2182 df-clel 2185 df-nfc 2321 df-ne 2361 df-ral 2473 df-rex 2474 df-reu 2475 df-rmo 2476 df-rab 2477 df-v 2754 df-sbc 2978 df-csb 3073 df-dif 3146 df-un 3148 df-in 3150 df-ss 3157 df-nul 3438 df-pw 3592 df-sn 3613 df-pr 3614 df-op 3616 df-uni 3825 df-int 3860 df-iun 3903 df-br 4019 df-opab 4080 df-mpt 4081 df-tr 4117 df-eprel 4304 df-id 4308 df-po 4311 df-iso 4312 df-iord 4381 df-on 4383 df-suc 4386 df-iom 4605 df-xp 4647 df-rel 4648 df-cnv 4649 df-co 4650 df-dm 4651 df-rn 4652 df-res 4653 df-ima 4654 df-iota 5193 df-fun 5233 df-fn 5234 df-f 5235 df-f1 5236 df-fo 5237 df-f1o 5238 df-fv 5239 df-riota 5847 df-ov 5894 df-oprab 5895 df-mpo 5896 df-1st 6159 df-2nd 6160 df-recs 6324 df-irdg 6389 df-1o 6435 df-2o 6436 df-oadd 6439 df-omul 6440 df-er 6553 df-ec 6555 df-qs 6559 df-ni 7322 df-pli 7323 df-mi 7324 df-lti 7325 df-plpq 7362 df-mpq 7363 df-enq 7365 df-nqqs 7366 df-plqqs 7367 df-mqqs 7368 df-1nqqs 7369 df-rq 7370 df-ltnqqs 7371 df-enq0 7442 df-nq0 7443 df-0nq0 7444 df-plq0 7445 df-mq0 7446 df-inp 7484 df-i1p 7485 df-iplp 7486 df-enr 7744 df-nr 7745 df-plr 7746 df-0r 7749 df-1r 7750 df-c 7836 df-1 7838 df-r 7840 df-add 7841 |
This theorem is referenced by: axcaucvglemcau 7916 axcaucvglemres 7917 |
Copyright terms: Public domain | W3C validator |