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