This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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