Theorem th3qlem1 6144

Description: Lemma for Exercise 44 version of Theorem 3Q of [Enderton] p. 60. The third hypothesis is the compatibility assumption. (Contributed by NM, 3-Aug-1995.) (Revised by Mario Carneiro, 9-Jul-2014.)

Hypotheses

Ref	Expression
th3qlem1.1	|- .~ Er S
th3qlem1.3	|- (((y e. S /\ w e. S) /\ (z e. S /\ v e. S)) -> ((y .~ w /\ z .~ v) -> (y .+ z) .~ (w .+ v)))

Assertion

Ref	Expression
th3qlem1	|- ((A e. ( S /. .~ ) /\ B e. ( S /. .~ )) -> E*xE.yE.z((A = [y] .~ /\ B = [z] .~ ) /\ x = [(y .+ z)] .~ ))

Distinct variable groups:   x,y,z,w,v, .+   x, .~ ,y,z,w,v   x, S,y,z,w,v   x,A,y,z,w,v   x,B,y,z,w,v

Proof of Theorem th3qlem1

Dummy variable u is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ee4anv 1806	. . . 4 |- (E.yE.zE.wE.v(((A = [y] .~ /\ B = [z] .~ ) /\ x = [(y .+ z)] .~ ) /\ ((A = [w] .~ /\ B = [v] .~ ) /\ u = [(w .+ v)] .~ )) <-> (E.yE.z((A = [y] .~ /\ B = [z] .~ ) /\ x = [(y .+ z)] .~ ) /\ E.wE.v((A = [w] .~ /\ B = [v] .~ ) /\ u = [(w .+ v)] .~ )))
2		an4 520	. . . . . . 7 |- ((((A = [y] .~ /\ B = [z] .~ ) /\ x = [(y .+ z)] .~ ) /\ ((A = [w] .~ /\ B = [v] .~ ) /\ u = [(w .+ v)] .~ )) <-> (((A = [y] .~ /\ B = [z] .~ ) /\ (A = [w] .~ /\ B = [v] .~ )) /\ (x = [(y .+ z)] .~ /\ u = [(w .+ v)] .~ )))
3		eleq1 2097	. . . . . . . . . . . . 13 |- (A = [y] .~ -> (A e. ( S /. .~ ) <-> [y] .~ e. ( S /. .~ )))
4		eleq1 2097	. . . . . . . . . . . . 13 |- (B = [z] .~ -> (B e. ( S /. .~ ) <-> [z] .~ e. ( S /. .~ )))
5	3, 4	bi2anan9 538	. . . . . . . . . . . 12 |- ((A = [y] .~ /\ B = [z] .~ ) -> ((A e. ( S /. .~ ) /\ B e. ( S /. .~ )) <-> ([y] .~ e. ( S /. .~ ) /\ [z] .~ e. ( S /. .~ ))))
6	5	adantr 261	. . . . . . . . . . 11 |- (((A = [y] .~ /\ B = [z] .~ ) /\ (A = [w] .~ /\ B = [v] .~ )) -> ((A e. ( S /. .~ ) /\ B e. ( S /. .~ )) <-> ([y] .~ e. ( S /. .~ ) /\ [z] .~ e. ( S /. .~ ))))
7	6	biimpac 282	. . . . . . . . . 10 |- (((A e. ( S /. .~ ) /\ B e. ( S /. .~ )) /\ ((A = [y] .~ /\ B = [z] .~ ) /\ (A = [w] .~ /\ B = [v] .~ ))) -> ([y] .~ e. ( S /. .~ ) /\ [z] .~ e. ( S /. .~ )))
8		eqtr2 2055	. . . . . . . . . . . . 13 |- ((A = [y] .~ /\ A = [w] .~ ) -> [y] .~ = [w] .~ )
9		eqtr2 2055	. . . . . . . . . . . . 13 |- ((B = [z] .~ /\ B = [v] .~ ) -> [z] .~ = [v] .~ )
10	8, 9	anim12i 321	. . . . . . . . . . . 12 |- (((A = [y] .~ /\ A = [w] .~ ) /\ (B = [z] .~ /\ B = [v] .~ )) -> ([y] .~ = [w] .~ /\ [z] .~ = [v] .~ ))
11	10	an4s 522	. . . . . . . . . . 11 |- (((A = [y] .~ /\ B = [z] .~ ) /\ (A = [w] .~ /\ B = [v] .~ )) -> ([y] .~ = [w] .~ /\ [z] .~ = [v] .~ ))
12	11	adantl 262	. . . . . . . . . 10 |- (((A e. ( S /. .~ ) /\ B e. ( S /. .~ )) /\ ((A = [y] .~ /\ B = [z] .~ ) /\ (A = [w] .~ /\ B = [v] .~ ))) -> ([y] .~ = [w] .~ /\ [z] .~ = [v] .~ ))
13		th3qlem1.1	. . . . . . . . . . . 12 |- .~ Er S
14	13	a1i 9	. . . . . . . . . . 11 |- ((([y] .~ e. ( S /. .~ ) /\ [z] .~ e. ( S /. .~ )) /\ ([y] .~ = [w] .~ /\ [z] .~ = [v] .~ )) -> .~ Er S)
15		simprl 483	. . . . . . . . . . . . 13 |- ((([y] .~ e. ( S /. .~ ) /\ [z] .~ e. ( S /. .~ )) /\ ([y] .~ = [w] .~ /\ [z] .~ = [v] .~ )) -> [y] .~ = [w] .~ )
16		erdm 6052	. . . . . . . . . . . . . . . 16 |- ( .~ Er S -> dom .~ = S)
17	13, 16	ax-mp 7	. . . . . . . . . . . . . . 15 |- dom .~ = S
18		simpll 481	. . . . . . . . . . . . . . 15 |- ((([y] .~ e. ( S /. .~ ) /\ [z] .~ e. ( S /. .~ )) /\ ([y] .~ = [w] .~ /\ [z] .~ = [v] .~ )) -> [y] .~ e. ( S /. .~ ))
19		ecelqsdm 6112	. . . . . . . . . . . . . . 15 |- (( dom .~ = S /\ [y] .~ e. ( S /. .~ )) -> y e. S)
20	17, 18, 19	sylancr 393	. . . . . . . . . . . . . 14 |- ((([y] .~ e. ( S /. .~ ) /\ [z] .~ e. ( S /. .~ )) /\ ([y] .~ = [w] .~ /\ [z] .~ = [v] .~ )) -> y e. S)
21	14, 20	erth 6086	. . . . . . . . . . . . 13 |- ((([y] .~ e. ( S /. .~ ) /\ [z] .~ e. ( S /. .~ )) /\ ([y] .~ = [w] .~ /\ [z] .~ = [v] .~ )) -> (y .~ w <-> [y] .~ = [w] .~ ))
22	15, 21	mpbird 156	. . . . . . . . . . . 12 |- ((([y] .~ e. ( S /. .~ ) /\ [z] .~ e. ( S /. .~ )) /\ ([y] .~ = [w] .~ /\ [z] .~ = [v] .~ )) -> y .~ w)
23		simprr 484	. . . . . . . . . . . . 13 |- ((([y] .~ e. ( S /. .~ ) /\ [z] .~ e. ( S /. .~ )) /\ ([y] .~ = [w] .~ /\ [z] .~ = [v] .~ )) -> [z] .~ = [v] .~ )
24		simplr 482	. . . . . . . . . . . . . . 15 |- ((([y] .~ e. ( S /. .~ ) /\ [z] .~ e. ( S /. .~ )) /\ ([y] .~ = [w] .~ /\ [z] .~ = [v] .~ )) -> [z] .~ e. ( S /. .~ ))
25		ecelqsdm 6112	. . . . . . . . . . . . . . 15 |- (( dom .~ = S /\ [z] .~ e. ( S /. .~ )) -> z e. S)
26	17, 24, 25	sylancr 393	. . . . . . . . . . . . . 14 |- ((([y] .~ e. ( S /. .~ ) /\ [z] .~ e. ( S /. .~ )) /\ ([y] .~ = [w] .~ /\ [z] .~ = [v] .~ )) -> z e. S)
27	14, 26	erth 6086	. . . . . . . . . . . . 13 |- ((([y] .~ e. ( S /. .~ ) /\ [z] .~ e. ( S /. .~ )) /\ ([y] .~ = [w] .~ /\ [z] .~ = [v] .~ )) -> (z .~ v <-> [z] .~ = [v] .~ ))
28	23, 27	mpbird 156	. . . . . . . . . . . 12 |- ((([y] .~ e. ( S /. .~ ) /\ [z] .~ e. ( S /. .~ )) /\ ([y] .~ = [w] .~ /\ [z] .~ = [v] .~ )) -> z .~ v)
29	15, 18	eqeltrrd 2112	. . . . . . . . . . . . . 14 |- ((([y] .~ e. ( S /. .~ ) /\ [z] .~ e. ( S /. .~ )) /\ ([y] .~ = [w] .~ /\ [z] .~ = [v] .~ )) -> [w] .~ e. ( S /. .~ ))
30		ecelqsdm 6112	. . . . . . . . . . . . . 14 |- (( dom .~ = S /\ [w] .~ e. ( S /. .~ )) -> w e. S)
31	17, 29, 30	sylancr 393	. . . . . . . . . . . . 13 |- ((([y] .~ e. ( S /. .~ ) /\ [z] .~ e. ( S /. .~ )) /\ ([y] .~ = [w] .~ /\ [z] .~ = [v] .~ )) -> w e. S)
32	23, 24	eqeltrrd 2112	. . . . . . . . . . . . . 14 |- ((([y] .~ e. ( S /. .~ ) /\ [z] .~ e. ( S /. .~ )) /\ ([y] .~ = [w] .~ /\ [z] .~ = [v] .~ )) -> [v] .~ e. ( S /. .~ ))
33		ecelqsdm 6112	. . . . . . . . . . . . . 14 |- (( dom .~ = S /\ [v] .~ e. ( S /. .~ )) -> v e. S)
34	17, 32, 33	sylancr 393	. . . . . . . . . . . . 13 |- ((([y] .~ e. ( S /. .~ ) /\ [z] .~ e. ( S /. .~ )) /\ ([y] .~ = [w] .~ /\ [z] .~ = [v] .~ )) -> v e. S)
35		th3qlem1.3	. . . . . . . . . . . . 13 |- (((y e. S /\ w e. S) /\ (z e. S /\ v e. S)) -> ((y .~ w /\ z .~ v) -> (y .+ z) .~ (w .+ v)))
36	20, 31, 26, 34, 35	syl22anc 1135	. . . . . . . . . . . 12 |- ((([y] .~ e. ( S /. .~ ) /\ [z] .~ e. ( S /. .~ )) /\ ([y] .~ = [w] .~ /\ [z] .~ = [v] .~ )) -> ((y .~ w /\ z .~ v) -> (y .+ z) .~ (w .+ v)))
37	22, 28, 36	mp2and 409	. . . . . . . . . . 11 |- ((([y] .~ e. ( S /. .~ ) /\ [z] .~ e. ( S /. .~ )) /\ ([y] .~ = [w] .~ /\ [z] .~ = [v] .~ )) -> (y .+ z) .~ (w .+ v))
38	14, 37	erthi 6088	. . . . . . . . . 10 |- ((([y] .~ e. ( S /. .~ ) /\ [z] .~ e. ( S /. .~ )) /\ ([y] .~ = [w] .~ /\ [z] .~ = [v] .~ )) -> [(y .+ z)] .~ = [(w .+ v)] .~ )
39	7, 12, 38	syl2anc 391	. . . . . . . . 9 |- (((A e. ( S /. .~ ) /\ B e. ( S /. .~ )) /\ ((A = [y] .~ /\ B = [z] .~ ) /\ (A = [w] .~ /\ B = [v] .~ ))) -> [(y .+ z)] .~ = [(w .+ v)] .~ )
40		eqeq12 2049	. . . . . . . . 9 |- ((x = [(y .+ z)] .~ /\ u = [(w .+ v)] .~ ) -> (x = u <-> [(y .+ z)] .~ = [(w .+ v)] .~ ))
41	39, 40	syl5ibrcom 146	. . . . . . . 8 |- (((A e. ( S /. .~ ) /\ B e. ( S /. .~ )) /\ ((A = [y] .~ /\ B = [z] .~ ) /\ (A = [w] .~ /\ B = [v] .~ ))) -> ((x = [(y .+ z)] .~ /\ u = [(w .+ v)] .~ ) -> x = u))
42	41	expimpd 345	. . . . . . 7 |- ((A e. ( S /. .~ ) /\ B e. ( S /. .~ )) -> ((((A = [y] .~ /\ B = [z] .~ ) /\ (A = [w] .~ /\ B = [v] .~ )) /\ (x = [(y .+ z)] .~ /\ u = [(w .+ v)] .~ )) -> x = u))
43	2, 42	syl5bi 141	. . . . . 6 |- ((A e. ( S /. .~ ) /\ B e. ( S /. .~ )) -> ((((A = [y] .~ /\ B = [z] .~ ) /\ x = [(y .+ z)] .~ ) /\ ((A = [w] .~ /\ B = [v] .~ ) /\ u = [(w .+ v)] .~ )) -> x = u))
44	43	exlimdvv 1774	. . . . 5 |- ((A e. ( S /. .~ ) /\ B e. ( S /. .~ )) -> (E.wE.v(((A = [y] .~ /\ B = [z] .~ ) /\ x = [(y .+ z)] .~ ) /\ ((A = [w] .~ /\ B = [v] .~ ) /\ u = [(w .+ v)] .~ )) -> x = u))
45	44	exlimdvv 1774	. . . 4 |- ((A e. ( S /. .~ ) /\ B e. ( S /. .~ )) -> (E.yE.zE.wE.v(((A = [y] .~ /\ B = [z] .~ ) /\ x = [(y .+ z)] .~ ) /\ ((A = [w] .~ /\ B = [v] .~ ) /\ u = [(w .+ v)] .~ )) -> x = u))
46	1, 45	syl5bir 142	. . 3 |- ((A e. ( S /. .~ ) /\ B e. ( S /. .~ )) -> ((E.yE.z((A = [y] .~ /\ B = [z] .~ ) /\ x = [(y .+ z)] .~ ) /\ E.wE.v((A = [w] .~ /\ B = [v] .~ ) /\ u = [(w .+ v)] .~ )) -> x = u))
47	46	alrimivv 1752	. 2 |- ((A e. ( S /. .~ ) /\ B e. ( S /. .~ )) -> A.xA.u((E.yE.z((A = [y] .~ /\ B = [z] .~ ) /\ x = [(y .+ z)] .~ ) /\ E.wE.v((A = [w] .~ /\ B = [v] .~ ) /\ u = [(w .+ v)] .~ )) -> x = u))
48		eqeq1 2043	. . . . . 6 |- (x = u -> (x = [(y .+ z)] .~ <-> u = [(y .+ z)] .~ ))
49	48	anbi2d 437	. . . . 5 |- (x = u -> (((A = [y] .~ /\ B = [z] .~ ) /\ x = [(y .+ z)] .~ ) <-> ((A = [y] .~ /\ B = [z] .~ ) /\ u = [(y .+ z)] .~ )))
50	49	2exbidv 1745	. . . 4 |- (x = u -> (E.yE.z((A = [y] .~ /\ B = [z] .~ ) /\ x = [(y .+ z)] .~ ) <-> E.yE.z((A = [y] .~ /\ B = [z] .~ ) /\ u = [(y .+ z)] .~ )))
51		eceq1 6077	. . . . . . . 8 |- (y = w -> [y] .~ = [w] .~ )
52	51	eqeq2d 2048	. . . . . . 7 |- (y = w -> (A = [y] .~ <-> A = [w] .~ ))
53		eceq1 6077	. . . . . . . 8 |- (z = v -> [z] .~ = [v] .~ )
54	53	eqeq2d 2048	. . . . . . 7 |- (z = v -> (B = [z] .~ <-> B = [v] .~ ))
55	52, 54	bi2anan9 538	. . . . . 6 |- ((y = w /\ z = v) -> ((A = [y] .~ /\ B = [z] .~ ) <-> (A = [w] .~ /\ B = [v] .~ )))
56		oveq12 5464	. . . . . . . 8 |- ((y = w /\ z = v) -> (y .+ z) = (w .+ v))
57	56	eceq1d 6078	. . . . . . 7 |- ((y = w /\ z = v) -> [(y .+ z)] .~ = [(w .+ v)] .~ )
58	57	eqeq2d 2048	. . . . . 6 |- ((y = w /\ z = v) -> (u = [(y .+ z)] .~ <-> u = [(w .+ v)] .~ ))
59	55, 58	anbi12d 442	. . . . 5 |- ((y = w /\ z = v) -> (((A = [y] .~ /\ B = [z] .~ ) /\ u = [(y .+ z)] .~ ) <-> ((A = [w] .~ /\ B = [v] .~ ) /\ u = [(w .+ v)] .~ )))
60	59	cbvex2v 1796	. . . 4 |- (E.yE.z((A = [y] .~ /\ B = [z] .~ ) /\ u = [(y .+ z)] .~ ) <-> E.wE.v((A = [w] .~ /\ B = [v] .~ ) /\ u = [(w .+ v)] .~ ))
61	50, 60	syl6bb 185	. . 3 |- (x = u -> (E.yE.z((A = [y] .~ /\ B = [z] .~ ) /\ x = [(y .+ z)] .~ ) <-> E.wE.v((A = [w] .~ /\ B = [v] .~ ) /\ u = [(w .+ v)] .~ )))
62	61	mo4 1958	. 2 |- (E*xE.yE.z((A = [y] .~ /\ B = [z] .~ ) /\ x = [(y .+ z)] .~ ) <-> A.xA.u((E.yE.z((A = [y] .~ /\ B = [z] .~ ) /\ x = [(y .+ z)] .~ ) /\ E.wE.v((A = [w] .~ /\ B = [v] .~ ) /\ u = [(w .+ v)] .~ )) -> x = u))
63	47, 62	sylibr 137	1 |- ((A e. ( S /. .~ ) /\ B e. ( S /. .~ )) -> E*xE.yE.z((A = [y] .~ /\ B = [z] .~ ) /\ x = [(y .+ z)] .~ ))

Syntax hints:   -> wi 4   /\ wa 97   <-> wb 98  A.wal 1240   = wceq 1242  E.wex 1378   e. wcel 1390  E*wmo 1898   class class class wbr 3755   dom cdm 4288  (class class class)co 5455   Er wer 6039  [cec 6040   /.cqs 6041

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bndl 1396  ax-4 1397  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-pow 3918  ax-pr 3935

This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rex 2306  df-v 2553  df-sbc 2759  df-un 2916  df-in 2918  df-ss 2925  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-br 3756  df-opab 3810  df-xp 4294  df-rel 4295  df-cnv 4296  df-co 4297  df-dm 4298  df-rn 4299  df-res 4300  df-ima 4301  df-iota 4810  df-fv 4853  df-ov 5458  df-er 6042  df-ec 6044  df-qs 6048

This theorem is referenced by:  th3qlem2  6145