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	6	con3i	$⊢ \neg (A \in S \land B \in S \land C \in S) \to \neg (A F B \in S \land C \in S)$
8	1	ndmov	$⊢ \neg (A F B \in S \land C \in S) \to (A F B) F C = \emptyset$
9	7 8	syl	$⊢ \neg (A \in S \land B \in S \land C \in S) \to (A F B) F C = \emptyset$
10	1 2	ndmovrcl	$⊢ B F C \in S \to (B \in S \land C \in S)$
11	10	anim2i	$⊢ (A \in S \land B F C \in S) \to (A \in S \land (B \in S \land C \in S))$
12		3anass	$⊢ (A \in S \land B \in S \land C \in S) \leftrightarrow (A \in S \land (B \in S \land C \in S))$
13	11 12	sylibr	$⊢ (A \in S \land B F C \in S) \to (A \in S \land B \in S \land C \in S)$
14	13	con3i	$⊢ \neg (A \in S \land B \in S \land C \in S) \to \neg (A \in S \land B F C \in S)$
15	1	ndmov	$⊢ \neg (A \in S \land B F C \in S) \to A F (B F C) = \emptyset$
16	14 15	syl	$⊢ \neg (A \in S \land B \in S \land C \in S) \to A F (B F C) = \emptyset$
17	9 16	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