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