eceqoveq

Description: Equality of equivalence relation in terms of an operation. (Contributed by NM, 15-Feb-1996) (Proof shortened by Mario Carneiro, 12-Aug-2015)

	Ref	Expression
Hypotheses	eceqoveq.5	$⊢ \underset{˙}{\sim} Er (S \times S)$
	eceqoveq.7	$⊢ dom \underset{˙}{+} = S \times S$
	eceqoveq.8	$⊢ \neg \emptyset \in S$
	eceqoveq.9	$⊢ (x \in S \land y \in S) \to x \underset{˙}{+} y \in S$
	eceqoveq.10	$⊢ ((A \in S \land B \in S) \land (C \in S \land D \in S)) \to (⟨A, B⟩ \underset{˙}{\sim} ⟨C, D⟩ \leftrightarrow A \underset{˙}{+} D = B \underset{˙}{+} C)$
Assertion	eceqoveq	$⊢ (A \in S \land C \in S) \to ([⟨A, B⟩] \underset{˙}{\sim} = [⟨C, D⟩] \underset{˙}{\sim} \leftrightarrow A \underset{˙}{+} D = B \underset{˙}{+} C)$

Proof

Step	Hyp	Ref	Expression
1		eceqoveq.5	$⊢ \underset{˙}{\sim} Er (S \times S)$
2		eceqoveq.7	$⊢ dom \underset{˙}{+} = S \times S$
3		eceqoveq.8	$⊢ \neg \emptyset \in S$
4		eceqoveq.9	$⊢ (x \in S \land y \in S) \to x \underset{˙}{+} y \in S$
5		eceqoveq.10	$⊢ ((A \in S \land B \in S) \land (C \in S \land D \in S)) \to (⟨A, B⟩ \underset{˙}{\sim} ⟨C, D⟩ \leftrightarrow A \underset{˙}{+} D = B \underset{˙}{+} C)$
6		opelxpi	$⊢ (A \in S \land B \in S) \to ⟨A, B⟩ \in (S \times S)$
7	6	ad2antrr	$⊢ (((A \in S \land B \in S) \land C \in S) \land [⟨A, B⟩] \underset{˙}{\sim} = [⟨C, D⟩] \underset{˙}{\sim}) \to ⟨A, B⟩ \in (S \times S)$
8	1	a1i	$⊢ (((A \in S \land B \in S) \land C \in S) \land [⟨A, B⟩] \underset{˙}{\sim} = [⟨C, D⟩] \underset{˙}{\sim}) \to \underset{˙}{\sim} Er (S \times S)$
9		simpr	$⊢ (((A \in S \land B \in S) \land C \in S) \land [⟨A, B⟩] \underset{˙}{\sim} = [⟨C, D⟩] \underset{˙}{\sim}) \to [⟨A, B⟩] \underset{˙}{\sim} = [⟨C, D⟩] \underset{˙}{\sim}$
10	8 9	ereldm	$⊢ (((A \in S \land B \in S) \land C \in S) \land [⟨A, B⟩] \underset{˙}{\sim} = [⟨C, D⟩] \underset{˙}{\sim}) \to (⟨A, B⟩ \in (S \times S) \leftrightarrow ⟨C, D⟩ \in (S \times S))$
11	7 10	mpbid	$⊢ (((A \in S \land B \in S) \land C \in S) \land [⟨A, B⟩] \underset{˙}{\sim} = [⟨C, D⟩] \underset{˙}{\sim}) \to ⟨C, D⟩ \in (S \times S)$
12		opelxp2	$⊢ ⟨C, D⟩ \in (S \times S) \to D \in S$
13	11 12	syl	$⊢ (((A \in S \land B \in S) \land C \in S) \land [⟨A, B⟩] \underset{˙}{\sim} = [⟨C, D⟩] \underset{˙}{\sim}) \to D \in S$
14	13	ex	$⊢ ((A \in S \land B \in S) \land C \in S) \to ([⟨A, B⟩] \underset{˙}{\sim} = [⟨C, D⟩] \underset{˙}{\sim} \to D \in S)$
15	4	caovcl	$⊢ (B \in S \land C \in S) \to B \underset{˙}{+} C \in S$
16		eleq1	$⊢ A \underset{˙}{+} D = B \underset{˙}{+} C \to (A \underset{˙}{+} D \in S \leftrightarrow B \underset{˙}{+} C \in S)$
17	15 16	imbitrrid	$⊢ A \underset{˙}{+} D = B \underset{˙}{+} C \to ((B \in S \land C \in S) \to A \underset{˙}{+} D \in S)$
18	2 3	ndmovrcl	$⊢ A \underset{˙}{+} D \in S \to (A \in S \land D \in S)$
19	18	simprd	$⊢ A \underset{˙}{+} D \in S \to D \in S$
20	17 19	syl6com	$⊢ (B \in S \land C \in S) \to (A \underset{˙}{+} D = B \underset{˙}{+} C \to D \in S)$
21	20	adantll	$⊢ ((A \in S \land B \in S) \land C \in S) \to (A \underset{˙}{+} D = B \underset{˙}{+} C \to D \in S)$
22	1	a1i	$⊢ ((A \in S \land B \in S) \land (C \in S \land D \in S)) \to \underset{˙}{\sim} Er (S \times S)$
23	6	adantr	$⊢ ((A \in S \land B \in S) \land (C \in S \land D \in S)) \to ⟨A, B⟩ \in (S \times S)$
24	22 23	erth	$⊢ ((A \in S \land B \in S) \land (C \in S \land D \in S)) \to (⟨A, B⟩ \underset{˙}{\sim} ⟨C, D⟩ \leftrightarrow [⟨A, B⟩] \underset{˙}{\sim} = [⟨C, D⟩] \underset{˙}{\sim})$
25	24 5	bitr3d	$⊢ ((A \in S \land B \in S) \land (C \in S \land D \in S)) \to ([⟨A, B⟩] \underset{˙}{\sim} = [⟨C, D⟩] \underset{˙}{\sim} \leftrightarrow A \underset{˙}{+} D = B \underset{˙}{+} C)$
26	25	expr	$⊢ ((A \in S \land B \in S) \land C \in S) \to (D \in S \to ([⟨A, B⟩] \underset{˙}{\sim} = [⟨C, D⟩] \underset{˙}{\sim} \leftrightarrow A \underset{˙}{+} D = B \underset{˙}{+} C))$
27	14 21 26	pm5.21ndd	$⊢ ((A \in S \land B \in S) \land C \in S) \to ([⟨A, B⟩] \underset{˙}{\sim} = [⟨C, D⟩] \underset{˙}{\sim} \leftrightarrow A \underset{˙}{+} D = B \underset{˙}{+} C)$
28	27	an32s	$⊢ ((A \in S \land C \in S) \land B \in S) \to ([⟨A, B⟩] \underset{˙}{\sim} = [⟨C, D⟩] \underset{˙}{\sim} \leftrightarrow A \underset{˙}{+} D = B \underset{˙}{+} C)$
29		eqcom	$⊢ \emptyset = [⟨C, D⟩] \underset{˙}{\sim} \leftrightarrow [⟨C, D⟩] \underset{˙}{\sim} = \emptyset$
30		erdm	$⊢ \underset{˙}{\sim} Er (S \times S) \to dom \underset{˙}{\sim} = S \times S$
31	1 30	ax-mp	$⊢ dom \underset{˙}{\sim} = S \times S$
32	31	eleq2i	$⊢ ⟨C, D⟩ \in dom \underset{˙}{\sim} \leftrightarrow ⟨C, D⟩ \in (S \times S)$
33		ecdmn0	$⊢ ⟨C, D⟩ \in dom \underset{˙}{\sim} \leftrightarrow [⟨C, D⟩] \underset{˙}{\sim} \neq \emptyset$
34		opelxp	$⊢ ⟨C, D⟩ \in (S \times S) \leftrightarrow (C \in S \land D \in S)$
35	32 33 34	3bitr3i	$⊢ [⟨C, D⟩] \underset{˙}{\sim} \neq \emptyset \leftrightarrow (C \in S \land D \in S)$
36	35	simplbi2	$⊢ C \in S \to (D \in S \to [⟨C, D⟩] \underset{˙}{\sim} \neq \emptyset)$
37	36	ad2antlr	$⊢ ((A \in S \land C \in S) \land \neg B \in S) \to (D \in S \to [⟨C, D⟩] \underset{˙}{\sim} \neq \emptyset)$
38	37	necon2bd	$⊢ ((A \in S \land C \in S) \land \neg B \in S) \to ([⟨C, D⟩] \underset{˙}{\sim} = \emptyset \to \neg D \in S)$
39		simpr	$⊢ (A \in S \land D \in S) \to D \in S$
40	2	ndmov	$⊢ \neg (A \in S \land D \in S) \to A \underset{˙}{+} D = \emptyset$
41	39 40	nsyl5	$⊢ \neg D \in S \to A \underset{˙}{+} D = \emptyset$
42	38 41	syl6	$⊢ ((A \in S \land C \in S) \land \neg B \in S) \to ([⟨C, D⟩] \underset{˙}{\sim} = \emptyset \to A \underset{˙}{+} D = \emptyset)$
43		eleq1	$⊢ A \underset{˙}{+} D = \emptyset \to (A \underset{˙}{+} D \in S \leftrightarrow \emptyset \in S)$
44	3 43	mtbiri	$⊢ A \underset{˙}{+} D = \emptyset \to \neg A \underset{˙}{+} D \in S$
45	35	simprbi	$⊢ [⟨C, D⟩] \underset{˙}{\sim} \neq \emptyset \to D \in S$
46	4	caovcl	$⊢ (A \in S \land D \in S) \to A \underset{˙}{+} D \in S$
47	46	ex	$⊢ A \in S \to (D \in S \to A \underset{˙}{+} D \in S)$
48	47	ad2antrr	$⊢ ((A \in S \land C \in S) \land \neg B \in S) \to (D \in S \to A \underset{˙}{+} D \in S)$
49	45 48	syl5	$⊢ ((A \in S \land C \in S) \land \neg B \in S) \to ([⟨C, D⟩] \underset{˙}{\sim} \neq \emptyset \to A \underset{˙}{+} D \in S)$
50	49	necon1bd	$⊢ ((A \in S \land C \in S) \land \neg B \in S) \to (\neg A \underset{˙}{+} D \in S \to [⟨C, D⟩] \underset{˙}{\sim} = \emptyset)$
51	44 50	syl5	$⊢ ((A \in S \land C \in S) \land \neg B \in S) \to (A \underset{˙}{+} D = \emptyset \to [⟨C, D⟩] \underset{˙}{\sim} = \emptyset)$
52	42 51	impbid	$⊢ ((A \in S \land C \in S) \land \neg B \in S) \to ([⟨C, D⟩] \underset{˙}{\sim} = \emptyset \leftrightarrow A \underset{˙}{+} D = \emptyset)$
53	29 52	bitrid	$⊢ ((A \in S \land C \in S) \land \neg B \in S) \to (\emptyset = [⟨C, D⟩] \underset{˙}{\sim} \leftrightarrow A \underset{˙}{+} D = \emptyset)$
54	31	eleq2i	$⊢ ⟨A, B⟩ \in dom \underset{˙}{\sim} \leftrightarrow ⟨A, B⟩ \in (S \times S)$
55		ecdmn0	$⊢ ⟨A, B⟩ \in dom \underset{˙}{\sim} \leftrightarrow [⟨A, B⟩] \underset{˙}{\sim} \neq \emptyset$
56		opelxp	$⊢ ⟨A, B⟩ \in (S \times S) \leftrightarrow (A \in S \land B \in S)$
57	54 55 56	3bitr3i	$⊢ [⟨A, B⟩] \underset{˙}{\sim} \neq \emptyset \leftrightarrow (A \in S \land B \in S)$
58	57	simprbi	$⊢ [⟨A, B⟩] \underset{˙}{\sim} \neq \emptyset \to B \in S$
59	58	necon1bi	$⊢ \neg B \in S \to [⟨A, B⟩] \underset{˙}{\sim} = \emptyset$
60	59	adantl	$⊢ ((A \in S \land C \in S) \land \neg B \in S) \to [⟨A, B⟩] \underset{˙}{\sim} = \emptyset$
61	60	eqeq1d	$⊢ ((A \in S \land C \in S) \land \neg B \in S) \to ([⟨A, B⟩] \underset{˙}{\sim} = [⟨C, D⟩] \underset{˙}{\sim} \leftrightarrow \emptyset = [⟨C, D⟩] \underset{˙}{\sim})$
62		simpl	$⊢ (B \in S \land C \in S) \to B \in S$
63	2	ndmov	$⊢ \neg (B \in S \land C \in S) \to B \underset{˙}{+} C = \emptyset$
64	62 63	nsyl5	$⊢ \neg B \in S \to B \underset{˙}{+} C = \emptyset$
65	64	adantl	$⊢ ((A \in S \land C \in S) \land \neg B \in S) \to B \underset{˙}{+} C = \emptyset$
66	65	eqeq2d	$⊢ ((A \in S \land C \in S) \land \neg B \in S) \to (A \underset{˙}{+} D = B \underset{˙}{+} C \leftrightarrow A \underset{˙}{+} D = \emptyset)$
67	53 61 66	3bitr4d	$⊢ ((A \in S \land C \in S) \land \neg B \in S) \to ([⟨A, B⟩] \underset{˙}{\sim} = [⟨C, D⟩] \underset{˙}{\sim} \leftrightarrow A \underset{˙}{+} D = B \underset{˙}{+} C)$
68	28 67	pm2.61dan	$⊢ (A \in S \land C \in S) \to ([⟨A, B⟩] \underset{˙}{\sim} = [⟨C, D⟩] \underset{˙}{\sim} \leftrightarrow A \underset{˙}{+} D = B \underset{˙}{+} C)$

Metamath Proof Explorer

Theorem eceqoveq

Proof