Step |
Hyp |
Ref |
Expression |
1 |
|
isprs.b |
|- B = ( Base ` K ) |
2 |
|
isprs.l |
|- .<_ = ( le ` K ) |
3 |
1 2
|
isprs |
|- ( 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 ) ) ) ) |
4 |
3
|
simprbi |
|- ( K e. Proset -> A. x e. B A. y e. B A. z e. B ( x .<_ x /\ ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) ) ) |
5 |
|
breq12 |
|- ( ( x = X /\ x = X ) -> ( x .<_ x <-> X .<_ X ) ) |
6 |
5
|
anidms |
|- ( x = X -> ( x .<_ x <-> X .<_ X ) ) |
7 |
|
breq1 |
|- ( x = X -> ( x .<_ y <-> X .<_ y ) ) |
8 |
7
|
anbi1d |
|- ( x = X -> ( ( x .<_ y /\ y .<_ z ) <-> ( X .<_ y /\ y .<_ z ) ) ) |
9 |
|
breq1 |
|- ( x = X -> ( x .<_ z <-> X .<_ z ) ) |
10 |
8 9
|
imbi12d |
|- ( x = X -> ( ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) <-> ( ( X .<_ y /\ y .<_ z ) -> X .<_ z ) ) ) |
11 |
6 10
|
anbi12d |
|- ( x = X -> ( ( x .<_ x /\ ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) ) <-> ( X .<_ X /\ ( ( X .<_ y /\ y .<_ z ) -> X .<_ z ) ) ) ) |
12 |
|
breq2 |
|- ( y = Y -> ( X .<_ y <-> X .<_ Y ) ) |
13 |
|
breq1 |
|- ( y = Y -> ( y .<_ z <-> Y .<_ z ) ) |
14 |
12 13
|
anbi12d |
|- ( y = Y -> ( ( X .<_ y /\ y .<_ z ) <-> ( X .<_ Y /\ Y .<_ z ) ) ) |
15 |
14
|
imbi1d |
|- ( y = Y -> ( ( ( X .<_ y /\ y .<_ z ) -> X .<_ z ) <-> ( ( X .<_ Y /\ Y .<_ z ) -> X .<_ z ) ) ) |
16 |
15
|
anbi2d |
|- ( y = Y -> ( ( X .<_ X /\ ( ( X .<_ y /\ y .<_ z ) -> X .<_ z ) ) <-> ( X .<_ X /\ ( ( X .<_ Y /\ Y .<_ z ) -> X .<_ z ) ) ) ) |
17 |
|
breq2 |
|- ( z = Z -> ( Y .<_ z <-> Y .<_ Z ) ) |
18 |
17
|
anbi2d |
|- ( z = Z -> ( ( X .<_ Y /\ Y .<_ z ) <-> ( X .<_ Y /\ Y .<_ Z ) ) ) |
19 |
|
breq2 |
|- ( z = Z -> ( X .<_ z <-> X .<_ Z ) ) |
20 |
18 19
|
imbi12d |
|- ( z = Z -> ( ( ( X .<_ Y /\ Y .<_ z ) -> X .<_ z ) <-> ( ( X .<_ Y /\ Y .<_ Z ) -> X .<_ Z ) ) ) |
21 |
20
|
anbi2d |
|- ( z = Z -> ( ( X .<_ X /\ ( ( X .<_ Y /\ Y .<_ z ) -> X .<_ z ) ) <-> ( X .<_ X /\ ( ( X .<_ Y /\ Y .<_ Z ) -> X .<_ Z ) ) ) ) |
22 |
11 16 21
|
rspc3v |
|- ( ( X e. B /\ Y e. B /\ Z e. B ) -> ( A. x e. B A. y e. B A. z e. B ( x .<_ x /\ ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) ) -> ( X .<_ X /\ ( ( X .<_ Y /\ Y .<_ Z ) -> X .<_ Z ) ) ) ) |
23 |
4 22
|
mpan9 |
|- ( ( K e. Proset /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X .<_ X /\ ( ( X .<_ Y /\ Y .<_ Z ) -> X .<_ Z ) ) ) |