Theorem latjcom 18636

Description: The join of a lattice commutes. (chjcom 32123 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 2763	. . . . . . 7 ⊢ (meet‘𝐾) = (meet‘𝐾)
6	3, 4, 5	islat 18622	. . . . . 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 2867	. . 3 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ⟨𝑋, 𝑌⟩ ∈ dom ∨ )
11		opelxpi 5692	. . . . . 6 ⊢ ((𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → ⟨𝑌, 𝑋⟩ ∈ (𝐵 × 𝐵))
12	11	ancoms 464	. . . . 5 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ⟨𝑌, 𝑋⟩ ∈ (𝐵 × 𝐵))
13	12	3adant1 1148	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ⟨𝑌, 𝑋⟩ ∈ (𝐵 × 𝐵))
14	13, 9	eleqtrrd 2867	. . 3 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ⟨𝑌, 𝑋⟩ ∈ dom ∨ )
15	10, 14	jca 521	. 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (⟨𝑋, 𝑌⟩ ∈ dom ∨ ∧ ⟨𝑌, 𝑋⟩ ∈ dom ∨ ))
16		latpos 18627	. . 3 ⊢ (𝐾 ∈ Lat → 𝐾 ∈ Poset)
17	3, 4	joincom 18589	. . 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 1569   ∈ wcel 2146  ⟨cop 4838   × cxp 5653  dom cdm 5655  ‘cfv 6547  (class class class)co 7430  Basecbs 17402  Posetcpo 18496  joincjn 18500  meetcmee 18501  Latclat 18620

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2196  ax-12 2215  ax-ext 2735  ax-rep 5235  ax-sep 5252  ax-nul 5263  ax-pow 5331  ax-pr 5395  ax-un 7761

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2101  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-iun 4956  df-br 5107  df-opab 5171  df-mpt 5190  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 6501  df-fun 6549  df-fn 6550  df-f 6551  df-f1 6552  df-fo 6553  df-f1o 6554  df-fv 6555  df-riota 7387  df-ov 7433  df-oprab 7434  df-lub 18533  df-join 18535  df-lat 18621

This theorem is used by:  latleeqj2  18641  latjlej2  18643  latnle  18662  latmlej12  18668  latj12  18673  latj32  18674  latj13  18675  latj31  18676  latj4rot  18679  mod2ile  18683  latdisdlem  18685  olj02  40426  omllaw4  40446  cmt2N  40450  cmtbr3N  40454  cvlexch2  40529  cvlexchb2  40531  cvlatexchb2  40535  cvlatexch2  40537  cvlatexch3  40538  cvlatcvr2  40542  cvlsupr2  40543  cvlsupr7  40548  cvlsupr8  40549  hlatjcom  40568  hlrelat5N  40601  cvrval5  40615  cvrexch  40620  cvratlem  40621  cvrat  40622  2atlt  40639  cvrat3  40642  cvrat4  40643  cvrat42  40644  4noncolr3  40653  1cvrat  40676  3atlem1  40683  4atlem4d  40802  4atlem12  40812  paddcom  41013  paddasslem2  41021  pmapjat2  41054  atmod2i1  41061  atmod2i2  41062  llnmod2i2  41063  atmod4i1  41066  atmod4i2  41067  dalawlem4  41074  dalawlem9  41079  dalawlem12  41082  lhpjat2  41221  lhple  41242  trljat1  41366  trljat2  41367  cdlemc1  41391  cdlemc6  41396  cdlemd1  41398  cdleme5  41440  cdleme9  41453  cdleme10  41454  cdleme19e  41507  trlcolem  41926  trljco2  41941  cdlemk7  42048  cdlemk7u  42070  cdlemkid1  42122  dih1  42486  dihjatc2N  42512