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

Theorem pofun 4040
Description: A function preserves a partial order relation. (Contributed by Jeff Madsen, 18-Jun-2011.)
Hypotheses
Ref Expression
pofun.1  S  { <. , 
>.  |  X R Y }
pofun.2  X  Y
Assertion
Ref Expression
pofun  R  Po  X  S  Po
Distinct variable groups:   , R,   , X   , Y   ,   ,
Allowed substitution hints:   ()   ()    S(,)    X()    Y()

Proof of Theorem pofun
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nfcsb1v 2876 . . . . . . 7  F/_ [_  ]_ X
21nfel1 2185 . . . . . 6  F/ [_  ]_ X
3 csbeq1a 2854 . . . . . . 7  X  [_  ]_ X
43eleq1d 2103 . . . . . 6  X  [_  ]_ X
52, 4rspc 2644 . . . . 5  X  [_  ]_ X
65impcom 116 . . . 4  X  [_  ]_ X
7 poirr 4035 . . . . 5  R  Po  [_  ]_ X  [_  ]_ X R [_  ]_ X
8 df-br 3756 . . . . . 6  S  <. ,  >.  S
9 pofun.1 . . . . . . 7  S  { <. , 
>.  |  X R Y }
109eleq2i 2101 . . . . . 6  <. ,  >.  S  <. ,  >. 
{ <. , 
>.  |  X R Y }
11 nfcv 2175 . . . . . . . 8  F/_ R
12 nfcv 2175 . . . . . . . 8  F/_ Y
131, 11, 12nfbr 3799 . . . . . . 7  F/ [_  ]_ X R Y
14 nfv 1418 . . . . . . 7  F/
[_  ]_ X R [_  ]_ X
15 vex 2554 . . . . . . 7 
_V
163breq1d 3765 . . . . . . 7  X R Y  [_  ]_ X R Y
17 vex 2554 . . . . . . . . . 10 
_V
18 pofun.2 . . . . . . . . . 10  X  Y
1917, 12, 18csbief 2885 . . . . . . . . 9  [_  ]_ X  Y
20 csbeq1 2849 . . . . . . . . 9  [_  ]_ X 
[_  ]_ X
2119, 20syl5eqr 2083 . . . . . . . 8  Y  [_  ]_ X
2221breq2d 3767 . . . . . . 7  [_  ]_ X R Y  [_  ]_ X R
[_  ]_ X
2313, 14, 15, 15, 16, 22opelopabf 4002 . . . . . 6  <. ,  >.  { <. ,  >.  |  X R Y }  [_  ]_ X R [_  ]_ X
248, 10, 233bitri 195 . . . . 5  S  [_  ]_ X R
[_  ]_ X
257, 24sylnibr 601 . . . 4  R  Po  [_  ]_ X  S
266, 25sylan2 270 . . 3  R  Po  X  S
2726anassrs 380 . 2  R  Po  X  S
285com12 27 . . . . . 6  X  [_  ]_ X
29 nfcsb1v 2876 . . . . . . . . 9  F/_ [_  ]_ X
3029nfel1 2185 . . . . . . . 8  F/ [_  ]_ X
31 csbeq1a 2854 . . . . . . . . 9  X  [_  ]_ X
3231eleq1d 2103 . . . . . . . 8  X  [_  ]_ X
3330, 32rspc 2644 . . . . . . 7  X  [_  ]_ X
3433com12 27 . . . . . 6  X  [_  ]_ X
35 nfcsb1v 2876 . . . . . . . . 9  F/_ [_  ]_ X
3635nfel1 2185 . . . . . . . 8  F/ [_  ]_ X
37 csbeq1a 2854 . . . . . . . . 9  X  [_  ]_ X
3837eleq1d 2103 . . . . . . . 8  X  [_  ]_ X
3936, 38rspc 2644 . . . . . . 7  X  [_  ]_ X
4039com12 27 . . . . . 6  X  [_  ]_ X
4128, 34, 403anim123d 1213 . . . . 5  X  [_  ]_ X  [_  ]_ X  [_  ]_ X
4241imp 115 . . . 4  X  [_  ]_ X  [_  ]_ X  [_  ]_ X
4342adantll 445 . . 3  R  Po  X  [_  ]_ X  [_  ]_ X  [_  ]_ X
44 potr 4036 . . . . 5  R  Po  [_  ]_ X  [_  ]_ X  [_  ]_ X  [_  ]_ X R [_  ]_ X  [_  ]_ X R
[_  ]_ X  [_  ]_ X R
[_  ]_ X
45 df-br 3756 . . . . . . 7  S  <. ,  >.  S
469eleq2i 2101 . . . . . . 7  <. ,  >.  S  <. ,  >. 
{ <. , 
>.  |  X R Y }
47 nfv 1418 . . . . . . . 8  F/
[_  ]_ X R [_  ]_ X
48 vex 2554 . . . . . . . 8 
_V
49 csbeq1 2849 . . . . . . . . . 10  [_  ]_ X 
[_  ]_ X
5019, 49syl5eqr 2083 . . . . . . . . 9  Y  [_  ]_ X
5150breq2d 3767 . . . . . . . 8  [_  ]_ X R Y  [_  ]_ X R
[_  ]_ X
5213, 47, 15, 48, 16, 51opelopabf 4002 . . . . . . 7  <. ,  >.  { <. ,  >.  |  X R Y }  [_  ]_ X R [_  ]_ X
5345, 46, 523bitri 195 . . . . . 6  S  [_  ]_ X R
[_  ]_ X
54 df-br 3756 . . . . . . 7  S  <. ,  >.  S
559eleq2i 2101 . . . . . . 7  <. ,  >.  S  <. ,  >. 
{ <. , 
>.  |  X R Y }
5629, 11, 12nfbr 3799 . . . . . . . 8  F/ [_  ]_ X R Y
57 nfv 1418 . . . . . . . 8  F/
[_  ]_ X R [_  ]_ X
58 vex 2554 . . . . . . . 8 
_V
5931breq1d 3765 . . . . . . . 8  X R Y  [_  ]_ X R Y
60 csbeq1 2849 . . . . . . . . . 10  [_  ]_ X 
[_  ]_ X
6119, 60syl5eqr 2083 . . . . . . . . 9  Y  [_  ]_ X
6261breq2d 3767 . . . . . . . 8  [_  ]_ X R Y  [_  ]_ X R
[_  ]_ X
6356, 57, 48, 58, 59, 62opelopabf 4002 . . . . . . 7  <. ,  >.  { <. ,  >.  |  X R Y }  [_  ]_ X R [_  ]_ X
6454, 55, 633bitri 195 . . . . . 6  S  [_  ]_ X R
[_  ]_ X
6553, 64anbi12i 433 . . . . 5  S  S  [_  ]_ X R [_  ]_ X  [_  ]_ X R
[_  ]_ X
66 df-br 3756 . . . . . 6  S  <. ,  >.  S
679eleq2i 2101 . . . . . 6  <. ,  >.  S  <. ,  >. 
{ <. , 
>.  |  X R Y }
68 nfv 1418 . . . . . . 7  F/
[_  ]_ X R [_  ]_ X
6961breq2d 3767 . . . . . . 7  [_  ]_ X R Y  [_  ]_ X R
[_  ]_ X
7013, 68, 15, 58, 16, 69opelopabf 4002 . . . . . 6  <. ,  >.  { <. ,  >.  |  X R Y }  [_  ]_ X R [_  ]_ X
7166, 67, 703bitri 195 . . . . 5  S  [_  ]_ X R
[_  ]_ X
7244, 65, 713imtr4g 194 . . . 4  R  Po  [_  ]_ X  [_  ]_ X  [_  ]_ X  S  S  S
7372adantlr 446 . . 3  R  Po  X  [_  ]_ X  [_  ]_ X  [_  ]_ X  S  S  S
7443, 73syldan 266 . 2  R  Po  X  S  S  S
7527, 74ispod 4032 1  R  Po  X  S  Po
Colors of variables: wff set class
Syntax hints:   wn 3   wi 4   wa 97   w3a 884   wceq 1242   wcel 1390  wral 2300   [_csb 2846   <.cop 3370   class class class wbr 3755   {copab 3808    Po wpo 4022
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 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bndl 1396  ax-4 1397  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-pow 3918  ax-pr 3935
This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rex 2306  df-v 2553  df-sbc 2759  df-csb 2847  df-un 2916  df-in 2918  df-ss 2925  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-br 3756  df-opab 3810  df-po 4024
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator