Metamath Proof Explorer


Theorem pospo

Description: Write a poset structure in terms of the proper-class poset predicate (strict less than version). (Contributed by Mario Carneiro, 8-Feb-2015)

Ref Expression
Hypotheses pospo.b
|- B = ( Base ` K )
pospo.l
|- .<_ = ( le ` K )
pospo.s
|- .< = ( lt ` K )
Assertion pospo
|- ( K e. V -> ( K e. Poset <-> ( .< Po B /\ ( _I |` B ) C_ .<_ ) ) )

Proof

Step Hyp Ref Expression
1 pospo.b
 |-  B = ( Base ` K )
2 pospo.l
 |-  .<_ = ( le ` K )
3 pospo.s
 |-  .< = ( lt ` K )
4 3 pltirr
 |-  ( ( K e. Poset /\ x e. B ) -> -. x .< x )
5 1 3 plttr
 |-  ( ( K e. Poset /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x .< y /\ y .< z ) -> x .< z ) )
6 4 5 ispod
 |-  ( K e. Poset -> .< Po B )
7 relres
 |-  Rel ( _I |` B )
8 7 a1i
 |-  ( K e. Poset -> Rel ( _I |` B ) )
9 opabresid
 |-  ( _I |` B ) = { <. x , y >. | ( x e. B /\ y = x ) }
10 9 eqcomi
 |-  { <. x , y >. | ( x e. B /\ y = x ) } = ( _I |` B )
11 10 eleq2i
 |-  ( <. x , y >. e. { <. x , y >. | ( x e. B /\ y = x ) } <-> <. x , y >. e. ( _I |` B ) )
12 opabidw
 |-  ( <. x , y >. e. { <. x , y >. | ( x e. B /\ y = x ) } <-> ( x e. B /\ y = x ) )
13 11 12 bitr3i
 |-  ( <. x , y >. e. ( _I |` B ) <-> ( x e. B /\ y = x ) )
14 1 2 posref
 |-  ( ( K e. Poset /\ x e. B ) -> x .<_ x )
15 df-br
 |-  ( x .<_ y <-> <. x , y >. e. .<_ )
16 breq2
 |-  ( y = x -> ( x .<_ y <-> x .<_ x ) )
17 15 16 bitr3id
 |-  ( y = x -> ( <. x , y >. e. .<_ <-> x .<_ x ) )
18 14 17 syl5ibrcom
 |-  ( ( K e. Poset /\ x e. B ) -> ( y = x -> <. x , y >. e. .<_ ) )
19 18 expimpd
 |-  ( K e. Poset -> ( ( x e. B /\ y = x ) -> <. x , y >. e. .<_ ) )
20 13 19 syl5bi
 |-  ( K e. Poset -> ( <. x , y >. e. ( _I |` B ) -> <. x , y >. e. .<_ ) )
21 8 20 relssdv
 |-  ( K e. Poset -> ( _I |` B ) C_ .<_ )
22 6 21 jca
 |-  ( K e. Poset -> ( .< Po B /\ ( _I |` B ) C_ .<_ ) )
23 simpl
 |-  ( ( K e. V /\ ( .< Po B /\ ( _I |` B ) C_ .<_ ) ) -> K e. V )
24 1 a1i
 |-  ( ( K e. V /\ ( .< Po B /\ ( _I |` B ) C_ .<_ ) ) -> B = ( Base ` K ) )
25 2 a1i
 |-  ( ( K e. V /\ ( .< Po B /\ ( _I |` B ) C_ .<_ ) ) -> .<_ = ( le ` K ) )
26 equid
 |-  x = x
27 simpr
 |-  ( ( ( K e. V /\ ( .< Po B /\ ( _I |` B ) C_ .<_ ) ) /\ x e. B ) -> x e. B )
28 resieq
 |-  ( ( x e. B /\ x e. B ) -> ( x ( _I |` B ) x <-> x = x ) )
29 27 27 28 syl2anc
 |-  ( ( ( K e. V /\ ( .< Po B /\ ( _I |` B ) C_ .<_ ) ) /\ x e. B ) -> ( x ( _I |` B ) x <-> x = x ) )
30 26 29 mpbiri
 |-  ( ( ( K e. V /\ ( .< Po B /\ ( _I |` B ) C_ .<_ ) ) /\ x e. B ) -> x ( _I |` B ) x )
31 simplrr
 |-  ( ( ( K e. V /\ ( .< Po B /\ ( _I |` B ) C_ .<_ ) ) /\ x e. B ) -> ( _I |` B ) C_ .<_ )
32 31 ssbrd
 |-  ( ( ( K e. V /\ ( .< Po B /\ ( _I |` B ) C_ .<_ ) ) /\ x e. B ) -> ( x ( _I |` B ) x -> x .<_ x ) )
33 30 32 mpd
 |-  ( ( ( K e. V /\ ( .< Po B /\ ( _I |` B ) C_ .<_ ) ) /\ x e. B ) -> x .<_ x )
34 1 2 3 pleval2i
 |-  ( ( x e. B /\ y e. B ) -> ( x .<_ y -> ( x .< y \/ x = y ) ) )
35 34 3adant1
 |-  ( ( ( K e. V /\ ( .< Po B /\ ( _I |` B ) C_ .<_ ) ) /\ x e. B /\ y e. B ) -> ( x .<_ y -> ( x .< y \/ x = y ) ) )
36 1 2 3 pleval2i
 |-  ( ( y e. B /\ x e. B ) -> ( y .<_ x -> ( y .< x \/ y = x ) ) )
37 36 ancoms
 |-  ( ( x e. B /\ y e. B ) -> ( y .<_ x -> ( y .< x \/ y = x ) ) )
38 37 3adant1
 |-  ( ( ( K e. V /\ ( .< Po B /\ ( _I |` B ) C_ .<_ ) ) /\ x e. B /\ y e. B ) -> ( y .<_ x -> ( y .< x \/ y = x ) ) )
39 simprl
 |-  ( ( K e. V /\ ( .< Po B /\ ( _I |` B ) C_ .<_ ) ) -> .< Po B )
40 po2nr
 |-  ( ( .< Po B /\ ( x e. B /\ y e. B ) ) -> -. ( x .< y /\ y .< x ) )
41 40 3impb
 |-  ( ( .< Po B /\ x e. B /\ y e. B ) -> -. ( x .< y /\ y .< x ) )
42 39 41 syl3an1
 |-  ( ( ( K e. V /\ ( .< Po B /\ ( _I |` B ) C_ .<_ ) ) /\ x e. B /\ y e. B ) -> -. ( x .< y /\ y .< x ) )
43 42 pm2.21d
 |-  ( ( ( K e. V /\ ( .< Po B /\ ( _I |` B ) C_ .<_ ) ) /\ x e. B /\ y e. B ) -> ( ( x .< y /\ y .< x ) -> x = y ) )
44 simpl
 |-  ( ( x = y /\ y .< x ) -> x = y )
45 44 a1i
 |-  ( ( ( K e. V /\ ( .< Po B /\ ( _I |` B ) C_ .<_ ) ) /\ x e. B /\ y e. B ) -> ( ( x = y /\ y .< x ) -> x = y ) )
46 simpr
 |-  ( ( x .< y /\ y = x ) -> y = x )
47 46 equcomd
 |-  ( ( x .< y /\ y = x ) -> x = y )
48 47 a1i
 |-  ( ( ( K e. V /\ ( .< Po B /\ ( _I |` B ) C_ .<_ ) ) /\ x e. B /\ y e. B ) -> ( ( x .< y /\ y = x ) -> x = y ) )
49 simpl
 |-  ( ( x = y /\ y = x ) -> x = y )
50 49 a1i
 |-  ( ( ( K e. V /\ ( .< Po B /\ ( _I |` B ) C_ .<_ ) ) /\ x e. B /\ y e. B ) -> ( ( x = y /\ y = x ) -> x = y ) )
51 43 45 48 50 ccased
 |-  ( ( ( K e. V /\ ( .< Po B /\ ( _I |` B ) C_ .<_ ) ) /\ x e. B /\ y e. B ) -> ( ( ( x .< y \/ x = y ) /\ ( y .< x \/ y = x ) ) -> x = y ) )
52 35 38 51 syl2and
 |-  ( ( ( K e. V /\ ( .< Po B /\ ( _I |` B ) C_ .<_ ) ) /\ x e. B /\ y e. B ) -> ( ( x .<_ y /\ y .<_ x ) -> x = y ) )
53 simpr1
 |-  ( ( ( K e. V /\ ( .< Po B /\ ( _I |` B ) C_ .<_ ) ) /\ ( x e. B /\ y e. B /\ z e. B ) ) -> x e. B )
54 simpr2
 |-  ( ( ( K e. V /\ ( .< Po B /\ ( _I |` B ) C_ .<_ ) ) /\ ( x e. B /\ y e. B /\ z e. B ) ) -> y e. B )
55 53 54 34 syl2anc
 |-  ( ( ( K e. V /\ ( .< Po B /\ ( _I |` B ) C_ .<_ ) ) /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( x .<_ y -> ( x .< y \/ x = y ) ) )
56 simpr3
 |-  ( ( ( K e. V /\ ( .< Po B /\ ( _I |` B ) C_ .<_ ) ) /\ ( x e. B /\ y e. B /\ z e. B ) ) -> z e. B )
57 1 2 3 pleval2i
 |-  ( ( y e. B /\ z e. B ) -> ( y .<_ z -> ( y .< z \/ y = z ) ) )
58 54 56 57 syl2anc
 |-  ( ( ( K e. V /\ ( .< Po B /\ ( _I |` B ) C_ .<_ ) ) /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( y .<_ z -> ( y .< z \/ y = z ) ) )
59 potr
 |-  ( ( .< Po B /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x .< y /\ y .< z ) -> x .< z ) )
60 39 59 sylan
 |-  ( ( ( K e. V /\ ( .< Po B /\ ( _I |` B ) C_ .<_ ) ) /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x .< y /\ y .< z ) -> x .< z ) )
61 simpll
 |-  ( ( ( K e. V /\ ( .< Po B /\ ( _I |` B ) C_ .<_ ) ) /\ ( x e. B /\ y e. B /\ z e. B ) ) -> K e. V )
62 2 3 pltle
 |-  ( ( K e. V /\ x e. B /\ z e. B ) -> ( x .< z -> x .<_ z ) )
63 61 53 56 62 syl3anc
 |-  ( ( ( K e. V /\ ( .< Po B /\ ( _I |` B ) C_ .<_ ) ) /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( x .< z -> x .<_ z ) )
64 60 63 syld
 |-  ( ( ( K e. V /\ ( .< Po B /\ ( _I |` B ) C_ .<_ ) ) /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x .< y /\ y .< z ) -> x .<_ z ) )
65 breq1
 |-  ( x = y -> ( x .< z <-> y .< z ) )
66 65 biimpar
 |-  ( ( x = y /\ y .< z ) -> x .< z )
67 66 63 syl5
 |-  ( ( ( K e. V /\ ( .< Po B /\ ( _I |` B ) C_ .<_ ) ) /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x = y /\ y .< z ) -> x .<_ z ) )
68 breq2
 |-  ( y = z -> ( x .< y <-> x .< z ) )
69 68 biimpac
 |-  ( ( x .< y /\ y = z ) -> x .< z )
70 69 63 syl5
 |-  ( ( ( K e. V /\ ( .< Po B /\ ( _I |` B ) C_ .<_ ) ) /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x .< y /\ y = z ) -> x .<_ z ) )
71 53 33 syldan
 |-  ( ( ( K e. V /\ ( .< Po B /\ ( _I |` B ) C_ .<_ ) ) /\ ( x e. B /\ y e. B /\ z e. B ) ) -> x .<_ x )
72 eqtr
 |-  ( ( x = y /\ y = z ) -> x = z )
73 72 breq2d
 |-  ( ( x = y /\ y = z ) -> ( x .<_ x <-> x .<_ z ) )
74 71 73 syl5ibcom
 |-  ( ( ( K e. V /\ ( .< Po B /\ ( _I |` B ) C_ .<_ ) ) /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x = y /\ y = z ) -> x .<_ z ) )
75 64 67 70 74 ccased
 |-  ( ( ( K e. V /\ ( .< Po B /\ ( _I |` B ) C_ .<_ ) ) /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( ( x .< y \/ x = y ) /\ ( y .< z \/ y = z ) ) -> x .<_ z ) )
76 55 58 75 syl2and
 |-  ( ( ( K e. V /\ ( .< Po B /\ ( _I |` B ) C_ .<_ ) ) /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) )
77 23 24 25 33 52 76 isposd
 |-  ( ( K e. V /\ ( .< Po B /\ ( _I |` B ) C_ .<_ ) ) -> K e. Poset )
78 77 ex
 |-  ( K e. V -> ( ( .< Po B /\ ( _I |` B ) C_ .<_ ) -> K e. Poset ) )
79 22 78 impbid2
 |-  ( K e. V -> ( K e. Poset <-> ( .< Po B /\ ( _I |` B ) C_ .<_ ) ) )