Description: Domain of closure of an operation. In contrast to oprssdm , no additional property for S ( -. (/) e. S ) is required! (Contributed by Alexander van der Vekens, 26-May-2017)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | aoprssdm.1 | ⊢ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) → (( 𝑥 𝐹 𝑦 )) ∈ 𝑆 ) | |
| Assertion | aoprssdm | ⊢ ( 𝑆 × 𝑆 ) ⊆ dom 𝐹 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | aoprssdm.1 | ⊢ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) → (( 𝑥 𝐹 𝑦 )) ∈ 𝑆 ) | |
| 2 | relxp | ⊢ Rel ( 𝑆 × 𝑆 ) | |
| 3 | opelxp | ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑆 × 𝑆 ) ↔ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) | |
| 4 | df-aov | ⊢ (( 𝑥 𝐹 𝑦 )) = ( 𝐹 ''' ⟨ 𝑥 , 𝑦 ⟩ ) | |
| 5 | 4 1 | eqeltrrid | ⊢ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) → ( 𝐹 ''' ⟨ 𝑥 , 𝑦 ⟩ ) ∈ 𝑆 ) |
| 6 | afvvdm | ⊢ ( ( 𝐹 ''' ⟨ 𝑥 , 𝑦 ⟩ ) ∈ 𝑆 → ⟨ 𝑥 , 𝑦 ⟩ ∈ dom 𝐹 ) | |
| 7 | 5 6 | syl | ⊢ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ dom 𝐹 ) |
| 8 | 3 7 | sylbi | ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑆 × 𝑆 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ dom 𝐹 ) |
| 9 | 2 8 | relssi | ⊢ ( 𝑆 × 𝑆 ) ⊆ dom 𝐹 |