Metamath Proof Explorer


Theorem prslem

Description: Lemma for prsref and prstr . (Contributed by Mario Carneiro, 1-Feb-2015)

Ref Expression
Hypotheses isprs.b
|- B = ( Base ` K )
isprs.l
|- .<_ = ( le ` K )
Assertion prslem
|- ( ( K e. Proset /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X .<_ X /\ ( ( X .<_ Y /\ Y .<_ Z ) -> X .<_ Z ) ) )

Proof

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