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 ⁡ V O E
Assertion brovex ⊢ F V O E P → 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 ⁡ V O E
3 df-br ⊢ F V O E P ↔ F P ∈ V O E
4 ne0i ⊢ F P ∈ V O E → V O E ≠ ∅
5 1 mpondm0 ⊢ ¬ V ∈ V ∧ E ∈ V → V O E = ∅
6 5 necon1ai ⊢ V O E ≠ ∅ → V ∈ V ∧ E ∈ V
7 brrelex12 ⊢ Rel ⁡ V O E ∧ F V O E P → F ∈ V ∧ P ∈ V
8 2 7 sylan ⊢ V ∈ V ∧ E ∈ V ∧ F V O E P → 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 ∧ F V O E P → V ∈ V ∧ E ∈ V ∧ F ∈ V ∧ P ∈ V
11 10 ex ⊢ V ∈ V ∧ E ∈ V → F V O E P → V ∈ V ∧ E ∈ V ∧ F ∈ V ∧ P ∈ V
12 4 6 11 3syl ⊢ F P ∈ V O E → F V O E P → V ∈ V ∧ E ∈ V ∧ F ∈ V ∧ P ∈ V
13 3 12 sylbi ⊢ F V O E P → F V O E P → V ∈ V ∧ E ∈ V ∧ F ∈ V ∧ P ∈ V
14 13 pm2.43i ⊢ F V O E P → V ∈ V ∧ E ∈ V ∧ F ∈ V ∧ P ∈ V