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	⊢ ( ∀ 𝑎 ∈ 𝐷 ∀ 𝑏 ∈ 𝐸 ( 𝑎 𝐹 𝑏 ) ≠ ∅ → ( ( 𝐷 × 𝐸 ) ⊆ dom 𝐹 ∧ Fun ( 𝐹 ↾ ( 𝐷 × 𝐸 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		fveq2	⊢ ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ ⟨ 𝑎 , 𝑏 ⟩ ) )
2		df-ov	⊢ ( 𝑎 𝐹 𝑏 ) = ( 𝐹 ‘ ⟨ 𝑎 , 𝑏 ⟩ )
3	1 2	eqtr4di	⊢ ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝐹 ‘ 𝑝 ) = ( 𝑎 𝐹 𝑏 ) )
4	3	neeq1d	⊢ ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( 𝐹 ‘ 𝑝 ) ≠ ∅ ↔ ( 𝑎 𝐹 𝑏 ) ≠ ∅ ) )
5	4	ralxp	⊢ ( ∀ 𝑝 ∈ ( 𝐷 × 𝐸 ) ( 𝐹 ‘ 𝑝 ) ≠ ∅ ↔ ∀ 𝑎 ∈ 𝐷 ∀ 𝑏 ∈ 𝐸 ( 𝑎 𝐹 𝑏 ) ≠ ∅ )
6		fvn0ssdmfun	⊢ ( ∀ 𝑝 ∈ ( 𝐷 × 𝐸 ) ( 𝐹 ‘ 𝑝 ) ≠ ∅ → ( ( 𝐷 × 𝐸 ) ⊆ dom 𝐹 ∧ Fun ( 𝐹 ↾ ( 𝐷 × 𝐸 ) ) ) )
7	5 6	sylbir	⊢ ( ∀ 𝑎 ∈ 𝐷 ∀ 𝑏 ∈ 𝐸 ( 𝑎 𝐹 𝑏 ) ≠ ∅ → ( ( 𝐷 × 𝐸 ) ⊆ dom 𝐹 ∧ Fun ( 𝐹 ↾ ( 𝐷 × 𝐸 ) ) ) )