Metamath Proof Explorer

Theorem psss

Description: Any subset of a partially ordered set is partially ordered. (Contributed by FL, 24-Jan-2010)

Ref Expression
Assertion psss 
|- ( R e. PosetRel -> ( R i^i ( A X. A ) ) e. PosetRel )

Proof

Step Hyp Ref Expression
1 inss1 
 |-  ( R i^i ( A X. A ) ) C_ R
2 psrel 
 |-  ( R e. PosetRel -> Rel R )
3 relss 
 |-  ( ( R i^i ( A X. A ) ) C_ R -> ( Rel R -> Rel ( R i^i ( A X. A ) ) ) )
4 1 2 3 mpsyl 
 |-  ( R e. PosetRel -> Rel ( R i^i ( A X. A ) ) )
5 pstr2 
 |-  ( R e. PosetRel -> ( R o. R ) C_ R )
6 trinxp 
 |-  ( ( R o. R ) C_ R -> ( ( R i^i ( A X. A ) ) o. ( R i^i ( A X. A ) ) ) C_ ( R i^i ( A X. A ) ) )
7 5 6 syl 
 |-  ( R e. PosetRel -> ( ( R i^i ( A X. A ) ) o. ( R i^i ( A X. A ) ) ) C_ ( R i^i ( A X. A ) ) )
8 uniin 
 |-  U. ( R i^i ( A X. A ) ) C_ ( U. R i^i U. ( A X. A ) )
9 8 unissi 
 |-  U. U. ( R i^i ( A X. A ) ) C_ U. ( U. R i^i U. ( A X. A ) )
10 uniin 
 |-  U. ( U. R i^i U. ( A X. A ) ) C_ ( U. U. R i^i U. U. ( A X. A ) )
11 9 10 sstri 
 |-  U. U. ( R i^i ( A X. A ) ) C_ ( U. U. R i^i U. U. ( A X. A ) )
12 elin 
 |-  ( x e. ( U. U. R i^i U. U. ( A X. A ) ) <-> ( x e. U. U. R /\ x e. U. U. ( A X. A ) ) )
13 unixpid 
 |-  U. U. ( A X. A ) = A
14 13 eleq2i 
 |-  ( x e. U. U. ( A X. A ) <-> x e. A )
15 simprr 
 |-  ( ( R e. PosetRel /\ ( x e. U. U. R /\ x e. A ) ) -> x e. A )
16 psdmrn 
 |-  ( R e. PosetRel -> ( dom R = U. U. R /\ ran R = U. U. R ) )
17 16 simpld 
 |-  ( R e. PosetRel -> dom R = U. U. R )
18 17 eleq2d 
 |-  ( R e. PosetRel -> ( x e. dom R <-> x e. U. U. R ) )
19 18 biimpar 
 |-  ( ( R e. PosetRel /\ x e. U. U. R ) -> x e. dom R )
20 eqid 
 |-  dom R = dom R
21 20 psref 
 |-  ( ( R e. PosetRel /\ x e. dom R ) -> x R x )
22 19 21 syldan 
 |-  ( ( R e. PosetRel /\ x e. U. U. R ) -> x R x )
23 22 adantrr 
 |-  ( ( R e. PosetRel /\ ( x e. U. U. R /\ x e. A ) ) -> x R x )
24 brinxp2 
 |-  ( x ( R i^i ( A X. A ) ) x <-> ( ( x e. A /\ x e. A ) /\ x R x ) )
25 15 15 23 24 syl21anbrc 
 |-  ( ( R e. PosetRel /\ ( x e. U. U. R /\ x e. A ) ) -> x ( R i^i ( A X. A ) ) x )
26 25 expr 
 |-  ( ( R e. PosetRel /\ x e. U. U. R ) -> ( x e. A -> x ( R i^i ( A X. A ) ) x ) )
27 14 26 syl5bi 
 |-  ( ( R e. PosetRel /\ x e. U. U. R ) -> ( x e. U. U. ( A X. A ) -> x ( R i^i ( A X. A ) ) x ) )
28 27 expimpd 
 |-  ( R e. PosetRel -> ( ( x e. U. U. R /\ x e. U. U. ( A X. A ) ) -> x ( R i^i ( A X. A ) ) x ) )
29 12 28 syl5bi 
 |-  ( R e. PosetRel -> ( x e. ( U. U. R i^i U. U. ( A X. A ) ) -> x ( R i^i ( A X. A ) ) x ) )
30 29 ralrimiv 
 |-  ( R e. PosetRel -> A. x e. ( U. U. R i^i U. U. ( A X. A ) ) x ( R i^i ( A X. A ) ) x )
31 ssralv 
 |-  ( U. U. ( R i^i ( A X. A ) ) C_ ( U. U. R i^i U. U. ( A X. A ) ) -> ( A. x e. ( U. U. R i^i U. U. ( A X. A ) ) x ( R i^i ( A X. A ) ) x -> A. x e. U. U. ( R i^i ( A X. A ) ) x ( R i^i ( A X. A ) ) x ) )
32 11 30 31 mpsyl 
 |-  ( R e. PosetRel -> A. x e. U. U. ( R i^i ( A X. A ) ) x ( R i^i ( A X. A ) ) x )
33 1 ssbri 
 |-  ( x ( R i^i ( A X. A ) ) y -> x R y )
34 1 ssbri 
 |-  ( y ( R i^i ( A X. A ) ) x -> y R x )
35 psasym 
 |-  ( ( R e. PosetRel /\ x R y /\ y R x ) -> x = y )
36 35 3expib 
 |-  ( R e. PosetRel -> ( ( x R y /\ y R x ) -> x = y ) )
37 33 34 36 syl2ani 
 |-  ( R e. PosetRel -> ( ( x ( R i^i ( A X. A ) ) y /\ y ( R i^i ( A X. A ) ) x ) -> x = y ) )
38 37 alrimivv 
 |-  ( R e. PosetRel -> A. x A. y ( ( x ( R i^i ( A X. A ) ) y /\ y ( R i^i ( A X. A ) ) x ) -> x = y ) )
39 asymref2 
 |-  ( ( ( R i^i ( A X. A ) ) i^i `' ( R i^i ( A X. A ) ) ) = ( _I |` U. U. ( R i^i ( A X. A ) ) ) <-> ( A. x e. U. U. ( R i^i ( A X. A ) ) x ( R i^i ( A X. A ) ) x /\ A. x A. y ( ( x ( R i^i ( A X. A ) ) y /\ y ( R i^i ( A X. A ) ) x ) -> x = y ) ) )
40 32 38 39 sylanbrc 
 |-  ( R e. PosetRel -> ( ( R i^i ( A X. A ) ) i^i `' ( R i^i ( A X. A ) ) ) = ( _I |` U. U. ( R i^i ( A X. A ) ) ) )
41 inex1g 
 |-  ( R e. PosetRel -> ( R i^i ( A X. A ) ) e. _V )
42 isps 
 |-  ( ( R i^i ( A X. A ) ) e. _V -> ( ( R i^i ( A X. A ) ) e. PosetRel <-> ( Rel ( R i^i ( A X. A ) ) /\ ( ( R i^i ( A X. A ) ) o. ( R i^i ( A X. A ) ) ) C_ ( R i^i ( A X. A ) ) /\ ( ( R i^i ( A X. A ) ) i^i `' ( R i^i ( A X. A ) ) ) = ( _I |` U. U. ( R i^i ( A X. A ) ) ) ) ) )
43 41 42 syl 
 |-  ( R e. PosetRel -> ( ( R i^i ( A X. A ) ) e. PosetRel <-> ( Rel ( R i^i ( A X. A ) ) /\ ( ( R i^i ( A X. A ) ) o. ( R i^i ( A X. A ) ) ) C_ ( R i^i ( A X. A ) ) /\ ( ( R i^i ( A X. A ) ) i^i `' ( R i^i ( A X. A ) ) ) = ( _I |` U. U. ( R i^i ( A X. A ) ) ) ) ) )
44 4 7 40 43 mpbir3and 
 |-  ( R e. PosetRel -> ( R i^i ( A X. A ) ) e. PosetRel )