Theorem th3qlem1 4314

Description: Lemma for Exercise 44 version of Theorem 3Q of [Enderton] p. 60. The third hypothesis is the compatibility assumption.

Hypotheses

Ref	Expression
th3qlem1.1	|- Er R
th3qlem1.2	|- dom R = S
th3qlem1.3	|- (((y e. S /\ w e. S) /\ (z e. S /\ v e. S)) -> ((yRw /\ zRv) -> (yFz)R(wFv)))

Assertion

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

Distinct variable groups:   x,y,z,w,v,F   x,R,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

Step	Hyp	Ref	Expression
1		an4 506	. . . . . . . . . . . . 13 |- (((A = [y]R /\ B = [z]R) /\ (A = [w]R /\ B = [v]R)) <-> ((A = [y]R /\ A = [w]R) /\ (B = [z]R /\ B = [v]R)))
2	1	anbi2i 480	. . . . . . . . . . . 12 |- ((((A e. (S/.R) /\ A e. (S/.R)) /\ (B e. (S/.R) /\ B e. (S/.R))) /\ ((A = [y]R /\ B = [z]R) /\ (A = [w]R /\ B = [v]R))) <-> (((A e. (S/.R) /\ A e. (S/.R)) /\ (B e. (S/.R) /\ B e. (S/.R))) /\ ((A = [y]R /\ A = [w]R) /\ (B = [z]R /\ B = [v]R))))
3		an4 506	. . . . . . . . . . . 12 |- ((((A e. (S/.R) /\ A e. (S/.R)) /\ (B e. (S/.R) /\ B e. (S/.R))) /\ ((A = [y]R /\ A = [w]R) /\ (B = [z]R /\ B = [v]R))) <-> (((A e. (S/.R) /\ A e. (S/.R)) /\ (A = [y]R /\ A = [w]R)) /\ ((B e. (S/.R) /\ B e. (S/.R)) /\ (B = [z]R /\ B = [v]R))))
4		an4 506	. . . . . . . . . . . . . 14 |- (((A e. (S/.R) /\ A e. (S/.R)) /\ (A = [y]R /\ A = [w]R)) <-> ((A e. (S/.R) /\ A = [y]R) /\ (A e. (S/.R) /\ A = [w]R)))
5		eleq1 1534	. . . . . . . . . . . . . . . 16 |- (A = [y]R -> (A e. (S/.R) <-> [y]R e. (S/.R)))
6	5	pm5.32ri 646	. . . . . . . . . . . . . . 15 |- ((A e. (S/.R) /\ A = [y]R) <-> ([y]R e. (S/.R) /\ A = [y]R))
7		eleq1 1534	. . . . . . . . . . . . . . . 16 |- (A = [w]R -> (A e. (S/.R) <-> [w]R e. (S/.R)))
8	7	pm5.32ri 646	. . . . . . . . . . . . . . 15 |- ((A e. (S/.R) /\ A = [w]R) <-> ([w]R e. (S/.R) /\ A = [w]R))
9	6, 8	anbi12i 482	. . . . . . . . . . . . . 14 |- (((A e. (S/.R) /\ A = [y]R) /\ (A e. (S/.R) /\ A = [w]R)) <-> (([y]R e. (S/.R) /\ A = [y]R) /\ ([w]R e. (S/.R) /\ A = [w]R)))
10	4, 9	bitr 173	. . . . . . . . . . . . 13 |- (((A e. (S/.R) /\ A e. (S/.R)) /\ (A = [y]R /\ A = [w]R)) <-> (([y]R e. (S/.R) /\ A = [y]R) /\ ([w]R e. (S/.R) /\ A = [w]R)))
11		an4 506	. . . . . . . . . . . . . 14 |- (((B e. (S/.R) /\ B e. (S/.R)) /\ (B = [z]R /\ B = [v]R)) <-> ((B e. (S/.R) /\ B = [z]R) /\ (B e. (S/.R) /\ B = [v]R)))
12		eleq1 1534	. . . . . . . . . . . . . . . 16 |- (B = [z]R -> (B e. (S/.R) <-> [z]R e. (S/.R)))
13	12	pm5.32ri 646	. . . . . . . . . . . . . . 15 |- ((B e. (S/.R) /\ B = [z]R) <-> ([z]R e. (S/.R) /\ B = [z]R))
14		eleq1 1534	. . . . . . . . . . . . . . . 16 |- (B = [v]R -> (B e. (S/.R) <-> [v]R e. (S/.R)))
15	14	pm5.32ri 646	. . . . . . . . . . . . . . 15 |- ((B e. (S/.R) /\ B = [v]R) <-> ([v]R e. (S/.R) /\ B = [v]R))
16	13, 15	anbi12i 482	. . . . . . . . . . . . . 14 |- (((B e. (S/.R) /\ B = [z]R) /\ (B e. (S/.R) /\ B = [v]R)) <-> (([z]R e. (S/.R) /\ B = [z]R) /\ ([v]R e. (S/.R) /\ B = [v]R)))
17	11, 16	bitr 173	. . . . . . . . . . . . 13 |- (((B e. (S/.R) /\ B e. (S/.R)) /\ (B = [z]R /\ B = [v]R)) <-> (([z]R e. (S/.R) /\ B = [z]R) /\ ([v]R e. (S/.R) /\ B = [v]R)))
18	10, 17	anbi12i 482	. . . . . . . . . . . 12 |- ((((A e. (S/.R) /\ A e. (S/.R)) /\ (A = [y]R /\ A = [w]R)) /\ ((B e. (S/.R) /\ B e. (S/.R)) /\ (B = [z]R /\ B = [v]R))) <-> ((([y]R e. (S/.R) /\ A = [y]R) /\ ([w]R e. (S/.R) /\ A = [w]R)) /\ (([z]R e. (S/.R) /\ B = [z]R) /\ ([v]R e. (S/.R) /\ B = [v]R))))
19	2, 3, 18	3bitr 177	. . . . . . . . . . 11 |- ((((A e. (S/.R) /\ A e. (S/.R)) /\ (B e. (S/.R) /\ B e. (S/.R))) /\ ((A = [y]R /\ B = [z]R) /\ (A = [w]R /\ B = [v]R))) <-> ((([y]R e. (S/.R) /\ A = [y]R) /\ ([w]R e. (S/.R) /\ A = [w]R)) /\ (([z]R e. (S/.R) /\ B = [z]R) /\ ([v]R e. (S/.R) /\ B = [v]R))))
20		pm3.26 319	. . . . . . . . . . . . . . . . . . . . 21 |- ((y e. S /\ w e. S) -> y e. S)
21		th3qlem1.2	. . . . . . . . . . . . . . . . . . . . 21 |- dom R = S
22	20, 21	syl6eleqr 1559	. . . . . . . . . . . . . . . . . . . 20 |- ((y e. S /\ w e. S) -> y e. dom R)
23		visset 1813	. . . . . . . . . . . . . . . . . . . . 21 |- w e. V
24		th3qlem1.1	. . . . . . . . . . . . . . . . . . . . 21 |- Er R
25	23, 24	erthdm 4283	. . . . . . . . . . . . . . . . . . . 20 |- (y e. dom R -> ([y]R = [w]R <-> yRw))
26	22, 25	syl 10	. . . . . . . . . . . . . . . . . . 19 |- ((y e. S /\ w e. S) -> ([y]R = [w]R <-> yRw))
27		pm3.26 319	. . . . . . . . . . . . . . . . . . . . 21 |- ((z e. S /\ v e. S) -> z e. S)
28	27, 21	syl6eleqr 1559	. . . . . . . . . . . . . . . . . . . 20 |- ((z e. S /\ v e. S) -> z e. dom R)
29		visset 1813	. . . . . . . . . . . . . . . . . . . . 21 |- v e. V
30	29, 24	erthdm 4283	. . . . . . . . . . . . . . . . . . . 20 |- (z e. dom R -> ([z]R = [v]R <-> zRv))
31	28, 30	syl 10	. . . . . . . . . . . . . . . . . . 19 |- ((z e. S /\ v e. S) -> ([z]R = [v]R <-> zRv))
32	26, 31	bi2anan9 632	. . . . . . . . . . . . . . . . . 18 |- (((y e. S /\ w e. S) /\ (z e. S /\ v e. S)) -> (([y]R = [w]R /\ [z]R = [v]R) <-> (yRw /\ zRv)))
33		th3qlem1.3	. . . . . . . . . . . . . . . . . 18 |- (((y e. S /\ w e. S) /\ (z e. S /\ v e. S)) -> ((yRw /\ zRv) -> (yFz)R(wFv)))
34	32, 33	sylbid 203	. . . . . . . . . . . . . . . . 17 |- (((y e. S /\ w e. S) /\ (z e. S /\ v e. S)) -> (([y]R = [w]R /\ [z]R = [v]R) -> (yFz)R(wFv)))
35		eqeq12 1487	. . . . . . . . . . . . . . . . . 18 |- ((x = [(yFz)]R /\ u = [(wFv)]R) -> (x = u <-> [(yFz)]R = [(wFv)]R))
36		oprex 3983	. . . . . . . . . . . . . . . . . . 19 |- (yFz) e. V
37		oprex 3983	. . . . . . . . . . . . . . . . . . 19 |- (wFv) e. V
38	36, 37, 24	erthi 4281	. . . . . . . . . . . . . . . . . 18 |- ((yFz)R(wFv) -> [(yFz)]R = [(wFv)]R)
39	35, 38	syl5bir 210	. . . . . . . . . . . . . . . . 17 |- ((x = [(yFz)]R /\ u = [(wFv)]R) -> ((yFz)R(wFv) -> x = u))
40	34, 39	syl9 57	. . . . . . . . . . . . . . . 16 |- (((y e. S /\ w e. S)