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 )