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

Theorem acsfn2 16928
 Description: Algebraicity of a two-argument closure condition. (Contributed by Stefan O'Rear, 3-Apr-2015.)
Assertion
Ref Expression
acsfn2 ((𝑋𝑉 ∧ ∀𝑏𝑋𝑐𝑋 𝐸𝑋) → {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑏𝑎𝑐𝑎 𝐸𝑎} ∈ (ACS‘𝑋))
Distinct variable groups:   𝑎,𝑏,𝑐,𝑉   𝑋,𝑎,𝑏,𝑐   𝐸,𝑎
Allowed substitution hints:   𝐸(𝑏,𝑐)

Proof of Theorem acsfn2
StepHypRef Expression
1 elpwi 4550 . . . . 5 (𝑎 ∈ 𝒫 𝑋𝑎𝑋)
2 ralss 4036 . . . . . 6 (𝑎𝑋 → (∀𝑏𝑎𝑐𝑎 𝐸𝑎 ↔ ∀𝑏𝑋 (𝑏𝑎 → ∀𝑐𝑎 𝐸𝑎)))
3 ralss 4036 . . . . . . . 8 (𝑎𝑋 → (∀𝑐𝑎 (𝑏𝑎𝐸𝑎) ↔ ∀𝑐𝑋 (𝑐𝑎 → (𝑏𝑎𝐸𝑎))))
4 r19.21v 3175 . . . . . . . 8 (∀𝑐𝑎 (𝑏𝑎𝐸𝑎) ↔ (𝑏𝑎 → ∀𝑐𝑎 𝐸𝑎))
5 impexp 453 . . . . . . . . . 10 (((𝑐𝑎𝑏𝑎) → 𝐸𝑎) ↔ (𝑐𝑎 → (𝑏𝑎𝐸𝑎)))
6 vex 3497 . . . . . . . . . . . 12 𝑐 ∈ V
7 vex 3497 . . . . . . . . . . . 12 𝑏 ∈ V
86, 7prss 4746 . . . . . . . . . . 11 ((𝑐𝑎𝑏𝑎) ↔ {𝑐, 𝑏} ⊆ 𝑎)
98imbi1i 352 . . . . . . . . . 10 (((𝑐𝑎𝑏𝑎) → 𝐸𝑎) ↔ ({𝑐, 𝑏} ⊆ 𝑎𝐸𝑎))
105, 9bitr3i 279 . . . . . . . . 9 ((𝑐𝑎 → (𝑏𝑎𝐸𝑎)) ↔ ({𝑐, 𝑏} ⊆ 𝑎𝐸𝑎))
1110ralbii 3165 . . . . . . . 8 (∀𝑐𝑋 (𝑐𝑎 → (𝑏𝑎𝐸𝑎)) ↔ ∀𝑐𝑋 ({𝑐, 𝑏} ⊆ 𝑎𝐸𝑎))
123, 4, 113bitr3g 315 . . . . . . 7 (𝑎𝑋 → ((𝑏𝑎 → ∀𝑐𝑎 𝐸𝑎) ↔ ∀𝑐𝑋 ({𝑐, 𝑏} ⊆ 𝑎𝐸𝑎)))
1312ralbidv 3197 . . . . . 6 (𝑎𝑋 → (∀𝑏𝑋 (𝑏𝑎 → ∀𝑐𝑎 𝐸𝑎) ↔ ∀𝑏𝑋𝑐𝑋 ({𝑐, 𝑏} ⊆ 𝑎𝐸𝑎)))
142, 13bitrd 281 . . . . 5 (𝑎𝑋 → (∀𝑏𝑎𝑐𝑎 𝐸𝑎 ↔ ∀𝑏𝑋𝑐𝑋 ({𝑐, 𝑏} ⊆ 𝑎𝐸𝑎)))
151, 14syl 17 . . . 4 (𝑎 ∈ 𝒫 𝑋 → (∀𝑏𝑎𝑐𝑎 𝐸𝑎 ↔ ∀𝑏𝑋𝑐𝑋 ({𝑐, 𝑏} ⊆ 𝑎𝐸𝑎)))
1615rabbiia 3472 . . 3 {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑏𝑎𝑐𝑎 𝐸𝑎} = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑏𝑋𝑐𝑋 ({𝑐, 𝑏} ⊆ 𝑎𝐸𝑎)}
17 riinrab 4998 . . 3 (𝒫 𝑋 𝑏𝑋 {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑐𝑋 ({𝑐, 𝑏} ⊆ 𝑎𝐸𝑎)}) = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑏𝑋𝑐𝑋 ({𝑐, 𝑏} ⊆ 𝑎𝐸𝑎)}
1816, 17eqtr4i 2847 . 2 {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑏𝑎𝑐𝑎 𝐸𝑎} = (𝒫 𝑋 𝑏𝑋 {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑐𝑋 ({𝑐, 𝑏} ⊆ 𝑎𝐸𝑎)})
19 mreacs 16923 . . 3 (𝑋𝑉 → (ACS‘𝑋) ∈ (Moore‘𝒫 𝑋))
20 riinrab 4998 . . . . . . 7 (𝒫 𝑋 𝑐𝑋 {𝑎 ∈ 𝒫 𝑋 ∣ ({𝑐, 𝑏} ⊆ 𝑎𝐸𝑎)}) = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑐𝑋 ({𝑐, 𝑏} ⊆ 𝑎𝐸𝑎)}
2119ad2antrr 724 . . . . . . . 8 (((𝑋𝑉𝑏𝑋) ∧ ∀𝑐𝑋 𝐸𝑋) → (ACS‘𝑋) ∈ (Moore‘𝒫 𝑋))
22 simpll 765 . . . . . . . . . . . 12 (((𝑋𝑉𝑏𝑋) ∧ (𝑐𝑋𝐸𝑋)) → 𝑋𝑉)
23 simprr 771 . . . . . . . . . . . 12 (((𝑋𝑉𝑏𝑋) ∧ (𝑐𝑋𝐸𝑋)) → 𝐸𝑋)
24 prssi 4747 . . . . . . . . . . . . . 14 ((𝑐𝑋𝑏𝑋) → {𝑐, 𝑏} ⊆ 𝑋)
2524ancoms 461 . . . . . . . . . . . . 13 ((𝑏𝑋𝑐𝑋) → {𝑐, 𝑏} ⊆ 𝑋)
2625ad2ant2lr 746 . . . . . . . . . . . 12 (((𝑋𝑉𝑏𝑋) ∧ (𝑐𝑋𝐸𝑋)) → {𝑐, 𝑏} ⊆ 𝑋)
27 prfi 8787 . . . . . . . . . . . . 13 {𝑐, 𝑏} ∈ Fin
2827a1i 11 . . . . . . . . . . . 12 (((𝑋𝑉𝑏𝑋) ∧ (𝑐𝑋𝐸𝑋)) → {𝑐, 𝑏} ∈ Fin)
29 acsfn 16924 . . . . . . . . . . . 12 (((𝑋𝑉𝐸𝑋) ∧ ({𝑐, 𝑏} ⊆ 𝑋 ∧ {𝑐, 𝑏} ∈ Fin)) → {𝑎 ∈ 𝒫 𝑋 ∣ ({𝑐, 𝑏} ⊆ 𝑎𝐸𝑎)} ∈ (ACS‘𝑋))
3022, 23, 26, 28, 29syl22anc 836 . . . . . . . . . . 11 (((𝑋𝑉𝑏𝑋) ∧ (𝑐𝑋𝐸𝑋)) → {𝑎 ∈ 𝒫 𝑋 ∣ ({𝑐, 𝑏} ⊆ 𝑎𝐸𝑎)} ∈ (ACS‘𝑋))
3130expr 459 . . . . . . . . . 10 (((𝑋𝑉𝑏𝑋) ∧ 𝑐𝑋) → (𝐸𝑋 → {𝑎 ∈ 𝒫 𝑋 ∣ ({𝑐, 𝑏} ⊆ 𝑎𝐸𝑎)} ∈ (ACS‘𝑋)))
3231ralimdva 3177 . . . . . . . . 9 ((𝑋𝑉𝑏𝑋) → (∀𝑐𝑋 𝐸𝑋 → ∀𝑐𝑋 {𝑎 ∈ 𝒫 𝑋 ∣ ({𝑐, 𝑏} ⊆ 𝑎𝐸𝑎)} ∈ (ACS‘𝑋)))
3332imp 409 . . . . . . . 8 (((𝑋𝑉𝑏𝑋) ∧ ∀𝑐𝑋 𝐸𝑋) → ∀𝑐𝑋 {𝑎 ∈ 𝒫 𝑋 ∣ ({𝑐, 𝑏} ⊆ 𝑎𝐸𝑎)} ∈ (ACS‘𝑋))
34 mreriincl 16863 . . . . . . . 8 (((ACS‘𝑋) ∈ (Moore‘𝒫 𝑋) ∧ ∀𝑐𝑋 {𝑎 ∈ 𝒫 𝑋 ∣ ({𝑐, 𝑏} ⊆ 𝑎𝐸𝑎)} ∈ (ACS‘𝑋)) → (𝒫 𝑋 𝑐𝑋 {𝑎 ∈ 𝒫 𝑋 ∣ ({𝑐, 𝑏} ⊆ 𝑎𝐸𝑎)}) ∈ (ACS‘𝑋))
3521, 33, 34syl2anc 586 . . . . . . 7 (((𝑋𝑉𝑏𝑋) ∧ ∀𝑐𝑋 𝐸𝑋) → (𝒫 𝑋 𝑐𝑋 {𝑎 ∈ 𝒫 𝑋 ∣ ({𝑐, 𝑏} ⊆ 𝑎𝐸𝑎)}) ∈ (ACS‘𝑋))
3620, 35eqeltrrid 2918 . . . . . 6 (((𝑋𝑉𝑏𝑋) ∧ ∀𝑐𝑋 𝐸𝑋) → {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑐𝑋 ({𝑐, 𝑏} ⊆ 𝑎𝐸𝑎)} ∈ (ACS‘𝑋))
3736ex 415 . . . . 5 ((𝑋𝑉𝑏𝑋) → (∀𝑐𝑋 𝐸𝑋 → {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑐𝑋 ({𝑐, 𝑏} ⊆ 𝑎𝐸𝑎)} ∈ (ACS‘𝑋)))
3837ralimdva 3177 . . . 4 (𝑋𝑉 → (∀𝑏𝑋𝑐𝑋 𝐸𝑋 → ∀𝑏𝑋 {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑐𝑋 ({𝑐, 𝑏} ⊆ 𝑎𝐸𝑎)} ∈ (ACS‘𝑋)))
3938imp 409 . . 3 ((𝑋𝑉 ∧ ∀𝑏𝑋𝑐𝑋 𝐸𝑋) → ∀𝑏𝑋 {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑐𝑋 ({𝑐, 𝑏} ⊆ 𝑎𝐸𝑎)} ∈ (ACS‘𝑋))
40 mreriincl 16863 . . 3 (((ACS‘𝑋) ∈ (Moore‘𝒫 𝑋) ∧ ∀𝑏𝑋 {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑐𝑋 ({𝑐, 𝑏} ⊆ 𝑎𝐸𝑎)} ∈ (ACS‘𝑋)) → (𝒫 𝑋 𝑏𝑋 {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑐𝑋 ({𝑐, 𝑏} ⊆ 𝑎𝐸𝑎)}) ∈ (ACS‘𝑋))
4119, 39, 40syl2an2r 683 . 2 ((𝑋𝑉 ∧ ∀𝑏𝑋𝑐𝑋 𝐸𝑋) → (𝒫 𝑋 𝑏𝑋 {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑐𝑋 ({𝑐, 𝑏} ⊆ 𝑎𝐸𝑎)}) ∈ (ACS‘𝑋))
4218, 41eqeltrid 2917 1 ((𝑋𝑉 ∧ ∀𝑏𝑋𝑐𝑋 𝐸𝑋) → {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑏𝑎𝑐𝑎 𝐸𝑎} ∈ (ACS‘𝑋))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   ∈ wcel 2110  ∀wral 3138  {crab 3142   ∩ cin 3934   ⊆ wss 3935  𝒫 cpw 4538  {cpr 4562  ∩ ciin 4912  ‘cfv 6349  Fincfn 8503  Moorecmre 16847  ACScacs 16850 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7455 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3496  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-pss 3953  df-nul 4291  df-if 4467  df-pw 4540  df-sn 4561  df-pr 4563  df-tp 4565  df-op 4567  df-uni 4832  df-int 4869  df-iun 4913  df-iin 4914  df-br 5059  df-opab 5121  df-mpt 5139  df-tr 5165  df-id 5454  df-eprel 5459  df-po 5468  df-so 5469  df-fr 5508  df-we 5510  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-pred 6142  df-ord 6188  df-on 6189  df-lim 6190  df-suc 6191  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356  df-fv 6357  df-ov 7153  df-oprab 7154  df-mpo 7155  df-om 7575  df-wrecs 7941  df-recs 8002  df-rdg 8040  df-1o 8096  df-oadd 8100  df-er 8283  df-en 8504  df-fin 8507  df-mre 16851  df-mrc 16852  df-acs 16854 This theorem is referenced by:  submacs  17985  submgmacs  44065
 Copyright terms: Public domain W3C validator