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

Theorem isacs 17348
Description: A set is an algebraic closure system iff it is specified by some function of the finite subsets, such that a set is closed iff it does not expand under the operation. (Contributed by Stefan O'Rear, 2-Apr-2015.)
Assertion
Ref Expression
isacs (𝐶 ∈ (ACS‘𝑋) ↔ (𝐶 ∈ (Moore‘𝑋) ∧ ∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑠 ∈ 𝒫 𝑋(𝑠𝐶 (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠))))
Distinct variable groups:   𝐶,𝑓,𝑠   𝑓,𝑋,𝑠

Proof of Theorem isacs
Dummy variables 𝑐 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elfvex 6800 . 2 (𝐶 ∈ (ACS‘𝑋) → 𝑋 ∈ V)
2 elfvex 6800 . . 3 (𝐶 ∈ (Moore‘𝑋) → 𝑋 ∈ V)
32adantr 481 . 2 ((𝐶 ∈ (Moore‘𝑋) ∧ ∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑠 ∈ 𝒫 𝑋(𝑠𝐶 (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠))) → 𝑋 ∈ V)
4 fveq2 6767 . . . . . 6 (𝑥 = 𝑋 → (Moore‘𝑥) = (Moore‘𝑋))
5 pweq 4550 . . . . . . . . 9 (𝑥 = 𝑋 → 𝒫 𝑥 = 𝒫 𝑋)
65, 5feq23d 6588 . . . . . . . 8 (𝑥 = 𝑋 → (𝑓:𝒫 𝑥⟶𝒫 𝑥𝑓:𝒫 𝑋⟶𝒫 𝑋))
75raleqdv 3346 . . . . . . . 8 (𝑥 = 𝑋 → (∀𝑠 ∈ 𝒫 𝑥(𝑠𝑐 (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠) ↔ ∀𝑠 ∈ 𝒫 𝑋(𝑠𝑐 (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠)))
86, 7anbi12d 631 . . . . . . 7 (𝑥 = 𝑋 → ((𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑠 ∈ 𝒫 𝑥(𝑠𝑐 (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠)) ↔ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑠 ∈ 𝒫 𝑋(𝑠𝑐 (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠))))
98exbidv 1924 . . . . . 6 (𝑥 = 𝑋 → (∃𝑓(𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑠 ∈ 𝒫 𝑥(𝑠𝑐 (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠)) ↔ ∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑠 ∈ 𝒫 𝑋(𝑠𝑐 (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠))))
104, 9rabeqbidv 3418 . . . . 5 (𝑥 = 𝑋 → {𝑐 ∈ (Moore‘𝑥) ∣ ∃𝑓(𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑠 ∈ 𝒫 𝑥(𝑠𝑐 (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠))} = {𝑐 ∈ (Moore‘𝑋) ∣ ∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑠 ∈ 𝒫 𝑋(𝑠𝑐 (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠))})
11 df-acs 17286 . . . . 5 ACS = (𝑥 ∈ V ↦ {𝑐 ∈ (Moore‘𝑥) ∣ ∃𝑓(𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑠 ∈ 𝒫 𝑥(𝑠𝑐 (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠))})
12 fvex 6780 . . . . . 6 (Moore‘𝑋) ∈ V
1312rabex 5255 . . . . 5 {𝑐 ∈ (Moore‘𝑋) ∣ ∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑠 ∈ 𝒫 𝑋(𝑠𝑐 (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠))} ∈ V
1410, 11, 13fvmpt 6868 . . . 4 (𝑋 ∈ V → (ACS‘𝑋) = {𝑐 ∈ (Moore‘𝑋) ∣ ∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑠 ∈ 𝒫 𝑋(𝑠𝑐 (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠))})
1514eleq2d 2824 . . 3 (𝑋 ∈ V → (𝐶 ∈ (ACS‘𝑋) ↔ 𝐶 ∈ {𝑐 ∈ (Moore‘𝑋) ∣ ∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑠 ∈ 𝒫 𝑋(𝑠𝑐 (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠))}))
16 eleq2 2827 . . . . . . . 8 (𝑐 = 𝐶 → (𝑠𝑐𝑠𝐶))
1716bibi1d 344 . . . . . . 7 (𝑐 = 𝐶 → ((𝑠𝑐 (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠) ↔ (𝑠𝐶 (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠)))
1817ralbidv 3108 . . . . . 6 (𝑐 = 𝐶 → (∀𝑠 ∈ 𝒫 𝑋(𝑠𝑐 (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠) ↔ ∀𝑠 ∈ 𝒫 𝑋(𝑠𝐶 (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠)))
1918anbi2d 629 . . . . 5 (𝑐 = 𝐶 → ((𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑠 ∈ 𝒫 𝑋(𝑠𝑐 (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠)) ↔ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑠 ∈ 𝒫 𝑋(𝑠𝐶 (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠))))
2019exbidv 1924 . . . 4 (𝑐 = 𝐶 → (∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑠 ∈ 𝒫 𝑋(𝑠𝑐 (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠)) ↔ ∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑠 ∈ 𝒫 𝑋(𝑠𝐶 (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠))))
2120elrab 3624 . . 3 (𝐶 ∈ {𝑐 ∈ (Moore‘𝑋) ∣ ∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑠 ∈ 𝒫 𝑋(𝑠𝑐 (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠))} ↔ (𝐶 ∈ (Moore‘𝑋) ∧ ∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑠 ∈ 𝒫 𝑋(𝑠𝐶 (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠))))
2215, 21bitrdi 287 . 2 (𝑋 ∈ V → (𝐶 ∈ (ACS‘𝑋) ↔ (𝐶 ∈ (Moore‘𝑋) ∧ ∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑠 ∈ 𝒫 𝑋(𝑠𝐶 (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠)))))
231, 3, 22pm5.21nii 380 1 (𝐶 ∈ (ACS‘𝑋) ↔ (𝐶 ∈ (Moore‘𝑋) ∧ ∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑠 ∈ 𝒫 𝑋(𝑠𝐶 (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠))))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 396   = wceq 1539  wex 1782  wcel 2106  wral 3064  {crab 3068  Vcvv 3430  cin 3886  wss 3887  𝒫 cpw 4534   cuni 4840  cima 5588  wf 6423  cfv 6427  Fincfn 8721  Moorecmre 17279  ACScacs 17282
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5222  ax-nul 5229  ax-pr 5351
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3432  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4258  df-if 4461  df-pw 4536  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-br 5075  df-opab 5137  df-mpt 5158  df-id 5485  df-xp 5591  df-rel 5592  df-cnv 5593  df-co 5594  df-dm 5595  df-rn 5596  df-iota 6385  df-fun 6429  df-fn 6430  df-f 6431  df-fv 6435  df-acs 17286
This theorem is referenced by:  acsmre  17349  isacs2  17350  isacs1i  17354  mreacs  17355
  Copyright terms: Public domain W3C validator