Metamath Proof Explorer

Theorem tsrss

Description: Any subset of a totally ordered set is totally ordered. (Contributed by FL, 24-Jan-2010) (Proof shortened by Mario Carneiro, 21-Nov-2013)

Ref Expression
Assertion tsrss 
|- ( R e. TosetRel -> ( R i^i ( A X. A ) ) e. TosetRel )

Proof

Step Hyp Ref Expression
1 psss 
 |-  ( R e. PosetRel -> ( R i^i ( A X. A ) ) e. PosetRel )
2 inss1 
 |-  ( R i^i ( A X. A ) ) C_ R
3 dmss 
 |-  ( ( R i^i ( A X. A ) ) C_ R -> dom ( R i^i ( A X. A ) ) C_ dom R )
4 ssralv 
 |-  ( dom ( R i^i ( A X. A ) ) C_ dom R -> ( A. x e. dom R A. y e. dom R ( x R y \/ y R x ) -> A. x e. dom ( R i^i ( A X. A ) ) A. y e. dom R ( x R y \/ y R x ) ) )
5 2 3 4 mp2b 
 |-  ( A. x e. dom R A. y e. dom R ( x R y \/ y R x ) -> A. x e. dom ( R i^i ( A X. A ) ) A. y e. dom R ( x R y \/ y R x ) )
6 ssralv 
 |-  ( dom ( R i^i ( A X. A ) ) C_ dom R -> ( A. y e. dom R ( x R y \/ y R x ) -> A. y e. dom ( R i^i ( A X. A ) ) ( x R y \/ y R x ) ) )
7 2 3 6 mp2b 
 |-  ( A. y e. dom R ( x R y \/ y R x ) -> A. y e. dom ( R i^i ( A X. A ) ) ( x R y \/ y R x ) )
8 7 ralimi 
 |-  ( A. x e. dom ( R i^i ( A X. A ) ) A. y e. dom R ( x R y \/ y R x ) -> A. x e. dom ( R i^i ( A X. A ) ) A. y e. dom ( R i^i ( A X. A ) ) ( x R y \/ y R x ) )
9 5 8 syl 
 |-  ( A. x e. dom R A. y e. dom R ( x R y \/ y R x ) -> A. x e. dom ( R i^i ( A X. A ) ) A. y e. dom ( R i^i ( A X. A ) ) ( x R y \/ y R x ) )
10 inss2 
 |-  ( R i^i ( A X. A ) ) C_ ( A X. A )
11 dmss 
 |-  ( ( R i^i ( A X. A ) ) C_ ( A X. A ) -> dom ( R i^i ( A X. A ) ) C_ dom ( A X. A ) )
12 10 11 ax-mp 
 |-  dom ( R i^i ( A X. A ) ) C_ dom ( A X. A )
13 dmxpid 
 |-  dom ( A X. A ) = A
14 12 13 sseqtri 
 |-  dom ( R i^i ( A X. A ) ) C_ A
15 14 sseli 
 |-  ( x e. dom ( R i^i ( A X. A ) ) -> x e. A )
16 14 sseli 
 |-  ( y e. dom ( R i^i ( A X. A ) ) -> y e. A )
17 brinxp 
 |-  ( ( x e. A /\ y e. A ) -> ( x R y <-> x ( R i^i ( A X. A ) ) y ) )
18 brinxp 
 |-  ( ( y e. A /\ x e. A ) -> ( y R x <-> y ( R i^i ( A X. A ) ) x ) )
19 18 ancoms 
 |-  ( ( x e. A /\ y e. A ) -> ( y R x <-> y ( R i^i ( A X. A ) ) x ) )
20 17 19 orbi12d 
 |-  ( ( x e. A /\ y e. A ) -> ( ( x R y \/ y R x ) <-> ( x ( R i^i ( A X. A ) ) y \/ y ( R i^i ( A X. A ) ) x ) ) )
21 15 16 20 syl2an 
 |-  ( ( x e. dom ( R i^i ( A X. A ) ) /\ y e. dom ( R i^i ( A X. A ) ) ) -> ( ( x R y \/ y R x ) <-> ( x ( R i^i ( A X. A ) ) y \/ y ( R i^i ( A X. A ) ) x ) ) )
22 21 ralbidva 
 |-  ( x e. dom ( R i^i ( A X. A ) ) -> ( A. y e. dom ( R i^i ( A X. A ) ) ( x R y \/ y R x ) <-> A. y e. dom ( R i^i ( A X. A ) ) ( x ( R i^i ( A X. A ) ) y \/ y ( R i^i ( A X. A ) ) x ) ) )
23 22 ralbiia 
 |-  ( A. x e. dom ( R i^i ( A X. A ) ) A. y e. dom ( R i^i ( A X. A ) ) ( x R y \/ y R x ) <-> A. x e. dom ( R i^i ( A X. A ) ) A. y e. dom ( R i^i ( A X. A ) ) ( x ( R i^i ( A X. A ) ) y \/ y ( R i^i ( A X. A ) ) x ) )
24 9 23 sylib 
 |-  ( A. x e. dom R A. y e. dom R ( x R y \/ y R x ) -> A. x e. dom ( R i^i ( A X. A ) ) A. y e. dom ( R i^i ( A X. A ) ) ( x ( R i^i ( A X. A ) ) y \/ y ( R i^i ( A X. A ) ) x ) )
25 1 24 anim12i 
 |-  ( ( R e. PosetRel /\ A. x e. dom R A. y e. dom R ( x R y \/ y R x ) ) -> ( ( R i^i ( A X. A ) ) e. PosetRel /\ A. x e. dom ( R i^i ( A X. A ) ) A. y e. dom ( R i^i ( A X. A ) ) ( x ( R i^i ( A X. A ) ) y \/ y ( R i^i ( A X. A ) ) x ) ) )
26 eqid 
 |-  dom R = dom R
27 26 istsr2 
 |-  ( R e. TosetRel <-> ( R e. PosetRel /\ A. x e. dom R A. y e. dom R ( x R y \/ y R x ) ) )
28 eqid 
 |-  dom ( R i^i ( A X. A ) ) = dom ( R i^i ( A X. A ) )
29 28 istsr2 
 |-  ( ( R i^i ( A X. A ) ) e. TosetRel <-> ( ( R i^i ( A X. A ) ) e. PosetRel /\ A. x e. dom ( R i^i ( A X. A ) ) A. y e. dom ( R i^i ( A X. A ) ) ( x ( R i^i ( A X. A ) ) y \/ y ( R i^i ( A X. A ) ) x ) ) )
30 25 27 29 3imtr4i 
 |-  ( R e. TosetRel -> ( R i^i ( A X. A ) ) e. TosetRel )