This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐹