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

Theorem mreacs 16313
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 6189 . . 3 (𝑥 = 𝑋 → (ACS‘𝑥) = (ACS‘𝑋))
2 pweq 4159 . . . 4 (𝑥 = 𝑋 → 𝒫 𝑥 = 𝒫 𝑋)
32fveq2d 6193 . . 3 (𝑥 = 𝑋 → (Moore‘𝒫 𝑥) = (Moore‘𝒫 𝑋))
41, 3eleq12d 2694 . 2 (𝑥 = 𝑋 → ((ACS‘𝑥) ∈ (Moore‘𝒫 𝑥) ↔ (ACS‘𝑋) ∈ (Moore‘𝒫 𝑋)))
5 acsmre 16307 . . . . . . . 8 (𝑎 ∈ (ACS‘𝑥) → 𝑎 ∈ (Moore‘𝑥))
6 mresspw 16246 . . . . . . . 8 (𝑎 ∈ (Moore‘𝑥) → 𝑎 ⊆ 𝒫 𝑥)
75, 6syl 17 . . . . . . 7 (𝑎 ∈ (ACS‘𝑥) → 𝑎 ⊆ 𝒫 𝑥)
8 selpw 4163 . . . . . . 7 (𝑎 ∈ 𝒫 𝒫 𝑥𝑎 ⊆ 𝒫 𝑥)
97, 8sylibr 224 . . . . . 6 (𝑎 ∈ (ACS‘𝑥) → 𝑎 ∈ 𝒫 𝒫 𝑥)
109ssriv 3605 . . . . 5 (ACS‘𝑥) ⊆ 𝒫 𝒫 𝑥
1110a1i 11 . . . 4 (⊤ → (ACS‘𝑥) ⊆ 𝒫 𝒫 𝑥)
12 vex 3201 . . . . . . . 8 𝑥 ∈ V
13 mremre 16258 . . . . . . . 8 (𝑥 ∈ V → (Moore‘𝑥) ∈ (Moore‘𝒫 𝑥))
1412, 13mp1i 13 . . . . . . 7 (𝑎 ⊆ (ACS‘𝑥) → (Moore‘𝑥) ∈ (Moore‘𝒫 𝑥))
155ssriv 3605 . . . . . . . 8 (ACS‘𝑥) ⊆ (Moore‘𝑥)
16 sstr 3609 . . . . . . . 8 ((𝑎 ⊆ (ACS‘𝑥) ∧ (ACS‘𝑥) ⊆ (Moore‘𝑥)) → 𝑎 ⊆ (Moore‘𝑥))
1715, 16mpan2 707 . . . . . . 7 (𝑎 ⊆ (ACS‘𝑥) → 𝑎 ⊆ (Moore‘𝑥))
18 mrerintcl 16251 . . . . . . 7 (((Moore‘𝑥) ∈ (Moore‘𝒫 𝑥) ∧ 𝑎 ⊆ (Moore‘𝑥)) → (𝒫 𝑥 𝑎) ∈ (Moore‘𝑥))
1914, 17, 18syl2anc 693 . . . . . 6 (𝑎 ⊆ (ACS‘𝑥) → (𝒫 𝑥 𝑎) ∈ (Moore‘𝑥))
20 ssel2 3596 . . . . . . . . . . . . . . . 16 ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑑𝑎) → 𝑑 ∈ (ACS‘𝑥))
2120acsmred 16311 . . . . . . . . . . . . . . 15 ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑑𝑎) → 𝑑 ∈ (Moore‘𝑥))
22 eqid 2621 . . . . . . . . . . . . . . 15 (mrCls‘𝑑) = (mrCls‘𝑑)
2321, 22mrcssvd 16277 . . . . . . . . . . . . . 14 ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑑𝑎) → ((mrCls‘𝑑)‘𝑐) ⊆ 𝑥)
2423ralrimiva 2965 . . . . . . . . . . . . 13 (𝑎 ⊆ (ACS‘𝑥) → ∀𝑑𝑎 ((mrCls‘𝑑)‘𝑐) ⊆ 𝑥)
2524adantr 481 . . . . . . . . . . . 12 ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑐 ∈ 𝒫 𝑥) → ∀𝑑𝑎 ((mrCls‘𝑑)‘𝑐) ⊆ 𝑥)
26 iunss 4559 . . . . . . . . . . . 12 ( 𝑑𝑎 ((mrCls‘𝑑)‘𝑐) ⊆ 𝑥 ↔ ∀𝑑𝑎 ((mrCls‘𝑑)‘𝑐) ⊆ 𝑥)
2725, 26sylibr 224 . . . . . . . . . . 11 ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑐 ∈ 𝒫 𝑥) → 𝑑𝑎 ((mrCls‘𝑑)‘𝑐) ⊆ 𝑥)
2812elpw2 4826 . . . . . . . . . . 11 ( 𝑑𝑎 ((mrCls‘𝑑)‘𝑐) ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐) ⊆ 𝑥)
2927, 28sylibr 224 . . . . . . . . . 10 ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑐 ∈ 𝒫 𝑥) → 𝑑𝑎 ((mrCls‘𝑑)‘𝑐) ∈ 𝒫 𝑥)
30 eqid 2621 . . . . . . . . . 10 (𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) = (𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐))
3129, 30fmptd 6383 . . . . . . . . 9 (𝑎 ⊆ (ACS‘𝑥) → (𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)):𝒫 𝑥⟶𝒫 𝑥)
32 fssxp 6058 . . . . . . . . 9 ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)):𝒫 𝑥⟶𝒫 𝑥 → (𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) ⊆ (𝒫 𝑥 × 𝒫 𝑥))
3331, 32syl 17 . . . . . . . 8 (𝑎 ⊆ (ACS‘𝑥) → (𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) ⊆ (𝒫 𝑥 × 𝒫 𝑥))
34 vpwex 4847 . . . . . . . . 9 𝒫 𝑥 ∈ V
3534, 34xpex 6959 . . . . . . . 8 (𝒫 𝑥 × 𝒫 𝑥) ∈ V
36 ssexg 4802 . . . . . . . 8 (((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) ⊆ (𝒫 𝑥 × 𝒫 𝑥) ∧ (𝒫 𝑥 × 𝒫 𝑥) ∈ V) → (𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) ∈ V)
3733, 35, 36sylancl 694 . . . . . . 7 (𝑎 ⊆ (ACS‘𝑥) → (𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) ∈ V)
3820adantlr 751 . . . . . . . . . . . . 13 (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑑𝑎) → 𝑑 ∈ (ACS‘𝑥))
39 elpwi 4166 . . . . . . . . . . . . . 14 (𝑏 ∈ 𝒫 𝑥𝑏𝑥)
4039ad2antlr 763 . . . . . . . . . . . . 13 (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑑𝑎) → 𝑏𝑥)
4122acsfiel2 16310 . . . . . . . . . . . . 13 ((𝑑 ∈ (ACS‘𝑥) ∧ 𝑏𝑥) → (𝑏𝑑 ↔ ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)((mrCls‘𝑑)‘𝑒) ⊆ 𝑏))
4238, 40, 41syl2anc 693 . . . . . . . . . . . 12 (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑑𝑎) → (𝑏𝑑 ↔ ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)((mrCls‘𝑑)‘𝑒) ⊆ 𝑏))
4342ralbidva 2984 . . . . . . . . . . 11 ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → (∀𝑑𝑎 𝑏𝑑 ↔ ∀𝑑𝑎𝑒 ∈ (𝒫 𝑏 ∩ Fin)((mrCls‘𝑑)‘𝑒) ⊆ 𝑏))
44 iunss 4559 . . . . . . . . . . . . 13 ( 𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏 ↔ ∀𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏)
4544ralbii 2979 . . . . . . . . . . . 12 (∀𝑒 ∈ (𝒫 𝑏 ∩ Fin) 𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏 ↔ ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)∀𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏)
46 ralcom 3096 . . . . . . . . . . . 12 (∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)∀𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏 ↔ ∀𝑑𝑎𝑒 ∈ (𝒫 𝑏 ∩ Fin)((mrCls‘𝑑)‘𝑒) ⊆ 𝑏)
4745, 46bitri 264 . . . . . . . . . . 11 (∀𝑒 ∈ (𝒫 𝑏 ∩ Fin) 𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏 ↔ ∀𝑑𝑎𝑒 ∈ (𝒫 𝑏 ∩ Fin)((mrCls‘𝑑)‘𝑒) ⊆ 𝑏)
4843, 47syl6bbr 278 . . . . . . . . . 10 ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → (∀𝑑𝑎 𝑏𝑑 ↔ ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin) 𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏))
49 elrint2 4517 . . . . . . . . . . 11 (𝑏 ∈ 𝒫 𝑥 → (𝑏 ∈ (𝒫 𝑥 𝑎) ↔ ∀𝑑𝑎 𝑏𝑑))
5049adantl 482 . . . . . . . . . 10 ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → (𝑏 ∈ (𝒫 𝑥 𝑎) ↔ ∀𝑑𝑎 𝑏𝑑))
51 funmpt 5924 . . . . . . . . . . . . 13 Fun (𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐))
52 funiunfv 6503 . . . . . . . . . . . . 13 (Fun (𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) → 𝑒 ∈ (𝒫 𝑏 ∩ Fin)((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) = ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)))
5351, 52ax-mp 5 . . . . . . . . . . . 12 𝑒 ∈ (𝒫 𝑏 ∩ Fin)((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) = ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin))
5453sseq1i 3627 . . . . . . . . . . 11 ( 𝑒 ∈ (𝒫 𝑏 ∩ Fin)((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) ⊆ 𝑏 ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏)
55 iunss 4559 . . . . . . . . . . . 12 ( 𝑒 ∈ (𝒫 𝑏 ∩ Fin)((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) ⊆ 𝑏 ↔ ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) ⊆ 𝑏)
56 inss1 3831 . . . . . . . . . . . . . . . . 17 (𝒫 𝑏 ∩ Fin) ⊆ 𝒫 𝑏
57 sspwb 4915 . . . . . . . . . . . . . . . . . . 19 (𝑏𝑥 ↔ 𝒫 𝑏 ⊆ 𝒫 𝑥)
5839, 57sylib 208 . . . . . . . . . . . . . . . . . 18 (𝑏 ∈ 𝒫 𝑥 → 𝒫 𝑏 ⊆ 𝒫 𝑥)
5958adantl 482 . . . . . . . . . . . . . . . . 17 ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → 𝒫 𝑏 ⊆ 𝒫 𝑥)
6056, 59syl5ss 3612 . . . . . . . . . . . . . . . 16 ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → (𝒫 𝑏 ∩ Fin) ⊆ 𝒫 𝑥)
6160sselda 3601 . . . . . . . . . . . . . . 15 (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)) → 𝑒 ∈ 𝒫 𝑥)
6221, 22mrcssvd 16277 . . . . . . . . . . . . . . . . . . 19 ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑑𝑎) → ((mrCls‘𝑑)‘𝑒) ⊆ 𝑥)
6362ralrimiva 2965 . . . . . . . . . . . . . . . . . 18 (𝑎 ⊆ (ACS‘𝑥) → ∀𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑥)
6463ad2antrr 762 . . . . . . . . . . . . . . . . 17 (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)) → ∀𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑥)
65 iunss 4559 . . . . . . . . . . . . . . . . 17 ( 𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑥 ↔ ∀𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑥)
6664, 65sylibr 224 . . . . . . . . . . . . . . . 16 (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)) → 𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑥)
67 ssexg 4802 . . . . . . . . . . . . . . . 16 (( 𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑥𝑥 ∈ V) → 𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ∈ V)
6866, 12, 67sylancl 694 . . . . . . . . . . . . . . 15 (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)) → 𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ∈ V)
69 fveq2 6189 . . . . . . . . . . . . . . . . 17 (𝑐 = 𝑒 → ((mrCls‘𝑑)‘𝑐) = ((mrCls‘𝑑)‘𝑒))
7069iuneq2d 4545 . . . . . . . . . . . . . . . 16 (𝑐 = 𝑒 𝑑𝑎 ((mrCls‘𝑑)‘𝑐) = 𝑑𝑎 ((mrCls‘𝑑)‘𝑒))
7170, 30fvmptg 6278 . . . . . . . . . . . . . . 15 ((𝑒 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ∈ V) → ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) = 𝑑𝑎 ((mrCls‘𝑑)‘𝑒))
7261, 68, 71syl2anc 693 . . . . . . . . . . . . . 14 (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)) → ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) = 𝑑𝑎 ((mrCls‘𝑑)‘𝑒))
7372sseq1d 3630 . . . . . . . . . . . . 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 6024 . . . . . . . . 9 (𝑓 = (𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) → (𝑓:𝒫 𝑥⟶𝒫 𝑥 ↔ (𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)):𝒫 𝑥⟶𝒫 𝑥))
81 imaeq1 5459 . . . . . . . . . . . . 13 (𝑓 = (𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) → (𝑓 “ (𝒫 𝑏 ∩ Fin)) = ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)))
8281unieqd 4444 . . . . . . . . . . . 12 (𝑓 = (𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) → (𝑓 “ (𝒫 𝑏 ∩ Fin)) = ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)))
8382sseq1d 3630 . . . . . . . . . . 11 (𝑓 = (𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) → ( (𝑓 “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏 ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏))
8483bibi2d 332 . . . . . . . . . 10 (𝑓 = (𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) → ((𝑏 ∈ (𝒫 𝑥 𝑎) ↔ (𝑓 “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏) ↔ (𝑏 ∈ (𝒫 𝑥 𝑎) ↔ ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏)))
8584ralbidv 2985 . . . . . . . . 9 (𝑓 = (𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) → (∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 𝑎) ↔ (𝑓 “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏) ↔ ∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 𝑎) ↔ ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏)))
8680, 85anbi12d 747 . . . . . . . 8 (𝑓 = (𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) → ((𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 𝑎) ↔ (𝑓 “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏)) ↔ ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)):𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 𝑎) ↔ ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏))))
8786spcegv 3292 . . . . . . 7 ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) ∈ V → (((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)):𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 𝑎) ↔ ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏)) → ∃𝑓(𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 𝑎) ↔ (𝑓 “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏))))
8837, 79, 87sylc 65 . . . . . 6 (𝑎 ⊆ (ACS‘𝑥) → ∃𝑓(𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 𝑎) ↔ (𝑓 “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏)))
89 isacs 16306 . . . . . 6 ((𝒫 𝑥 𝑎) ∈ (ACS‘𝑥) ↔ ((𝒫 𝑥 𝑎) ∈ (Moore‘𝑥) ∧ ∃𝑓(𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 𝑎) ↔ (𝑓 “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏))))
9019, 88, 89sylanbrc 698 . . . . 5 (𝑎 ⊆ (ACS‘𝑥) → (𝒫 𝑥 𝑎) ∈ (ACS‘𝑥))
9190adantl 482 . . . 4 ((⊤ ∧ 𝑎 ⊆ (ACS‘𝑥)) → (𝒫 𝑥 𝑎) ∈ (ACS‘𝑥))
9211, 91ismred2 16257 . . 3 (⊤ → (ACS‘𝑥) ∈ (Moore‘𝒫 𝑥))
9392trud 1492 . 2 (ACS‘𝑥) ∈ (Moore‘𝒫 𝑥)
944, 93vtoclg 3264 1 (𝑋𝑉 → (ACS‘𝑋) ∈ (Moore‘𝒫 𝑋))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384   = wceq 1482  wtru 1483  wex 1703  wcel 1989  wral 2911  Vcvv 3198  cin 3571  wss 3572  𝒫 cpw 4156   cuni 4434   cint 4473   ciun 4518  cmpt 4727   × cxp 5110  cima 5115  Fun wfun 5880  wf 5882  cfv 5886  Fincfn 7952  Moorecmre 16236  mrClscmrc 16237  ACScacs 16239
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-8 1991  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601  ax-sep 4779  ax-nul 4787  ax-pow 4841  ax-pr 4904  ax-un 6946
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1485  df-ex 1704  df-nf 1709  df-sb 1880  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-ne 2794  df-ral 2916  df-rex 2917  df-rab 2920  df-v 3200  df-sbc 3434  df-csb 3532  df-dif 3575  df-un 3577  df-in 3579  df-ss 3586  df-nul 3914  df-if 4085  df-pw 4158  df-sn 4176  df-pr 4178  df-op 4182  df-uni 4435  df-int 4474  df-iun 4520  df-br 4652  df-opab 4711  df-mpt 4728  df-id 5022  df-xp 5118  df-rel 5119  df-cnv 5120  df-co 5121  df-dm 5122  df-rn 5123  df-res 5124  df-ima 5125  df-iota 5849  df-fun 5888  df-fn 5889  df-f 5890  df-fv 5894  df-mre 16240  df-mrc 16241  df-acs 16243
This theorem is referenced by:  acsfn1  16316  acsfn1c  16317  acsfn2  16318  submacs  17359  subgacs  17623  nsgacs  17624  lssacs  18961  acsfn1p  37595  subrgacs  37596  sdrgacs  37597
  Copyright terms: Public domain W3C validator