Theorem lecmtN 36424

Description: Ordered elements commute. (lecmi 29363 analog.) (Contributed by NM, 10-Nov-2011.) (New usage is discouraged.)

Hypotheses

Ref	Expression
lecmt.b	⊢ 𝐵 = (Base‘𝐾)
lecmt.l	⊢ ≤ = (le‘𝐾)
lecmt.c	⊢ 𝐶 = (cm‘𝐾)

Assertion

Ref	Expression
lecmtN	⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 → 𝑋𝐶𝑌))

Proof of Theorem lecmtN

Step	Hyp	Ref	Expression
1		omllat 36410	. . . . 5 ⊢ (𝐾 ∈ OML → 𝐾 ∈ Lat)
2	1	3ad2ant1 1129	. . . 4 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝐾 ∈ Lat)
3		simp2 1133	. . . 4 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑋 ∈ 𝐵)
4		omlop 36409	. . . . . . 7 ⊢ (𝐾 ∈ OML → 𝐾 ∈ OP)
5	4	3ad2ant1 1129	. . . . . 6 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝐾 ∈ OP)
6		lecmt.b	. . . . . . 7 ⊢ 𝐵 = (Base‘𝐾)
7		eqid 2821	. . . . . . 7 ⊢ (oc‘𝐾) = (oc‘𝐾)
8	6, 7	opoccl 36362	. . . . . 6 ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → ((oc‘𝐾)‘𝑋) ∈ 𝐵)
9	5, 3, 8	syl2anc 586	. . . . 5 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((oc‘𝐾)‘𝑋) ∈ 𝐵)
10		simp3 1134	. . . . 5 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑌 ∈ 𝐵)
11		eqid 2821	. . . . . 6 ⊢ (join‘𝐾) = (join‘𝐾)
12	6, 11	latjcl 17644	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ ((oc‘𝐾)‘𝑋) ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌) ∈ 𝐵)
13	2, 9, 10, 12	syl3anc 1367	. . . 4 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌) ∈ 𝐵)
14		lecmt.l	. . . . 5 ⊢ ≤ = (le‘𝐾)
15		eqid 2821	. . . . 5 ⊢ (meet‘𝐾) = (meet‘𝐾)
16	6, 14, 15	latmle1 17669	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ (((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌) ∈ 𝐵) → (𝑋(meet‘𝐾)(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌)) ≤ 𝑋)
17	2, 3, 13, 16	syl3anc 1367	. . 3 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋(meet‘𝐾)(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌)) ≤ 𝑋)
18	6, 15	latmcl 17645	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ (((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌) ∈ 𝐵) → (𝑋(meet‘𝐾)(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌)) ∈ 𝐵)
19	2, 3, 13, 18	syl3anc 1367	. . . 4 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋(meet‘𝐾)(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌)) ∈ 𝐵)
20	6, 14	lattr 17649	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ ((𝑋(meet‘𝐾)(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌)) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (((𝑋(meet‘𝐾)(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌)) ≤ 𝑋 ∧ 𝑋 ≤ 𝑌) → (𝑋(meet‘𝐾)(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌)) ≤ 𝑌))
21	2, 19, 3, 10, 20	syl13anc 1368	. . 3 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (((𝑋(meet‘𝐾)(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌)) ≤ 𝑋 ∧ 𝑋 ≤ 𝑌) → (𝑋(meet‘𝐾)(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌)) ≤ 𝑌))
22	17, 21	mpand 693	. 2 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 → (𝑋(meet‘𝐾)(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌)) ≤ 𝑌))
23		lecmt.c	. . 3 ⊢ 𝐶 = (cm‘𝐾)
24	6, 14, 11, 15, 7, 23	cmtbr4N 36423	. 2 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ (𝑋(meet‘𝐾)(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌)) ≤ 𝑌))
25	22, 24	sylibrd 261	1 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 → 𝑋𝐶𝑌))

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083   = wceq 1537   ∈ wcel 2114   class class class wbr 5052  ‘cfv 6341  (class class class)co 7142  Basecbs 16466  lecple 16555  occoc 16556  joincjn 17537  meetcmee 17538  Latclat 17638  OPcops 36340  cmccmtN 36341  OMLcoml 36343

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-rep 5176  ax-sep 5189  ax-nul 5196  ax-pow 5252  ax-pr 5316  ax-un 7447

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3488  df-sbc 3764  df-csb 3872  df-dif 3927  df-un 3929  df-in 3931  df-ss 3940  df-nul 4280  df-if 4454  df-pw 4527  df-sn 4554  df-pr 4556  df-op 4560  df-uni 4825  df-iun 4907  df-br 5053  df-opab 5115  df-mpt 5133  df-id 5446  df-xp 5547  df-rel 5548  df-cnv 5549  df-co 5550  df-dm 5551  df-rn 5552  df-res 5553  df-ima 5554  df-iota 6300  df-fun 6343  df-fn 6344  df-f 6345  df-f1 6346  df-fo 6347  df-f1o 6348  df-fv 6349  df-riota 7100  df-ov 7145  df-oprab 7146  df-proset 17521  df-poset 17539  df-lub 17567  df-glb 17568  df-join 17569  df-meet 17570  df-lat 17639  df-oposet 36344  df-cmtN 36345  df-ol 36346  df-oml 36347

This theorem is referenced by:  cmtidN  36425  omlmod1i2N  36428