Metamath Proof Explorer

Theorem tsrdir

Description: A totally ordered set is a directed set. (Contributed by Jeff Hankins, 25-Nov-2009) (Revised by Mario Carneiro, 22-Nov-2013)

Ref Expression
Assertion tsrdir 
|- ( A e. TosetRel -> A e. DirRel )

Proof

Step Hyp Ref Expression
1 tsrps 
 |-  ( A e. TosetRel -> A e. PosetRel )
2 psrel 
 |-  ( A e. PosetRel -> Rel A )
3 1 2 syl 
 |-  ( A e. TosetRel -> Rel A )
4 psref2 
 |-  ( A e. PosetRel -> ( A i^i `' A ) = ( _I |` U. U. A ) )
5 inss1 
 |-  ( A i^i `' A ) C_ A
6 4 5 eqsstrrdi 
 |-  ( A e. PosetRel -> ( _I |` U. U. A ) C_ A )
7 1 6 syl 
 |-  ( A e. TosetRel -> ( _I |` U. U. A ) C_ A )
8 3 7 jca 
 |-  ( A e. TosetRel -> ( Rel A /\ ( _I |` U. U. A ) C_ A ) )
9 pstr2 
 |-  ( A e. PosetRel -> ( A o. A ) C_ A )
10 1 9 syl 
 |-  ( A e. TosetRel -> ( A o. A ) C_ A )
11 psdmrn 
 |-  ( A e. PosetRel -> ( dom A = U. U. A /\ ran A = U. U. A ) )
12 1 11 syl 
 |-  ( A e. TosetRel -> ( dom A = U. U. A /\ ran A = U. U. A ) )
13 12 simpld 
 |-  ( A e. TosetRel -> dom A = U. U. A )
14 13 sqxpeqd 
 |-  ( A e. TosetRel -> ( dom A X. dom A ) = ( U. U. A X. U. U. A ) )
15 eqid 
 |-  dom A = dom A
16 15 istsr 
 |-  ( A e. TosetRel <-> ( A e. PosetRel /\ ( dom A X. dom A ) C_ ( A u. `' A ) ) )
17 16 simprbi 
 |-  ( A e. TosetRel -> ( dom A X. dom A ) C_ ( A u. `' A ) )
18 relcoi2 
 |-  ( Rel A -> ( ( _I |` U. U. A ) o. A ) = A )
19 3 18 syl 
 |-  ( A e. TosetRel -> ( ( _I |` U. U. A ) o. A ) = A )
20 cnvresid 
 |-  `' ( _I |` U. U. A ) = ( _I |` U. U. A )
21 cnvss 
 |-  ( ( _I |` U. U. A ) C_ A -> `' ( _I |` U. U. A ) C_ `' A )
22 7 21 syl 
 |-  ( A e. TosetRel -> `' ( _I |` U. U. A ) C_ `' A )
23 20 22 eqsstrrid 
 |-  ( A e. TosetRel -> ( _I |` U. U. A ) C_ `' A )
24 coss1 
 |-  ( ( _I |` U. U. A ) C_ `' A -> ( ( _I |` U. U. A ) o. A ) C_ ( `' A o. A ) )
25 23 24 syl 
 |-  ( A e. TosetRel -> ( ( _I |` U. U. A ) o. A ) C_ ( `' A o. A ) )
26 19 25 eqsstrrd 
 |-  ( A e. TosetRel -> A C_ ( `' A o. A ) )
27 relcnv 
 |-  Rel `' A
28 relcoi1 
 |-  ( Rel `' A -> ( `' A o. ( _I |` U. U. `' A ) ) = `' A )
29 27 28 ax-mp 
 |-  ( `' A o. ( _I |` U. U. `' A ) ) = `' A
30 relcnvfld 
 |-  ( Rel A -> U. U. A = U. U. `' A )
31 3 30 syl 
 |-  ( A e. TosetRel -> U. U. A = U. U. `' A )
32 31 reseq2d 
 |-  ( A e. TosetRel -> ( _I |` U. U. A ) = ( _I |` U. U. `' A ) )
33 32 7 eqsstrrd 
 |-  ( A e. TosetRel -> ( _I |` U. U. `' A ) C_ A )
34 coss2 
 |-  ( ( _I |` U. U. `' A ) C_ A -> ( `' A o. ( _I |` U. U. `' A ) ) C_ ( `' A o. A ) )
35 33 34 syl 
 |-  ( A e. TosetRel -> ( `' A o. ( _I |` U. U. `' A ) ) C_ ( `' A o. A ) )
36 29 35 eqsstrrid 
 |-  ( A e. TosetRel -> `' A C_ ( `' A o. A ) )
37 26 36 unssd 
 |-  ( A e. TosetRel -> ( A u. `' A ) C_ ( `' A o. A ) )
38 17 37 sstrd 
 |-  ( A e. TosetRel -> ( dom A X. dom A ) C_ ( `' A o. A ) )
39 14 38 eqsstrrd 
 |-  ( A e. TosetRel -> ( U. U. A X. U. U. A ) C_ ( `' A o. A ) )
40 10 39 jca 
 |-  ( A e. TosetRel -> ( ( A o. A ) C_ A /\ ( U. U. A X. U. U. A ) C_ ( `' A o. A ) ) )
41 eqid 
 |-  U. U. A = U. U. A
42 41 isdir 
 |-  ( A e. TosetRel -> ( A e. DirRel <-> ( ( Rel A /\ ( _I |` U. U. A ) C_ A ) /\ ( ( A o. A ) C_ A /\ ( U. U. A X. U. U. A ) C_ ( `' A o. A ) ) ) ) )
43 8 40 42 mpbir2and 
 |-  ( A e. TosetRel -> A e. DirRel )