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

Theorem cdleme17d4 40026
Description: TODO: FIX COMMENT. (Contributed by NM, 11-Apr-2013.)
Hypotheses
Ref Expression
cdlemef46.b 𝐡 = (Baseβ€˜πΎ)
cdlemef46.l ≀ = (leβ€˜πΎ)
cdlemef46.j ∨ = (joinβ€˜πΎ)
cdlemef46.m ∧ = (meetβ€˜πΎ)
cdlemef46.a 𝐴 = (Atomsβ€˜πΎ)
cdlemef46.h 𝐻 = (LHypβ€˜πΎ)
cdlemef46.u π‘ˆ = ((𝑃 ∨ 𝑄) ∧ π‘Š)
cdlemef46.d 𝐷 = ((𝑑 ∨ π‘ˆ) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑑) ∧ π‘Š)))
cdlemefs46.e 𝐸 = ((𝑃 ∨ 𝑄) ∧ (𝐷 ∨ ((𝑠 ∨ 𝑑) ∧ π‘Š)))
cdlemef46.f 𝐹 = (π‘₯ ∈ 𝐡 ↦ if((𝑃 β‰  𝑄 ∧ Β¬ π‘₯ ≀ π‘Š), (℩𝑧 ∈ 𝐡 βˆ€π‘  ∈ 𝐴 ((Β¬ 𝑠 ≀ π‘Š ∧ (𝑠 ∨ (π‘₯ ∧ π‘Š)) = π‘₯) β†’ 𝑧 = (if(𝑠 ≀ (𝑃 ∨ 𝑄), (℩𝑦 ∈ 𝐡 βˆ€π‘‘ ∈ 𝐴 ((Β¬ 𝑑 ≀ π‘Š ∧ Β¬ 𝑑 ≀ (𝑃 ∨ 𝑄)) β†’ 𝑦 = 𝐸)), ⦋𝑠 / π‘‘β¦Œπ·) ∨ (π‘₯ ∧ π‘Š)))), π‘₯))
Assertion
Ref Expression
cdleme17d4 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š)) ∧ 𝑃 = 𝑄) β†’ (πΉβ€˜π‘ƒ) = 𝑄)
Distinct variable groups:   𝑑,𝑠,π‘₯,𝑦,𝑧,𝐴   𝐡,𝑠,𝑑,π‘₯,𝑦,𝑧   𝐷,𝑠,π‘₯,𝑦,𝑧   π‘₯,𝐸,𝑦,𝑧   𝐻,𝑠,𝑑,π‘₯,𝑦,𝑧   ∨ ,𝑠,𝑑,π‘₯,𝑦,𝑧   𝐾,𝑠,𝑑,π‘₯,𝑦,𝑧   ≀ ,𝑠,𝑑,π‘₯,𝑦,𝑧   ∧ ,𝑠,𝑑,π‘₯,𝑦,𝑧   𝑃,𝑠,𝑑,π‘₯,𝑦,𝑧   𝑄,𝑠,𝑑,π‘₯,𝑦,𝑧   π‘ˆ,𝑠,𝑑,π‘₯,𝑦,𝑧   π‘Š,𝑠,𝑑,π‘₯,𝑦,𝑧
Allowed substitution hints:   𝐷(𝑑)   𝐸(𝑑,𝑠)   𝐹(π‘₯,𝑦,𝑧,𝑑,𝑠)

Proof of Theorem cdleme17d4
StepHypRef Expression
1 simp2l 1196 . . . 4 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š)) β†’ 𝑃 ∈ 𝐴)
2 cdlemef46.b . . . . 5 𝐡 = (Baseβ€˜πΎ)
3 cdlemef46.a . . . . 5 𝐴 = (Atomsβ€˜πΎ)
42, 3atbase 38817 . . . 4 (𝑃 ∈ 𝐴 β†’ 𝑃 ∈ 𝐡)
51, 4syl 17 . . 3 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š)) β†’ 𝑃 ∈ 𝐡)
6 cdlemef46.f . . . 4 𝐹 = (π‘₯ ∈ 𝐡 ↦ if((𝑃 β‰  𝑄 ∧ Β¬ π‘₯ ≀ π‘Š), (℩𝑧 ∈ 𝐡 βˆ€π‘  ∈ 𝐴 ((Β¬ 𝑠 ≀ π‘Š ∧ (𝑠 ∨ (π‘₯ ∧ π‘Š)) = π‘₯) β†’ 𝑧 = (if(𝑠 ≀ (𝑃 ∨ 𝑄), (℩𝑦 ∈ 𝐡 βˆ€π‘‘ ∈ 𝐴 ((Β¬ 𝑑 ≀ π‘Š ∧ Β¬ 𝑑 ≀ (𝑃 ∨ 𝑄)) β†’ 𝑦 = 𝐸)), ⦋𝑠 / π‘‘β¦Œπ·) ∨ (π‘₯ ∧ π‘Š)))), π‘₯))
76cdleme31id 39923 . . 3 ((𝑃 ∈ 𝐡 ∧ 𝑃 = 𝑄) β†’ (πΉβ€˜π‘ƒ) = 𝑃)
85, 7sylan 578 . 2 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š)) ∧ 𝑃 = 𝑄) β†’ (πΉβ€˜π‘ƒ) = 𝑃)
9 simpr 483 . 2 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š)) ∧ 𝑃 = 𝑄) β†’ 𝑃 = 𝑄)
108, 9eqtrd 2765 1 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š)) ∧ 𝑃 = 𝑄) β†’ (πΉβ€˜π‘ƒ) = 𝑄)
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ∧ wa 394   ∧ w3a 1084   = wceq 1533   ∈ wcel 2098   β‰  wne 2930  βˆ€wral 3051  β¦‹csb 3884  ifcif 4524   class class class wbr 5143   ↦ cmpt 5226  β€˜cfv 6543  β„©crio 7371  (class class class)co 7416  Basecbs 17179  lecple 17239  joincjn 18302  meetcmee 18303  Atomscatm 38791  HLchlt 38878  LHypclh 39513
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5294  ax-nul 5301  ax-pr 5423
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2931  df-ral 3052  df-rex 3061  df-rab 3420  df-v 3465  df-sbc 3769  df-csb 3885  df-dif 3942  df-un 3944  df-in 3946  df-ss 3956  df-nul 4319  df-if 4525  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-br 5144  df-opab 5206  df-mpt 5227  df-id 5570  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-iota 6495  df-fun 6545  df-fv 6551  df-ats 38795
This theorem is referenced by:  cdleme17d  40027
  Copyright terms: Public domain W3C validator