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	$⊢ dom F = S \times S$
	ndmov.5	$⊢ \neg \emptyset \in S$
Assertion	ndmovass	$⊢ \neg (A \in S \land B \in S \land C \in S) \to (A F B) F C = A F (B F C)$

Step	Hyp	Ref	Expression
1		ndmov.1	$⊢ dom F = S \times S$
2		ndmov.5	$⊢ \neg \emptyset \in S$
3	1 2	ndmovrcl	$⊢ A F B \in S \to (A \in S \land B \in S)$
4	3	anim1i	$⊢ (A F B \in S \land C \in S) \to ((A \in S \land B \in S) \land C \in S)$
5		df-3an	$⊢ (A \in S \land B \in S \land C \in S) \leftrightarrow ((A \in S \land B \in S) \land C \in S)$
6	4 5	sylibr	$⊢ (A F B \in S \land C \in S) \to (A \in S \land B \in S \land C \in S)$
7	1	ndmov	$⊢ \neg (A F B \in S \land C \in S) \to (A F B) F C = \emptyset$
8	6 7	nsyl5	$⊢ \neg (A \in S \land B \in S \land C \in S) \to (A F B) F C = \emptyset$
9	1 2	ndmovrcl	$⊢ B F C \in S \to (B \in S \land C \in S)$
10	9	anim2i	$⊢ (A \in S \land B F C \in S) \to (A \in S \land (B \in S \land C \in S))$
11		3anass	$⊢ (A \in S \land B \in S \land C \in S) \leftrightarrow (A \in S \land (B \in S \land C \in S))$
12	10 11	sylibr	$⊢ (A \in S \land B F C \in S) \to (A \in S \land B \in S \land C \in S)$
13	1	ndmov	$⊢ \neg (A \in S \land B F C \in S) \to A F (B F C) = \emptyset$
14	12 13	nsyl5	$⊢ \neg (A \in S \land B \in S \land C \in S) \to A F (B F C) = \emptyset$
15	8 14	eqtr4d	$⊢ \neg (A \in S \land B \in S \land C \in S) \to (A F B) F C = A F (B F C)$

Metamath Proof Explorer