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

Theorem mreacs 16235
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 6150 . . 3 (𝑥 = 𝑋 → (ACS‘𝑥) = (ACS‘𝑋))
2 pweq 4138 . . . 4 (𝑥 = 𝑋 → 𝒫 𝑥 = 𝒫 𝑋)
32fveq2d 6154 . . 3 (𝑥 = 𝑋 → (Moore‘𝒫 𝑥) = (Moore‘𝒫 𝑋))
41, 3eleq12d 2698 . 2 (𝑥 = 𝑋 → ((ACS‘𝑥) ∈ (Moore‘𝒫 𝑥) ↔ (ACS‘𝑋) ∈ (Moore‘𝒫 𝑋)))
5 acsmre 16229 . . . . . . . 8 (𝑎 ∈ (ACS‘𝑥) → 𝑎 ∈ (Moore‘𝑥))
6 mresspw 16168 . . . . . . . 8 (𝑎 ∈ (Moore‘𝑥) → 𝑎 ⊆ 𝒫 𝑥)
75, 6syl 17 . . . . . . 7 (𝑎 ∈ (ACS‘𝑥) → 𝑎 ⊆ 𝒫 𝑥)
8 selpw 4142 . . . . . . 7 (𝑎 ∈ 𝒫 𝒫 𝑥𝑎 ⊆ 𝒫 𝑥)
97, 8sylibr 224 . . . . . 6 (𝑎 ∈ (ACS‘𝑥) → 𝑎 ∈ 𝒫 𝒫 𝑥)
109ssriv 3592 . . . . 5 (ACS‘𝑥) ⊆ 𝒫 𝒫 𝑥
1110a1i 11 . . . 4 (⊤ → (ACS‘𝑥) ⊆ 𝒫 𝒫 𝑥)
12 vex 3194 . . . . . . . 8 𝑥 ∈ V
13 mremre 16180 . . . . . . . 8 (𝑥 ∈ V → (Moore‘𝑥) ∈ (Moore‘𝒫 𝑥))
1412, 13mp1i 13 . . . . . . 7 (𝑎 ⊆ (ACS‘𝑥) → (Moore‘𝑥) ∈ (Moore‘𝒫 𝑥))
155ssriv 3592 . . . . . . . 8 (ACS‘𝑥) ⊆ (Moore‘𝑥)
16 sstr 3596 . . . . . . . 8 ((𝑎 ⊆ (ACS‘𝑥) ∧ (ACS‘𝑥) ⊆ (Moore‘𝑥)) → 𝑎 ⊆ (Moore‘𝑥))
1715, 16mpan2 706 . . . . . . 7 (𝑎 ⊆ (ACS‘𝑥) → 𝑎 ⊆ (Moore‘𝑥))
18 mrerintcl 16173 . . . . . . 7 (((Moore‘𝑥) ∈ (Moore‘𝒫 𝑥) ∧ 𝑎 ⊆ (Moore‘𝑥)) → (𝒫 𝑥 𝑎) ∈ (Moore‘𝑥))
1914, 17, 18syl2anc 692 . . . . . 6 (𝑎 ⊆ (ACS‘𝑥) → (𝒫 𝑥 𝑎) ∈ (Moore‘𝑥))
20 ssel2 3583 . . . . . . . . . . . . . . . 16 ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑑𝑎) → 𝑑 ∈ (ACS‘𝑥))
2120acsmred 16233 . . . . . . . . . . . . . . 15 ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑑𝑎) → 𝑑 ∈ (Moore‘𝑥))
22 eqid 2626 . . . . . . . . . . . . . . 15 (mrCls‘𝑑) = (mrCls‘𝑑)
2321, 22mrcssvd 16199 . . . . . . . . . . . . . 14 ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑑𝑎) → ((mrCls‘𝑑)‘𝑐) ⊆ 𝑥)
2423ralrimiva 2965 . . . . . . . . . . . . 13 (𝑎 ⊆ (ACS‘𝑥) → ∀𝑑𝑎 ((mrCls‘𝑑)‘𝑐) ⊆ 𝑥)
2524adantr 481 . . . . . . . . . . . 12 ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑐 ∈ 𝒫 𝑥) → ∀𝑑𝑎 ((mrCls‘𝑑)‘𝑐) ⊆ 𝑥)
26 iunss 4532 . . . . . . . . . . . 12 ( 𝑑𝑎 ((mrCls‘𝑑)‘𝑐) ⊆ 𝑥 ↔ ∀𝑑𝑎 ((mrCls‘𝑑)‘𝑐) ⊆ 𝑥)
2725, 26sylibr 224 . . . . . . . . . . 11 ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑐 ∈ 𝒫 𝑥) → 𝑑𝑎 ((mrCls‘𝑑)‘𝑐) ⊆ 𝑥)
2812elpw2 4793 . . . . . . . . . . 11 ( 𝑑𝑎 ((mrCls‘𝑑)‘𝑐) ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐) ⊆ 𝑥)
2927, 28sylibr 224 . . . . . . . . . 10 ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑐 ∈ 𝒫 𝑥) → 𝑑𝑎 ((mrCls‘𝑑)‘𝑐) ∈ 𝒫 𝑥)
30 eqid 2626 . . . . . . . . . 10 (𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) = (𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐))
3129, 30fmptd 6341 . . . . . . . . 9 (𝑎 ⊆ (ACS‘𝑥) → (𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)):𝒫 𝑥⟶𝒫 𝑥)
32 fssxp 6019 . . . . . . . . 9 ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)):𝒫 𝑥⟶𝒫 𝑥 → (𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) ⊆ (𝒫 𝑥 × 𝒫 𝑥))
3331, 32syl 17 . . . . . . . 8 (𝑎 ⊆ (ACS‘𝑥) → (𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) ⊆ (𝒫 𝑥 × 𝒫 𝑥))
34 vpwex 4814 . . . . . . . . 9 𝒫 𝑥 ∈ V
3534, 34xpex 6916 . . . . . . . 8 (𝒫 𝑥 × 𝒫 𝑥) ∈ V
36 ssexg 4769 . . . . . . . 8 (((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) ⊆ (𝒫 𝑥 × 𝒫 𝑥) ∧ (𝒫 𝑥 × 𝒫 𝑥) ∈ V) → (𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) ∈ V)
3733, 35, 36sylancl 693 . . . . . . 7 (𝑎 ⊆ (ACS‘𝑥) → (𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) ∈ V)
3820adantlr 750 . . . . . . . . . . . . 13 (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑑𝑎) → 𝑑 ∈ (ACS‘𝑥))
39 elpwi 4145 . . . . . . . . . . . . . 14 (𝑏 ∈ 𝒫 𝑥𝑏𝑥)
4039ad2antlr 762 . . . . . . . . . . . . 13 (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑑𝑎) → 𝑏𝑥)
4122acsfiel2 16232 . . . . . . . . . . . . 13 ((𝑑 ∈ (ACS‘𝑥) ∧ 𝑏𝑥) → (𝑏𝑑 ↔ ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)((mrCls‘𝑑)‘𝑒) ⊆ 𝑏))
4238, 40, 41syl2anc 692 . . . . . . . . . . . 12 (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑑𝑎) → (𝑏𝑑 ↔ ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)((mrCls‘𝑑)‘𝑒) ⊆ 𝑏))
4342ralbidva 2984 . . . . . . . . . . 11 ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → (∀𝑑𝑎 𝑏𝑑 ↔ ∀𝑑𝑎𝑒 ∈ (𝒫 𝑏 ∩ Fin)((mrCls‘𝑑)‘𝑒) ⊆ 𝑏))
44 iunss 4532 . . . . . . . . . . . . 13 ( 𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏 ↔ ∀𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏)
4544ralbii 2979 . . . . . . . . . . . 12 (∀𝑒 ∈ (𝒫 𝑏 ∩ Fin) 𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏 ↔ ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)∀𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏)
46 ralcom 3095 . . . . . . . . . . . 12 (∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)∀𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏 ↔ ∀𝑑𝑎𝑒 ∈ (𝒫 𝑏 ∩ Fin)((mrCls‘𝑑)‘𝑒) ⊆ 𝑏)
4745, 46bitri 264 . . . . . . . . . . 11 (∀𝑒 ∈ (𝒫 𝑏 ∩ Fin) 𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏 ↔ ∀𝑑𝑎𝑒 ∈ (𝒫 𝑏 ∩ Fin)((mrCls‘𝑑)‘𝑒) ⊆ 𝑏)
4843, 47syl6bbr 278 . . . . . . . . . 10 ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → (∀𝑑𝑎 𝑏𝑑 ↔ ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin) 𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏))
49 elrint2 4489 . . . . . . . . . . 11 (𝑏 ∈ 𝒫 𝑥 → (𝑏 ∈ (𝒫 𝑥 𝑎) ↔ ∀𝑑𝑎 𝑏𝑑))
5049adantl 482 . . . . . . . . . 10 ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → (𝑏 ∈ (𝒫 𝑥 𝑎) ↔ ∀𝑑𝑎 𝑏𝑑))
51 funmpt 5886 . . . . . . . . . . . . 13 Fun (𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐))
52 funiunfv 6461 . . . . . . . . . . . . 13 (Fun (𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) → 𝑒 ∈ (𝒫 𝑏 ∩ Fin)((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) = ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)))
5351, 52ax-mp 5 . . . . . . . . . . . 12 𝑒 ∈ (𝒫 𝑏 ∩ Fin)((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) = ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin))
5453sseq1i 3613 . . . . . . . . . . 11 ( 𝑒 ∈ (𝒫 𝑏 ∩ Fin)((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) ⊆ 𝑏 ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏)
55 iunss 4532 . . . . . . . . . . . 12 ( 𝑒 ∈ (𝒫 𝑏 ∩ Fin)((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) ⊆ 𝑏 ↔ ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) ⊆ 𝑏)
56 inss1 3816 . . . . . . . . . . . . . . . . 17 (𝒫 𝑏 ∩ Fin) ⊆ 𝒫 𝑏
57 sspwb 4883 . . . . . . . . . . . . . . . . . . 19 (𝑏𝑥 ↔ 𝒫 𝑏 ⊆ 𝒫 𝑥)
5839, 57sylib 208 . . . . . . . . . . . . . . . . . 18 (𝑏 ∈ 𝒫 𝑥 → 𝒫 𝑏 ⊆ 𝒫 𝑥)
5958adantl 482 . . . . . . . . . . . . . . . . 17 ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → 𝒫 𝑏 ⊆ 𝒫 𝑥)
6056, 59syl5ss 3599 . . . . . . . . . . . . . . . 16 ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → (𝒫 𝑏 ∩ Fin) ⊆ 𝒫 𝑥)
6160sselda 3588 . . . . . . . . . . . . . . 15 (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)) → 𝑒 ∈ 𝒫 𝑥)
6221, 22mrcssvd 16199 . . . . . . . . . . . . . . . . . . 19 ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑑𝑎) → ((mrCls‘𝑑)‘𝑒) ⊆ 𝑥)
6362ralrimiva 2965 . . . . . . . . . . . . . . . . . 18 (𝑎 ⊆ (ACS‘𝑥) → ∀𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑥)
6463ad2antrr 761 . . . . . . . . . . . . . . . . 17 (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)) → ∀𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑥)
65 iunss 4532 . . . . . . . . . . . . . . . . 17 ( 𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑥 ↔ ∀𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑥)
6664, 65sylibr 224 . . . . . . . . . . . . . . . 16 (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)) → 𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑥)
67 ssexg 4769 . . . . . . . . . . . . . . . 16 (( 𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑥𝑥 ∈ V) → 𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ∈ V)
6866, 12, 67sylancl 693 . . . . . . . . . . . . . . 15 (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)) → 𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ∈ V)
69 fveq2 6150 . . . . . . . . . . . . . . . . 17 (𝑐 = 𝑒 → ((mrCls‘𝑑)‘𝑐) = ((mrCls‘𝑑)‘𝑒))
7069iuneq2d 4518 . . . . . . . . . . . . . . . 16 (𝑐 = 𝑒 𝑑𝑎 ((mrCls‘𝑑)‘𝑐) = 𝑑𝑎 ((mrCls‘𝑑)‘𝑒))
7170, 30fvmptg 6238 . . . . . . . . . . . . . . 15 ((𝑒 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ∈ V) → ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) = 𝑑𝑎 ((mrCls‘𝑑)‘𝑒))
7261, 68, 71syl2anc 692 . . . . . . . . . . . . . 14 (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)) → ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) = 𝑑𝑎 ((mrCls‘𝑑)‘𝑒))
7372sseq1d 3616 . . . . . . . . . . . . 13 (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)) → (((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) ⊆ 𝑏 𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏))
7473ralbidva 2984 . . . . . . . . . . . 12 ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → (∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) ⊆ 𝑏 ↔ ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin) 𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏))
7555, 74syl5bb 272 . . . . . . . . . . 11 ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → ( 𝑒 ∈ (𝒫 𝑏 ∩ Fin)((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) ⊆ 𝑏 ↔ ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin) 𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏))
7654, 75syl5bbr 274 . . . . . . . . . 10 ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → ( ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏 ↔ ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin) 𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏))
7748, 50, 763bitr4d 300 . . . . . . . . 9 ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → (𝑏 ∈ (𝒫 𝑥 𝑎) ↔ ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏))
7877ralrimiva 2965 . . . . . . . 8 (𝑎 ⊆ (ACS‘𝑥) → ∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 𝑎) ↔ ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏))
7931, 78jca 554 . . . . . . 7 (𝑎 ⊆ (ACS‘𝑥) → ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)):𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 𝑎) ↔ ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏)))
80 feq1 5985 . . . . . . . . 9 (𝑓 = (𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) → (𝑓:𝒫 𝑥⟶𝒫 𝑥 ↔ (𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)):𝒫 𝑥⟶𝒫 𝑥))
81 imaeq1 5424 . . . . . . . . . . . . 13 (𝑓 = (𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) → (𝑓 “ (𝒫 𝑏 ∩ Fin)) = ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)))
8281unieqd 4417 . . . . . . . . . . . 12 (𝑓 = (𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) → (𝑓 “ (𝒫 𝑏 ∩ Fin)) = ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)))
8382sseq1d 3616 . . . . . . . . . . 11 (𝑓 = (𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) → ( (𝑓 “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏 ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏))
8483bibi2d 332 . . . . . . . . . 10 (𝑓 = (𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) → ((𝑏 ∈ (𝒫 𝑥 𝑎) ↔ (𝑓 “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏) ↔ (𝑏 ∈ (𝒫 𝑥 𝑎) ↔ ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏)))
8584ralbidv 2985 . . . . . . . . 9 (𝑓 = (𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) → (∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 𝑎) ↔ (𝑓 “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏) ↔ ∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 𝑎) ↔ ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏)))
8680, 85anbi12d 746 . . . . . . . 8 (𝑓 = (𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) → ((𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 𝑎) ↔ (𝑓 “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏)) ↔ ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)):𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 𝑎) ↔ ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏))))
8786spcegv 3285 . . . . . . 7 ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) ∈ V → (((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)):𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 𝑎) ↔ ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏)) → ∃𝑓(𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 𝑎) ↔ (𝑓 “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏))))
8837, 79, 87sylc 65 . . . . . 6 (𝑎 ⊆ (ACS‘𝑥) → ∃𝑓(𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 𝑎) ↔ (𝑓 “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏)))
89 isacs 16228 . . . . . 6 ((𝒫 𝑥 𝑎) ∈ (ACS‘𝑥) ↔ ((𝒫 𝑥 𝑎) ∈ (Moore‘𝑥) ∧ ∃𝑓(𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 𝑎) ↔ (𝑓 “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏))))
9019, 88, 89sylanbrc 697 . . . . 5 (𝑎 ⊆ (ACS‘𝑥) → (𝒫 𝑥 𝑎) ∈ (ACS‘𝑥))
9190adantl 482 . . . 4 ((⊤ ∧ 𝑎 ⊆ (ACS‘𝑥)) → (𝒫 𝑥 𝑎) ∈ (ACS‘𝑥))
9211, 91ismred2 16179 . . 3 (⊤ → (ACS‘𝑥) ∈ (Moore‘𝒫 𝑥))
9392trud 1490 . 2 (ACS‘𝑥) ∈ (Moore‘𝒫 𝑥)
944, 93vtoclg 3257 1 (𝑋𝑉 → (ACS‘𝑋) ∈ (Moore‘𝒫 𝑋))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384   = wceq 1480  wtru 1481  wex 1701  wcel 1992  wral 2912  Vcvv 3191  cin 3559  wss 3560  𝒫 cpw 4135   cuni 4407   cint 4445   ciun 4490  cmpt 4678   × cxp 5077  cima 5082  Fun wfun 5844  wf 5846  cfv 5850  Fincfn 7900  Moorecmre 16158  mrClscmrc 16159  ACScacs 16161
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-8 1994  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6903
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-eu 2478  df-mo 2479  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-ne 2797  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3193  df-sbc 3423  df-csb 3520  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-op 4160  df-uni 4408  df-int 4446  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-id 4994  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-iota 5813  df-fun 5852  df-fn 5853  df-f 5854  df-fv 5858  df-mre 16162  df-mrc 16163  df-acs 16165
This theorem is referenced by:  acsfn1  16238  acsfn1c  16239  acsfn2  16240  submacs  17281  subgacs  17545  nsgacs  17546  lssacs  18881  acsfn1p  37236  subrgacs  37237  sdrgacs  37238
  Copyright terms: Public domain W3C validator