Theorem islatalg 14531

Description: The predicate "is a lattice".

Hypothesis

Ref	Expression
islatalg.1	|- X = dom dom J

Assertion

Ref	Expression
islatalg	|- ((J e. A /\ M e. B) -> (<.J, M>. e. LatAlg <-> (J:(X X. X)-->X /\ M:(X X. X)-->X /\ A.x e. X A.y e. X ((xJy) = (yJx) /\ (xMy) = (yMx) /\ ((xM(xJy)) = x /\ (xJ(xMy)) = x /\ A.z e. X ((xM(yMz)) = ((xMy)Mz) /\ (xJ(yJz)) = ((xJy)Jz)))))))

Distinct variable groups:   x,J,y,z   x,M,y,z   x,X,y,z

Proof of Theorem islatalg

Step	Hyp	Ref	Expression
1		df-latalg 14530	. . . 4 |- LatAlg = {<.j, m>. | E.t(j:(t X. t)-->t /\ m:(t X. t)-->t /\ A.x e. t A.y e. t ((xjy) = (yjx) /\ (xmy) = (ymx) /\ ((xm(xjy)) = x /\ (xj(xmy)) = x /\ A.z e. t ((xm(ymz)) = ((xmy)mz) /\ (xj(yjz)) = ((xjy)jz)))))}
2	1	a1i 8	. . 3 |- ((J e. A /\ M e. B) -> LatAlg = {<.j, m>. | E.t(j:(t X. t)-->t /\ m:(t X. t)-->t /\ A.x e. t A.y e. t ((xjy) = (yjx) /\ (xmy) = (ymx) /\ ((xm(xjy)) = x /\ (xj(xmy)) = x /\ A.z e. t ((xm(ymz)) = ((xmy)mz) /\ (xj(yjz)) = ((xjy)jz)))))})
3	2	eleq2d 1964	. 2 |- ((J e. A /\ M e. B) -> (<.J, M>. e. LatAlg <-> <.J, M>. e. {<.j, m>. | E.t(j:(t X. t)-->t /\ m:(t X. t)-->t /\ A.x e. t A.y e. t ((xjy) = (yjx) /\ (xmy) = (ymx) /\ ((xm(xjy)) = x /\ (xj(xmy)) = x /\ A.z e. t ((xm(ymz)) = ((xmy)mz) /\ (xj(yjz)) = ((xjy)jz)))))}))
4		fdm 4567	. . . . . . . . 9 |- (j:(t X. t)-->t -> dom j = (t X. t))
5		dmeq 4157	. . . . . . . . . . 11 |- ((t X. t) = dom j -> dom ( t X. t) = dom dom j)
6		dmxpid 4179	. . . . . . . . . . 11 |- dom ( t X. t) = t
7	5, 6	syl5eqr 1942	. . . . . . . . . 10 |- ((t X. t) = dom j -> t = dom dom j)
8	7	eqcoms 1887	. . . . . . . . 9 |- (dom j = (t X. t) -> t = dom dom j)
9	4, 8	syl 12	. . . . . . . 8 |- (j:(t X. t)-->t -> t = dom dom j)
10	9	3ad2ant1 897	. . . . . . 7 |- ((j:(t X. t)-->t /\ m:(t X. t)-->t /\ A.x e. t A.y e. t ((xjy) = (yjx) /\ (xmy) = (ymx) /\ ((xm(xjy)) = x /\ (xj(xmy)) = x /\ A.z e. t ((xm(ymz)) = ((xmy)mz) /\ (xj(yjz)) = ((xjy)jz))))) -> t = dom dom j)
11	10	pm4.71ri 700	. . . . . 6 |- ((j:(t X. t)-->t /\ m:(t X. t)-->t /\ A.x e. t A.y e. t ((xjy) = (yjx) /\ (xmy) = (ymx) /\ ((xm(xjy)) = x /\ (xj(xmy)) = x /\ A.z e. t ((xm(ymz)) = ((xmy)mz) /\ (xj(yjz)) = ((xjy)jz))))) <-> (t = dom dom j /\ (j:(t X. t)-->t /\ m:(t X. t)-->t /\ A.x e. t A.y e. t ((xjy) = (yjx) /\ (xmy) = (ymx) /\ ((xm(xjy)) = x /\ (xj(xmy)) = x /\ A.z e. t ((xm(ymz)) = ((xmy)mz) /\ (xj(yjz)) = ((xjy)jz)))))))
12	11	exbii 1398	. . . . 5 |- (E.t(j:(t X. t)-->t /\ m:(t X. t)-->t /\ A.x e. t A.y e. t ((xjy) = (yjx) /\ (xmy) = (ymx) /\ ((xm(xjy)) = x /\ (xj(xmy)) = x /\ A.z e. t ((xm(ymz)) = ((xmy)mz) /\ (xj(yjz)) = ((xjy)jz))))) <-> E.t(t = dom dom j /\ (j:(t X. t)-->t /\ m:(t X. t)-->t /\ A.x e. t A.y e. t ((xjy) = (yjx) /\ (xmy) = (ymx) /\ ((xm(xjy)) = x /\ (xj(xmy)) = x /\ A.z e. t ((xm(ymz)) = ((xmy)mz) /\ (xj(yjz)) = ((xjy)jz)))))))
13	12	a1i 8	. . . 4 |- (j = J -> (E.t(j:(t X. t)-->t /\ m:(t X. t)-->t /\ A.x e. t A.y e. t ((xjy) = (yjx) /\ (xmy) = (ymx) /\ ((xm(xjy)) = x /\ (xj(xmy)) = x /\ A.z e. t ((xm(ymz)) = ((xmy)mz) /\ (xj(yjz)) = ((xjy)jz))))) <-> E.t(t = dom dom j /\ (j:(t X. t)-->t /\ m:(t X. t)-->t /\ A.x e. t A.y e. t ((xjy) = (yjx) /\ (xmy) = (ymx) /\ ((xm(xjy)) = x /\ (xj(xmy)) = x /\ A.z e. t ((xm(ymz)) = ((xmy)mz) /\ (xj(yjz)) = ((xjy)jz))))))))
14		dmeq 4157	. . . . . . . . 9 |- (j = J -> dom j = dom J)
15	14	dmeqd 4159	. . . . . . . 8 |- (j = J -> dom dom j = dom dom J)
16	15	eqeq2d 1895	. . . . . . 7 |- (j = J -> (t = dom dom j <-> t = dom dom J))
17		feq1 4551	. . . . . . . 8 |- (j = J -> (j:(t X. t)-->t <-> J:(t X. t)-->t))
18		opreq 4888	. . . . . . . . . . . 12 |- (j = J -> (xjy) = (xJy))
19		opreq 4888	. . . . . . . . . . . 12 |- (j = J -> (yjx) = (yJx))
20	18, 19	eqeq12d 1899	. . . . . . . . . . 11 |- (j = J -> ((xjy) = (yjx) <-> (xJy) = (yJx)))
21	18	opreq2d 4898	. . . . . . . . . . . . 13 |- (j = J -> (xm(xjy)) = (xm(xJy)))
22	21	eqeq1d 1892	. . . . . . . . . . . 12 |- (j = J -> ((xm(xjy)) = x <-> (xm(xJy)) = x))
23		opreq 4888	. . . . . . . . . . . . 13 |- (j = J -> (xj(xmy)) = (xJ(xmy)))
24	23	eqeq1d 1892	. . . . . . . . . . . 12 |- (j = J -> ((xj(xmy)) = x <-> (xJ(xmy)) = x))
25		id 73	. . . . . . . . . . . . . . . 16 |- (j = J -> j = J)
26		eqidd 1885	. . . . . . . . . . . . . . . 16 |- (j = J -> x = x)
27		opreq 4888	. . . . . . . . . . . . . . . 16 |- (j = J -> (yjz) = (yJz))
28	25, 26, 27	opreq123d 10153	. . . . . . . . . . . . . . 15 |- (j = J -> (xj(yjz)) = (xJ(yJz)))
29		eqidd 1885	. . . . . . . . . . . . . . . 16 |- (j = J -> z = z)
30	25, 18, 29	opreq123d 10153	. . . . . . . . . . . . . . 15 |- (j = J -> ((xjy)jz) = ((xJy)Jz))
31	28, 30	eqeq12d 1899	. . . . . . . . . . . . . 14 |- (j = J -> ((xj(yjz)) = ((xjy)jz) <-> (xJ(yJz)) = ((xJy)Jz)))
32	31	anbi2d 678	. . . . . . . . . . . . 13 |- (j = J -> (((xm(ymz)) = ((xmy)mz) /\ (xj(yjz)) = ((xjy)jz)) <-> ((xm(ymz)) = ((xmy)mz) /\ (xJ(yJz)) = ((xJy)Jz))))
33	32	ralbidv 2123	. . . . . . . . . . . 12 |- (j = J -> (A.z e. t ((xm(ymz)) = ((xmy)mz) /\ (xj(yjz)) = ((xjy)jz)) <-> A.z e. t ((xm(ymz)) = ((xmy)mz) /\ (xJ(yJz)) = ((xJy)Jz))))
34	22, 24, 33	3anbi123d 1168	. . . . . . . . . . 11 |- (j = J -> (((xm(xjy)) = x /\ (xj(xmy)) = x /\ A.z e. t ((xm(ymz)) = ((xmy)mz) /\ (xj(yjz)) = ((xjy)jz))) <-> ((xm(xJy)) = x /\ (xJ(xmy)) = x /\ A.z e. t ((xm(ymz)) = ((xmy)mz) /\ (xJ(yJz)) = ((xJy)Jz)))))
35	20, 34	3anbi13d 1170	. . . . . . . . . 10 |- (j = J -> (((xjy) = (yjx) /\ (xmy) = (ymx) /\ ((xm(xjy)) = x /\ (xj(xmy)) = x /\ A.z e. t ((xm(ymz)) = ((xmy)mz) /\ (xj(yjz)) = ((xjy)jz)))) <-> ((xJy) = (yJx) /\ (xmy) = (ymx) /\ ((xm(xJy)) = x /\ (xJ(xmy)) = x /\ A.z e. t ((xm(ymz)) = ((xmy)mz) /\ (xJ(yJz)) = ((xJy)Jz))))))
36	35	ralbidv 2123	. . . . . . . . 9 |- (j = J -> (A.y e. t ((xjy) = (yjx) /\ (xmy) = (ymx) /\ ((xm(xjy)) = x /\ (xj(xmy)) = x /\ A.z e. t ((xm(ymz)) = ((xmy)mz) /\ (xj(yjz)) = ((xjy)jz)))) <-> A.y e. t ((xJy) = (yJx) /\ (xmy) = (ymx) /\ ((xm(xJy)) = x /\ (xJ(xmy)) = x /\ A.z e. t ((xm(ymz)) = ((xmy)mz) /\ (xJ(yJz)) = ((xJy)Jz))))))
37	36	ralbidv 2123	. . . . . . . 8 |- (j = J -> (A.x e. t A.y e. t ((xjy) = (yjx) /\ (xmy) = (ymx) /\ ((xm(xjy)) = x /\ (xj(xmy)) = x /\ A.z e. t ((xm(ymz)) = ((xmy)mz) /\ (xj(yjz)) = ((xjy)jz)))) <-> A.x e. t A.y e. t ((xJy) = (yJx) /\ (xmy) = (ymx) /\ ((xm(xJy)) = x /\ (xJ(xmy)) = x /\ A.z e. t ((xm(ymz)) = ((xmy)mz) /\ (xJ(yJz)) = ((xJy)Jz))))))
38	17, 37	3anbi13d 1170	. . . . . . 7 |- (j = J -> ((j:(t X. t)-->t /\ m:(t X. t)-->t /\ A.x e. t A.y e. t ((xjy) = (yjx) /\ (xmy) = (ymx) /\ ((xm(xjy)) = x /\ (xj(xmy)) = x /\ A.z e. t ((xm(ymz)) = ((xmy)mz) /\ (xj(yjz)) = ((xjy)jz))))) <-> (J:(t X. t)-->t /\ m:(t X. t)-->t /\ A.x e. t A.y e. t ((xJy) = (yJx) /\ (xmy) = (ymx) /\ ((xm(xJy)) = x /\ (xJ(xmy)) = x /\ A.z e. t ((xm(ymz)) = ((xmy)mz) /\ (xJ(yJz)) = ((xJy)Jz)))))))
39	16, 38	anbi12d 690	. . . . . 6 |- (j = J -> ((t = dom dom j /\ (j:(t X. t)-->t /\ m:(t X. t)-->t /\ A.x e. t A.y e. t ((xjy) = (yjx) /\ (xmy) = (ymx) /\ ((xm(xjy)) = x /\ (xj(xmy)) = x /\ A.z e. t ((xm(ymz)) = ((xmy)mz) /\ (xj(yjz)) = ((xjy)jz)))))) <-> (t = dom dom J /\ (J:(t X. t)-->t /\ m:(t X. t)-->t /\ A.x e. t A.y e. t ((xJy) = (yJx) /\ (xmy) = (ymx) /\ ((xm(xJy)) = x /\ (xJ(xmy)) = x /\ A.z e. t ((xm(ymz)) = ((xmy)mz) /\ (xJ(yJz)) = ((xJy)Jz))))))))
40	39	exbidv 1657	. . . . 5 |- (j = J -> (E.t(t = dom dom j /\ (j:(t X. t)-->t /\ m:(t X. t)-->t /\ A.x e. t A.y e. t ((xjy) = (yjx) /\ (xmy) = (ymx) /\ ((xm(xjy)) = x /\ (xj(xmy)) = x /\ A.z e. t ((xm(ymz)) = ((xmy)mz) /\ (xj(yjz)) = ((xjy)jz)))))) <-> E.t(t = dom dom J /\ (J:(t X. t)-->t /\ m:(t X. t)-->t /\ A.x e. t A.y e. t ((xJy) = (yJx) /\ (xmy) = (ymx) /\ ((xm(xJy)) = x /\ (xJ(xmy)) = x /\ A.z e. t ((xm(ymz)) = ((xmy)mz) /\ (xJ(yJz)) = ((xJy)Jz))))))))
41		islatalg.1	. . . . . . . . . 10 |- X = dom dom J
42	41	eqcomi 1888	. . . . . . . . 9 |- dom dom J = X
43	42	eqeq2i 1894	. . . . . . . 8 |- (t = dom dom J <-> t = X)
44	43	a1i 8	. . . . . . 7 |- (j = J -> (t = dom dom J <-> t = X))
45	44	anbi1d 679	. . . . . 6 |- (j = J -> ((t = dom dom J /\ (J:(t X. t)-->t /\ m:(t X. t)-->t /\ A.x e. t A.y e. t ((xJy) = (yJx) /\ (xmy) = (ymx) /\ ((xm(xJy)) = x /\ (xJ(xmy)) = x /\ A.z e. t ((xm(ymz)) = ((xmy)mz) /\ (xJ(yJz)) = ((xJy)Jz)))))) <-> (t = X /\ (J:(t X. t)-->t /\ m:(t X. t)-->t /\ A.x e. t A.y e. t ((xJy) = (yJx) /\ (xmy) = (ymx) /\ ((xm(xJy)) = x /\ (xJ(xmy)) = x /\ A.z e. t ((xm(ymz)) = ((xmy)mz) /\ (xJ(yJz)) = ((xJy)Jz))))))))
46	45	exbidv 1657	. . . . 5 |- (j = J -> (E.t(t = dom dom J /\ (J:(t X. t)-->t /\ m:(t X. t)-->t /\ A.x e. t A.y e. t ((xJy) = (yJx) /\ (xmy) = (ymx) /\ ((xm(xJy)) = x /\ (xJ(xmy)) = x /\ A.z e. t ((xm(ymz)) = ((xmy)mz) /\ (xJ(yJz)) = ((xJy)Jz)))))) <-> E.t(t = X /\ (J:(t X. t)-->t /\ m:(t X. t)-->t /\ A.x e. t A.y e. t ((xJy) = (yJx) /\ (xmy) = (ymx) /\ ((xm(xJy)) = x /\ (xJ(xmy)) = x /\ A.z e. t ((xm(ymz)) = ((xmy)mz) /\ (xJ(yJz)) = ((xJy)Jz))))))))
47	40, 46	bitrd 587	. . . 4 |- (j = J -> (E.t(t = dom dom j /\ (j:(t X. t)-->t /\ m:(t X. t)-->t /\ A.x e. t A.y e. t ((xjy) = (yjx) /\ (xmy) = (ymx) /\ ((xm(xjy)) = x /\ (xj(xmy)) = x /\ A.z e. t ((xm(ymz)) = ((xmy)mz) /\ (xj(yjz)) = ((xjy)jz)))))) <-> E.t(t = X /\ (J:(t X. t)-->t /\ m:(t X. t)-->t /\ A.x e. t A.y e. t ((xJy) = (yJx) /\ (xmy) = (ymx) /\ ((xm(xJy)) = x /\ (xJ(xmy)) = x /\ A.z e. t ((xm(ymz)) = ((xmy)mz) /\ (xJ(yJz)) = ((xJy)Jz))))))))
48		dmeq 4157	. . . . . 6 |- (dom j = dom J -> dom dom j = dom dom J)
49		visset 2295	. . . . . . . . 9 |- j e. _V
50	49	dmex 4208	. . . . . . . 8 |- dom j e. _V
51	50	dmex 4208	. . . . . . 7 |- dom dom j e. _V
52		eleq1 1957	. . . . . . . . 9 |- (dom dom j = dom dom J -> (dom dom j e. _V <-> dom dom J e. _V))
53	52	biimpd 170	. . . . . . . 8 |- (dom dom j = dom dom J -> (dom dom j e. _V -> dom dom J e. _V))
54	42	eleq1i 1960	. . . . . . . 8 |- (dom dom J e. _V <-> X e. _V)
55	53, 54	syl6ib 229	. . . . . . 7 |- (dom dom j = dom dom J -> (dom dom j e. _V -> X e. _V))
56	51, 55	mpi 55	. . . . . 6 |- (dom dom j = dom dom J -> X e. _V)
57	14, 48, 56	3syl 24	. . . . 5 |- (j = J -> X e. _V)
58		xpeq12 4020	. . . . . . . . 9 |- ((t = X /\ t = X) -> (t X. t) = (X X. X))
59	58	anidms 480	. . . . . . . 8 |- (t = X -> (t X. t) = (X X. X))
60		feq23 4554	. . . . . . . 8 |- (((t X. t) = (X X. X) /\ t = X) -> (J:(t X. t)-->t <-> J:(X X. X)-->X))
61	59, 60	mpancom 769	. . . . . . 7 |- (t = X -> (J:(t X. t)-->t <-> J:(X X. X)-->X))
62		feq23 4554	. . . . . . . 8 |- (((t X. t) = (X X. X) /\ t = X) -> (m:(t X. t)-->t <-> m:(X X. X)-->X))
63	59, 62	mpancom 769	. . . . . . 7 |- (t = X -> (m:(t X. t)-->t <-> m:(X X. X)-->X))
64		id 73	. . . . . . . 8 |- (t = X -> t = X)
65		raleq 2266	. . . . . . . . . . 11 |- (t = X -> (A.z e. t ((xm(ymz)) = ((xmy)mz) /\ (xJ(yJz)) = ((xJy)Jz)) <-> A.z e. X ((xm(ymz)) = ((xmy)mz) /\ (xJ(yJz)) = ((xJy)Jz))))
66	65	3anbi3d 1174	. . . . . . . . . 10 |- (t = X -> (((xm(xJy)) = x /\ (xJ(xmy)) = x /\ A.z e. t ((xm(ymz)) = ((xmy)mz) /\ (xJ(yJz)) = ((xJy)Jz))) <-> ((xm(xJy)) = x /\ (xJ(xmy)) = x /\ A.z e. X ((xm(ymz)) = ((xmy)mz) /\ (xJ(yJz)) = ((xJy)Jz)))))
67	66	3anbi3d 1174	. . . . . . . . 9 |- (t = X -> (((xJy) = (yJx) /\ (xmy) = (ymx) /\ ((xm(xJy)) = x /\ (xJ(xmy)) = x /\ A.z e. t ((xm(ymz)) = ((xmy)mz) /\ (xJ(yJz)) = ((xJy)Jz)))) <-> ((xJy) = (yJx) /\ (xmy) = (ymx) /\ ((xm(xJy)) = x /\ (xJ(xmy)) = x /\ A.z e. X ((xm(ymz)) = ((xmy)mz) /\ (xJ(yJz)) = ((xJy)Jz))))))
68	64, 67	raleqbidv 2274	. . . . . . . 8 |- (t = X -> (A.y e. t ((xJy) = (yJx) /\ (xmy) = (ymx) /\ ((xm(xJy)) = x /\ (xJ(xmy)) = x /\ A.z e. t ((xm(ymz)) = ((xmy)mz) /\ (xJ(yJz)) = ((xJy)Jz)))) <-> A.y e. X ((xJy) = (yJx) /\ (xmy) = (ymx) /\ ((xm(xJy)) = x /\ (xJ(xmy)) = x /\ A.z e. X ((xm(ymz)) = ((xmy)mz) /\ (xJ(yJz)) = ((xJy)Jz))))))
69	64, 68	raleqbidv 2274	. . . . . . 7 |- (t = X -> (A.x e. t A.y e. t ((xJy) = (yJx) /\ (xmy) = (ymx) /\ ((xm(xJy)) = x /\ (xJ(xmy)) = x /\ A.z e. t ((xm(ymz)) = ((xmy)mz) /\ (xJ(yJz)) = ((xJy)Jz)))) <-> A.x e. X A.y e. X ((xJy) = (yJx) /\ (xmy) = (ymx) /\ ((xm(xJy)) = x /\ (xJ(xmy)) = x /\ A.z e. X ((xm(ymz)) = ((xmy)mz) /\ (xJ(yJz)) = ((xJy)Jz))))))
70	61, 63, 69	3anbi123d 1168	. . . . . 6 |- (t = X -> ((J:(t X. t)-->t /\ m:(t X. t)-->t /\ A.x e. t A.y e. t ((xJy) = (yJx) /\ (xmy) = (ymx) /\ ((xm(xJy)) = x /\ (xJ(xmy)) = x /\ A.z e. t ((xm(ymz)) = ((xmy)mz) /\ (xJ(yJz)) = ((xJy)Jz))))) <-> (J:(X X. X)-->X /\ m:(X X. X)-->X /\ A.x e. X A.y e. X ((xJy) = (yJx) /\ (xmy) = (ymx) /\ ((xm(xJy)) = x /\ (xJ(xmy)) = x /\ A.z e. X ((xm(ymz)) = ((xmy)mz) /\ (xJ(yJz)) = ((xJy)Jz)))))))
71	70	ceqsexgv 2393	. . . . 5 |- (X e. _V -> (E.t(t = X /\ (J:(t X. t)-->t /\ m:(t X. t)-->t /\ A.x e. t A.y e. t ((xJy) = (yJx) /\ (xmy) = (ymx) /\ ((xm(xJy)) = x /\ (xJ(xmy)) = x /\ A.z e. t ((xm(ymz)) = ((xmy)mz) /\ (xJ(yJz)) = ((xJy)Jz)))))) <-> (J:(X X. X)-->X /\ m:(X X. X)-->X /\ A.x e. X A.y e. X ((xJy) = (yJx) /\ (xmy) = (ymx) /\ ((xm(xJy)) = x /\ (xJ(xmy)) = x /\ A.z e. X ((xm(ymz)) = ((xmy)mz) /\ (xJ(yJz)) = ((xJy)Jz)))))))
72	57, 71	syl 12	. . . 4 |- (j = J -> (E.t(t = X /\ (J:(t X. t)-->t /\ m:(t X. t)-->t /\ A.x e. t A.y e. t ((xJy) = (yJx) /\ (xmy) = (ymx) /\ ((xm(xJy)) = x /\ (xJ(xmy)) = x /\ A.z e. t ((xm(ymz)) = ((xmy)mz) /\ (xJ(yJz)) = ((xJy)Jz)))))) <-> (J:(X X. X)-->X /\ m:(X X. X)-->X /\ A.x e. X A.y e. X ((xJy) = (yJx) /\ (xmy) = (ymx) /\ ((xm(xJy)) = x /\ (xJ(xmy)) = x /\ A.z e. X ((xm(ymz)) = ((xmy)mz) /\ (xJ(yJz)) = ((xJy)Jz)))))))
73	13, 47, 72	3bitrd 603	. . 3 |- (j = J -> (E.t(j:(t X. t)-->t /\ m:(t X. t)-->t /\ A.x e. t A.y e. t ((xjy) = (yjx) /\ (xmy) = (ymx) /\ ((xm(xjy)) = x /\ (xj(xmy)) = x /\ A.z e. t ((xm(ymz)) = ((xmy)mz) /\ (xj(yjz)) = ((xjy)jz))))) <-> (J:(X X. X)-->X /\ m:(X X. X)-->X /\ A.x e. X A.y e. X ((xJy) = (yJx) /\ (xmy) = (ymx) /\ ((xm(xJy)) = x /\ (xJ(xmy)) = x /\ A.z e. X ((xm(ymz)) = ((xmy)mz) /\ (xJ(yJz)) = ((xJy)Jz)))))))
74		feq1 4551	. . . 4 |- (m = M -> (m:(X X. X)-->X <-> M:(X X. X)-->X))
75		opreq 4888	. . . . . . . 8 |- (m = M -> (xmy) = (xMy))
76		opreq 4888	. . . . . . . 8 |- (m = M -> (ymx) = (yMx))
77	75, 76	eqeq12d 1899	. . . . . . 7 |- (m = M -> ((xmy) = (ymx) <-> (xMy) = (yMx)))
78		opreq 4888	. . . . . . . . 9 |- (m = M -> (xm(xJy)) = (xM(xJy)))
79	78	eqeq1d 1892	. . . . . . . 8 |- (m = M -> ((xm(xJy)) = x <-> (xM(xJy)) = x))
80	75	opreq2d 4898	. . . . . . . . 9 |- (m = M -> (xJ(xmy)) = (xJ(xMy)))
81	80	eqeq1d 1892	. . . . . . . 8 |- (m = M -> ((xJ(xmy)) = x <-> (xJ(xMy)) = x))
82		id 73	. . . . . . . . . . . 12 |- (m = M -> m = M)
83		eqidd 1885	. . . . . . . . . . . 12 |- (m = M -> x = x)
84		opreq 4888	. . . . . . . . . . . 12 |- (m = M -> (ymz) = (yMz))
85	82, 83, 84	opreq123d 10153	. . . . . . . . . . 11 |- (m = M -> (xm(ymz)) = (xM(yMz)))
86		eqidd 1885	. . . . . . . . . . . 12 |- (m = M -> z = z)
87	82, 75, 86	opreq123d 10153	. . . . . . . . . . 11 |- (m = M -> ((xmy)mz) = ((xMy)Mz))
88	85, 87	eqeq12d 1899	. . . . . . . . . 10 |- (m = M -> ((xm(ymz)) = ((xmy)mz) <-> (xM(yMz)) = ((xMy)Mz)))
89	88	anbi1d 679	. . . . . . . . 9 |- (m = M -> (((xm(ymz)) = ((xmy)mz) /\ (xJ(yJz)) = ((xJy)Jz)) <-> ((xM(yMz)) = ((xMy)Mz) /\ (xJ(yJz)) = ((xJy)Jz))))
90	89	ralbidv 2123	. . . . . . . 8 |- (m = M -> (A.z e. X ((xm(ymz)) = ((xmy)mz) /\ (xJ(yJz)) = ((xJy)Jz)) <-> A.z e. X ((xM(yMz)) = ((xMy)Mz) /\ (xJ(yJz)) = ((xJy)Jz))))
91	79, 81, 90	3anbi123d 1168	. . . . . . 7 |- (m = M -> (((xm(xJy)) = x /\ (xJ(xmy)) = x /\ A.z e. X ((xm(ymz)) = ((xmy)mz) /\ (xJ(yJz)) = ((xJy)Jz))) <-> ((xM(xJy)) = x /\ (xJ(xMy)) = x /\ A.z e. X ((xM(yMz)) = ((xMy)Mz) /\ (xJ(yJz)) = ((xJy)Jz)))))
92	77, 91	3anbi23d 1171	. . . . . 6 |- (m = M -> (((xJy) = (yJx) /\ (xmy) = (ymx) /\ ((xm(xJy)) = x /\ (xJ(xmy)) = x /\ A.z e. X ((xm(ymz)) = ((xmy)mz) /\ (xJ(yJz)) = ((xJy)Jz)))) <-> ((xJy) = (yJx) /\ (xMy) = (yMx) /\ ((xM(xJy)) = x /\ (xJ(xMy)) = x /\ A.z e. X ((xM(yMz)) = ((xMy)Mz) /\ (xJ(yJz)) = ((xJy)Jz))))))
93	92	ralbidv 2123	. . . . 5 |- (m = M -> (A.y e. X ((xJy) = (yJx) /\ (xmy) = (ymx) /\ ((xm(xJy)) = x /\ (xJ(xmy)) = x /\ A.z e. X ((xm(ymz)) = ((xmy)mz) /\ (xJ(yJz)) = ((xJy)Jz)))) <-> A.y e. X ((xJy) = (yJx) /\ (xMy) = (yMx) /\ ((xM(xJy)) = x /\ (xJ(xMy)) = x /\ A.z e. X ((xM(yMz)) = ((xMy)Mz) /\ (xJ(yJz)) = ((xJy)Jz))))))
94	93	ralbidv 2123	. . . 4 |- (m = M -> (A.x e. X A.y e. X ((xJy) = (yJx) /\ (xmy) = (ymx) /\ ((xm(xJy)) = x /\ (xJ(xmy)) = x /\ A.z e. X ((xm(ymz)) = ((xmy)mz) /\ (xJ(yJz)) = ((xJy)Jz)))) <-> A.x e. X A.y e. X ((xJy) = (yJx) /\ (xMy) = (yMx) /\ ((xM(xJy)) = x /\ (xJ(xMy)) = x /\ A.z e. X ((xM(yMz)) = ((xMy)Mz) /\ (xJ(yJz)) = ((xJy)Jz))))))
95	74, 94	3anbi23d 1171	. . 3 |- (m = M -> ((J:(X X. X)-->X /\ m:(X X. X)-->X /\ A.x e. X A.y e. X ((xJy) = (yJx) /\ (xmy) = (ymx) /\ ((xm(xJy)) = x /\ (xJ(xmy)) = x /\ A.z e. X ((xm(ymz)) = ((xmy)mz) /\ (xJ(yJz)) = ((xJy)Jz))))) <-> (J:(X X. X)-->X /\ M:(X X. X)-->X /\ A.x e. X A.y e. X ((xJy) = (yJx) /\ (xMy) = (yMx) /\ ((xM(xJy)) = x /\ (xJ(xMy)) = x /\ A.z e. X ((xM(yMz)) = ((xMy)Mz) /\ (xJ(yJz)) = ((xJy)Jz)))))))
96	73, 95	opelopabg 3567	. 2 |- ((J e. A /\ M e. B) -> (<.J, M>. e. {<.j, m>. | E.t(j:(t X. t)-->t /\ m:(t X. t)-->t /\ A.x e. t A.y e. t ((xjy) = (yjx) /\ (xmy) = (ymx) /\ ((xm(xjy)) = x /\ (xj(xmy)) = x /\ A.z e. t ((xm(ymz)) = ((xmy)mz) /\ (xj(yjz)) = ((xjy)jz)))))} <-> (J:(X X. X)-->X /\ M:(X X. X)-->X /\ A.x e. X A.y e. X ((xJy) = (yJx) /\ (xMy) = (yMx) /\ ((xM(xJy)) = x /\ (xJ(xMy)) = x /\ A.z e. X ((xM(yMz)) = ((xMy)Mz) /\ (xJ(yJz)) = ((xJy)Jz)))))))
97	3, 96	bitrd 587	1 |- ((J e. A /\ M e. B) -> (<.J, M>. e. LatAlg <-> (J:(X X. X)-->X /\ M:(X X. X)-->X /\ A.x e. X A.y e. X ((xJy) = (yJx) /\ (xMy) = (yMx) /\ ((xM(xJy)) = x /\ (xJ(xMy)) = x /\ A.z e. X ((xM(yMz)) = ((xMy)Mz) /\ (xJ(yJz)) = ((xJy)Jz)))))))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  E.wex 1326  A.wral 2105  _Vcvv 2292  <.cop 3046  {copab 3395   X. cxp 3984  dom cdm 3986  -->wf 3994  (class class class)co 4884  LatAlgclatalg 14529

This theorem is referenced by:  jop 14532  mop 14533  labs1 14536  labs2 14538

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-v 2294  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-br 3339  df-opab 3396  df-id 3586  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-fv 4014  df-opr 4886  df-latalg 14530

Copyright terms: Public domain