# Metamath Proof Explorer

## Theorem ndmovass

Description: Any operation is associative outside its domain, if the domain doesn't contain the empty set. (Contributed by NM, 24-Aug-1995)

Ref Expression
Hypotheses ndmov.1 ${⊢}\mathrm{dom}{F}={S}×{S}$
ndmov.5 ${⊢}¬\varnothing \in {S}$
Assertion ndmovass ${⊢}¬\left({A}\in {S}\wedge {B}\in {S}\wedge {C}\in {S}\right)\to \left({A}{F}{B}\right){F}{C}={A}{F}\left({B}{F}{C}\right)$

### Proof

Step Hyp Ref Expression
1 ndmov.1 ${⊢}\mathrm{dom}{F}={S}×{S}$
2 ndmov.5 ${⊢}¬\varnothing \in {S}$
3 1 2 ndmovrcl ${⊢}{A}{F}{B}\in {S}\to \left({A}\in {S}\wedge {B}\in {S}\right)$
4 3 anim1i ${⊢}\left({A}{F}{B}\in {S}\wedge {C}\in {S}\right)\to \left(\left({A}\in {S}\wedge {B}\in {S}\right)\wedge {C}\in {S}\right)$
5 df-3an ${⊢}\left({A}\in {S}\wedge {B}\in {S}\wedge {C}\in {S}\right)↔\left(\left({A}\in {S}\wedge {B}\in {S}\right)\wedge {C}\in {S}\right)$
6 4 5 sylibr ${⊢}\left({A}{F}{B}\in {S}\wedge {C}\in {S}\right)\to \left({A}\in {S}\wedge {B}\in {S}\wedge {C}\in {S}\right)$
7 1 ndmov ${⊢}¬\left({A}{F}{B}\in {S}\wedge {C}\in {S}\right)\to \left({A}{F}{B}\right){F}{C}=\varnothing$
8 6 7 nsyl5 ${⊢}¬\left({A}\in {S}\wedge {B}\in {S}\wedge {C}\in {S}\right)\to \left({A}{F}{B}\right){F}{C}=\varnothing$
9 1 2 ndmovrcl ${⊢}{B}{F}{C}\in {S}\to \left({B}\in {S}\wedge {C}\in {S}\right)$
10 9 anim2i ${⊢}\left({A}\in {S}\wedge {B}{F}{C}\in {S}\right)\to \left({A}\in {S}\wedge \left({B}\in {S}\wedge {C}\in {S}\right)\right)$
11 3anass ${⊢}\left({A}\in {S}\wedge {B}\in {S}\wedge {C}\in {S}\right)↔\left({A}\in {S}\wedge \left({B}\in {S}\wedge {C}\in {S}\right)\right)$
12 10 11 sylibr ${⊢}\left({A}\in {S}\wedge {B}{F}{C}\in {S}\right)\to \left({A}\in {S}\wedge {B}\in {S}\wedge {C}\in {S}\right)$
13 1 ndmov ${⊢}¬\left({A}\in {S}\wedge {B}{F}{C}\in {S}\right)\to {A}{F}\left({B}{F}{C}\right)=\varnothing$
14 12 13 nsyl5 ${⊢}¬\left({A}\in {S}\wedge {B}\in {S}\wedge {C}\in {S}\right)\to {A}{F}\left({B}{F}{C}\right)=\varnothing$
15 8 14 eqtr4d ${⊢}¬\left({A}\in {S}\wedge {B}\in {S}\wedge {C}\in {S}\right)\to \left({A}{F}{B}\right){F}{C}={A}{F}\left({B}{F}{C}\right)$