Metamath Proof Explorer

Theorem pslem

Description: Lemma for psref and others. (Contributed by NM, 12-May-2008) (Revised by Mario Carneiro, 30-Apr-2015)

Ref Expression
Assertion pslem 
|- ( R e. PosetRel -> ( ( ( A R B /\ B R C ) -> A R C ) /\ ( A e. U. U. R -> A R A ) /\ ( ( A R B /\ B R A ) -> A = B ) ) )

Proof

Step Hyp Ref Expression
1 psrel 
 |-  ( R e. PosetRel -> Rel R )
2 brrelex12 
 |-  ( ( Rel R /\ A R B ) -> ( A e. _V /\ B e. _V ) )
3 1 2 sylan 
 |-  ( ( R e. PosetRel /\ A R B ) -> ( A e. _V /\ B e. _V ) )
4 brrelex2 
 |-  ( ( Rel R /\ B R C ) -> C e. _V )
5 1 4 sylan 
 |-  ( ( R e. PosetRel /\ B R C ) -> C e. _V )
6 3 5 anim12dan 
 |-  ( ( R e. PosetRel /\ ( A R B /\ B R C ) ) -> ( ( A e. _V /\ B e. _V ) /\ C e. _V ) )
7 pstr2 
 |-  ( R e. PosetRel -> ( R o. R ) C_ R )
8 cotr 
 |-  ( ( R o. R ) C_ R <-> A. x A. y A. z ( ( x R y /\ y R z ) -> x R z ) )
9 7 8 sylib 
 |-  ( R e. PosetRel -> A. x A. y A. z ( ( x R y /\ y R z ) -> x R z ) )
10 9 adantr 
 |-  ( ( R e. PosetRel /\ ( A R B /\ B R C ) ) -> A. x A. y A. z ( ( x R y /\ y R z ) -> x R z ) )
11 simpr 
 |-  ( ( R e. PosetRel /\ ( A R B /\ B R C ) ) -> ( A R B /\ B R C ) )
12 breq12 
 |-  ( ( x = A /\ y = B ) -> ( x R y <-> A R B ) )
13 12 3adant3 
 |-  ( ( x = A /\ y = B /\ z = C ) -> ( x R y <-> A R B ) )
14 breq12 
 |-  ( ( y = B /\ z = C ) -> ( y R z <-> B R C ) )
15 14 3adant1 
 |-  ( ( x = A /\ y = B /\ z = C ) -> ( y R z <-> B R C ) )
16 13 15 anbi12d 
 |-  ( ( x = A /\ y = B /\ z = C ) -> ( ( x R y /\ y R z ) <-> ( A R B /\ B R C ) ) )
17 breq12 
 |-  ( ( x = A /\ z = C ) -> ( x R z <-> A R C ) )
18 17 3adant2 
 |-  ( ( x = A /\ y = B /\ z = C ) -> ( x R z <-> A R C ) )
19 16 18 imbi12d 
 |-  ( ( x = A /\ y = B /\ z = C ) -> ( ( ( x R y /\ y R z ) -> x R z ) <-> ( ( A R B /\ B R C ) -> A R C ) ) )
20 19 spc3gv 
 |-  ( ( A e. _V /\ B e. _V /\ C e. _V ) -> ( A. x A. y A. z ( ( x R y /\ y R z ) -> x R z ) -> ( ( A R B /\ B R C ) -> A R C ) ) )
21 20 3expa 
 |-  ( ( ( A e. _V /\ B e. _V ) /\ C e. _V ) -> ( A. x A. y A. z ( ( x R y /\ y R z ) -> x R z ) -> ( ( A R B /\ B R C ) -> A R C ) ) )
22 6 10 11 21 syl3c 
 |-  ( ( R e. PosetRel /\ ( A R B /\ B R C ) ) -> A R C )
23 22 ex 
 |-  ( R e. PosetRel -> ( ( A R B /\ B R C ) -> A R C ) )
24 psref2 
 |-  ( R e. PosetRel -> ( R i^i `' R ) = ( _I |` U. U. R ) )
25 asymref2 
 |-  ( ( R i^i `' R ) = ( _I |` U. U. R ) <-> ( A. x e. U. U. R x R x /\ A. x A. y ( ( x R y /\ y R x ) -> x = y ) ) )
26 25 simplbi 
 |-  ( ( R i^i `' R ) = ( _I |` U. U. R ) -> A. x e. U. U. R x R x )
27 breq12 
 |-  ( ( x = A /\ x = A ) -> ( x R x <-> A R A ) )
28 27 anidms 
 |-  ( x = A -> ( x R x <-> A R A ) )
29 28 rspccv 
 |-  ( A. x e. U. U. R x R x -> ( A e. U. U. R -> A R A ) )
30 24 26 29 3syl 
 |-  ( R e. PosetRel -> ( A e. U. U. R -> A R A ) )
31 3 adantrr 
 |-  ( ( R e. PosetRel /\ ( A R B /\ B R A ) ) -> ( A e. _V /\ B e. _V ) )
32 25 simprbi 
 |-  ( ( R i^i `' R ) = ( _I |` U. U. R ) -> A. x A. y ( ( x R y /\ y R x ) -> x = y ) )
33 24 32 syl 
 |-  ( R e. PosetRel -> A. x A. y ( ( x R y /\ y R x ) -> x = y ) )
34 33 adantr 
 |-  ( ( R e. PosetRel /\ ( A R B /\ B R A ) ) -> A. x A. y ( ( x R y /\ y R x ) -> x = y ) )
35 simpr 
 |-  ( ( R e. PosetRel /\ ( A R B /\ B R A ) ) -> ( A R B /\ B R A ) )
36 breq12 
 |-  ( ( y = B /\ x = A ) -> ( y R x <-> B R A ) )
37 36 ancoms 
 |-  ( ( x = A /\ y = B ) -> ( y R x <-> B R A ) )
38 12 37 anbi12d 
 |-  ( ( x = A /\ y = B ) -> ( ( x R y /\ y R x ) <-> ( A R B /\ B R A ) ) )
39 eqeq12 
 |-  ( ( x = A /\ y = B ) -> ( x = y <-> A = B ) )
40 38 39 imbi12d 
 |-  ( ( x = A /\ y = B ) -> ( ( ( x R y /\ y R x ) -> x = y ) <-> ( ( A R B /\ B R A ) -> A = B ) ) )
41 40 spc2gv 
 |-  ( ( A e. _V /\ B e. _V ) -> ( A. x A. y ( ( x R y /\ y R x ) -> x = y ) -> ( ( A R B /\ B R A ) -> A = B ) ) )
42 31 34 35 41 syl3c 
 |-  ( ( R e. PosetRel /\ ( A R B /\ B R A ) ) -> A = B )
43 42 ex 
 |-  ( R e. PosetRel -> ( ( A R B /\ B R A ) -> A = B ) )
44 23 30 43 3jca 
 |-  ( R e. PosetRel -> ( ( ( A R B /\ B R C ) -> A R C ) /\ ( A e. U. U. R -> A R A ) /\ ( ( A R B /\ B R A ) -> A = B ) ) )