Description: Reverse closure law, in contrast to ndmovrcl where it is required that the operation's domain doesn't contain the empty set ( -. (/) e. S ), no additional asumption is required. (Contributed by Alexander van der Vekens, 26-May-2017)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | ndmaov.1 | ⊢ dom 𝐹 = ( 𝑆 × 𝑆 ) | |
| Assertion | ndmaovrcl | ⊢ ( (( 𝐴 𝐹 𝐵 )) ∈ 𝑆 → ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ndmaov.1 | ⊢ dom 𝐹 = ( 𝑆 × 𝑆 ) | |
| 2 | aovvdm | ⊢ ( (( 𝐴 𝐹 𝐵 )) ∈ 𝑆 → ⟨ 𝐴 , 𝐵 ⟩ ∈ dom 𝐹 ) | |
| 3 | opelxp | ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑆 × 𝑆 ) ↔ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ) | |
| 4 | 3 | biimpi | ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑆 × 𝑆 ) → ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ) |
| 5 | 4 1 | eleq2s | ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ dom 𝐹 → ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ) |
| 6 | 2 5 | syl | ⊢ ( (( 𝐴 𝐹 𝐵 )) ∈ 𝑆 → ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ) |