Metamath Proof Explorer


Theorem brovex

Description: A binary relation of the value of an operation given by the maps-to notation. (Contributed by Alexander van der Vekens, 21-Oct-2017)

Ref Expression
Hypotheses brovex.1
|- O = ( x e. _V , y e. _V |-> C )
brovex.2
|- ( ( V e. _V /\ E e. _V ) -> Rel ( V O E ) )
Assertion brovex
|- ( F ( V O E ) P -> ( ( V e. _V /\ E e. _V ) /\ ( F e. _V /\ P e. _V ) ) )

Proof

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 ) ) )