Step |
Hyp |
Ref |
Expression |
1 |
|
isprs.b |
|- B = ( Base ` K ) |
2 |
|
isprs.l |
|- .<_ = ( le ` K ) |
3 |
|
fveq2 |
|- ( f = K -> ( Base ` f ) = ( Base ` K ) ) |
4 |
|
fveq2 |
|- ( f = K -> ( le ` f ) = ( le ` K ) ) |
5 |
4
|
sbceq1d |
|- ( f = K -> ( [. ( le ` f ) / r ]. A. x e. b A. y e. b A. z e. b ( x r x /\ ( ( x r y /\ y r z ) -> x r z ) ) <-> [. ( le ` K ) / r ]. A. x e. b A. y e. b A. z e. b ( x r x /\ ( ( x r y /\ y r z ) -> x r z ) ) ) ) |
6 |
3 5
|
sbceqbid |
|- ( f = K -> ( [. ( Base ` f ) / b ]. [. ( le ` f ) / r ]. A. x e. b A. y e. b A. z e. b ( x r x /\ ( ( x r y /\ y r z ) -> x r z ) ) <-> [. ( Base ` K ) / b ]. [. ( le ` K ) / r ]. A. x e. b A. y e. b A. z e. b ( x r x /\ ( ( x r y /\ y r z ) -> x r z ) ) ) ) |
7 |
|
fvex |
|- ( Base ` K ) e. _V |
8 |
|
fvex |
|- ( le ` K ) e. _V |
9 |
|
eqtr3 |
|- ( ( b = ( Base ` K ) /\ B = ( Base ` K ) ) -> b = B ) |
10 |
1 9
|
mpan2 |
|- ( b = ( Base ` K ) -> b = B ) |
11 |
|
raleq |
|- ( b = B -> ( A. z e. b ( x r x /\ ( ( x r y /\ y r z ) -> x r z ) ) <-> A. z e. B ( x r x /\ ( ( x r y /\ y r z ) -> x r z ) ) ) ) |
12 |
11
|
raleqbi1dv |
|- ( b = B -> ( A. y e. b A. z e. b ( x r x /\ ( ( x r y /\ y r z ) -> x r z ) ) <-> A. y e. B A. z e. B ( x r x /\ ( ( x r y /\ y r z ) -> x r z ) ) ) ) |
13 |
12
|
raleqbi1dv |
|- ( b = B -> ( A. x e. b A. y e. b A. z e. b ( x r x /\ ( ( x r y /\ y r z ) -> x r z ) ) <-> A. x e. B A. y e. B A. z e. B ( x r x /\ ( ( x r y /\ y r z ) -> x r z ) ) ) ) |
14 |
10 13
|
syl |
|- ( b = ( Base ` K ) -> ( A. x e. b A. y e. b A. z e. b ( x r x /\ ( ( x r y /\ y r z ) -> x r z ) ) <-> A. x e. B A. y e. B A. z e. B ( x r x /\ ( ( x r y /\ y r z ) -> x r z ) ) ) ) |
15 |
|
eqtr3 |
|- ( ( r = ( le ` K ) /\ .<_ = ( le ` K ) ) -> r = .<_ ) |
16 |
2 15
|
mpan2 |
|- ( r = ( le ` K ) -> r = .<_ ) |
17 |
|
breq |
|- ( r = .<_ -> ( x r x <-> x .<_ x ) ) |
18 |
|
breq |
|- ( r = .<_ -> ( x r y <-> x .<_ y ) ) |
19 |
|
breq |
|- ( r = .<_ -> ( y r z <-> y .<_ z ) ) |
20 |
18 19
|
anbi12d |
|- ( r = .<_ -> ( ( x r y /\ y r z ) <-> ( x .<_ y /\ y .<_ z ) ) ) |
21 |
|
breq |
|- ( r = .<_ -> ( x r z <-> x .<_ z ) ) |
22 |
20 21
|
imbi12d |
|- ( r = .<_ -> ( ( ( x r y /\ y r z ) -> x r z ) <-> ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) ) ) |
23 |
17 22
|
anbi12d |
|- ( r = .<_ -> ( ( x r x /\ ( ( x r y /\ y r z ) -> x r z ) ) <-> ( x .<_ x /\ ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) ) ) ) |
24 |
23
|
ralbidv |
|- ( r = .<_ -> ( A. z e. B ( x r x /\ ( ( x r y /\ y r z ) -> x r z ) ) <-> A. z e. B ( x .<_ x /\ ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) ) ) ) |
25 |
24
|
2ralbidv |
|- ( r = .<_ -> ( A. x e. B A. y e. B A. z e. B ( x r x /\ ( ( x r y /\ y r z ) -> x r z ) ) <-> A. x e. B A. y e. B A. z e. B ( x .<_ x /\ ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) ) ) ) |
26 |
16 25
|
syl |
|- ( r = ( le ` K ) -> ( A. x e. B A. y e. B A. z e. B ( x r x /\ ( ( x r y /\ y r z ) -> x r z ) ) <-> A. x e. B A. y e. B A. z e. B ( x .<_ x /\ ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) ) ) ) |
27 |
14 26
|
sylan9bb |
|- ( ( b = ( Base ` K ) /\ r = ( le ` K ) ) -> ( A. x e. b A. y e. b A. z e. b ( x r x /\ ( ( x r y /\ y r z ) -> x r z ) ) <-> A. x e. B A. y e. B A. z e. B ( x .<_ x /\ ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) ) ) ) |
28 |
7 8 27
|
sbc2ie |
|- ( [. ( Base ` K ) / b ]. [. ( le ` K ) / r ]. A. x e. b A. y e. b A. z e. b ( x r x /\ ( ( x r y /\ y r z ) -> x r z ) ) <-> A. x e. B A. y e. B A. z e. B ( x .<_ x /\ ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) ) ) |
29 |
6 28
|
bitrdi |
|- ( f = K -> ( [. ( Base ` f ) / b ]. [. ( le ` f ) / r ]. A. x e. b A. y e. b A. z e. b ( x r x /\ ( ( x r y /\ y r z ) -> x r z ) ) <-> A. x e. B A. y e. B A. z e. B ( x .<_ x /\ ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) ) ) ) |
30 |
|
df-proset |
|- Proset = { f | [. ( Base ` f ) / b ]. [. ( le ` f ) / r ]. A. x e. b A. y e. b A. z e. b ( x r x /\ ( ( x r y /\ y r z ) -> x r z ) ) } |
31 |
29 30
|
elab4g |
|- ( K e. Proset <-> ( K e. _V /\ A. x e. B A. y e. B A. z e. B ( x .<_ x /\ ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) ) ) ) |