Metamath Proof Explorer

Theorem oduprs

Description: Being a proset is a self-dual property. (Contributed by Thierry Arnoux, 13-Sep-2018)

Ref Expression
Hypothesis oduprs.d 
|- D = ( ODual ` K )
Assertion oduprs 
|- ( K e. Proset -> D e. Proset )

Proof

Step Hyp Ref Expression
1 oduprs.d 
 |-  D = ( ODual ` K )
2 eqid 
 |-  ( Base ` K ) = ( Base ` K )
3 eqid 
 |-  ( le ` K ) = ( le ` K )
4 2 3 isprs 
 |-  ( K e. Proset <-> ( K e. _V /\ A. x e. ( Base ` K ) A. y e. ( Base ` K ) A. z e. ( Base ` K ) ( x ( le ` K ) x /\ ( ( x ( le ` K ) y /\ y ( le ` K ) z ) -> x ( le ` K ) z ) ) ) )
5 4 simprbi 
 |-  ( K e. Proset -> A. x e. ( Base ` K ) A. y e. ( Base ` K ) A. z e. ( Base ` K ) ( x ( le ` K ) x /\ ( ( x ( le ` K ) y /\ y ( le ` K ) z ) -> x ( le ` K ) z ) ) )
6 5 r19.21bi 
 |-  ( ( K e. Proset /\ x e. ( Base ` K ) ) -> A. y e. ( Base ` K ) A. z e. ( Base ` K ) ( x ( le ` K ) x /\ ( ( x ( le ` K ) y /\ y ( le ` K ) z ) -> x ( le ` K ) z ) ) )
7 6 r19.21bi 
 |-  ( ( ( K e. Proset /\ x e. ( Base ` K ) ) /\ y e. ( Base ` K ) ) -> A. z e. ( Base ` K ) ( x ( le ` K ) x /\ ( ( x ( le ` K ) y /\ y ( le ` K ) z ) -> x ( le ` K ) z ) ) )
8 7 r19.21bi 
 |-  ( ( ( ( K e. Proset /\ x e. ( Base ` K ) ) /\ y e. ( Base ` K ) ) /\ z e. ( Base ` K ) ) -> ( x ( le ` K ) x /\ ( ( x ( le ` K ) y /\ y ( le ` K ) z ) -> x ( le ` K ) z ) ) )
9 8 simpld 
 |-  ( ( ( ( K e. Proset /\ x e. ( Base ` K ) ) /\ y e. ( Base ` K ) ) /\ z e. ( Base ` K ) ) -> x ( le ` K ) x )
10 vex 
 |-  x e. _V
11 10 10 brcnv 
 |-  ( x `' ( le ` K ) x <-> x ( le ` K ) x )
12 9 11 sylibr 
 |-  ( ( ( ( K e. Proset /\ x e. ( Base ` K ) ) /\ y e. ( Base ` K ) ) /\ z e. ( Base ` K ) ) -> x `' ( le ` K ) x )
13 2 3 isprs 
 |-  ( K e. Proset <-> ( K e. _V /\ A. z e. ( Base ` K ) A. y e. ( Base ` K ) A. x e. ( Base ` K ) ( z ( le ` K ) z /\ ( ( z ( le ` K ) y /\ y ( le ` K ) x ) -> z ( le ` K ) x ) ) ) )
14 13 simprbi 
 |-  ( K e. Proset -> A. z e. ( Base ` K ) A. y e. ( Base ` K ) A. x e. ( Base ` K ) ( z ( le ` K ) z /\ ( ( z ( le ` K ) y /\ y ( le ` K ) x ) -> z ( le ` K ) x ) ) )
15 14 r19.21bi 
 |-  ( ( K e. Proset /\ z e. ( Base ` K ) ) -> A. y e. ( Base ` K ) A. x e. ( Base ` K ) ( z ( le ` K ) z /\ ( ( z ( le ` K ) y /\ y ( le ` K ) x ) -> z ( le ` K ) x ) ) )
16 15 r19.21bi 
 |-  ( ( ( K e. Proset /\ z e. ( Base ` K ) ) /\ y e. ( Base ` K ) ) -> A. x e. ( Base ` K ) ( z ( le ` K ) z /\ ( ( z ( le ` K ) y /\ y ( le ` K ) x ) -> z ( le ` K ) x ) ) )
17 16 r19.21bi 
 |-  ( ( ( ( K e. Proset /\ z e. ( Base ` K ) ) /\ y e. ( Base ` K ) ) /\ x e. ( Base ` K ) ) -> ( z ( le ` K ) z /\ ( ( z ( le ` K ) y /\ y ( le ` K ) x ) -> z ( le ` K ) x ) ) )
18 17 simprd 
 |-  ( ( ( ( K e. Proset /\ z e. ( Base ` K ) ) /\ y e. ( Base ` K ) ) /\ x e. ( Base ` K ) ) -> ( ( z ( le ` K ) y /\ y ( le ` K ) x ) -> z ( le ` K ) x ) )
19 18 an32s 
 |-  ( ( ( ( K e. Proset /\ z e. ( Base ` K ) ) /\ x e. ( Base ` K ) ) /\ y e. ( Base ` K ) ) -> ( ( z ( le ` K ) y /\ y ( le ` K ) x ) -> z ( le ` K ) x ) )
20 19 ex 
 |-  ( ( ( K e. Proset /\ z e. ( Base ` K ) ) /\ x e. ( Base ` K ) ) -> ( y e. ( Base ` K ) -> ( ( z ( le ` K ) y /\ y ( le ` K ) x ) -> z ( le ` K ) x ) ) )
21 20 an32s 
 |-  ( ( ( K e. Proset /\ x e. ( Base ` K ) ) /\ z e. ( Base ` K ) ) -> ( y e. ( Base ` K ) -> ( ( z ( le ` K ) y /\ y ( le ` K ) x ) -> z ( le ` K ) x ) ) )
22 21 imp 
 |-  ( ( ( ( K e. Proset /\ x e. ( Base ` K ) ) /\ z e. ( Base ` K ) ) /\ y e. ( Base ` K ) ) -> ( ( z ( le ` K ) y /\ y ( le ` K ) x ) -> z ( le ` K ) x ) )
23 22 an32s 
 |-  ( ( ( ( K e. Proset /\ x e. ( Base ` K ) ) /\ y e. ( Base ` K ) ) /\ z e. ( Base ` K ) ) -> ( ( z ( le ` K ) y /\ y ( le ` K ) x ) -> z ( le ` K ) x ) )
24 vex 
 |-  y e. _V
25 10 24 brcnv 
 |-  ( x `' ( le ` K ) y <-> y ( le ` K ) x )
26 vex 
 |-  z e. _V
27 24 26 brcnv 
 |-  ( y `' ( le ` K ) z <-> z ( le ` K ) y )
28 25 27 anbi12ci 
 |-  ( ( x `' ( le ` K ) y /\ y `' ( le ` K ) z ) <-> ( z ( le ` K ) y /\ y ( le ` K ) x ) )
29 10 26 brcnv 
 |-  ( x `' ( le ` K ) z <-> z ( le ` K ) x )
30 23 28 29 3imtr4g 
 |-  ( ( ( ( K e. Proset /\ x e. ( Base ` K ) ) /\ y e. ( Base ` K ) ) /\ z e. ( Base ` K ) ) -> ( ( x `' ( le ` K ) y /\ y `' ( le ` K ) z ) -> x `' ( le ` K ) z ) )
31 12 30 jca 
 |-  ( ( ( ( K e. Proset /\ x e. ( Base ` K ) ) /\ y e. ( Base ` K ) ) /\ z e. ( Base ` K ) ) -> ( x `' ( le ` K ) x /\ ( ( x `' ( le ` K ) y /\ y `' ( le ` K ) z ) -> x `' ( le ` K ) z ) ) )
32 31 ralrimiva 
 |-  ( ( ( K e. Proset /\ x e. ( Base ` K ) ) /\ y e. ( Base ` K ) ) -> A. z e. ( Base ` K ) ( x `' ( le ` K ) x /\ ( ( x `' ( le ` K ) y /\ y `' ( le ` K ) z ) -> x `' ( le ` K ) z ) ) )
33 32 ralrimiva 
 |-  ( ( K e. Proset /\ x e. ( Base ` K ) ) -> A. y e. ( Base ` K ) A. z e. ( Base ` K ) ( x `' ( le ` K ) x /\ ( ( x `' ( le ` K ) y /\ y `' ( le ` K ) z ) -> x `' ( le ` K ) z ) ) )
34 33 ralrimiva 
 |-  ( K e. Proset -> A. x e. ( Base ` K ) A. y e. ( Base ` K ) A. z e. ( Base ` K ) ( x `' ( le ` K ) x /\ ( ( x `' ( le ` K ) y /\ y `' ( le ` K ) z ) -> x `' ( le ` K ) z ) ) )
35 1 fvexi 
 |-  D e. _V
36 34 35 jctil 
 |-  ( K e. Proset -> ( D e. _V /\ A. x e. ( Base ` K ) A. y e. ( Base ` K ) A. z e. ( Base ` K ) ( x `' ( le ` K ) x /\ ( ( x `' ( le ` K ) y /\ y `' ( le ` K ) z ) -> x `' ( le ` K ) z ) ) ) )
37 1 2 odubas 
 |-  ( Base ` K ) = ( Base ` D )
38 1 3 oduleval 
 |-  `' ( le ` K ) = ( le ` D )
39 37 38 isprs 
 |-  ( D e. Proset <-> ( D e. _V /\ A. x e. ( Base ` K ) A. y e. ( Base ` K ) A. z e. ( Base ` K ) ( x `' ( le ` K ) x /\ ( ( x `' ( le ` K ) y /\ y `' ( le ` K ) z ) -> x `' ( le ` K ) z ) ) ) )
40 36 39 sylibr 
 |-  ( K e. Proset -> D e. Proset )