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	14	con3i	$⊢ \neg (A \in S \land B \in S \land C \in S) \to \neg ⟨((A F B)), C⟩ \in dom F$
16		ndmaov	$⊢ \neg ⟨((A F B)), C⟩ \in dom F \to ((((A F B)) F C)) = V$
17	15 16	syl	$⊢ \neg (A \in S \land B \in S \land C \in S) \to ((((A F B)) F C)) = V$
18	1	eleq2i	$⊢ ⟨A, ((B F C))⟩ \in dom F \leftrightarrow ⟨A, ((B F C))⟩ \in (S \times S)$
19		opelxp	$⊢ ⟨A, ((B F C))⟩ \in (S \times S) \leftrightarrow (A \in S \land ((B F C)) \in S)$
20	18 19	bitri	$⊢ ⟨A, ((B F C))⟩ \in dom F \leftrightarrow (A \in S \land ((B F C)) \in S)$
21		aovvdm	$⊢ ((B F C)) \in S \to ⟨B, C⟩ \in dom F$
22	1	eleq2i	$⊢ ⟨B, C⟩ \in dom F \leftrightarrow ⟨B, C⟩ \in (S \times S)$
23		opelxp	$⊢ ⟨B, C⟩ \in (S \times S) \leftrightarrow (B \in S \land C \in S)$
24	22 23	bitri	$⊢ ⟨B, C⟩ \in dom F \leftrightarrow (B \in S \land C \in S)$
25		3anass	$⊢ (A \in S \land B \in S \land C \in S) \leftrightarrow (A \in S \land (B \in S \land C \in S))$
26	25	biimpri	$⊢ (A \in S \land (B \in S \land C \in S)) \to (A \in S \land B \in S \land C \in S)$
27	26	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))$
28	27	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)))$
29	24 28	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)))$
30	21 29	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)))$
31	30	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))$
32	20 31	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))$
33	32	pm2.43i	$⊢ ⟨A, ((B F C))⟩ \in dom F \to (A \in S \land B \in S \land C \in S)$
34	33	con3i	$⊢ \neg (A \in S \land B \in S \land C \in S) \to \neg ⟨A, ((B F C))⟩ \in dom F$
35		ndmaov	$⊢ \neg ⟨A, ((B F C))⟩ \in dom F \to ((A F ((B F C)))) = V$
36	34 35	syl	$⊢ \neg (A \in S \land B \in S \land C \in S) \to ((A F ((B F C)))) = V$
37	17 36	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