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 | ⊢ 𝐹 = ( 𝑥 ∈ 𝐸 , 𝑦 ∈ 𝐺 ↦ 𝐻 ) | |
| brovmptimex.br | ⊢ ( 𝜑 → 𝐴 𝑅 𝐵 ) | ||
| brovmptimex.ov | ⊢ ( 𝜑 → 𝑅 = ( 𝐶 𝐹 𝐷 ) ) | ||
| Assertion | brovmptimex | ⊢ ( 𝜑 → ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | brovmptimex.mpt | ⊢ 𝐹 = ( 𝑥 ∈ 𝐸 , 𝑦 ∈ 𝐺 ↦ 𝐻 ) | |
| 2 | brovmptimex.br | ⊢ ( 𝜑 → 𝐴 𝑅 𝐵 ) | |
| 3 | brovmptimex.ov | ⊢ ( 𝜑 → 𝑅 = ( 𝐶 𝐹 𝐷 ) ) | |
| 4 | 3 2 | breqdi | ⊢ ( 𝜑 → 𝐴 ( 𝐶 𝐹 𝐷 ) 𝐵 ) |
| 5 | brne0 | ⊢ ( 𝐴 ( 𝐶 𝐹 𝐷 ) 𝐵 → ( 𝐶 𝐹 𝐷 ) ≠ ∅ ) | |
| 6 | 1 | reldmmpo | ⊢ Rel dom 𝐹 |
| 7 | 6 | ovprc | ⊢ ( ¬ ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) → ( 𝐶 𝐹 𝐷 ) = ∅ ) |
| 8 | 7 | necon1ai | ⊢ ( ( 𝐶 𝐹 𝐷 ) ≠ ∅ → ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) ) |
| 9 | 4 5 8 | 3syl | ⊢ ( 𝜑 → ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) ) |