oprssdm

Description: Domain of closure of an operation. (Contributed by NM, 24-Aug-1995)

Step	Hyp	Ref	Expression
1		oprssdm.1	$⊢ \neg \emptyset \in S$
2		oprssdm.2	$⊢ (x \in S \land y \in S) \to x F y \in S$
3		relxp	$⊢ Rel (S \times S)$
4		opelxp	$⊢ ⟨x, y⟩ \in (S \times S) \leftrightarrow (x \in S \land y \in S)$
5		df-ov	$⊢ x F y = F (⟨x, y⟩)$
6	5 2	eqeltrrid	$⊢ (x \in S \land y \in S) \to F (⟨x, y⟩) \in S$
7		ndmfv	$⊢ \neg ⟨x, y⟩ \in dom F \to F (⟨x, y⟩) = \emptyset$
8	7	eleq1d	$⊢ \neg ⟨x, y⟩ \in dom F \to (F (⟨x, y⟩) \in S \leftrightarrow \emptyset \in S)$
9	1 8	mtbiri	$⊢ \neg ⟨x, y⟩ \in dom F \to \neg F (⟨x, y⟩) \in S$
10	9	con4i	$⊢ F (⟨x, y⟩) \in S \to ⟨x, y⟩ \in dom F$
11	6 10	syl	$⊢ (x \in S \land y \in S) \to ⟨x, y⟩ \in dom F$
12	4 11	sylbi	$⊢ ⟨x, y⟩ \in (S \times S) \to ⟨x, y⟩ \in dom F$
13	3 12	relssi	$⊢ S \times S \subseteq dom F$

Metamath Proof Explorer