Metamath Proof Explorer

Theorem ovn0ssdmfun

Description: If a class' operation value for two operands is not the empty set, the operands are contained in the domain of the class, and the class restricted to the operands is a function, analogous to fvfundmfvn0 . (Contributed by AV, 27-Jan-2020)

Ref Expression
Assertion ovn0ssdmfun ⊢ ∀ a ∈ D ∀ b ∈ E a F b ≠ ∅ → D × E ⊆ dom ⁡ F ∧ Fun ⁡ F ↾ D × E

Proof

Step Hyp Ref Expression
1 fveq2 ⊢ p = a b → F ⁡ p = F ⁡ a b
2 df-ov ⊢ a F b = F ⁡ a b
3 1 2 eqtr4di ⊢ p = a b → F ⁡ p = a F b
4 3 neeq1d ⊢ p = a b → F ⁡ p ≠ ∅ ↔ a F b ≠ ∅
5 4 ralxp ⊢ ∀ p ∈ D × E F ⁡ p ≠ ∅ ↔ ∀ a ∈ D ∀ b ∈ E a F b ≠ ∅
6 fvn0ssdmfun ⊢ ∀ p ∈ D × E F ⁡ p ≠ ∅ → D × E ⊆ dom ⁡ F ∧ Fun ⁡ F ↾ D × E
7 5 6 sylbir ⊢ ∀ a ∈ D ∀ b ∈ E a F b ≠ ∅ → D × E ⊆ dom ⁡ F ∧ Fun ⁡ F ↾ D × E