Theorem cvrexchlem 17059

Description: Lemma for cvrexch 17060. (Th. cvexchlem 11940 analog.)

Hypotheses

Ref	Expression
cvrexch.b	|- B = (base` K)
cvrexch.j	|- J = (join` K)
cvrexch.m	|- M = (meet` K)
cvrexch.c	|- C = ( <oNEW ` K)

Assertion

Ref	Expression
cvrexchlem	|- ((K e. HL /\ X e. B /\ Y e. B) -> ((XMY)CY -> XC(XJY)))

Proof of Theorem cvrexchlem

Step	Hyp	Ref	Expression
1		cvrexch.b	. . . . . . . 8 |- B = (base` K)
2		eqid 1884	. . . . . . . 8 |- (lt` K) = (lt` K)
3		cvrexch.c	. . . . . . . 8 |- C = ( <oNEW ` K)
4	1, 2, 3	cvrlt 16989	. . . . . . 7 |- (((K e. HL /\ (XMY) e. B /\ Y e. B) /\ (XMY)CY) -> (XMY)(lt` K)Y)
5	4	ex 402	. . . . . 6 |- ((K e. HL /\ (XMY) e. B /\ Y e. B) -> ((XMY)CY -> (XMY)(lt` K)Y))
6		cvrexch.m	. . . . . . . 8 |- M = (meet` K)
7	1, 6	latmcl 16853	. . . . . . 7 |- ((K e. LatNEW /\ X e. B /\ Y e. B) -> (XMY) e. B)
8		hllat 17026	. . . . . . 7 |- (K e. HL -> K e. LatNEW)
9	7, 8	syl3an1 1130	. . . . . 6 |- ((K e. HL /\ X e. B /\ Y e. B) -> (XMY) e. B)
10	5, 9	syld3an2 1144	. . . . 5 |- ((K e. HL /\ X e. B /\ Y e. B) -> ((XMY)CY -> (XMY)(lt` K)Y))
11		eqid 1884	. . . . . . 7 |- (le` K) = (le` K)
12		eqid 1884	. . . . . . 7 |- (AtomsNEW` K) = (AtomsNEW` K)
13	1, 11, 2, 12	hlrelat1 17049	. . . . . 6 |- ((K e. HL /\ (XMY) e. B /\ Y e. B) -> ((XMY)(lt` K)Y -> E.p e. (AtomsNEW` K)(-. p(le` K)(XMY) /\ p(le` K)Y)))
14	13, 9	syld3an2 1144	. . . . 5 |- ((K e. HL /\ X e. B /\ Y e. B) -> ((XMY)(lt` K)Y -> E.p e. (AtomsNEW` K)(-. p(le` K)(XMY) /\ p(le` K)Y)))
15	10, 14	syld 30	. . . 4 |- ((K e. HL /\ X e. B /\ Y e. B) -> ((XMY)CY -> E.p e. (AtomsNEW` K)(-. p(le` K)(XMY) /\ p(le` K)Y)))
16	15	imp 377	. . 3 |- (((K e. HL /\ X e. B /\ Y e. B) /\ (XMY)CY) -> E.p e. (AtomsNEW` K)(-. p(le` K)(XMY) /\ p(le` K)Y))
17		simpl1 879	. . . . . . . . . . . . . . . . . 18 |- (((K e. HL /\ X e. B /\ Y e. B) /\ p e. (AtomsNEW` K)) -> K e. HL)
18	17, 8	syl 12	. . . . . . . . . . . . . . . . 17 |- (((K e. HL /\ X e. B /\ Y e. B) /\ p e. (AtomsNEW` K)) -> K e. LatNEW)
19	1, 12	atombase 17003	. . . . . . . . . . . . . . . . . 18 |- (p e. (AtomsNEW` K) -> p e. B)
20	19	adantl 424	. . . . . . . . . . . . . . . . 17 |- (((K e. HL /\ X e. B /\ Y e. B) /\ p e. (AtomsNEW` K)) -> p e. B)
21		simpl2 880	. . . . . . . . . . . . . . . . 17 |- (((K e. HL /\ X e. B /\ Y e. B) /\ p e. (AtomsNEW` K)) -> X e. B)
22		simpl3 881	. . . . . . . . . . . . . . . . 17 |- (((K e. HL /\ X e. B /\ Y e. B) /\ p e. (AtomsNEW` K)) -> Y e. B)
23	1, 11, 6	latlem12 16873	. . . . . . . . . . . . . . . . 17 |- ((K e. LatNEW /\ (p e. B /\ X e. B /\ Y e. B)) -> ((p(le` K)X /\ p(le` K)Y) <-> p(le` K)(XMY)))
24	18, 20, 21, 22, 23	syl13anc 1102	. . . . . . . . . . . . . . . 16 |- (((K e. HL /\ X e. B /\ Y e. B) /\ p e. (AtomsNEW` K)) -> ((p(le` K)X /\ p(le` K)Y) <-> p(le` K)(XMY)))
25	24	biimpd 170	. . . . . . . . . . . . . . 15 |- (((K e. HL /\ X e. B /\ Y e. B) /\ p e. (AtomsNEW` K)) -> ((p(le` K)X /\ p(le` K)Y) -> p(le` K)(XMY)))
26	25	exp3a 405	. . . . . . . . . . . . . 14 |- (((K e. HL /\ X e. B /\ Y e. B) /\ p e. (AtomsNEW` K)) -> (p(le` K)X -> (p(le` K)Y -> p(le` K)(XMY))))
27	26	com23 36	. . . . . . . . . . . . 13 |- (((K e. HL /\ X e. B /\ Y e. B) /\ p e. (AtomsNEW` K)) -> (p(le` K)Y -> (p(le` K)X -> p(le` K)(XMY))))
28		con3 110	. . . . . . . . . . . . 13 |- ((p(le` K)X -> p(le` K)(XMY)) -> (-. p(le` K)(XMY) -> -. p(le` K)X))
29	27, 28	syl6 25	. . . . . . . . . . . 12 |- (((K e. HL /\ X e. B /\ Y e. B) /\ p e. (AtomsNEW` K)) -> (p(le` K)Y -> (-. p(le` K)(XMY) -> -. p(le` K)X)))
30	29	com23 36	. . . . . . . . . . 11 |- (((K e. HL /\ X e. B /\ Y e. B) /\ p e. (AtomsNEW` K)) -> (-. p(le` K)(XMY) -> (p(le` K)Y -> -. p(le` K)X)))
31	30	a1d 15	. . . . . . . . . 10 |- (((K e. HL /\ X e. B /\ Y e. B) /\ p e. (AtomsNEW` K)) -> ((XMY)CY -> (-. p(le` K)(XMY) -> (p(le` K)Y -> -. p(le` K)X))))
32	31	imp4d 394	. . . . . . . . 9 |- (((K e. HL /\ X e. B /\ Y e. B) /\ p e. (AtomsNEW` K)) -> (((XMY)CY /\ (-. p(le` K)(XMY) /\ p(le` K)Y)) -> -. p(le` K)X))
33		simpr 350	. . . . . . . . . 10 |- (((K e. HL /\ X e. B /\ Y e. B) /\ p e. (AtomsNEW` K)) -> p e. (AtomsNEW` K))
34		cvrexch.j	. . . . . . . . . . 11 |- J = (join` K)
35	1, 11, 34, 3, 12	cvr1 17054	. . . . . . . . . 10 |- ((K e. HL /\ X e. B /\ p e. (AtomsNEW` K)) -> (-. p(le` K)X <-> XC(XJp)))
36	17, 21, 33, 35	syl111anc 1100	. . . . . . . . 9 |- (((K e. HL /\ X e. B /\ Y e. B) /\ p e. (AtomsNEW` K)) -> (-. p(le` K)X <-> XC(XJp)))
37	32, 36	sylibd 219	. . . . . . . 8 |- (((K e. HL /\ X e. B /\ Y e. B) /\ p e. (AtomsNEW` K)) -> (((XMY)CY /\ (-. p(le` K)(XMY) /\ p(le` K)Y)) -> XC(XJp)))
38	37	imp 377	. . . . . . 7 |- ((((K e. HL /\ X e. B /\ Y e. B) /\ p e. (AtomsNEW` K)) /\ ((XMY)CY /\ (-. p(le` K)(XMY) /\ p(le` K)Y))) -> XC(XJp))
39		simpl1 879	. . . . . . . . . . . . 13 |- (((K e. HL /\ X e. B /\ Y e. B) /\ p e. B) -> K e. HL)
40	39, 8	syl 12	. . . . . . . . . . . 12 |- (((K e. HL /\ X e. B /\ Y e. B) /\ p e. B) -> K e. LatNEW)
41		simpl2 880	. . . . . . . . . . . 12 |- (((K e. HL /\ X e. B /\ Y e. B) /\ p e. B) -> X e. B)
42		simpl3 881	. . . . . . . . . . . . 13 |- (((K e. HL /\ X e. B /\ Y e. B) /\ p e. B) -> Y e. B)
43	40, 41, 42, 7	syl111anc 1100	. . . . . . . . . . . 12 |- (((K e. HL /\ X e. B /\ Y e. B) /\ p e. B) -> (XMY) e. B)
44		simpr 350	. . . . . . . . . . . 12 |- (((K e. HL /\ X e. B /\ Y e. B) /\ p e. B) -> p e. B)
45	1, 34	latjass 16886	. . . . . . . . . . . 12 |- ((K e. LatNEW /\ (X e. B /\ (XMY) e. B /\ p e. B)) -> ((XJ(XMY))Jp) = (XJ((XMY)Jp)))
46	40, 41, 43, 44, 45	syl13anc 1102	. . . . . . . . . . 11 |- (((K e. HL /\ X e. B /\ Y e. B) /\ p e. B) -> ((XJ(XMY))Jp) = (XJ((XMY)Jp)))
47	1, 34, 6	latabs1 16882	. . . . . . . . . . . . . 14 |- ((K e. LatNEW /\ X e. B /\ Y e. B) -> (XJ(XMY)) = X)
48	47, 8	syl3an1 1130	. . . . . . . . . . . . 13 |- ((K e. HL /\ X e. B /\ Y e. B) -> (XJ(XMY)) = X)
49	48	adantr 425	. . . . . . . . . . . 12 |- (((K e. HL /\ X e. B /\ Y e. B) /\ p e. B) -> (XJ(XMY)) = X)
50	49	opreq1d 4897	. . . . . . . . . . 11 |- (((K e. HL /\ X e. B /\ Y e. B) /\ p e. B) -> ((XJ(XMY))Jp) = (XJp))
51	46, 50	eqtr3d 1927	. . . . . . . . . 10 |- (((K e. HL /\ X e. B /\ Y e. B) /\ p e. B) -> (XJ((XMY)Jp)) = (XJp))
52	51	adantr 425	. . . . . . . . 9 |- ((((K e. HL /\ X e. B /\ Y e. B) /\ p e. B) /\ ((XMY)CY /\ (-. p(le` K)(XMY) /\ p(le` K)Y))) -> (XJ((XMY)Jp)) = (XJp))
53	1, 11, 2, 34	latnle 16880	. . . . . . . . . . . . . . 15 |- ((K e. LatNEW /\ (XMY) e. B /\ p e. B) -> (-. p(le` K)(XMY) <-> (XMY)(lt` K)((XMY)Jp)))
54	40, 43, 44, 53	syl111anc 1100	. . . . . . . . . . . . . 14 |- (((K e. HL /\ X e. B /\ Y e. B) /\ p e. B) -> (-. p(le` K)(XMY) <-> (XMY)(lt` K)((XMY)Jp)))
55	1, 11, 6	latmle2 16872	. . . . . . . . . . . . . . . . 17 |- ((K e. LatNEW /\ X e. B /\ Y e. B) -> (XMY)(le` K)Y)
56	40, 41, 42, 55	syl111anc 1100	. . . . . . . . . . . . . . . 16 |- (((K e. HL /\ X e. B /\ Y e. B) /\ p e. B) -> (XMY)(le` K)Y)
57	56	biantrurd 796	. . . . . . . . . . . . . . 15 |- (((K e. HL /\ X e. B /\ Y e. B) /\ p e. B) -> (p(le` K)Y <-> ((XMY)(le` K)Y /\ p(le` K)Y)))
58	1, 11, 34	latjle12 16863	. . . . . . . . . . . . . . . 16 |- ((K e. LatNEW /\ ((XMY) e. B /\ p e. B /\ Y e. B)) -> (((XMY)(le` K)Y /\ p(le` K)Y) <-> ((XMY)Jp)(le` K)Y))
59	40, 43, 44, 42, 58	syl13anc 1102	. . . . . . . . . . . . . . 15 |- (((K e. HL /\ X e. B /\ Y e. B) /\ p e. B) -> (((XMY)(le` K)Y /\ p(le` K)Y) <-> ((XMY)Jp)(le` K)Y))
60	57, 59	bitrd 587	. . . . . . . . . . . . . 14 |- (((K e. HL /\ X e. B /\ Y e. B) /\ p e. B) -> (p(le` K)Y <-> ((XMY)Jp)(le` K)Y))
61	54, 60	anbi12d 690	. . . . . . . . . . . . 13 |- (((K e. HL /\ X e. B /\ Y e. B) /\ p e. B) -> ((-. p(le` K)(XMY) /\ p(le` K)Y) <-> ((XMY)(lt` K)((XMY)Jp) /\ ((XMY)Jp)(le` K)Y)))
62		hlpos 17027	. . . . . . . . . . . . . . . 16 |- (K e. HL -> K e. PosetNEW)
63	39, 62	syl 12	. . . . . . . . . . . . . . 15 |- (((K e. HL /\ X e. B /\ Y e. B) /\ p e. B) -> K e. PosetNEW)
64	1, 34	latjcl 16852	. . . . . . . . . . . . . . . . 17 |- ((K e. LatNEW /\ (XMY) e. B /\ p e. B) -> ((XMY)Jp) e. B)
65	40, 43, 44, 64	syl111anc 1100	. . . . . . . . . . . . . . . 16 |- (((K e. HL /\ X e. B /\ Y e. B) /\ p e. B) -> ((XMY)Jp) e. B)
66	43, 42, 65	3jca 1050	. . . . . . . . . . . . . . 15 |- (((K e. HL /\ X e. B /\ Y e. B) /\ p e. B) -> ((XMY) e. B /\ Y e. B /\ ((XMY)Jp) e. B))
67	1, 11, 2, 3	cvrnbtwn2 16992	. . . . . . . . . . . . . . . . 17 |- ((K e. PosetNEW /\ ((XMY) e. B /\ Y e. B /\ ((XMY)Jp) e. B) /\ (XMY)CY) -> (((XMY)(lt` K)((XMY)Jp) /\ ((XMY)Jp)(le` K)Y) <-> ((XMY)Jp) = Y))
68	67	biimpd 170	. . . . . . . . . . . . . . . 16 |- ((K e. PosetNEW /\ ((XMY) e. B /\ Y e. B /\ ((XMY)Jp) e. B) /\ (XMY)CY) -> (((XMY)(lt` K)((XMY)Jp) /\ ((XMY)Jp)(le` K)Y) -> ((XMY)Jp) = Y))
69	68	3exp 1066	. . . . . . . . . . . . . . 15 |- (K e. PosetNEW -> (((XMY) e. B /\ Y e. B /\ ((XMY)Jp) e. B) -> ((XMY)CY -> (((XMY)(lt` K)((XMY)Jp) /\ ((XMY)Jp)(le` K)Y) -> ((XMY)Jp) = Y))))
70	63, 66, 69	sylc 83	. . . . . . . . . . . . . 14 |- (((K e. HL /\ X e. B /\ Y e. B) /\ p e. B) -> ((XMY)CY -> (((XMY)(lt` K)((XMY)Jp) /\ ((XMY)Jp)(le` K)Y) -> ((XMY)Jp) = Y)))
71	70	com23 36	. . . . . . . . . . . . 13 |- (((K e. HL /\ X e. B /\ Y e. B) /\ p e. B) -> (((XMY)(lt` K)((XMY)Jp) /\ ((XMY)Jp)(le` K)Y) -> ((XMY)CY -> ((XMY)Jp) = Y)))
72	61, 71	sylbid 220	. . . . . . . . . . . 12 |- (((K e. HL /\ X e. B /\ Y e. B) /\ p e. B) -> ((-. p(le` K)(XMY) /\ p(le` K)Y) -> ((XMY)CY -> ((XMY)Jp) = Y)))
73	72	com23 36	. . . . . . . . . . 11 |- (((K e. HL /\ X e. B /\ Y e. B) /\ p e. B) -> ((XMY)CY -> ((-. p(le` K)(XMY) /\ p(le` K)Y) -> ((XMY)Jp) = Y)))
74	73	imp32 390	. . . . . . . . . 10 |- ((((K e. HL /\ X e. B /\ Y e. B) /\ p e. B) /\ ((XMY)CY /\ (-. p(le` K)(XMY) /\ p(le` K)Y))) -> ((XMY)Jp) = Y)
75	74	opreq2d 4898	. . . . . . . . 9 |- ((((K e. HL /\ X e. B /\ Y e. B) /\ p e. B) /\ ((XMY)CY /\ (-. p(le` K)(XMY) /\ p(le` K)Y))) -> (XJ((XMY)Jp)) = (XJY))
76	52, 75	eqtr3d 1927	. . . . . . . 8 |- ((((K e. HL /\ X e. B /\ Y e. B) /\ p e. B) /\ ((XMY)CY /\ (-. p(le` K)(XMY) /\ p(le` K)Y))) -> (XJp) = (XJY))
77	76, 19	sylanl2 510	. . . . . . 7 |- ((((K e. HL /\ X e. B /\ Y e. B) /\ p e. (AtomsNEW` K)) /\ ((XMY)CY /\ (-. p(le` K)(XMY) /\ p(le` K)Y))) -> (XJp) = (XJY))
78	38, 77	breqtrd 3361	. . . . . 6 |- ((((K e. HL /\ X e. B /\ Y e. B) /\ p e. (AtomsNEW` K)) /\ ((XMY)CY /\ (-. p(le` K)(XMY) /\ p(le` K)Y))) -> XC(XJY))
79	78	expr 418	. . . . 5 |- ((((K e. HL /\ X e. B /\ Y e. B) /\ p e. (AtomsNEW` K)) /\ (XMY)CY) -> ((-. p(le` K)(XMY) /\ p(le` K)Y) -> XC(XJY)))
80	79	an1rs 547	. . . 4 |- ((((K e. HL /\ X e. B /\ Y e. B) /\ (XMY)CY) /\ p e. (AtomsNEW` K)) -> ((-. p(le` K)(XMY) /\ p(le` K)Y) -> XC(XJY)))
81	80	r19.23adva 2216	. . 3 |- (((K e. HL /\ X e. B /\ Y e. B) /\ (XMY)CY) -> (E.p e. (AtomsNEW` K)(-. p(le` K)(XMY) /\ p(le` K)Y) -> XC(XJY)))
82	16, 81	mpd 29	. 2 |- (((K e. HL /\ X e. B /\ Y e. B) /\ (XMY)CY) -> XC(XJY))
83	82	ex 402	1 |- ((K e. HL /\ X e. B /\ Y e. B) -> ((XMY)CY -> XC(XJY)))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  E.wrex 2106   class class class wbr 3338  ` cfv 3998  (class class class)co 4884  basecbs 16758  lecple 16759  PosetNEWcpo 16760  ltcplt 16761  joincjn 16766  meetcmee 16767  LatNEWclat 16834   <o_NEW ccvr 16980  AtomsNEWcatm 16981  HLchlt 16983

This theorem is referenced by:  cvrexch 17060

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-rep 3428  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-tru 1262  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-reu 2111  df-rab 2112  df-v 2294  df-sbc 2454  df-csb 2541  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-if 2983  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-f1 4011  df-fo 4012  df-f1o 4013  df-fv 4014  df-opr 4886  df-oprab 4887  df-mpt 5006  df-mpt2 5007  df-iota 5089  df-er 5318  df-en 5427  df-dom 5428  df-sdom 5429  df-undef 5556  df-riota 5560  df-struct 16708  df-poset 16772  df-plt 16780  df-pge 16792  df-lub 16799  df-glb 16800  df-join 16801  df-meet 16802  df-p0 16841  df-lat 16847  df-clat 16848  df-oposet 16905  df-ol 16907  df-oml 16908  df-covers 16984  df-atoms 16985  df-atlat 16986  df-hlat 17017

Copyright terms: Public domain