Theorem th3qlem1 3250

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 group(s):   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 388	. . . . . . . . . . . . 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 367	. . . . . . . . . . . 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 388	. . . . . . . . . . . 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 388	. . . . . . . . . . . . . 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 1149	. . . . . . . . . . . . . . . 16 |- (A = [y]R -> (A e. (S/.R) <-> [y]R e. (S/.R)))
6	5	pm5.32ri 490	. . . . . . . . . . . . . . 15 |- ((A e. (S/.R) /\ A = [y]R) <-> ([y]R e. (S/.R) /\ A = [y]R))
7		eleq1 1149	. . . . . . . . . . . . . . . 16 |- (A = [w]R -> (A e. (S/.R) <-> [w]R e. (S/.R)))
8	7	pm5.32ri 490	. . . . . . . . . . . . . . 15 |- ((A e. (S/.R) /\ A = [w]R) <-> ([w]R e. (S/.R) /\ A = [w]R))
9	6, 8	anbi12i 369	. . . . . . . . . . . . . 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 151	. . . . . . . . . . . . 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 388	. . . . . . . . . . . . . 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 1149	. . . . . . . . . . . . . . . 16 |- (B = [z]R -> (B e. (S/.R) <-> [z]R e. (S/.R)))
13	12	pm5.32ri 490	. . . . . . . . . . . . . . 15 |- ((B e. (S/.R) /\ B = [z]R) <-> ([z]R e. (S/.R) /\ B = [z]R))
14		eleq1 1149	. . . . . . . . . . . . . . . 16 |- (B = [v]R -> (B e. (S/.R) <-> [v]R e. (S/.R)))
15	14	pm5.32ri 490	. . . . . . . . . . . . . . 15 |- ((B e. (S/.R) /\ B = [v]R) <-> ([v]R e. (S/.R) /\ B = [v]R))
16	13, 15	anbi12i 369	. . . . . . . . . . . . . 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 151	. . . . . . . . . . . . 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 369	. . . . . . . . . . . 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 155	. . . . . . . . . . 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 256	. . . . . . . . . . . . . . . . . . . . 21 |- ((y e. S /\ w e. S) -> y e. S)
21		th3qlem1.2	. . . . . . . . . . . . . . . . . . . . . 22 |- dom R = S
22	21	eleq2i 1153	. . . . . . . . . . . . . . . . . . . . 21 |- (y e. dom R <-> y e. S)
23	20, 22	sylibr 175	. . . . . . . . . . . . . . . . . . . 20 |- ((y e. S /\ w e. S) -> y e. dom R)
24		visset 1350	. . . . . . . . . . . . . . . . . . . . 21 |- w e. V
25		th3qlem1.1	. . . . . . . . . . . . . . . . . . . . 21 |- Er R
26	24, 25	erthdm 3220	. . . . . . . . . . . . . . . . . . . 20 |- (y e. dom R -> ([y]R = [w]R <-> yRw))
27	23, 26	syl 12	. . . . . . . . . . . . . . . . . . 19 |- ((y e. S /\ w e. S) -> ([y]R = [w]R <-> yRw))
28		pm3.26 256	. . . . . . . . . . . . . . . . . . . . 21 |- ((z e. S /\ v e. S) -> z e. S)
29	21	eleq2i 1153	. . . . . . . . . . . . . . . . . . . . 21 |- (z e. dom R <-> z e. S)
30	28, 29	sylibr 175	. . . . . . . . . . . . . . . . . . . 20 |- ((z e. S /\ v e. S) -> z e. dom R)
31		visset 1350	. . . . . . . . . . . . . . . . . . . . 21 |- v e. V
32	31, 25	erthdm 3220	. . . . . . . . . . . . . . . . . . . 20 |- (z e. dom R -> ([z]R = [v]R <-> zRv))
33	30, 32	syl 12	. . . . . . . . . . . . . . . . . . 19 |- ((z e. S /\ v e. S) -> ([z]R = [v]R <-> zRv))
34	27, 33	bi2anan9 478	. . . . . . . . . . . . . . . . . 18 |- (((y e. S /\ w e. S) /\ (z e. S /\ v e. S)) -> (([y]R = [w]R /\ [z]R = [v]R) <-> (yRw /\ zRv)))
35		th3qlem1.3	. . . . . . . . . . . . . . . . . 18 |- (((y e. S /\ w e. S) /\ (z e. S /\ v e. S)) -> ((yRw /\ zRv) -> (yFz)R(wFv)))
36	34, 35	sylbid 178	. . . . . . . . . . . . . . . . 17 |- (((y e. S /\ w e. S) /\ (z e. S /\ v e. S)) -> (([y]R = [w]R /\ [z]R = [v]R) -> (yFz)R(wFv)))
37		cleq12 1113	. . . . . . . . . . . . . . . . . 18 |- ((x = [(yFz)]R /\ u = [(wFv)]R) -> (x = u <-> [(yFz)]R = [(wFv)]R))
38		oprex 3018	. . . . . . . . . . . . . . . . . . 19 |- (yFz) e. V
39		oprex 3018	. . . . . . . . . . . . . . . . . . 19 |- (wFv) e. V
40	38, 39, 25	erthi 3218	. . . . . . . . . . . . . . . . . 18 |- ((yFz)R(wFv) -> [(yFz)]R = [(wFv)]R)
41	37, 40	syl5bir 184	. . . . . . . . . . . . . . . . 17 |- ((x = [(yFz)]R /\ u = [(wFv)]R) -> ((yFz)R(wFv) -> x = u))
42	36, 41	syl9 55	. . . . . . . . . . . . . . . 16 |- (((y e. S /\ w e. S) /\ (z e. S /\ v e. S)) ->