ndmaovass

Description: Any operation is associative outside its domain. In contrast to ndmovass where it is required that the operation's domain doesn't contain the empty set ( -. (/) e. S ), no additional assumption is required. (Contributed by Alexander van der Vekens, 26-May-2017)

		Ref	Expression
	Hypothesis	ndmaov.1	$⊢ dom F = S \times S$
	Assertion	ndmaovass	$⊢ \neg (A \in S \land B \in S \land C \in S) \to ((((A F B)) F C)) = ((A F ((B F C))))$

Proof

Step	Hyp	Ref	Expression
1		ndmaov.1	$⊢ dom F = S \times S$
2	1	eleq2i	$⊢ ⟨((A F B)), C⟩ \in dom F \leftrightarrow ⟨((A F B)), C⟩ \in (S \times S)$
3		opelxp	$⊢ ⟨((A F B)), C⟩ \in (S \times S) \leftrightarrow (((A F B)) \in S \land C \in S)$
4	2 3	bitri	$⊢ ⟨((A F B)), C⟩ \in dom F \leftrightarrow (((A F B)) \in S \land C \in S)$
5		aovvdm	$⊢ ((A F B)) \in S \to ⟨A, B⟩ \in dom F$
6	1	eleq2i	$⊢ ⟨A, B⟩ \in dom F \leftrightarrow ⟨A, B⟩ \in (S \times S)$
7		opelxp	$⊢ ⟨A, B⟩ \in (S \times S) \leftrightarrow (A \in S \land B \in S)$
8	6 7	bitri	$⊢ ⟨A, B⟩ \in dom F \leftrightarrow (A \in S \land B \in S)$
9		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)$
10	9	simplbi2	$⊢ (A \in S \land B \in S) \to (C \in S \to (A \in S \land B \in S \land C \in S))$
11	8 10	sylbi	$⊢ ⟨A, B⟩ \in dom F \to (C \in S \to (A \in S \land B \in S \land C \in S))$
12	5 11	syl	$⊢ ((A F B)) \in S \to (C \in S \to (A \in S \land B \in S \land C \in S))$
13	12	imp	$⊢ (((A F B)) \in S \land C \in S) \to (A \in S \land B \in S \land C \in S)$
14	4 13	sylbi	$⊢ ⟨((A F B)), C⟩ \in dom F \to (A \in S \land B \in S \land C \in S)$
15		ndmaov	$⊢ \neg ⟨((A F B)), C⟩ \in dom F \to ((((A F B)) F C)) = V$
16	14 15	nsyl5	$⊢ \neg (A \in S \land B \in S \land C \in S) \to ((((A F B)) F C)) = V$
17	1	eleq2i	$⊢ ⟨A, ((B F C))⟩ \in dom F \leftrightarrow ⟨A, ((B F C))⟩ \in (S \times S)$
18		opelxp	$⊢ ⟨A, ((B F C))⟩ \in (S \times S) \leftrightarrow (A \in S \land ((B F C)) \in S)$
19	17 18	bitri	$⊢ ⟨A, ((B F C))⟩ \in dom F \leftrightarrow (A \in S \land ((B F C)) \in S)$
20		aovvdm	$⊢ ((B F C)) \in S \to ⟨B, C⟩ \in dom F$
21	1	eleq2i	$⊢ ⟨B, C⟩ \in dom F \leftrightarrow ⟨B, C⟩ \in (S \times S)$
22		opelxp	$⊢ ⟨B, C⟩ \in (S \times S) \leftrightarrow (B \in S \land C \in S)$
23	21 22	bitri	$⊢ ⟨B, C⟩ \in dom F \leftrightarrow (B \in S \land C \in S)$
24		3anass	$⊢ (A \in S \land B \in S \land C \in S) \leftrightarrow (A \in S \land (B \in S \land C \in S))$
25	24	biimpri	$⊢ (A \in S \land (B \in S \land C \in S)) \to (A \in S \land B \in S \land C \in S)$
26	25	a1d	$⊢ (A \in S \land (B \in S \land C \in S)) \to (⟨A, ((B F C))⟩ \in dom F \to (A \in S \land B \in S \land C \in S))$
27	26	expcom	$⊢ (B \in S \land C \in S) \to (A \in S \to (⟨A, ((B F C))⟩ \in dom F \to (A \in S \land B \in S \land C \in S)))$
28	23 27	sylbi	$⊢ ⟨B, C⟩ \in dom F \to (A \in S \to (⟨A, ((B F C))⟩ \in dom F \to (A \in S \land B \in S \land C \in S)))$
29	20 28	syl	$⊢ ((B F C)) \in S \to (A \in S \to (⟨A, ((B F C))⟩ \in dom F \to (A \in S \land B \in S \land C \in S)))$
30	29	impcom	$⊢ (A \in S \land ((B F C)) \in S) \to (⟨A, ((B F C))⟩ \in dom F \to (A \in S \land B \in S \land C \in S))$
31	19 30	sylbi	$⊢ ⟨A, ((B F C))⟩ \in dom F \to (⟨A, ((B F C))⟩ \in dom F \to (A \in S \land B \in S \land C \in S))$
32	31	pm2.43i	$⊢ ⟨A, ((B F C))⟩ \in dom F \to (A \in S \land B \in S \land C \in S)$
33		ndmaov	$⊢ \neg ⟨A, ((B F C))⟩ \in dom F \to ((A F ((B F C)))) = V$
34	32 33	nsyl5	$⊢ \neg (A \in S \land B \in S \land C \in S) \to ((A F ((B F C)))) = V$
35	16 34	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

Theorem ndmaovass

Proof