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∈V,y∈V⟼C
brovex.2 ⊢V∈V∧E∈V→Rel⁡VOE
Assertion brovex ⊢FVOEP→V∈V∧E∈V∧F∈V∧P∈V

Proof

Step Hyp Ref Expression
1 brovex.1 ⊢O=x∈V,y∈V⟼C
2 brovex.2 ⊢V∈V∧E∈V→Rel⁡VOE
3 df-br ⊢FVOEP↔FP∈VOE
4 ne0i ⊢FP∈VOE→VOE≠∅
5 1 mpondm0 ⊢¬V∈V∧E∈V→VOE=∅
6 5 necon1ai ⊢VOE≠∅→V∈V∧E∈V
7 brrelex12 ⊢Rel⁡VOE∧FVOEP→F∈V∧P∈V
8 2 7 sylan ⊢V∈V∧E∈V∧FVOEP→F∈V∧P∈V
9 id ⊢V∈V∧E∈V∧F∈V∧P∈V→V∈V∧E∈V∧F∈V∧P∈V
10 8 9 syldan ⊢V∈V∧E∈V∧FVOEP→V∈V∧E∈V∧F∈V∧P∈V
11 10 ex ⊢V∈V∧E∈V→FVOEP→V∈V∧E∈V∧F∈V∧P∈V
12 4 6 11 3syl ⊢FP∈VOE→FVOEP→V∈V∧E∈V∧F∈V∧P∈V
13 3 12 sylbi ⊢FVOEP→FVOEP→V∈V∧E∈V∧F∈V∧P∈V
14 13 pm2.43i ⊢FVOEP→V∈V∧E∈V∧F∈V∧P∈V