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

Theorem mreacs 16585
Description: Algebraicity is a composable property; combining several algebraic closure properties gives another. (Contributed by Stefan O'Rear, 3-Apr-2015.)
Assertion
Ref Expression
mreacs (𝑋𝑉 → (ACS‘𝑋) ∈ (Moore‘𝒫 𝑋))

Proof of Theorem mreacs
Dummy variables 𝑎 𝑏 𝑐 𝑥 𝑑 𝑒 𝑓 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fveq2 6374 . . 3 (𝑥 = 𝑋 → (ACS‘𝑥) = (ACS‘𝑋))
2 pweq 4317 . . . 4 (𝑥 = 𝑋 → 𝒫 𝑥 = 𝒫 𝑋)
32fveq2d 6378 . . 3 (𝑥 = 𝑋 → (Moore‘𝒫 𝑥) = (Moore‘𝒫 𝑋))
41, 3eleq12d 2837 . 2 (𝑥 = 𝑋 → ((ACS‘𝑥) ∈ (Moore‘𝒫 𝑥) ↔ (ACS‘𝑋) ∈ (Moore‘𝒫 𝑋)))
5 acsmre 16579 . . . . . . . 8 (𝑎 ∈ (ACS‘𝑥) → 𝑎 ∈ (Moore‘𝑥))
6 mresspw 16519 . . . . . . . 8 (𝑎 ∈ (Moore‘𝑥) → 𝑎 ⊆ 𝒫 𝑥)
75, 6syl 17 . . . . . . 7 (𝑎 ∈ (ACS‘𝑥) → 𝑎 ⊆ 𝒫 𝑥)
8 selpw 4321 . . . . . . 7 (𝑎 ∈ 𝒫 𝒫 𝑥𝑎 ⊆ 𝒫 𝑥)
97, 8sylibr 225 . . . . . 6 (𝑎 ∈ (ACS‘𝑥) → 𝑎 ∈ 𝒫 𝒫 𝑥)
109ssriv 3764 . . . . 5 (ACS‘𝑥) ⊆ 𝒫 𝒫 𝑥
1110a1i 11 . . . 4 (⊤ → (ACS‘𝑥) ⊆ 𝒫 𝒫 𝑥)
12 vex 3352 . . . . . . . 8 𝑥 ∈ V
13 mremre 16531 . . . . . . . 8 (𝑥 ∈ V → (Moore‘𝑥) ∈ (Moore‘𝒫 𝑥))
1412, 13mp1i 13 . . . . . . 7 (𝑎 ⊆ (ACS‘𝑥) → (Moore‘𝑥) ∈ (Moore‘𝒫 𝑥))
155ssriv 3764 . . . . . . . 8 (ACS‘𝑥) ⊆ (Moore‘𝑥)
16 sstr 3768 . . . . . . . 8 ((𝑎 ⊆ (ACS‘𝑥) ∧ (ACS‘𝑥) ⊆ (Moore‘𝑥)) → 𝑎 ⊆ (Moore‘𝑥))
1715, 16mpan2 682 . . . . . . 7 (𝑎 ⊆ (ACS‘𝑥) → 𝑎 ⊆ (Moore‘𝑥))
18 mrerintcl 16524 . . . . . . 7 (((Moore‘𝑥) ∈ (Moore‘𝒫 𝑥) ∧ 𝑎 ⊆ (Moore‘𝑥)) → (𝒫 𝑥 𝑎) ∈ (Moore‘𝑥))
1914, 17, 18syl2anc 579 . . . . . 6 (𝑎 ⊆ (ACS‘𝑥) → (𝒫 𝑥 𝑎) ∈ (Moore‘𝑥))
20 ssel2 3755 . . . . . . . . . . . . . . . 16 ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑑𝑎) → 𝑑 ∈ (ACS‘𝑥))
2120acsmred 16583 . . . . . . . . . . . . . . 15 ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑑𝑎) → 𝑑 ∈ (Moore‘𝑥))
22 eqid 2764 . . . . . . . . . . . . . . 15 (mrCls‘𝑑) = (mrCls‘𝑑)
2321, 22mrcssvd 16550 . . . . . . . . . . . . . 14 ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑑𝑎) → ((mrCls‘𝑑)‘𝑐) ⊆ 𝑥)
2423ralrimiva 3112 . . . . . . . . . . . . 13 (𝑎 ⊆ (ACS‘𝑥) → ∀𝑑𝑎 ((mrCls‘𝑑)‘𝑐) ⊆ 𝑥)
2524adantr 472 . . . . . . . . . . . 12 ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑐 ∈ 𝒫 𝑥) → ∀𝑑𝑎 ((mrCls‘𝑑)‘𝑐) ⊆ 𝑥)
26 iunss 4716 . . . . . . . . . . . 12 ( 𝑑𝑎 ((mrCls‘𝑑)‘𝑐) ⊆ 𝑥 ↔ ∀𝑑𝑎 ((mrCls‘𝑑)‘𝑐) ⊆ 𝑥)
2725, 26sylibr 225 . . . . . . . . . . 11 ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑐 ∈ 𝒫 𝑥) → 𝑑𝑎 ((mrCls‘𝑑)‘𝑐) ⊆ 𝑥)
2812elpw2 4985 . . . . . . . . . . 11 ( 𝑑𝑎 ((mrCls‘𝑑)‘𝑐) ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐) ⊆ 𝑥)
2927, 28sylibr 225 . . . . . . . . . 10 ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑐 ∈ 𝒫 𝑥) → 𝑑𝑎 ((mrCls‘𝑑)‘𝑐) ∈ 𝒫 𝑥)
3029fmpttd 6574 . . . . . . . . 9 (𝑎 ⊆ (ACS‘𝑥) → (𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)):𝒫 𝑥⟶𝒫 𝑥)
31 fssxp 6241 . . . . . . . . 9 ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)):𝒫 𝑥⟶𝒫 𝑥 → (𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) ⊆ (𝒫 𝑥 × 𝒫 𝑥))
3230, 31syl 17 . . . . . . . 8 (𝑎 ⊆ (ACS‘𝑥) → (𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) ⊆ (𝒫 𝑥 × 𝒫 𝑥))
33 vpwex 5012 . . . . . . . . 9 𝒫 𝑥 ∈ V
3433, 33xpex 7159 . . . . . . . 8 (𝒫 𝑥 × 𝒫 𝑥) ∈ V
35 ssexg 4964 . . . . . . . 8 (((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) ⊆ (𝒫 𝑥 × 𝒫 𝑥) ∧ (𝒫 𝑥 × 𝒫 𝑥) ∈ V) → (𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) ∈ V)
3632, 34, 35sylancl 580 . . . . . . 7 (𝑎 ⊆ (ACS‘𝑥) → (𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) ∈ V)
3720adantlr 706 . . . . . . . . . . . . 13 (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑑𝑎) → 𝑑 ∈ (ACS‘𝑥))
38 elpwi 4324 . . . . . . . . . . . . . 14 (𝑏 ∈ 𝒫 𝑥𝑏𝑥)
3938ad2antlr 718 . . . . . . . . . . . . 13 (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑑𝑎) → 𝑏𝑥)
4022acsfiel2 16582 . . . . . . . . . . . . 13 ((𝑑 ∈ (ACS‘𝑥) ∧ 𝑏𝑥) → (𝑏𝑑 ↔ ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)((mrCls‘𝑑)‘𝑒) ⊆ 𝑏))
4137, 39, 40syl2anc 579 . . . . . . . . . . . 12 (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑑𝑎) → (𝑏𝑑 ↔ ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)((mrCls‘𝑑)‘𝑒) ⊆ 𝑏))
4241ralbidva 3131 . . . . . . . . . . 11 ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → (∀𝑑𝑎 𝑏𝑑 ↔ ∀𝑑𝑎𝑒 ∈ (𝒫 𝑏 ∩ Fin)((mrCls‘𝑑)‘𝑒) ⊆ 𝑏))
43 iunss 4716 . . . . . . . . . . . . 13 ( 𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏 ↔ ∀𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏)
4443ralbii 3126 . . . . . . . . . . . 12 (∀𝑒 ∈ (𝒫 𝑏 ∩ Fin) 𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏 ↔ ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)∀𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏)
45 ralcom 3244 . . . . . . . . . . . 12 (∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)∀𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏 ↔ ∀𝑑𝑎𝑒 ∈ (𝒫 𝑏 ∩ Fin)((mrCls‘𝑑)‘𝑒) ⊆ 𝑏)
4644, 45bitri 266 . . . . . . . . . . 11 (∀𝑒 ∈ (𝒫 𝑏 ∩ Fin) 𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏 ↔ ∀𝑑𝑎𝑒 ∈ (𝒫 𝑏 ∩ Fin)((mrCls‘𝑑)‘𝑒) ⊆ 𝑏)
4742, 46syl6bbr 280 . . . . . . . . . 10 ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → (∀𝑑𝑎 𝑏𝑑 ↔ ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin) 𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏))
48 elrint2 4674 . . . . . . . . . . 11 (𝑏 ∈ 𝒫 𝑥 → (𝑏 ∈ (𝒫 𝑥 𝑎) ↔ ∀𝑑𝑎 𝑏𝑑))
4948adantl 473 . . . . . . . . . 10 ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → (𝑏 ∈ (𝒫 𝑥 𝑎) ↔ ∀𝑑𝑎 𝑏𝑑))
50 funmpt 6105 . . . . . . . . . . . . 13 Fun (𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐))
51 funiunfv 6697 . . . . . . . . . . . . 13 (Fun (𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) → 𝑒 ∈ (𝒫 𝑏 ∩ Fin)((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) = ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)))
5250, 51ax-mp 5 . . . . . . . . . . . 12 𝑒 ∈ (𝒫 𝑏 ∩ Fin)((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) = ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin))
5352sseq1i 3788 . . . . . . . . . . 11 ( 𝑒 ∈ (𝒫 𝑏 ∩ Fin)((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) ⊆ 𝑏 ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏)
54 iunss 4716 . . . . . . . . . . . 12 ( 𝑒 ∈ (𝒫 𝑏 ∩ Fin)((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) ⊆ 𝑏 ↔ ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) ⊆ 𝑏)
55 inss1 3991 . . . . . . . . . . . . . . . . 17 (𝒫 𝑏 ∩ Fin) ⊆ 𝒫 𝑏
56 sspwb 5072 . . . . . . . . . . . . . . . . . . 19 (𝑏𝑥 ↔ 𝒫 𝑏 ⊆ 𝒫 𝑥)
5738, 56sylib 209 . . . . . . . . . . . . . . . . . 18 (𝑏 ∈ 𝒫 𝑥 → 𝒫 𝑏 ⊆ 𝒫 𝑥)
5857adantl 473 . . . . . . . . . . . . . . . . 17 ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → 𝒫 𝑏 ⊆ 𝒫 𝑥)
5955, 58syl5ss 3771 . . . . . . . . . . . . . . . 16 ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → (𝒫 𝑏 ∩ Fin) ⊆ 𝒫 𝑥)
6059sselda 3760 . . . . . . . . . . . . . . 15 (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)) → 𝑒 ∈ 𝒫 𝑥)
6121, 22mrcssvd 16550 . . . . . . . . . . . . . . . . . . 19 ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑑𝑎) → ((mrCls‘𝑑)‘𝑒) ⊆ 𝑥)
6261ralrimiva 3112 . . . . . . . . . . . . . . . . . 18 (𝑎 ⊆ (ACS‘𝑥) → ∀𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑥)
6362ad2antrr 717 . . . . . . . . . . . . . . . . 17 (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)) → ∀𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑥)
64 iunss 4716 . . . . . . . . . . . . . . . . 17 ( 𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑥 ↔ ∀𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑥)
6563, 64sylibr 225 . . . . . . . . . . . . . . . 16 (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)) → 𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑥)
66 ssexg 4964 . . . . . . . . . . . . . . . 16 (( 𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑥𝑥 ∈ V) → 𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ∈ V)
6765, 12, 66sylancl 580 . . . . . . . . . . . . . . 15 (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)) → 𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ∈ V)
68 fveq2 6374 . . . . . . . . . . . . . . . . 17 (𝑐 = 𝑒 → ((mrCls‘𝑑)‘𝑐) = ((mrCls‘𝑑)‘𝑒))
6968iuneq2d 4702 . . . . . . . . . . . . . . . 16 (𝑐 = 𝑒 𝑑𝑎 ((mrCls‘𝑑)‘𝑐) = 𝑑𝑎 ((mrCls‘𝑑)‘𝑒))
70 eqid 2764 . . . . . . . . . . . . . . . 16 (𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) = (𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐))
7169, 70fvmptg 6468 . . . . . . . . . . . . . . 15 ((𝑒 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ∈ V) → ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) = 𝑑𝑎 ((mrCls‘𝑑)‘𝑒))
7260, 67, 71syl2anc 579 . . . . . . . . . . . . . 14 (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)) → ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) = 𝑑𝑎 ((mrCls‘𝑑)‘𝑒))
7372sseq1d 3791 . . . . . . . . . . . . 13 (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)) → (((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) ⊆ 𝑏 𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏))
7473ralbidva 3131 . . . . . . . . . . . 12 ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → (∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) ⊆ 𝑏 ↔ ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin) 𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏))
7554, 74syl5bb 274 . . . . . . . . . . 11 ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → ( 𝑒 ∈ (𝒫 𝑏 ∩ Fin)((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) ⊆ 𝑏 ↔ ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin) 𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏))
7653, 75syl5bbr 276 . . . . . . . . . 10 ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → ( ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏 ↔ ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin) 𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏))
7747, 49, 763bitr4d 302 . . . . . . . . 9 ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → (𝑏 ∈ (𝒫 𝑥 𝑎) ↔ ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏))
7877ralrimiva 3112 . . . . . . . 8 (𝑎 ⊆ (ACS‘𝑥) → ∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 𝑎) ↔ ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏))
7930, 78jca 507 . . . . . . 7 (𝑎 ⊆ (ACS‘𝑥) → ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)):𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 𝑎) ↔ ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏)))
80 feq1 6203 . . . . . . . . 9 (𝑓 = (𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) → (𝑓:𝒫 𝑥⟶𝒫 𝑥 ↔ (𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)):𝒫 𝑥⟶𝒫 𝑥))
81 imaeq1 5642 . . . . . . . . . . . . 13 (𝑓 = (𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) → (𝑓 “ (𝒫 𝑏 ∩ Fin)) = ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)))
8281unieqd 4603 . . . . . . . . . . . 12 (𝑓 = (𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) → (𝑓 “ (𝒫 𝑏 ∩ Fin)) = ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)))
8382sseq1d 3791 . . . . . . . . . . 11 (𝑓 = (𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) → ( (𝑓 “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏 ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏))
8483bibi2d 333 . . . . . . . . . 10 (𝑓 = (𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) → ((𝑏 ∈ (𝒫 𝑥 𝑎) ↔ (𝑓 “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏) ↔ (𝑏 ∈ (𝒫 𝑥 𝑎) ↔ ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏)))
8584ralbidv 3132 . . . . . . . . 9 (𝑓 = (𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) → (∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 𝑎) ↔ (𝑓 “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏) ↔ ∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 𝑎) ↔ ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏)))
8680, 85anbi12d 624 . . . . . . . 8 (𝑓 = (𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) → ((𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 𝑎) ↔ (𝑓 “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏)) ↔ ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)):𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 𝑎) ↔ ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏))))
8786spcegv 3445 . . . . . . 7 ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) ∈ V → (((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)):𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 𝑎) ↔ ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏)) → ∃𝑓(𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 𝑎) ↔ (𝑓 “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏))))
8836, 79, 87sylc 65 . . . . . 6 (𝑎 ⊆ (ACS‘𝑥) → ∃𝑓(𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 𝑎) ↔ (𝑓 “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏)))
89 isacs 16578 . . . . . 6 ((𝒫 𝑥 𝑎) ∈ (ACS‘𝑥) ↔ ((𝒫 𝑥 𝑎) ∈ (Moore‘𝑥) ∧ ∃𝑓(𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 𝑎) ↔ (𝑓 “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏))))
9019, 88, 89sylanbrc 578 . . . . 5 (𝑎 ⊆ (ACS‘𝑥) → (𝒫 𝑥 𝑎) ∈ (ACS‘𝑥))
9190adantl 473 . . . 4 ((⊤ ∧ 𝑎 ⊆ (ACS‘𝑥)) → (𝒫 𝑥 𝑎) ∈ (ACS‘𝑥))
9211, 91ismred2 16530 . . 3 (⊤ → (ACS‘𝑥) ∈ (Moore‘𝒫 𝑥))
9392mptru 1660 . 2 (ACS‘𝑥) ∈ (Moore‘𝒫 𝑥)
944, 93vtoclg 3417 1 (𝑋𝑉 → (ACS‘𝑋) ∈ (Moore‘𝒫 𝑋))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384   = wceq 1652  wtru 1653  wex 1874  wcel 2155  wral 3054  Vcvv 3349  cin 3730  wss 3731  𝒫 cpw 4314   cuni 4593   cint 4632   ciun 4675  cmpt 4887   × cxp 5274  cima 5279  Fun wfun 6061  wf 6063  cfv 6067  Fincfn 8159  Moorecmre 16509  mrClscmrc 16510  ACScacs 16512
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 2069  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2349  ax-ext 2742  ax-sep 4940  ax-nul 4948  ax-pow 5000  ax-pr 5061  ax-un 7146
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 2062  df-mo 2564  df-eu 2581  df-clab 2751  df-cleq 2757  df-clel 2760  df-nfc 2895  df-ne 2937  df-ral 3059  df-rex 3060  df-rab 3063  df-v 3351  df-sbc 3596  df-csb 3691  df-dif 3734  df-un 3736  df-in 3738  df-ss 3745  df-nul 4079  df-if 4243  df-pw 4316  df-sn 4334  df-pr 4336  df-op 4340  df-uni 4594  df-int 4633  df-iun 4677  df-br 4809  df-opab 4871  df-mpt 4888  df-id 5184  df-xp 5282  df-rel 5283  df-cnv 5284  df-co 5285  df-dm 5286  df-rn 5287  df-res 5288  df-ima 5289  df-iota 6030  df-fun 6069  df-fn 6070  df-f 6071  df-fv 6075  df-mre 16513  df-mrc 16514  df-acs 16516
This theorem is referenced by:  acsfn1  16588  acsfn1c  16589  acsfn2  16590  submacs  17632  subgacs  17894  nsgacs  17895  lssacs  19238  acsfn1p  38378  subrgacs  38379  sdrgacs  38380
  Copyright terms: Public domain W3C validator