Step |
Hyp |
Ref |
Expression |
1 |
|
wefr |
|- ( R We A -> R Fr A ) |
2 |
|
fri |
|- ( ( ( B e. V /\ R Fr A ) /\ ( B C_ A /\ B =/= (/) ) ) -> E. x e. B A. y e. B -. y R x ) |
3 |
2
|
exp32 |
|- ( ( B e. V /\ R Fr A ) -> ( B C_ A -> ( B =/= (/) -> E. x e. B A. y e. B -. y R x ) ) ) |
4 |
3
|
expcom |
|- ( R Fr A -> ( B e. V -> ( B C_ A -> ( B =/= (/) -> E. x e. B A. y e. B -. y R x ) ) ) ) |
5 |
4
|
3imp2 |
|- ( ( R Fr A /\ ( B e. V /\ B C_ A /\ B =/= (/) ) ) -> E. x e. B A. y e. B -. y R x ) |
6 |
1 5
|
sylan |
|- ( ( R We A /\ ( B e. V /\ B C_ A /\ B =/= (/) ) ) -> E. x e. B A. y e. B -. y R x ) |
7 |
|
weso |
|- ( R We A -> R Or A ) |
8 |
|
soss |
|- ( B C_ A -> ( R Or A -> R Or B ) ) |
9 |
7 8
|
mpan9 |
|- ( ( R We A /\ B C_ A ) -> R Or B ) |
10 |
|
somo |
|- ( R Or B -> E* x e. B A. y e. B -. y R x ) |
11 |
9 10
|
syl |
|- ( ( R We A /\ B C_ A ) -> E* x e. B A. y e. B -. y R x ) |
12 |
11
|
3ad2antr2 |
|- ( ( R We A /\ ( B e. V /\ B C_ A /\ B =/= (/) ) ) -> E* x e. B A. y e. B -. y R x ) |
13 |
|
reu5 |
|- ( E! x e. B A. y e. B -. y R x <-> ( E. x e. B A. y e. B -. y R x /\ E* x e. B A. y e. B -. y R x ) ) |
14 |
6 12 13
|
sylanbrc |
|- ( ( R We A /\ ( B e. V /\ B C_ A /\ B =/= (/) ) ) -> E! x e. B A. y e. B -. y R x ) |