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

Theorem mrcval 16468
Description: Evaluation of the Moore closure of a set. (Contributed by Stefan O'Rear, 31-Jan-2015.) (Proof shortened by Fan Zheng, 6-Jun-2016.)
Hypothesis
Ref Expression
mrcfval.f 𝐹 = (mrCls‘𝐶)
Assertion
Ref Expression
mrcval ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈𝑋) → (𝐹𝑈) = {𝑠𝐶𝑈𝑠})
Distinct variable groups:   𝐹,𝑠   𝐶,𝑠   𝑋,𝑠   𝑈,𝑠

Proof of Theorem mrcval
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 mrcfval.f . . . 4 𝐹 = (mrCls‘𝐶)
21mrcfval 16466 . . 3 (𝐶 ∈ (Moore‘𝑋) → 𝐹 = (𝑥 ∈ 𝒫 𝑋 {𝑠𝐶𝑥𝑠}))
32adantr 472 . 2 ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈𝑋) → 𝐹 = (𝑥 ∈ 𝒫 𝑋 {𝑠𝐶𝑥𝑠}))
4 sseq1 3763 . . . . 5 (𝑥 = 𝑈 → (𝑥𝑠𝑈𝑠))
54rabbidv 3325 . . . 4 (𝑥 = 𝑈 → {𝑠𝐶𝑥𝑠} = {𝑠𝐶𝑈𝑠})
65inteqd 4628 . . 3 (𝑥 = 𝑈 {𝑠𝐶𝑥𝑠} = {𝑠𝐶𝑈𝑠})
76adantl 473 . 2 (((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈𝑋) ∧ 𝑥 = 𝑈) → {𝑠𝐶𝑥𝑠} = {𝑠𝐶𝑈𝑠})
8 mre1cl 16452 . . . 4 (𝐶 ∈ (Moore‘𝑋) → 𝑋𝐶)
9 elpw2g 4972 . . . 4 (𝑋𝐶 → (𝑈 ∈ 𝒫 𝑋𝑈𝑋))
108, 9syl 17 . . 3 (𝐶 ∈ (Moore‘𝑋) → (𝑈 ∈ 𝒫 𝑋𝑈𝑋))
1110biimpar 503 . 2 ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈𝑋) → 𝑈 ∈ 𝒫 𝑋)
128adantr 472 . . . . 5 ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈𝑋) → 𝑋𝐶)
13 simpr 479 . . . . 5 ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈𝑋) → 𝑈𝑋)
14 sseq2 3764 . . . . . 6 (𝑠 = 𝑋 → (𝑈𝑠𝑈𝑋))
1514elrab 3500 . . . . 5 (𝑋 ∈ {𝑠𝐶𝑈𝑠} ↔ (𝑋𝐶𝑈𝑋))
1612, 13, 15sylanbrc 701 . . . 4 ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈𝑋) → 𝑋 ∈ {𝑠𝐶𝑈𝑠})
17 ne0i 4060 . . . 4 (𝑋 ∈ {𝑠𝐶𝑈𝑠} → {𝑠𝐶𝑈𝑠} ≠ ∅)
1816, 17syl 17 . . 3 ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈𝑋) → {𝑠𝐶𝑈𝑠} ≠ ∅)
19 intex 4965 . . 3 ({𝑠𝐶𝑈𝑠} ≠ ∅ ↔ {𝑠𝐶𝑈𝑠} ∈ V)
2018, 19sylib 208 . 2 ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈𝑋) → {𝑠𝐶𝑈𝑠} ∈ V)
213, 7, 11, 20fvmptd 6446 1 ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈𝑋) → (𝐹𝑈) = {𝑠𝐶𝑈𝑠})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383   = wceq 1628  wcel 2135  wne 2928  {crab 3050  Vcvv 3336  wss 3711  c0 4054  𝒫 cpw 4298   cint 4623  cmpt 4877  cfv 6045  Moorecmre 16440  mrClscmrc 16441
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1867  ax-4 1882  ax-5 1984  ax-6 2050  ax-7 2086  ax-8 2137  ax-9 2144  ax-10 2164  ax-11 2179  ax-12 2192  ax-13 2387  ax-ext 2736  ax-sep 4929  ax-nul 4937  ax-pow 4988  ax-pr 5051  ax-un 7110
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1631  df-ex 1850  df-nf 1855  df-sb 2043  df-eu 2607  df-mo 2608  df-clab 2743  df-cleq 2749  df-clel 2752  df-nfc 2887  df-ne 2929  df-ral 3051  df-rex 3052  df-rab 3055  df-v 3338  df-sbc 3573  df-csb 3671  df-dif 3714  df-un 3716  df-in 3718  df-ss 3725  df-nul 4055  df-if 4227  df-pw 4300  df-sn 4318  df-pr 4320  df-op 4324  df-uni 4585  df-int 4624  df-br 4801  df-opab 4861  df-mpt 4878  df-id 5170  df-xp 5268  df-rel 5269  df-cnv 5270  df-co 5271  df-dm 5272  df-rn 5273  df-res 5274  df-ima 5275  df-iota 6008  df-fun 6047  df-fn 6048  df-f 6049  df-fv 6053  df-mre 16444  df-mrc 16445
This theorem is referenced by:  mrcid  16471  mrcss  16474  mrcssid  16475  cycsubg2  17828  aspval2  19545
  Copyright terms: Public domain W3C validator