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 ) |