Metamath Proof Explorer

Theorem posi

Description: Lemma for poset properties. (Contributed by NM, 11-Sep-2011)

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

Proof

Step Hyp Ref Expression
1 posi.b 
 |-  B = ( Base ` K )
2 posi.l 
 |-  .<_ = ( le ` K )
3 1 2 ispos 
 |-  ( K e. Poset <-> ( K e. _V /\ A. x e. B A. y e. B A. z e. B ( x .<_ x /\ ( ( x .<_ y /\ y .<_ x ) -> x = y ) /\ ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) ) ) )
4 3 simprbi 
 |-  ( K e. Poset -> A. x e. B A. y e. B A. z e. B ( x .<_ x /\ ( ( x .<_ y /\ y .<_ x ) -> x = y ) /\ ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) ) )
5 breq1 
 |-  ( x = X -> ( x .<_ x <-> X .<_ x ) )
6 breq2 
 |-  ( x = X -> ( X .<_ x <-> X .<_ X ) )
7 5 6 bitrd 
 |-  ( x = X -> ( x .<_ x <-> X .<_ X ) )
8 breq1 
 |-  ( x = X -> ( x .<_ y <-> X .<_ y ) )
9 breq2 
 |-  ( x = X -> ( y .<_ x <-> y .<_ X ) )
10 8 9 anbi12d 
 |-  ( x = X -> ( ( x .<_ y /\ y .<_ x ) <-> ( X .<_ y /\ y .<_ X ) ) )
11 eqeq1 
 |-  ( x = X -> ( x = y <-> X = y ) )
12 10 11 imbi12d 
 |-  ( x = X -> ( ( ( x .<_ y /\ y .<_ x ) -> x = y ) <-> ( ( X .<_ y /\ y .<_ X ) -> X = y ) ) )
13 8 anbi1d 
 |-  ( x = X -> ( ( x .<_ y /\ y .<_ z ) <-> ( X .<_ y /\ y .<_ z ) ) )
14 breq1 
 |-  ( x = X -> ( x .<_ z <-> X .<_ z ) )
15 13 14 imbi12d 
 |-  ( x = X -> ( ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) <-> ( ( X .<_ y /\ y .<_ z ) -> X .<_ z ) ) )
16 7 12 15 3anbi123d 
 |-  ( x = X -> ( ( x .<_ x /\ ( ( x .<_ y /\ y .<_ x ) -> x = y ) /\ ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) ) <-> ( X .<_ X /\ ( ( X .<_ y /\ y .<_ X ) -> X = y ) /\ ( ( X .<_ y /\ y .<_ z ) -> X .<_ z ) ) ) )
17 breq2 
 |-  ( y = Y -> ( X .<_ y <-> X .<_ Y ) )
18 breq1 
 |-  ( y = Y -> ( y .<_ X <-> Y .<_ X ) )
19 17 18 anbi12d 
 |-  ( y = Y -> ( ( X .<_ y /\ y .<_ X ) <-> ( X .<_ Y /\ Y .<_ X ) ) )
20 eqeq2 
 |-  ( y = Y -> ( X = y <-> X = Y ) )
21 19 20 imbi12d 
 |-  ( y = Y -> ( ( ( X .<_ y /\ y .<_ X ) -> X = y ) <-> ( ( X .<_ Y /\ Y .<_ X ) -> X = Y ) ) )
22 breq1 
 |-  ( y = Y -> ( y .<_ z <-> Y .<_ z ) )
23 17 22 anbi12d 
 |-  ( y = Y -> ( ( X .<_ y /\ y .<_ z ) <-> ( X .<_ Y /\ Y .<_ z ) ) )
24 23 imbi1d 
 |-  ( y = Y -> ( ( ( X .<_ y /\ y .<_ z ) -> X .<_ z ) <-> ( ( X .<_ Y /\ Y .<_ z ) -> X .<_ z ) ) )
25 21 24 3anbi23d 
 |-  ( y = Y -> ( ( X .<_ X /\ ( ( X .<_ y /\ y .<_ X ) -> X = y ) /\ ( ( X .<_ y /\ y .<_ z ) -> X .<_ z ) ) <-> ( X .<_ X /\ ( ( X .<_ Y /\ Y .<_ X ) -> X = Y ) /\ ( ( X .<_ Y /\ Y .<_ z ) -> X .<_ z ) ) ) )
26 breq2 
 |-  ( z = Z -> ( Y .<_ z <-> Y .<_ Z ) )
27 26 anbi2d 
 |-  ( z = Z -> ( ( X .<_ Y /\ Y .<_ z ) <-> ( X .<_ Y /\ Y .<_ Z ) ) )
28 breq2 
 |-  ( z = Z -> ( X .<_ z <-> X .<_ Z ) )
29 27 28 imbi12d 
 |-  ( z = Z -> ( ( ( X .<_ Y /\ Y .<_ z ) -> X .<_ z ) <-> ( ( X .<_ Y /\ Y .<_ Z ) -> X .<_ Z ) ) )
30 29 3anbi3d 
 |-  ( z = Z -> ( ( X .<_ X /\ ( ( X .<_ Y /\ Y .<_ X ) -> X = Y ) /\ ( ( X .<_ Y /\ Y .<_ z ) -> X .<_ z ) ) <-> ( X .<_ X /\ ( ( X .<_ Y /\ Y .<_ X ) -> X = Y ) /\ ( ( X .<_ Y /\ Y .<_ Z ) -> X .<_ Z ) ) ) )
31 16 25 30 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 .<_ x ) -> x = y ) /\ ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) ) -> ( X .<_ X /\ ( ( X .<_ Y /\ Y .<_ X ) -> X = Y ) /\ ( ( X .<_ Y /\ Y .<_ Z ) -> X .<_ Z ) ) ) )
32 4 31 mpan9 
 |-  ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X .<_ X /\ ( ( X .<_ Y /\ Y .<_ X ) -> X = Y ) /\ ( ( X .<_ Y /\ Y .<_ Z ) -> X .<_ Z ) ) )