Theorem oprssdm

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

	Ref	Expression
Hypotheses	oprssdm.1	⊢ ¬ ∅ ∈ 𝑆
	oprssdm.2	⊢ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) → ( 𝑥 𝐹 𝑦 ) ∈ 𝑆 )
Assertion	oprssdm	⊢ ( 𝑆 × 𝑆 ) ⊆ dom 𝐹

Proof

Step	Hyp	Ref	Expression
1		oprssdm.1	⊢ ¬ ∅ ∈ 𝑆
2		oprssdm.2	⊢ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) → ( 𝑥 𝐹 𝑦 ) ∈ 𝑆 )
3		relxp	⊢ Rel ( 𝑆 × 𝑆 )
4		opelxp	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑆 × 𝑆 ) ↔ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) )
5		df-ov	⊢ ( 𝑥 𝐹 𝑦 ) = ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ )
6	5 2	eqeltrrid	⊢ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) → ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ∈ 𝑆 )
7		ndmfv	⊢ ( ¬ ⟨ 𝑥 , 𝑦 ⟩ ∈ dom 𝐹 → ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = ∅ )
8	7	eleq1d	⊢ ( ¬ ⟨ 𝑥 , 𝑦 ⟩ ∈ dom 𝐹 → ( ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ∈ 𝑆 ↔ ∅ ∈ 𝑆 ) )
9	1 8	mtbiri	⊢ ( ¬ ⟨ 𝑥 , 𝑦 ⟩ ∈ dom 𝐹 → ¬ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ∈ 𝑆 )
10	9	con4i	⊢ ( ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ∈ 𝑆 → ⟨ 𝑥 , 𝑦 ⟩ ∈ dom 𝐹 )
11	6 10	syl	⊢ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ dom 𝐹 )
12	4 11	sylbi	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑆 × 𝑆 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ dom 𝐹 )
13	3 12	relssi	⊢ ( 𝑆 × 𝑆 ) ⊆ dom 𝐹