Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dihglblem2aN Structured version   Visualization version   GIF version

Theorem dihglblem2aN 39049
Description: Lemma for isomorphism H of a GLB. (Contributed by NM, 19-Mar-2014.) (New usage is discouraged.)
Hypotheses
Ref Expression
dihglblem.b 𝐵 = (Base‘𝐾)
dihglblem.l = (le‘𝐾)
dihglblem.m = (meet‘𝐾)
dihglblem.g 𝐺 = (glb‘𝐾)
dihglblem.h 𝐻 = (LHyp‘𝐾)
dihglblem.t 𝑇 = {𝑢𝐵 ∣ ∃𝑣𝑆 𝑢 = (𝑣 𝑊)}
Assertion
Ref Expression
dihglblem2aN (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆𝐵𝑆 ≠ ∅)) → 𝑇 ≠ ∅)
Distinct variable groups:   𝑣,𝑢,   𝑢,𝐵   𝑢,𝑆,𝑣   𝑢,𝑊,𝑣
Allowed substitution hints:   𝐵(𝑣)   𝑇(𝑣,𝑢)   𝐺(𝑣,𝑢)   𝐻(𝑣,𝑢)   𝐾(𝑣,𝑢)   (𝑣,𝑢)

Proof of Theorem dihglblem2aN
Dummy variables 𝑤 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dihglblem.t . . 3 𝑇 = {𝑢𝐵 ∣ ∃𝑣𝑆 𝑢 = (𝑣 𝑊)}
21a1i 11 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆𝐵𝑆 ≠ ∅)) → 𝑇 = {𝑢𝐵 ∣ ∃𝑣𝑆 𝑢 = (𝑣 𝑊)})
3 simprr 773 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆𝐵𝑆 ≠ ∅)) → 𝑆 ≠ ∅)
4 n0 4266 . . . 4 (𝑆 ≠ ∅ ↔ ∃𝑧 𝑧𝑆)
53, 4sylib 221 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆𝐵𝑆 ≠ ∅)) → ∃𝑧 𝑧𝑆)
6 hllat 37119 . . . . . . 7 (𝐾 ∈ HL → 𝐾 ∈ Lat)
76ad3antrrr 730 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆𝐵𝑆 ≠ ∅)) ∧ 𝑧𝑆) → 𝐾 ∈ Lat)
8 simplrl 777 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆𝐵𝑆 ≠ ∅)) ∧ 𝑧𝑆) → 𝑆𝐵)
9 simpr 488 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆𝐵𝑆 ≠ ∅)) ∧ 𝑧𝑆) → 𝑧𝑆)
108, 9sseldd 3907 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆𝐵𝑆 ≠ ∅)) ∧ 𝑧𝑆) → 𝑧𝐵)
11 dihglblem.b . . . . . . . 8 𝐵 = (Base‘𝐾)
12 dihglblem.h . . . . . . . 8 𝐻 = (LHyp‘𝐾)
1311, 12lhpbase 37754 . . . . . . 7 (𝑊𝐻𝑊𝐵)
1413ad3antlr 731 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆𝐵𝑆 ≠ ∅)) ∧ 𝑧𝑆) → 𝑊𝐵)
15 dihglblem.m . . . . . . 7 = (meet‘𝐾)
1611, 15latmcl 17951 . . . . . 6 ((𝐾 ∈ Lat ∧ 𝑧𝐵𝑊𝐵) → (𝑧 𝑊) ∈ 𝐵)
177, 10, 14, 16syl3anc 1373 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆𝐵𝑆 ≠ ∅)) ∧ 𝑧𝑆) → (𝑧 𝑊) ∈ 𝐵)
18 eqidd 2738 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆𝐵𝑆 ≠ ∅)) ∧ 𝑧𝑆) → (𝑧 𝑊) = (𝑧 𝑊))
19 oveq1 7225 . . . . . . 7 (𝑣 = 𝑧 → (𝑣 𝑊) = (𝑧 𝑊))
2019rspceeqv 3557 . . . . . 6 ((𝑧𝑆 ∧ (𝑧 𝑊) = (𝑧 𝑊)) → ∃𝑣𝑆 (𝑧 𝑊) = (𝑣 𝑊))
219, 18, 20syl2anc 587 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆𝐵𝑆 ≠ ∅)) ∧ 𝑧𝑆) → ∃𝑣𝑆 (𝑧 𝑊) = (𝑣 𝑊))
22 ovex 7251 . . . . . 6 (𝑧 𝑊) ∈ V
23 eleq1 2825 . . . . . . 7 (𝑤 = (𝑧 𝑊) → (𝑤 ∈ {𝑢𝐵 ∣ ∃𝑣𝑆 𝑢 = (𝑣 𝑊)} ↔ (𝑧 𝑊) ∈ {𝑢𝐵 ∣ ∃𝑣𝑆 𝑢 = (𝑣 𝑊)}))
24 eqeq1 2741 . . . . . . . . 9 (𝑢 = (𝑧 𝑊) → (𝑢 = (𝑣 𝑊) ↔ (𝑧 𝑊) = (𝑣 𝑊)))
2524rexbidv 3221 . . . . . . . 8 (𝑢 = (𝑧 𝑊) → (∃𝑣𝑆 𝑢 = (𝑣 𝑊) ↔ ∃𝑣𝑆 (𝑧 𝑊) = (𝑣 𝑊)))
2625elrab 3607 . . . . . . 7 ((𝑧 𝑊) ∈ {𝑢𝐵 ∣ ∃𝑣𝑆 𝑢 = (𝑣 𝑊)} ↔ ((𝑧 𝑊) ∈ 𝐵 ∧ ∃𝑣𝑆 (𝑧 𝑊) = (𝑣 𝑊)))
2723, 26bitrdi 290 . . . . . 6 (𝑤 = (𝑧 𝑊) → (𝑤 ∈ {𝑢𝐵 ∣ ∃𝑣𝑆 𝑢 = (𝑣 𝑊)} ↔ ((𝑧 𝑊) ∈ 𝐵 ∧ ∃𝑣𝑆 (𝑧 𝑊) = (𝑣 𝑊))))
2822, 27spcev 3526 . . . . 5 (((𝑧 𝑊) ∈ 𝐵 ∧ ∃𝑣𝑆 (𝑧 𝑊) = (𝑣 𝑊)) → ∃𝑤 𝑤 ∈ {𝑢𝐵 ∣ ∃𝑣𝑆 𝑢 = (𝑣 𝑊)})
2917, 21, 28syl2anc 587 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆𝐵𝑆 ≠ ∅)) ∧ 𝑧𝑆) → ∃𝑤 𝑤 ∈ {𝑢𝐵 ∣ ∃𝑣𝑆 𝑢 = (𝑣 𝑊)})
30 n0 4266 . . . 4 ({𝑢𝐵 ∣ ∃𝑣𝑆 𝑢 = (𝑣 𝑊)} ≠ ∅ ↔ ∃𝑤 𝑤 ∈ {𝑢𝐵 ∣ ∃𝑣𝑆 𝑢 = (𝑣 𝑊)})
3129, 30sylibr 237 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆𝐵𝑆 ≠ ∅)) ∧ 𝑧𝑆) → {𝑢𝐵 ∣ ∃𝑣𝑆 𝑢 = (𝑣 𝑊)} ≠ ∅)
325, 31exlimddv 1943 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆𝐵𝑆 ≠ ∅)) → {𝑢𝐵 ∣ ∃𝑣𝑆 𝑢 = (𝑣 𝑊)} ≠ ∅)
332, 32eqnetrd 3008 1 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆𝐵𝑆 ≠ ∅)) → 𝑇 ≠ ∅)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399   = wceq 1543  wex 1787  wcel 2110  wne 2940  wrex 3062  {crab 3065  wss 3871  c0 4242  cfv 6385  (class class class)co 7218  Basecbs 16765  lecple 16814  glbcglb 17822  meetcmee 17824  Latclat 17942  HLchlt 37106  LHypclh 37740
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-rep 5184  ax-sep 5197  ax-nul 5204  ax-pow 5263  ax-pr 5327  ax-un 7528
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-ral 3066  df-rex 3067  df-reu 3068  df-rab 3070  df-v 3415  df-sbc 3700  df-csb 3817  df-dif 3874  df-un 3876  df-in 3878  df-ss 3888  df-nul 4243  df-if 4445  df-pw 4520  df-sn 4547  df-pr 4549  df-op 4553  df-uni 4825  df-iun 4911  df-br 5059  df-opab 5121  df-mpt 5141  df-id 5460  df-xp 5562  df-rel 5563  df-cnv 5564  df-co 5565  df-dm 5566  df-rn 5567  df-res 5568  df-ima 5569  df-iota 6343  df-fun 6387  df-fn 6388  df-f 6389  df-f1 6390  df-fo 6391  df-f1o 6392  df-fv 6393  df-riota 7175  df-ov 7221  df-oprab 7222  df-lub 17857  df-glb 17858  df-join 17859  df-meet 17860  df-lat 17943  df-atl 37054  df-cvlat 37078  df-hlat 37107  df-lhyp 37744
This theorem is referenced by:  dihglblem3N  39051
  Copyright terms: Public domain W3C validator