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

Theorem meet0 17403
Description: Lemma for odujoin 17408. (Contributed by Stefan O'Rear, 29-Jan-2015.) TODO (df-riota 6803 update): This proof increased from 152 bytes to 547 bytes after the df-riota 6803 change. Any way to shorten it? join0 17404 also.
Assertion
Ref Expression
meet0 (meet‘∅) = ∅

Proof of Theorem meet0
Dummy variables 𝑥 𝑦 𝑧 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 0ex 4950 . . 3 ∅ ∈ V
2 eqid 2765 . . . 4 (glb‘∅) = (glb‘∅)
3 eqid 2765 . . . 4 (meet‘∅) = (meet‘∅)
42, 3meetfval 17281 . . 3 (∅ ∈ V → (meet‘∅) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ {𝑥, 𝑦} (glb‘∅)𝑧})
51, 4ax-mp 5 . 2 (meet‘∅) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ {𝑥, 𝑦} (glb‘∅)𝑧}
6 df-oprab 6846 . . 3 {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ {𝑥, 𝑦} (glb‘∅)𝑧} = {𝑤 ∣ ∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ {𝑥, 𝑦} (glb‘∅)𝑧)}
7 br0 4858 . . . . . . . . 9 ¬ {𝑥, 𝑦}∅𝑧
8 base0 16184 . . . . . . . . . . . . 13 ∅ = (Base‘∅)
9 eqid 2765 . . . . . . . . . . . . 13 (le‘∅) = (le‘∅)
10 biid 252 . . . . . . . . . . . . 13 ((∀𝑧𝑥 𝑦(le‘∅)𝑧 ∧ ∀𝑤 ∈ ∅ (∀𝑧𝑥 𝑤(le‘∅)𝑧𝑤(le‘∅)𝑦)) ↔ (∀𝑧𝑥 𝑦(le‘∅)𝑧 ∧ ∀𝑤 ∈ ∅ (∀𝑧𝑥 𝑤(le‘∅)𝑧𝑤(le‘∅)𝑦)))
11 id 22 . . . . . . . . . . . . 13 (∅ ∈ V → ∅ ∈ V)
128, 9, 2, 10, 11glbfval 17257 . . . . . . . . . . . 12 (∅ ∈ V → (glb‘∅) = ((𝑥 ∈ 𝒫 ∅ ↦ (𝑦 ∈ ∅ (∀𝑧𝑥 𝑦(le‘∅)𝑧 ∧ ∀𝑤 ∈ ∅ (∀𝑧𝑥 𝑤(le‘∅)𝑧𝑤(le‘∅)𝑦)))) ↾ {𝑥 ∣ ∃!𝑦 ∈ ∅ (∀𝑧𝑥 𝑦(le‘∅)𝑧 ∧ ∀𝑤 ∈ ∅ (∀𝑧𝑥 𝑤(le‘∅)𝑧𝑤(le‘∅)𝑦))}))
131, 12ax-mp 5 . . . . . . . . . . 11 (glb‘∅) = ((𝑥 ∈ 𝒫 ∅ ↦ (𝑦 ∈ ∅ (∀𝑧𝑥 𝑦(le‘∅)𝑧 ∧ ∀𝑤 ∈ ∅ (∀𝑧𝑥 𝑤(le‘∅)𝑧𝑤(le‘∅)𝑦)))) ↾ {𝑥 ∣ ∃!𝑦 ∈ ∅ (∀𝑧𝑥 𝑦(le‘∅)𝑧 ∧ ∀𝑤 ∈ ∅ (∀𝑧𝑥 𝑤(le‘∅)𝑧𝑤(le‘∅)𝑦))})
14 rex0 4102 . . . . . . . . . . . . . . 15 ¬ ∃𝑦 ∈ ∅ (∀𝑧𝑥 𝑦(le‘∅)𝑧 ∧ ∀𝑤 ∈ ∅ (∀𝑧𝑥 𝑤(le‘∅)𝑧𝑤(le‘∅)𝑦))
15 reurex 3308 . . . . . . . . . . . . . . 15 (∃!𝑦 ∈ ∅ (∀𝑧𝑥 𝑦(le‘∅)𝑧 ∧ ∀𝑤 ∈ ∅ (∀𝑧𝑥 𝑤(le‘∅)𝑧𝑤(le‘∅)𝑦)) → ∃𝑦 ∈ ∅ (∀𝑧𝑥 𝑦(le‘∅)𝑧 ∧ ∀𝑤 ∈ ∅ (∀𝑧𝑥 𝑤(le‘∅)𝑧𝑤(le‘∅)𝑦)))
1614, 15mto 188 . . . . . . . . . . . . . 14 ¬ ∃!𝑦 ∈ ∅ (∀𝑧𝑥 𝑦(le‘∅)𝑧 ∧ ∀𝑤 ∈ ∅ (∀𝑧𝑥 𝑤(le‘∅)𝑧𝑤(le‘∅)𝑦))
1716abf 4140 . . . . . . . . . . . . 13 {𝑥 ∣ ∃!𝑦 ∈ ∅ (∀𝑧𝑥 𝑦(le‘∅)𝑧 ∧ ∀𝑤 ∈ ∅ (∀𝑧𝑥 𝑤(le‘∅)𝑧𝑤(le‘∅)𝑦))} = ∅
1817reseq2i 5562 . . . . . . . . . . . 12 ((𝑥 ∈ 𝒫 ∅ ↦ (𝑦 ∈ ∅ (∀𝑧𝑥 𝑦(le‘∅)𝑧 ∧ ∀𝑤 ∈ ∅ (∀𝑧𝑥 𝑤(le‘∅)𝑧𝑤(le‘∅)𝑦)))) ↾ {𝑥 ∣ ∃!𝑦 ∈ ∅ (∀𝑧𝑥 𝑦(le‘∅)𝑧 ∧ ∀𝑤 ∈ ∅ (∀𝑧𝑥 𝑤(le‘∅)𝑧𝑤(le‘∅)𝑦))}) = ((𝑥 ∈ 𝒫 ∅ ↦ (𝑦 ∈ ∅ (∀𝑧𝑥 𝑦(le‘∅)𝑧 ∧ ∀𝑤 ∈ ∅ (∀𝑧𝑥 𝑤(le‘∅)𝑧𝑤(le‘∅)𝑦)))) ↾ ∅)
19 res0 5569 . . . . . . . . . . . 12 ((𝑥 ∈ 𝒫 ∅ ↦ (𝑦 ∈ ∅ (∀𝑧𝑥 𝑦(le‘∅)𝑧 ∧ ∀𝑤 ∈ ∅ (∀𝑧𝑥 𝑤(le‘∅)𝑧𝑤(le‘∅)𝑦)))) ↾ ∅) = ∅
2018, 19eqtri 2787 . . . . . . . . . . 11 ((𝑥 ∈ 𝒫 ∅ ↦ (𝑦 ∈ ∅ (∀𝑧𝑥 𝑦(le‘∅)𝑧 ∧ ∀𝑤 ∈ ∅ (∀𝑧𝑥 𝑤(le‘∅)𝑧𝑤(le‘∅)𝑦)))) ↾ {𝑥 ∣ ∃!𝑦 ∈ ∅ (∀𝑧𝑥 𝑦(le‘∅)𝑧 ∧ ∀𝑤 ∈ ∅ (∀𝑧𝑥 𝑤(le‘∅)𝑧𝑤(le‘∅)𝑦))}) = ∅
2113, 20eqtri 2787 . . . . . . . . . 10 (glb‘∅) = ∅
2221breqi 4815 . . . . . . . . 9 ({𝑥, 𝑦} (glb‘∅)𝑧 ↔ {𝑥, 𝑦}∅𝑧)
237, 22mtbir 314 . . . . . . . 8 ¬ {𝑥, 𝑦} (glb‘∅)𝑧
2423intnan 480 . . . . . . 7 ¬ (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ {𝑥, 𝑦} (glb‘∅)𝑧)
2524nex 1895 . . . . . 6 ¬ ∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ {𝑥, 𝑦} (glb‘∅)𝑧)
2625nex 1895 . . . . 5 ¬ ∃𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ {𝑥, 𝑦} (glb‘∅)𝑧)
2726nex 1895 . . . 4 ¬ ∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ {𝑥, 𝑦} (glb‘∅)𝑧)
2827abf 4140 . . 3 {𝑤 ∣ ∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ {𝑥, 𝑦} (glb‘∅)𝑧)} = ∅
296, 28eqtri 2787 . 2 {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ {𝑥, 𝑦} (glb‘∅)𝑧} = ∅
305, 29eqtri 2787 1 (meet‘∅) = ∅
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384   = wceq 1652  wex 1874  wcel 2155  {cab 2751  wral 3055  wrex 3056  ∃!wreu 3057  Vcvv 3350  c0 4079  𝒫 cpw 4315  {cpr 4336  cop 4340   class class class wbr 4809  cmpt 4888  cres 5279  cfv 6068  crio 6802  {coprab 6843  lecple 16221  glbcglb 17209  meetcmee 17211
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4930  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-op 4341  df-uni 4595  df-iun 4678  df-br 4810  df-opab 4872  df-mpt 4889  df-id 5185  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-riota 6803  df-oprab 6846  df-slot 16134  df-base 16136  df-glb 17241  df-meet 17243
This theorem is referenced by:  odumeet  17406
  Copyright terms: Public domain W3C validator