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 biimtrid 
 |-  ( 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_ .<_ ) ) )