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