Step |
Hyp |
Ref |
Expression |
1 |
|
dirge.1 |
|- X = dom R |
2 |
|
dirdm |
|- ( R e. DirRel -> dom R = U. U. R ) |
3 |
1 2
|
syl5eq |
|- ( R e. DirRel -> X = U. U. R ) |
4 |
3
|
eleq2d |
|- ( R e. DirRel -> ( A e. X <-> A e. U. U. R ) ) |
5 |
3
|
eleq2d |
|- ( R e. DirRel -> ( B e. X <-> B e. U. U. R ) ) |
6 |
4 5
|
anbi12d |
|- ( R e. DirRel -> ( ( A e. X /\ B e. X ) <-> ( A e. U. U. R /\ B e. U. U. R ) ) ) |
7 |
|
eqid |
|- U. U. R = U. U. R |
8 |
7
|
isdir |
|- ( R e. DirRel -> ( R e. DirRel <-> ( ( Rel R /\ ( _I |` U. U. R ) C_ R ) /\ ( ( R o. R ) C_ R /\ ( U. U. R X. U. U. R ) C_ ( `' R o. R ) ) ) ) ) |
9 |
8
|
ibi |
|- ( R e. DirRel -> ( ( Rel R /\ ( _I |` U. U. R ) C_ R ) /\ ( ( R o. R ) C_ R /\ ( U. U. R X. U. U. R ) C_ ( `' R o. R ) ) ) ) |
10 |
9
|
simprrd |
|- ( R e. DirRel -> ( U. U. R X. U. U. R ) C_ ( `' R o. R ) ) |
11 |
|
codir |
|- ( ( U. U. R X. U. U. R ) C_ ( `' R o. R ) <-> A. y e. U. U. R A. z e. U. U. R E. x ( y R x /\ z R x ) ) |
12 |
10 11
|
sylib |
|- ( R e. DirRel -> A. y e. U. U. R A. z e. U. U. R E. x ( y R x /\ z R x ) ) |
13 |
|
breq1 |
|- ( y = A -> ( y R x <-> A R x ) ) |
14 |
13
|
anbi1d |
|- ( y = A -> ( ( y R x /\ z R x ) <-> ( A R x /\ z R x ) ) ) |
15 |
14
|
exbidv |
|- ( y = A -> ( E. x ( y R x /\ z R x ) <-> E. x ( A R x /\ z R x ) ) ) |
16 |
|
breq1 |
|- ( z = B -> ( z R x <-> B R x ) ) |
17 |
16
|
anbi2d |
|- ( z = B -> ( ( A R x /\ z R x ) <-> ( A R x /\ B R x ) ) ) |
18 |
17
|
exbidv |
|- ( z = B -> ( E. x ( A R x /\ z R x ) <-> E. x ( A R x /\ B R x ) ) ) |
19 |
15 18
|
rspc2v |
|- ( ( A e. U. U. R /\ B e. U. U. R ) -> ( A. y e. U. U. R A. z e. U. U. R E. x ( y R x /\ z R x ) -> E. x ( A R x /\ B R x ) ) ) |
20 |
12 19
|
syl5com |
|- ( R e. DirRel -> ( ( A e. U. U. R /\ B e. U. U. R ) -> E. x ( A R x /\ B R x ) ) ) |
21 |
6 20
|
sylbid |
|- ( R e. DirRel -> ( ( A e. X /\ B e. X ) -> E. x ( A R x /\ B R x ) ) ) |
22 |
|
reldir |
|- ( R e. DirRel -> Rel R ) |
23 |
|
relelrn |
|- ( ( Rel R /\ A R x ) -> x e. ran R ) |
24 |
22 23
|
sylan |
|- ( ( R e. DirRel /\ A R x ) -> x e. ran R ) |
25 |
24
|
ex |
|- ( R e. DirRel -> ( A R x -> x e. ran R ) ) |
26 |
|
ssun2 |
|- ran R C_ ( dom R u. ran R ) |
27 |
|
dmrnssfld |
|- ( dom R u. ran R ) C_ U. U. R |
28 |
26 27
|
sstri |
|- ran R C_ U. U. R |
29 |
28 3
|
sseqtrrid |
|- ( R e. DirRel -> ran R C_ X ) |
30 |
29
|
sseld |
|- ( R e. DirRel -> ( x e. ran R -> x e. X ) ) |
31 |
25 30
|
syld |
|- ( R e. DirRel -> ( A R x -> x e. X ) ) |
32 |
31
|
adantrd |
|- ( R e. DirRel -> ( ( A R x /\ B R x ) -> x e. X ) ) |
33 |
32
|
ancrd |
|- ( R e. DirRel -> ( ( A R x /\ B R x ) -> ( x e. X /\ ( A R x /\ B R x ) ) ) ) |
34 |
33
|
eximdv |
|- ( R e. DirRel -> ( E. x ( A R x /\ B R x ) -> E. x ( x e. X /\ ( A R x /\ B R x ) ) ) ) |
35 |
|
df-rex |
|- ( E. x e. X ( A R x /\ B R x ) <-> E. x ( x e. X /\ ( A R x /\ B R x ) ) ) |
36 |
34 35
|
syl6ibr |
|- ( R e. DirRel -> ( E. x ( A R x /\ B R x ) -> E. x e. X ( A R x /\ B R x ) ) ) |
37 |
21 36
|
syld |
|- ( R e. DirRel -> ( ( A e. X /\ B e. X ) -> E. x e. X ( A R x /\ B R x ) ) ) |
38 |
37
|
3impib |
|- ( ( R e. DirRel /\ A e. X /\ B e. X ) -> E. x e. X ( A R x /\ B R x ) ) |