lattr - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > lattr		Structured version Visualization version GIF version

Theorem lattr 18435

Description: A lattice ordering is transitive. (sstr 3988 analog.) (Contributed by NM, 17-Nov-2011.)

**Hypotheses**
Ref	Expression
latref.b	⊢ 𝐵 = (Base‘𝐾)
latref.l	⊢ ≤ = (le‘𝐾)

**Assertion**
Ref	Expression
lattr	⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍) → 𝑋 ≤ 𝑍))

**Proof of Theorem lattr**
Step	Hyp	Ref	Expression
1		latpos 18429	. 2 ⊢ (𝐾 ∈ Lat → 𝐾 ∈ Poset)
2		latref.b	. . 3 ⊢ 𝐵 = (Base‘𝐾)
3		latref.l	. . 3 ⊢ ≤ = (le‘𝐾)
4	2, 3	postr 18311	. 2 ⊢ ((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍) → 𝑋 ≤ 𝑍))
5	1, 4	sylan 579	1 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍) → 𝑋 ≤ 𝑍))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1085 = wceq 1534 ∈ wcel 2099 class class class wbr 5148 ‘cfv 6548 Basecbs 17179 lecple 17239 Posetcpo 18298 Latclat 18422

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2699 ax-nul 5306

This theorem depends on definitions: df-bi 206 df-an 396 df-or 847 df-3an 1087 df-tru 1537 df-fal 1547 df-ex 1775 df-sb 2061 df-clab 2706 df-cleq 2720 df-clel 2806 df-ne 2938 df-ral 3059 df-rex 3068 df-rab 3430 df-v 3473 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4324 df-if 4530 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4909 df-br 5149 df-opab 5211 df-xp 5684 df-dm 5688 df-iota 6500 df-fv 6556 df-poset 18304 df-lat 18423

This theorem is referenced by: lattrd 18437 latjlej1 18444 latjlej12 18446 latnlej2 18450 latmlem1 18460 latmlem12 18462 clatleglb 18509 lecmtN 38728 hlrelat2 38876 ps-2 38951 dalem3 39137 dalem17 39153 dalem21 39167 dalem25 39171 linepsubN 39225 pmapsub 39241 cdlemblem 39266 pmapjoin 39325 lhpmcvr4N 39499 4atexlemnclw 39543 cdlemd3 39673 cdleme3g 39707 cdleme3h 39708 cdleme7d 39719 cdleme21c 39800 cdleme32b 39915 cdleme35fnpq 39922 cdleme35f 39927 cdleme48bw 39975 cdlemf1 40034 cdlemg2fv2 40073 cdlemg7fvbwN 40080 cdlemg4 40090 cdlemg6c 40093 cdlemg27a 40165 cdlemg33b0 40174 cdlemg33a 40179 cdlemk3 40306 dia2dimlem1 40537 dihord6b 40733 dihord5apre 40735 dihglbcpreN 40773

W3C validator

	
		OSZAR »