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

Theorem ctssdclemn0 7048
 Description: Lemma for ctssdc 7051. The case. (Contributed by Jim Kingdon, 16-Aug-2023.)
Hypotheses
Ref Expression
ctssdclemn0.ss
ctssdclemn0.dc DECID
ctssdclemn0.f
ctssdclemn0.n0
Assertion
Ref Expression
ctssdclemn0
Distinct variable groups:   ,   ,   ,   ,
Allowed substitution hints:   (,)   ()   ()

Proof of Theorem ctssdclemn0
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ctssdclemn0.f . . . . . . . . 9
21ad2antrr 480 . . . . . . . 8
3 fof 5391 . . . . . . . 8
42, 3syl 14 . . . . . . 7
5 simpr 109 . . . . . . 7
64, 5ffvelrnd 5602 . . . . . 6
7 djulcl 6989 . . . . . 6 inl
86, 7syl 14 . . . . 5 inl
9 0lt1o 6384 . . . . . . 7
10 djurcl 6990 . . . . . . 7 inr
119, 10ax-mp 5 . . . . . 6 inr
1211a1i 9 . . . . 5 inr
13 eleq1 2220 . . . . . . 7
1413dcbid 824 . . . . . 6 DECID DECID
15 ctssdclemn0.dc . . . . . . 7 DECID
1615adantr 274 . . . . . 6 DECID
17 simpr 109 . . . . . 6
1814, 16, 17rspcdva 2821 . . . . 5 DECID
198, 12, 18ifcldadc 3534 . . . 4 inl inr
2019fmpttd 5621 . . 3 inl inr
211ad3antrrr 484 . . . . . . . . 9 inl
22 simplr 520 . . . . . . . . 9 inl
23 foelrn 5700 . . . . . . . . 9
2421, 22, 23syl2anc 409 . . . . . . . 8 inl
25 simplr 520 . . . . . . . . . . . 12 inl
2625iftrued 3512 . . . . . . . . . . 11 inl inl inr inl
27 eqid 2157 . . . . . . . . . . . 12 inl inr inl inr
28 eleq1 2220 . . . . . . . . . . . . 13
29 2fveq3 5472 . . . . . . . . . . . . 13 inl inl
3028, 29ifbieq1d 3527 . . . . . . . . . . . 12 inl inr inl inr
31 ctssdclemn0.ss . . . . . . . . . . . . . 14
3231ad5antr 488 . . . . . . . . . . . . 13 inl
3332, 25sseldd 3129 . . . . . . . . . . . 12 inl
341, 3syl 14 . . . . . . . . . . . . . . . 16
3534ad5antr 488 . . . . . . . . . . . . . . 15 inl
3635, 25ffvelrnd 5602 . . . . . . . . . . . . . 14 inl
37 djulcl 6989 . . . . . . . . . . . . . 14 inl
3836, 37syl 14 . . . . . . . . . . . . 13 inl inl
3926, 38eqeltrd 2234 . . . . . . . . . . . 12 inl inl inr
4027, 30, 33, 39fvmptd3 5560 . . . . . . . . . . 11 inl inl inr inl inr
41 simpllr 524 . . . . . . . . . . . 12 inl inl
42 simpr 109 . . . . . . . . . . . . 13 inl
4342fveq2d 5471 . . . . . . . . . . . 12 inl inl inl
4441, 43eqtrd 2190 . . . . . . . . . . 11 inl inl
4526, 40, 443eqtr4rd 2201 . . . . . . . . . 10 inl inl inr
4645ex 114 . . . . . . . . 9 inl inl inr
4746reximdva 2559 . . . . . . . 8 inl inl inr
4824, 47mpd 13 . . . . . . 7 inl inl inr
49 ssrexv 3193 . . . . . . . . 9 inl inr inl inr
5031, 49syl 14 . . . . . . . 8 inl inr inl inr
5150ad3antrrr 484 . . . . . . 7 inl inl inr inl inr
5248, 51mpd 13 . . . . . 6 inl inl inr
5352rexlimdva2 2577 . . . . 5 inl inl inr
54 peano1 4552 . . . . . . . 8
5554a1i 9 . . . . . . 7 inr
56 ctssdclemn0.n0 . . . . . . . . . 10
5756ad3antrrr 484 . . . . . . . . 9 inr
5857iffalsed 3515 . . . . . . . 8 inr inl inr inr
59 eleq1 2220 . . . . . . . . . 10
60 2fveq3 5472 . . . . . . . . . 10 inl inl
6159, 60ifbieq1d 3527 . . . . . . . . 9 inl inr inl inr
6258, 11eqeltrdi 2248 . . . . . . . . 9 inr inl inr
6327, 61, 55, 62fvmptd3 5560 . . . . . . . 8 inr inl inr inl inr
64 simpr 109 . . . . . . . . 9 inr inr
65 simplr 520 . . . . . . . . . . 11 inr
66 el1o 6381 . . . . . . . . . . 11
6765, 66sylib 121 . . . . . . . . . 10 inr
6867fveq2d 5471 . . . . . . . . 9 inr inr inr
6964, 68eqtrd 2190 . . . . . . . 8 inr inr
7058, 63, 693eqtr4rd 2201 . . . . . . 7 inr inl inr
71 fveq2 5467 . . . . . . . 8 inl inr inl inr
7271rspceeqv 2834 . . . . . . 7 inl inr inl inr
7355, 70, 72syl2anc 409 . . . . . 6 inr inl inr
7473rexlimdva2 2577 . . . . 5 inr inl inr
75 djur 7007 . . . . . . 7 inl inr
7675biimpi 119 . . . . . 6 inl inr
7776adantl 275 . . . . 5 inl inr
7853, 74, 77mpjaod 708 . . . 4 inl inr
7978ralrimiva 2530 . . 3 inl inr
80 dffo3 5613 . . 3 inl inr inl inr inl inr
8120, 79, 80sylanbrc 414 . 2 inl inr
82 omex 4551 . . . 4
8382mptex 5692 . . 3 inl inr
84 foeq1 5387 . . 3 inl inr inl inr
8583, 84spcev 2807 . 2 inl inr
8681, 85syl 14 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wa 103   wo 698  DECID wdc 820   wceq 1335  wex 1472   wcel 2128  wral 2435  wrex 2436   wss 3102  c0 3394  cif 3505   cmpt 4025  com 4548  wf 5165  wfo 5167  cfv 5169  c1o 6353   ⊔ cdju 6975  inlcinl 6983  inrcinr 6984 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-13 2130  ax-14 2131  ax-ext 2139  ax-coll 4079  ax-sep 4082  ax-nul 4090  ax-pow 4135  ax-pr 4169  ax-un 4393  ax-iinf 4546 This theorem depends on definitions:  df-bi 116  df-dc 821  df-3an 965  df-tru 1338  df-nf 1441  df-sb 1743  df-eu 2009  df-mo 2010  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-ral 2440  df-rex 2441  df-reu 2442  df-rab 2444  df-v 2714  df-sbc 2938  df-csb 3032  df-dif 3104  df-un 3106  df-in 3108  df-ss 3115  df-nul 3395  df-if 3506  df-pw 3545  df-sn 3566  df-pr 3567  df-op 3569  df-uni 3773  df-int 3808  df-iun 3851  df-br 3966  df-opab 4026  df-mpt 4027  df-tr 4063  df-id 4253  df-iord 4326  df-on 4328  df-suc 4331  df-iom 4549  df-xp 4591  df-rel 4592  df-cnv 4593  df-co 4594  df-dm 4595  df-rn 4596  df-res 4597  df-ima 4598  df-iota 5134  df-fun 5171  df-fn 5172  df-f 5173  df-f1 5174  df-fo 5175  df-f1o 5176  df-fv 5177  df-1st 6085  df-2nd 6086  df-1o 6360  df-dju 6976  df-inl 6985  df-inr 6986 This theorem is referenced by:  ctssdc  7051
 Copyright terms: Public domain W3C validator