Metamath Proof Explorer

Theorem brovmptimex

Description: If a binary relation holds and the relation is the value of a binary operation built with maps-to, then the arguments to that operation are sets. (Contributed by RP, 22-May-2021)

Ref Expression
Hypotheses brovmptimex.mpt ⊢ F = x ∈ E , y ∈ G ⟼ H
brovmptimex.br ⊢ φ → A R B
brovmptimex.ov ⊢ φ → R = C F D
Assertion brovmptimex ⊢ φ → C ∈ V ∧ D ∈ V

Proof

Step Hyp Ref Expression
1 brovmptimex.mpt ⊢ F = x ∈ E , y ∈ G ⟼ H
2 brovmptimex.br ⊢ φ → A R B
3 brovmptimex.ov ⊢ φ → R = C F D
4 3 2 breqdi ⊢ φ → A C F D B
5 brne0 ⊢ A C F D B → C F D ≠ ∅
6 1 reldmmpo ⊢ Rel ⁡ dom ⁡ F
7 6 ovprc ⊢ ¬ C ∈ V ∧ D ∈ V → C F D = ∅
8 7 necon1ai ⊢ C F D ≠ ∅ → C ∈ V ∧ D ∈ V
9 4 5 8 3syl ⊢ φ → C ∈ V ∧ D ∈ V