Theorem dibord 39152

Description: The isomorphism B for a lattice 𝐾 is order-preserving in the region under co-atom 𝑊. (Contributed by NM, 24-Feb-2014.)

Hypotheses

Ref	Expression
dib11.b	⊢ 𝐵 = (Base‘𝐾)
dib11.l	⊢ ≤ = (le‘𝐾)
dib11.h	⊢ 𝐻 = (LHyp‘𝐾)
dib11.i	⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊)

Assertion

Ref	Expression
dibord	⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊)) → ((𝐼‘𝑋) ⊆ (𝐼‘𝑌) ↔ 𝑋 ≤ 𝑌))

Proof of Theorem dibord

Dummy variable 𝑓 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		dib11.b	. . . . 5 ⊢ 𝐵 = (Base‘𝐾)
2		dib11.l	. . . . 5 ⊢ ≤ = (le‘𝐾)
3		dib11.h	. . . . 5 ⊢ 𝐻 = (LHyp‘𝐾)
4		eqid 2739	. . . . 5 ⊢ ((LTrn‘𝐾)‘𝑊) = ((LTrn‘𝐾)‘𝑊)
5		eqid 2739	. . . . 5 ⊢ (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵)) = (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))
6		eqid 2739	. . . . 5 ⊢ ((DIsoA‘𝐾)‘𝑊) = ((DIsoA‘𝐾)‘𝑊)
7		dib11.i	. . . . 5 ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊)
8	1, 2, 3, 4, 5, 6, 7	dibval2 39137	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (𝐼‘𝑋) = ((((DIsoA‘𝐾)‘𝑊)‘𝑋) × {(𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))}))
9	8	3adant3 1130	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊)) → (𝐼‘𝑋) = ((((DIsoA‘𝐾)‘𝑊)‘𝑋) × {(𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))}))
10	1, 2, 3, 4, 5, 6, 7	dibval2 39137	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊)) → (𝐼‘𝑌) = ((((DIsoA‘𝐾)‘𝑊)‘𝑌) × {(𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))}))
11	10	3adant2 1129	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊)) → (𝐼‘𝑌) = ((((DIsoA‘𝐾)‘𝑊)‘𝑌) × {(𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))}))
12	9, 11	sseq12d 3958	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊)) → ((𝐼‘𝑋) ⊆ (𝐼‘𝑌) ↔ ((((DIsoA‘𝐾)‘𝑊)‘𝑋) × {(𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))}) ⊆ ((((DIsoA‘𝐾)‘𝑊)‘𝑌) × {(𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))})))
13	1, 2, 3, 7	dibn0 39146	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (𝐼‘𝑋) ≠ ∅)
14	13	3adant3 1130	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊)) → (𝐼‘𝑋) ≠ ∅)
15	9, 14	eqnetrrd 3013	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊)) → ((((DIsoA‘𝐾)‘𝑊)‘𝑋) × {(𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))}) ≠ ∅)
16		ssxpb 6074	. . 3 ⊢ (((((DIsoA‘𝐾)‘𝑊)‘𝑋) × {(𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))}) ≠ ∅ → (((((DIsoA‘𝐾)‘𝑊)‘𝑋) × {(𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))}) ⊆ ((((DIsoA‘𝐾)‘𝑊)‘𝑌) × {(𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))}) ↔ ((((DIsoA‘𝐾)‘𝑊)‘𝑋) ⊆ (((DIsoA‘𝐾)‘𝑊)‘𝑌) ∧ {(𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))} ⊆ {(𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))})))
17	15, 16	syl 17	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊)) → (((((DIsoA‘𝐾)‘𝑊)‘𝑋) × {(𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))}) ⊆ ((((DIsoA‘𝐾)‘𝑊)‘𝑌) × {(𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))}) ↔ ((((DIsoA‘𝐾)‘𝑊)‘𝑋) ⊆ (((DIsoA‘𝐾)‘𝑊)‘𝑌) ∧ {(𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))} ⊆ {(𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))})))
18		ssid 3947	. . . 4 ⊢ {(𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))} ⊆ {(𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))}
19	18	biantru 529	. . 3 ⊢ ((((DIsoA‘𝐾)‘𝑊)‘𝑋) ⊆ (((DIsoA‘𝐾)‘𝑊)‘𝑌) ↔ ((((DIsoA‘𝐾)‘𝑊)‘𝑋) ⊆ (((DIsoA‘𝐾)‘𝑊)‘𝑌) ∧ {(𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))} ⊆ {(𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))}))
20	1, 2, 3, 6	diaord 39040	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊)) → ((((DIsoA‘𝐾)‘𝑊)‘𝑋) ⊆ (((DIsoA‘𝐾)‘𝑊)‘𝑌) ↔ 𝑋 ≤ 𝑌))
21	19, 20	bitr3id 284	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊)) → (((((DIsoA‘𝐾)‘𝑊)‘𝑋) ⊆ (((DIsoA‘𝐾)‘𝑊)‘𝑌) ∧ {(𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))} ⊆ {(𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))}) ↔ 𝑋 ≤ 𝑌))
22	12, 17, 21	3bitrd 304	1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊)) → ((𝐼‘𝑋) ⊆ (𝐼‘𝑌) ↔ 𝑋 ≤ 𝑌))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1085   = wceq 1541   ∈ wcel 2109   ≠ wne 2944   ⊆ wss 3891  ∅c0 4261  {csn 4566   class class class wbr 5078   ↦ cmpt 5161   I cid 5487   × cxp 5586   ↾ cres 5590  ‘cfv 6430  Basecbs 16893  lecple 16950  HLchlt 37343  LHypclh 37977  LTrncltrn 38094  DIsoAcdia 39021  DIsoBcdib 39131

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-10 2140  ax-11 2157  ax-12 2174  ax-ext 2710  ax-rep 5213  ax-sep 5226  ax-nul 5233  ax-pow 5291  ax-pr 5355  ax-un 7579  ax-riotaBAD 36946

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-nf 1790  df-sb 2071  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-ral 3070  df-rex 3071  df-reu 3072  df-rmo 3073  df-rab 3074  df-v 3432  df-sbc 3720  df-csb 3837  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-nul 4262  df-if 4465  df-pw 4540  df-sn 4567  df-pr 4569  df-op 4573  df-uni 4845  df-iun 4931  df-iin 4932  df-br 5079  df-opab 5141  df-mpt 5162  df-id 5488  df-xp 5594  df-rel 5595  df-cnv 5596  df-co 5597  df-dm 5598  df-rn 5599  df-res 5600  df-ima 5601  df-iota 6388  df-fun 6432  df-fn 6433  df-f 6434  df-f1 6435  df-fo 6436  df-f1o 6437  df-fv 6438  df-riota 7225  df-ov 7271  df-oprab 7272  df-mpo 7273  df-1st 7817  df-2nd 7818  df-undef 8073  df-map 8591  df-proset 17994  df-poset 18012  df-plt 18029  df-lub 18045  df-glb 18046  df-join 18047  df-meet 18048  df-p0 18124  df-p1 18125  df-lat 18131  df-clat 18198  df-oposet 37169  df-ol 37171  df-oml 37172  df-covers 37259  df-ats 37260  df-atl 37291  df-cvlat 37315  df-hlat 37344  df-llines 37491  df-lplanes 37492  df-lvols 37493  df-lines 37494  df-psubsp 37496  df-pmap 37497  df-padd 37789  df-lhyp 37981  df-laut 37982  df-ldil 38097  df-ltrn 38098  df-trl 38152  df-disoa 39022  df-dib 39132

This theorem is referenced by:  dib11N  39153  cdlemn2a  39189  dihord1  39211  dihord3  39250  dihord5b  39252