Step |
Hyp |
Ref |
Expression |
1 |
|
ordtval.1 |
|- X = dom R |
2 |
|
ordtval.2 |
|- A = ran ( x e. X |-> { y e. X | -. y R x } ) |
3 |
|
ordtval.3 |
|- B = ran ( x e. X |-> { y e. X | -. x R y } ) |
4 |
|
dmexg |
|- ( R e. V -> dom R e. _V ) |
5 |
1 4
|
eqeltrid |
|- ( R e. V -> X e. _V ) |
6 |
|
unisng |
|- ( X e. _V -> U. { X } = X ) |
7 |
5 6
|
syl |
|- ( R e. V -> U. { X } = X ) |
8 |
7
|
uneq1d |
|- ( R e. V -> ( U. { X } u. U. ( A u. B ) ) = ( X u. U. ( A u. B ) ) ) |
9 |
|
ssrab2 |
|- { y e. X | -. y R x } C_ X |
10 |
5
|
adantr |
|- ( ( R e. V /\ x e. X ) -> X e. _V ) |
11 |
|
elpw2g |
|- ( X e. _V -> ( { y e. X | -. y R x } e. ~P X <-> { y e. X | -. y R x } C_ X ) ) |
12 |
10 11
|
syl |
|- ( ( R e. V /\ x e. X ) -> ( { y e. X | -. y R x } e. ~P X <-> { y e. X | -. y R x } C_ X ) ) |
13 |
9 12
|
mpbiri |
|- ( ( R e. V /\ x e. X ) -> { y e. X | -. y R x } e. ~P X ) |
14 |
13
|
fmpttd |
|- ( R e. V -> ( x e. X |-> { y e. X | -. y R x } ) : X --> ~P X ) |
15 |
14
|
frnd |
|- ( R e. V -> ran ( x e. X |-> { y e. X | -. y R x } ) C_ ~P X ) |
16 |
2 15
|
eqsstrid |
|- ( R e. V -> A C_ ~P X ) |
17 |
|
ssrab2 |
|- { y e. X | -. x R y } C_ X |
18 |
|
elpw2g |
|- ( X e. _V -> ( { y e. X | -. x R y } e. ~P X <-> { y e. X | -. x R y } C_ X ) ) |
19 |
10 18
|
syl |
|- ( ( R e. V /\ x e. X ) -> ( { y e. X | -. x R y } e. ~P X <-> { y e. X | -. x R y } C_ X ) ) |
20 |
17 19
|
mpbiri |
|- ( ( R e. V /\ x e. X ) -> { y e. X | -. x R y } e. ~P X ) |
21 |
20
|
fmpttd |
|- ( R e. V -> ( x e. X |-> { y e. X | -. x R y } ) : X --> ~P X ) |
22 |
21
|
frnd |
|- ( R e. V -> ran ( x e. X |-> { y e. X | -. x R y } ) C_ ~P X ) |
23 |
3 22
|
eqsstrid |
|- ( R e. V -> B C_ ~P X ) |
24 |
16 23
|
unssd |
|- ( R e. V -> ( A u. B ) C_ ~P X ) |
25 |
|
sspwuni |
|- ( ( A u. B ) C_ ~P X <-> U. ( A u. B ) C_ X ) |
26 |
24 25
|
sylib |
|- ( R e. V -> U. ( A u. B ) C_ X ) |
27 |
|
ssequn2 |
|- ( U. ( A u. B ) C_ X <-> ( X u. U. ( A u. B ) ) = X ) |
28 |
26 27
|
sylib |
|- ( R e. V -> ( X u. U. ( A u. B ) ) = X ) |
29 |
8 28
|
eqtr2d |
|- ( R e. V -> X = ( U. { X } u. U. ( A u. B ) ) ) |
30 |
|
uniun |
|- U. ( { X } u. ( A u. B ) ) = ( U. { X } u. U. ( A u. B ) ) |
31 |
29 30
|
eqtr4di |
|- ( R e. V -> X = U. ( { X } u. ( A u. B ) ) ) |