Theorem eceqoveq 7853

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

Hypotheses

Ref	Expression
eceqoveq.5	|- .~ Er ( S X. S )
eceqoveq.7	|- dom .+ = ( S X. S )
eceqoveq.8	|- -. (/) e. S
eceqoveq.9	|- ( ( x e. S /\ y e. S ) -> ( x .+ y ) e. S )
eceqoveq.10	|- ( ( ( A e. S /\ B e. S ) /\ ( C e. S /\ D e. S ) ) -> ( <. A , B >. .~ <. C , D >. <-> ( A .+ D ) = ( B .+ C ) ) )

Assertion

Ref	Expression
eceqoveq	|- ( ( A e. S /\ C e. S ) -> ( [ <. A , B >. ] .~ = [ <. C , D >. ] .~ <-> ( A .+ D ) = ( B .+ C ) ) )

Distinct variable groups:   x, y, .+   x, S, y   x, A, y   x, B, y   x, C, y   x, D, y

Allowed substitution hints:   .~ ( x, y)

Proof of Theorem eceqoveq

Step	Hyp	Ref	Expression
1		opelxpi 5148	. . . . . . . 8 |- ( ( A e. S /\ B e. S ) -> <. A , B >. e. ( S X. S ) )
2	1	ad2antrr 762	. . . . . . 7 |- ( ( ( ( A e. S /\ B e. S ) /\ C e. S ) /\ [ <. A , B >. ] .~ = [ <. C , D >. ] .~ ) -> <. A , B >. e. ( S X. S ) )
3		eceqoveq.5	. . . . . . . . 9 |- .~ Er ( S X. S )
4	3	a1i 11	. . . . . . . 8 |- ( ( ( ( A e. S /\ B e. S ) /\ C e. S ) /\ [ <. A , B >. ] .~ = [ <. C , D >. ] .~ ) -> .~ Er ( S X. S ) )
5		simpr 477	. . . . . . . 8 |- ( ( ( ( A e. S /\ B e. S ) /\ C e. S ) /\ [ <. A , B >. ] .~ = [ <. C , D >. ] .~ ) -> [ <. A , B >. ] .~ = [ <. C , D >. ] .~ )
6	4, 5	ereldm 7790	. . . . . . 7 |- ( ( ( ( A e. S /\ B e. S ) /\ C e. S ) /\ [ <. A , B >. ] .~ = [ <. C , D >. ] .~ ) -> ( <. A , B >. e. ( S X. S ) <-> <. C , D >. e. ( S X. S ) ) )
7	2, 6	mpbid 222	. . . . . 6 |- ( ( ( ( A e. S /\ B e. S ) /\ C e. S ) /\ [ <. A , B >. ] .~ = [ <. C , D >. ] .~ ) -> <. C , D >. e. ( S X. S ) )
8		opelxp2 5151	. . . . . 6 |- ( <. C , D >. e. ( S X. S ) -> D e. S )
9	7, 8	syl 17	. . . . 5 |- ( ( ( ( A e. S /\ B e. S ) /\ C e. S ) /\ [ <. A , B >. ] .~ = [ <. C , D >. ] .~ ) -> D e. S )
10	9	ex 450	. . . 4 |- ( ( ( A e. S /\ B e. S ) /\ C e. S ) -> ( [ <. A , B >. ] .~ = [ <. C , D >. ] .~ -> D e. S ) )
11		eceqoveq.9	. . . . . . . 8 |- ( ( x e. S /\ y e. S ) -> ( x .+ y ) e. S )
12	11	caovcl 6828	. . . . . . 7 |- ( ( B e. S /\ C e. S ) -> ( B .+ C ) e. S )
13		eleq1 2689	. . . . . . 7 |- ( ( A .+ D ) = ( B .+ C ) -> ( ( A .+ D ) e. S <-> ( B .+ C ) e. S ) )
14	12, 13	syl5ibr 236	. . . . . 6 |- ( ( A .+ D ) = ( B .+ C ) -> ( ( B e. S /\ C e. S ) -> ( A .+ D ) e. S ) )
15		eceqoveq.7	. . . . . . . 8 |- dom .+ = ( S X. S )
16		eceqoveq.8	. . . . . . . 8 |- -. (/) e. S
17	15, 16	ndmovrcl 6820	. . . . . . 7 |- ( ( A .+ D ) e. S -> ( A e. S /\ D e. S ) )
18	17	simprd 479	. . . . . 6 |- ( ( A .+ D ) e. S -> D e. S )
19	14, 18	syl6com 37	. . . . 5 |- ( ( B e. S /\ C e. S ) -> ( ( A .+ D ) = ( B .+ C ) -> D e. S ) )
20	19	adantll 750	. . . 4 |- ( ( ( A e. S /\ B e. S ) /\ C e. S ) -> ( ( A .+ D ) = ( B .+ C ) -> D e. S ) )
21	3	a1i 11	. . . . . . 7 |- ( ( ( A e. S /\ B e. S ) /\ ( C e. S /\ D e. S ) ) -> .~ Er ( S X. S ) )
22	1	adantr 481	. . . . . . 7 |- ( ( ( A e. S /\ B e. S ) /\ ( C e. S /\ D e. S ) ) -> <. A , B >. e. ( S X. S ) )
23	21, 22	erth 7791	. . . . . 6 |- ( ( ( A e. S /\ B e. S ) /\ ( C e. S /\ D e. S ) ) -> ( <. A , B >. .~ <. C , D >. <-> [ <. A , B >. ] .~ = [ <. C , D >. ] .~ ) )
24		eceqoveq.10	. . . . . 6 |- ( ( ( A e. S /\ B e. S ) /\ ( C e. S /\ D e. S ) ) -> ( <. A , B >. .~ <. C , D >. <-> ( A .+ D ) = ( B .+ C ) ) )
25	23, 24	bitr3d 270	. . . . 5 |- ( ( ( A e. S /\ B e. S ) /\ ( C e. S /\ D e. S ) ) -> ( [ <. A , B >. ] .~ = [ <. C , D >. ] .~ <-> ( A .+ D ) = ( B .+ C ) ) )
26	25	expr 643	. . . 4 |- ( ( ( A e. S /\ B e. S ) /\ C e. S ) -> ( D e. S -> ( [ <. A , B >. ] .~ = [ <. C , D >. ] .~ <-> ( A .+ D ) = ( B .+ C ) ) ) )
27	10, 20, 26	pm5.21ndd 369	. . 3 |- ( ( ( A e. S /\ B e. S ) /\ C e. S ) -> ( [ <. A , B >. ] .~ = [ <. C , D >. ] .~ <-> ( A .+ D ) = ( B .+ C ) ) )
28	27	an32s 846	. 2 |- ( ( ( A e. S /\ C e. S ) /\ B e. S ) -> ( [ <. A , B >. ] .~ = [ <. C , D >. ] .~ <-> ( A .+ D ) = ( B .+ C ) ) )
29		eqcom 2629	. . . 4 |- ( (/) = [ <. C , D >. ] .~ <-> [ <. C , D >. ] .~ = (/) )
30		erdm 7752	. . . . . . . . . . . 12 |- ( .~ Er ( S X. S ) -> dom .~ = ( S X. S ) )
31	3, 30	ax-mp 5	. . . . . . . . . . 11 |- dom .~ = ( S X. S )
32	31	eleq2i 2693	. . . . . . . . . 10 |- ( <. C , D >. e. dom .~ <-> <. C , D >. e. ( S X. S ) )
33		ecdmn0 7789	. . . . . . . . . 10 |- ( <. C , D >. e. dom .~ <-> [ <. C , D >. ] .~ =/= (/) )
34		opelxp 5146	. . . . . . . . . 10 |- ( <. C , D >. e. ( S X. S ) <-> ( C e. S /\ D e. S ) )
35	32, 33, 34	3bitr3i 290	. . . . . . . . 9 |- ( [ <. C , D >. ] .~ =/= (/) <-> ( C e. S /\ D e. S ) )
36	35	simplbi2 655	. . . . . . . 8 |- ( C e. S -> ( D e. S -> [ <. C , D >. ] .~ =/= (/) ) )
37	36	ad2antlr 763	. . . . . . 7 |- ( ( ( A e. S /\ C e. S ) /\ -. B e. S ) -> ( D e. S -> [ <. C , D >. ] .~ =/= (/) ) )
38	37	necon2bd 2810	. . . . . 6 |- ( ( ( A e. S /\ C e. S ) /\ -. B e. S ) -> ( [ <. C , D >. ] .~ = (/) -> -. D e. S ) )
39		simpr 477	. . . . . . . 8 |- ( ( A e. S /\ D e. S ) -> D e. S )
40	39	con3i 150	. . . . . . 7 |- ( -. D e. S -> -. ( A e. S /\ D e. S ) )
41	15	ndmov 6818	. . . . . . 7 |- ( -. ( A e. S /\ D e. S ) -> ( A .+ D ) = (/) )
42	40, 41	syl 17	. . . . . 6 |- ( -. D e. S -> ( A .+ D ) = (/) )
43	38, 42	syl6 35	. . . . 5 |- ( ( ( A e. S /\ C e. S ) /\ -. B e. S ) -> ( [ <. C , D >. ] .~ = (/) -> ( A .+ D ) = (/) ) )
44		eleq1 2689	. . . . . . 7 |- ( ( A .+ D ) = (/) -> ( ( A .+ D ) e. S <-> (/) e. S ) )
45	16, 44	mtbiri 317	. . . . . 6 |- ( ( A .+ D ) = (/) -> -. ( A .+ D ) e. S )
46	35	simprbi 480	. . . . . . . 8 |- ( [ <. C , D >. ] .~ =/= (/) -> D e. S )
47	11	caovcl 6828	. . . . . . . . . 10 |- ( ( A e. S /\ D e. S ) -> ( A .+ D ) e. S )
48	47	ex 450	. . . . . . . . 9 |- ( A e. S -> ( D e. S -> ( A .+ D ) e. S ) )
49	48	ad2antrr 762	. . . . . . . 8 |- ( ( ( A e. S /\ C e. S ) /\ -. B e. S ) -> ( D e. S -> ( A .+ D ) e. S ) )
50	46, 49	syl5 34	. . . . . . 7 |- ( ( ( A e. S /\ C e. S ) /\ -. B e. S ) -> ( [ <. C , D >. ] .~ =/= (/) -> ( A .+ D ) e. S ) )
51	50	necon1bd 2812	. . . . . 6 |- ( ( ( A e. S /\ C e. S ) /\ -. B e. S ) -> ( -. ( A .+ D ) e. S -> [ <. C , D >. ] .~ = (/) ) )
52	45, 51	syl5 34	. . . . 5 |- ( ( ( A e. S /\ C e. S ) /\ -. B e. S ) -> ( ( A .+ D ) = (/) -> [ <. C , D >. ] .~ = (/) ) )
53	43, 52	impbid 202	. . . 4 |- ( ( ( A e. S /\ C e. S ) /\ -. B e. S ) -> ( [ <. C , D >. ] .~ = (/) <-> ( A .+ D ) = (/) ) )
54	29, 53	syl5bb 272	. . 3 |- ( ( ( A e. S /\ C e. S ) /\ -. B e. S ) -> ( (/) = [ <. C , D >. ] .~ <-> ( A .+ D ) = (/) ) )
55	31	eleq2i 2693	. . . . . . . 8 |- ( <. A , B >. e. dom .~ <-> <. A , B >. e. ( S X. S ) )
56		ecdmn0 7789	. . . . . . . 8 |- ( <. A , B >. e. dom .~ <-> [ <. A , B >. ] .~ =/= (/) )
57		opelxp 5146	. . . . . . . 8 |- ( <. A , B >. e. ( S X. S ) <-> ( A e. S /\ B e. S ) )
58	55, 56, 57	3bitr3i 290	. . . . . . 7 |- ( [ <. A , B >. ] .~ =/= (/) <-> ( A e. S /\ B e. S ) )
59	58	simprbi 480	. . . . . 6 |- ( [ <. A , B >. ] .~ =/= (/) -> B e. S )
60	59	necon1bi 2822	. . . . 5 |- ( -. B e. S -> [ <. A , B >. ] .~ = (/) )
61	60	adantl 482	. . . 4 |- ( ( ( A e. S /\ C e. S ) /\ -. B e. S ) -> [ <. A , B >. ] .~ = (/) )
62	61	eqeq1d 2624	. . 3 |- ( ( ( A e. S /\ C e. S ) /\ -. B e. S ) -> ( [ <. A , B >. ] .~ = [ <. C , D >. ] .~ <-> (/) = [ <. C , D >. ] .~ ) )
63		simpl 473	. . . . . . 7 |- ( ( B e. S /\ C e. S ) -> B e. S )
64	63	con3i 150	. . . . . 6 |- ( -. B e. S -> -. ( B e. S /\ C e. S ) )
65	15	ndmov 6818	. . . . . 6 |- ( -. ( B e. S /\ C e. S ) -> ( B .+ C ) = (/) )
66	64, 65	syl 17	. . . . 5 |- ( -. B e. S -> ( B .+ C ) = (/) )
67	66	adantl 482	. . . 4 |- ( ( ( A e. S /\ C e. S ) /\ -. B e. S ) -> ( B .+ C ) = (/) )
68	67	eqeq2d 2632	. . 3 |- ( ( ( A e. S /\ C e. S ) /\ -. B e. S ) -> ( ( A .+ D ) = ( B .+ C ) <-> ( A .+ D ) = (/) ) )
69	54, 62, 68	3bitr4d 300	. 2 |- ( ( ( A e. S /\ C e. S ) /\ -. B e. S ) -> ( [ <. A , B >. ] .~ = [ <. C , D >. ] .~ <-> ( A .+ D ) = ( B .+ C ) ) )
70	28, 69	pm2.61dan 832	1 |- ( ( A e. S /\ C e. S ) -> ( [ <. A , B >. ] .~ = [ <. C , D >. ] .~ <-> ( A .+ D ) = ( B .+ C ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   /\ wa 384   = wceq 1483   e. wcel 1990   =/= wne 2794   (/)c0 3915   <.cop 4183   class class class wbr 4653   X. cxp 5112   dom cdm 5114  (class class class)co 6650   Er wer 7739   [cec 7740

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fv 5896  df-ov 6653  df-er 7742  df-ec 7744

This theorem is referenced by: (None)