Step |
Hyp |
Ref |
Expression |
1 |
|
wefr |
|- ( R We A -> R Fr A ) |
2 |
1
|
adantr |
|- ( ( R We A /\ R Se A ) -> R Fr A ) |
3 |
|
weso |
|- ( R We A -> R Or A ) |
4 |
|
sopo |
|- ( R Or A -> R Po A ) |
5 |
3 4
|
syl |
|- ( R We A -> R Po A ) |
6 |
5
|
adantr |
|- ( ( R We A /\ R Se A ) -> R Po A ) |
7 |
|
simpr |
|- ( ( R We A /\ R Se A ) -> R Se A ) |
8 |
2 6 7
|
3jca |
|- ( ( R We A /\ R Se A ) -> ( R Fr A /\ R Po A /\ R Se A ) ) |
9 |
|
frpomin2 |
|- ( ( ( R Fr A /\ R Po A /\ R Se A ) /\ ( B C_ A /\ B =/= (/) ) ) -> E. y e. B Pred ( R , B , y ) = (/) ) |
10 |
8 9
|
sylan |
|- ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ B =/= (/) ) ) -> E. y e. B Pred ( R , B , y ) = (/) ) |