Step |
Hyp |
Ref |
Expression |
1 |
|
brovex.1 |
|- O = ( x e. _V , y e. _V |-> C ) |
2 |
|
brovex.2 |
|- ( ( V e. _V /\ E e. _V ) -> Rel ( V O E ) ) |
3 |
|
df-br |
|- ( F ( V O E ) P <-> <. F , P >. e. ( V O E ) ) |
4 |
|
ne0i |
|- ( <. F , P >. e. ( V O E ) -> ( V O E ) =/= (/) ) |
5 |
1
|
mpondm0 |
|- ( -. ( V e. _V /\ E e. _V ) -> ( V O E ) = (/) ) |
6 |
5
|
necon1ai |
|- ( ( V O E ) =/= (/) -> ( V e. _V /\ E e. _V ) ) |
7 |
|
brrelex12 |
|- ( ( Rel ( V O E ) /\ F ( V O E ) P ) -> ( F e. _V /\ P e. _V ) ) |
8 |
2 7
|
sylan |
|- ( ( ( V e. _V /\ E e. _V ) /\ F ( V O E ) P ) -> ( F e. _V /\ P e. _V ) ) |
9 |
|
id |
|- ( ( ( V e. _V /\ E e. _V ) /\ ( F e. _V /\ P e. _V ) ) -> ( ( V e. _V /\ E e. _V ) /\ ( F e. _V /\ P e. _V ) ) ) |
10 |
8 9
|
syldan |
|- ( ( ( V e. _V /\ E e. _V ) /\ F ( V O E ) P ) -> ( ( V e. _V /\ E e. _V ) /\ ( F e. _V /\ P e. _V ) ) ) |
11 |
10
|
ex |
|- ( ( V e. _V /\ E e. _V ) -> ( F ( V O E ) P -> ( ( V e. _V /\ E e. _V ) /\ ( F e. _V /\ P e. _V ) ) ) ) |
12 |
4 6 11
|
3syl |
|- ( <. F , P >. e. ( V O E ) -> ( F ( V O E ) P -> ( ( V e. _V /\ E e. _V ) /\ ( F e. _V /\ P e. _V ) ) ) ) |
13 |
3 12
|
sylbi |
|- ( F ( V O E ) P -> ( F ( V O E ) P -> ( ( V e. _V /\ E e. _V ) /\ ( F e. _V /\ P e. _V ) ) ) ) |
14 |
13
|
pm2.43i |
|- ( F ( V O E ) P -> ( ( V e. _V /\ E e. _V ) /\ ( F e. _V /\ P e. _V ) ) ) |