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

Theorem caucvgprprlemval 6786
 Description: Lemma for caucvgprpr 6810. Cauchy condition expressed in terms of classes. (Contributed by Jim Kingdon, 3-Mar-2021.)
Hypotheses
Ref Expression
caucvgprpr.f
caucvgprpr.cau
Assertion
Ref Expression
caucvgprprlemval
Distinct variable groups:   ,   ,   ,,   ,,   ,,   ,,   ,,
Allowed substitution hints:   (,,,,,)   (,)   (,,,,,)   (,,,)

Proof of Theorem caucvgprprlemval
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ltrelpi 6422 . . . . 5
21brel 4392 . . . 4
4 caucvgprpr.f . . . . 5
5 caucvgprpr.cau . . . . 5
64, 5caucvgprprlemcbv 6785 . . . 4
8 simpr 103 . . 3
9 breq1 3767 . . . . 5
10 fveq2 5178 . . . . . . 7
11 opeq1 3549 . . . . . . . . . . . . 13
1211eceq1d 6142 . . . . . . . . . . . 12
1312fveq2d 5182 . . . . . . . . . . 11
1413breq2d 3776 . . . . . . . . . 10
1514abbidv 2155 . . . . . . . . 9
1613breq1d 3774 . . . . . . . . . 10
1716abbidv 2155 . . . . . . . . 9
1815, 17opeq12d 3557 . . . . . . . 8
1918oveq2d 5528 . . . . . . 7
2010, 19breq12d 3777 . . . . . 6
2110, 18oveq12d 5530 . . . . . . 7
2221breq2d 3776 . . . . . 6
2320, 22anbi12d 442 . . . . 5
249, 23imbi12d 223 . . . 4
25 breq2 3768 . . . . 5
26 fveq2 5178 . . . . . . . 8
2726oveq1d 5527 . . . . . . 7
2827breq2d 3776 . . . . . 6
2926breq1d 3774 . . . . . 6
3028, 29anbi12d 442 . . . . 5
3125, 30imbi12d 223 . . . 4
3224, 31rspc2v 2662 . . 3
333, 7, 8, 32syl3c 57 . 2
34 breq1 3767 . . . . . . 7
3534cbvabv 2161 . . . . . 6
36 breq2 3768 . . . . . . 7
3736cbvabv 2161 . . . . . 6
3835, 37opeq12i 3554 . . . . 5
3938oveq2i 5523 . . . 4
4039breq2i 3772 . . 3
4138oveq2i 5523 . . . 4
4241breq2i 3772 . . 3
4340, 42anbi12i 433 . 2
4433, 43sylib 127 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 97   wceq 1243   wcel 1393  cab 2026  wral 2306  cop 3378   class class class wbr 3764  wf 4898  cfv 4902  (class class class)co 5512  c1o 5994  cec 6104  cnpi 6370   clti 6373   ceq 6377  crq 6382   cltq 6383  cnp 6389   cpp 6391   cltp 6393 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-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-14 1405  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022  ax-sep 3875  ax-pow 3927  ax-pr 3944 This theorem depends on definitions:  df-bi 110  df-3an 887  df-tru 1246  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-ral 2311  df-rex 2312  df-v 2559  df-un 2922  df-in 2924  df-ss 2931  df-pw 3361  df-sn 3381  df-pr 3382  df-op 3384  df-uni 3581  df-br 3765  df-opab 3819  df-xp 4351  df-cnv 4353  df-dm 4355  df-rn 4356  df-res 4357  df-ima 4358  df-iota 4867  df-fv 4910  df-ov 5515  df-ec 6108  df-lti 6405 This theorem is referenced by:  caucvgprprlemnkltj  6787  caucvgprprlemnjltk  6789  caucvgprprlemnbj  6791
 Copyright terms: Public domain W3C validator