Theorem latjcom 18538

Description: The join of a lattice commutes. (chjcom 31990 analog.) (Contributed by NM, 16-Sep-2011.)

Hypotheses

Ref	Expression
latjcom.b	⊢ 𝐵 = (Base‘𝐾)
latjcom.j	⊢ ∨ = (join‘𝐾)

Assertion

Ref	Expression
latjcom	⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∨ 𝑌) = (𝑌 ∨ 𝑋))

Proof of Theorem latjcom

Step	Hyp	Ref	Expression
1		opelxpi 5692	. . . . 5 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ⟨𝑋, 𝑌⟩ ∈ (𝐵 × 𝐵))
2	1	3adant1 1148	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ⟨𝑋, 𝑌⟩ ∈ (𝐵 × 𝐵))
3		latjcom.b	. . . . . . 7 ⊢ 𝐵 = (Base‘𝐾)
4		latjcom.j	. . . . . . 7 ⊢ ∨ = (join‘𝐾)
5		eqid 2760	. . . . . . 7 ⊢ (meet‘𝐾) = (meet‘𝐾)
6	3, 4, 5	islat 18524	. . . . . 6 ⊢ (𝐾 ∈ Lat ↔ (𝐾 ∈ Poset ∧ (dom ∨ = (𝐵 × 𝐵) ∧ dom (meet‘𝐾) = (𝐵 × 𝐵))))
7		simprl 783	. . . . . 6 ⊢ ((𝐾 ∈ Poset ∧ (dom ∨ = (𝐵 × 𝐵) ∧ dom (meet‘𝐾) = (𝐵 × 𝐵))) → dom ∨ = (𝐵 × 𝐵))
8	6, 7	sylbi 220	. . . . 5 ⊢ (𝐾 ∈ Lat → dom ∨ = (𝐵 × 𝐵))
9	8	3ad2ant1 1151	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → dom ∨ = (𝐵 × 𝐵))
10	2, 9	eleqtrrd 2863	. . 3 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ⟨𝑋, 𝑌⟩ ∈ dom ∨ )
11		opelxpi 5692	. . . . . 6 ⊢ ((𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → ⟨𝑌, 𝑋⟩ ∈ (𝐵 × 𝐵))
12	11	ancoms 464	. . . . 5 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ⟨𝑌, 𝑋⟩ ∈ (𝐵 × 𝐵))
13	12	3adant1 1148	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ⟨𝑌, 𝑋⟩ ∈ (𝐵 × 𝐵))
14	13, 9	eleqtrrd 2863	. . 3 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ⟨𝑌, 𝑋⟩ ∈ dom ∨ )
15	10, 14	jca 521	. 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (⟨𝑋, 𝑌⟩ ∈ dom ∨ ∧ ⟨𝑌, 𝑋⟩ ∈ dom ∨ ))
16		latpos 18529	. . 3 ⊢ (𝐾 ∈ Lat → 𝐾 ∈ Poset)
17	3, 4	joincom 18491	. . 3 ⊢ (((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (⟨𝑋, 𝑌⟩ ∈ dom ∨ ∧ ⟨𝑌, 𝑋⟩ ∈ dom ∨ )) → (𝑋 ∨ 𝑌) = (𝑌 ∨ 𝑋))
18	16, 17	syl3anl1 1439	. 2 ⊢ (((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (⟨𝑋, 𝑌⟩ ∈ dom ∨ ∧ ⟨𝑌, 𝑋⟩ ∈ dom ∨ )) → (𝑋 ∨ 𝑌) = (𝑌 ∨ 𝑋))
19	15, 18	mpdan 700	1 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∨ 𝑌) = (𝑌 ∨ 𝑋))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145  ⟨cop 4590   × cxp 5653  dom cdm 5655  ‘cfv 6533  (class class class)co 7414  Basecbs 17304  Posetcpo 18398  joincjn 18402  meetcmee 18403  Latclat 18522

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-rep 5232  ax-sep 5251  ax-nul 5263  ax-pow 5330  ax-pr 5398  ax-un 7737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-riota 7371  df-ov 7417  df-oprab 7418  df-lub 18435  df-join 18437  df-lat 18523

This theorem is used by:  latleeqj2  18543  latjlej2  18545  latnle  18564  latmlej12  18570  latj12  18575  latj32  18576  latj13  18577  latj31  18578  latj4rot  18581  mod2ile  18585  latdisdlem  18587  olj02  40102  omllaw4  40122  cmt2N  40126  cmtbr3N  40130  cvlexch2  40205  cvlexchb2  40207  cvlatexchb2  40211  cvlatexch2  40213  cvlatexch3  40214  cvlatcvr2  40218  cvlsupr2  40219  cvlsupr7  40224  cvlsupr8  40225  hlatjcom  40244  hlrelat5N  40277  cvrval5  40291  cvrexch  40296  cvratlem  40297  cvrat  40298  2atlt  40315  cvrat3  40318  cvrat4  40319  cvrat42  40320  4noncolr3  40329  1cvrat  40352  3atlem1  40359  4atlem4d  40478  4atlem12  40488  paddcom  40689  paddasslem2  40697  pmapjat2  40730  atmod2i1  40737  atmod2i2  40738  llnmod2i2  40739  atmod4i1  40742  atmod4i2  40743  dalawlem4  40750  dalawlem9  40755  dalawlem12  40758  lhpjat2  40897  lhple  40918  trljat1  41042  trljat2  41043  cdlemc1  41067  cdlemc6  41072  cdlemd1  41074  cdleme5  41116  cdleme9  41129  cdleme10  41130  cdleme19e  41183  trlcolem  41602  trljco2  41617  cdlemk7  41724  cdlemk7u  41746  cdlemkid1  41798  dih1  42162  dihjatc2N  42188