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

Theorem mreacs 16525
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 6332 . . 3 (𝑥 = 𝑋 → (ACS‘𝑥) = (ACS‘𝑋))
2 pweq 4298 . . . 4 (𝑥 = 𝑋 → 𝒫 𝑥 = 𝒫 𝑋)
32fveq2d 6336 . . 3 (𝑥 = 𝑋 → (Moore‘𝒫 𝑥) = (Moore‘𝒫 𝑋))
41, 3eleq12d 2843 . 2 (𝑥 = 𝑋 → ((ACS‘𝑥) ∈ (Moore‘𝒫 𝑥) ↔ (ACS‘𝑋) ∈ (Moore‘𝒫 𝑋)))
5 acsmre 16519 . . . . . . . 8 (𝑎 ∈ (ACS‘𝑥) → 𝑎 ∈ (Moore‘𝑥))
6 mresspw 16459 . . . . . . . 8 (𝑎 ∈ (Moore‘𝑥) → 𝑎 ⊆ 𝒫 𝑥)
75, 6syl 17 . . . . . . 7 (𝑎 ∈ (ACS‘𝑥) → 𝑎 ⊆ 𝒫 𝑥)
8 selpw 4302 . . . . . . 7 (𝑎 ∈ 𝒫 𝒫 𝑥𝑎 ⊆ 𝒫 𝑥)
97, 8sylibr 224 . . . . . 6 (𝑎 ∈ (ACS‘𝑥) → 𝑎 ∈ 𝒫 𝒫 𝑥)
109ssriv 3754 . . . . 5 (ACS‘𝑥) ⊆ 𝒫 𝒫 𝑥
1110a1i 11 . . . 4 (⊤ → (ACS‘𝑥) ⊆ 𝒫 𝒫 𝑥)
12 vex 3352 . . . . . . . 8 𝑥 ∈ V
13 mremre 16471 . . . . . . . 8 (𝑥 ∈ V → (Moore‘𝑥) ∈ (Moore‘𝒫 𝑥))
1412, 13mp1i 13 . . . . . . 7 (𝑎 ⊆ (ACS‘𝑥) → (Moore‘𝑥) ∈ (Moore‘𝒫 𝑥))
155ssriv 3754 . . . . . . . 8 (ACS‘𝑥) ⊆ (Moore‘𝑥)
16 sstr 3758 . . . . . . . 8 ((𝑎 ⊆ (ACS‘𝑥) ∧ (ACS‘𝑥) ⊆ (Moore‘𝑥)) → 𝑎 ⊆ (Moore‘𝑥))
1715, 16mpan2 663 . . . . . . 7 (𝑎 ⊆ (ACS‘𝑥) → 𝑎 ⊆ (Moore‘𝑥))
18 mrerintcl 16464 . . . . . . 7 (((Moore‘𝑥) ∈ (Moore‘𝒫 𝑥) ∧ 𝑎 ⊆ (Moore‘𝑥)) → (𝒫 𝑥 𝑎) ∈ (Moore‘𝑥))
1914, 17, 18syl2anc 565 . . . . . 6 (𝑎 ⊆ (ACS‘𝑥) → (𝒫 𝑥 𝑎) ∈ (Moore‘𝑥))
20 ssel2 3745 . . . . . . . . . . . . . . . 16 ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑑𝑎) → 𝑑 ∈ (ACS‘𝑥))
2120acsmred 16523 . . . . . . . . . . . . . . 15 ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑑𝑎) → 𝑑 ∈ (Moore‘𝑥))
22 eqid 2770 . . . . . . . . . . . . . . 15 (mrCls‘𝑑) = (mrCls‘𝑑)
2321, 22mrcssvd 16490 . . . . . . . . . . . . . 14 ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑑𝑎) → ((mrCls‘𝑑)‘𝑐) ⊆ 𝑥)
2423ralrimiva 3114 . . . . . . . . . . . . 13 (𝑎 ⊆ (ACS‘𝑥) → ∀𝑑𝑎 ((mrCls‘𝑑)‘𝑐) ⊆ 𝑥)
2524adantr 466 . . . . . . . . . . . 12 ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑐 ∈ 𝒫 𝑥) → ∀𝑑𝑎 ((mrCls‘𝑑)‘𝑐) ⊆ 𝑥)
26 iunss 4693 . . . . . . . . . . . 12 ( 𝑑𝑎 ((mrCls‘𝑑)‘𝑐) ⊆ 𝑥 ↔ ∀𝑑𝑎 ((mrCls‘𝑑)‘𝑐) ⊆ 𝑥)
2725, 26sylibr 224 . . . . . . . . . . 11 ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑐 ∈ 𝒫 𝑥) → 𝑑𝑎 ((mrCls‘𝑑)‘𝑐) ⊆ 𝑥)
2812elpw2 4956 . . . . . . . . . . 11 ( 𝑑𝑎 ((mrCls‘𝑑)‘𝑐) ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐) ⊆ 𝑥)
2927, 28sylibr 224 . . . . . . . . . 10 ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑐 ∈ 𝒫 𝑥) → 𝑑𝑎 ((mrCls‘𝑑)‘𝑐) ∈ 𝒫 𝑥)
30 eqid 2770 . . . . . . . . . 10 (𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) = (𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐))
3129, 30fmptd 6527 . . . . . . . . 9 (𝑎 ⊆ (ACS‘𝑥) → (𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)):𝒫 𝑥⟶𝒫 𝑥)
32 fssxp 6200 . . . . . . . . 9 ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)):𝒫 𝑥⟶𝒫 𝑥 → (𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) ⊆ (𝒫 𝑥 × 𝒫 𝑥))
3331, 32syl 17 . . . . . . . 8 (𝑎 ⊆ (ACS‘𝑥) → (𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) ⊆ (𝒫 𝑥 × 𝒫 𝑥))
34 vpwex 4977 . . . . . . . . 9 𝒫 𝑥 ∈ V
3534, 34xpex 7108 . . . . . . . 8 (𝒫 𝑥 × 𝒫 𝑥) ∈ V
36 ssexg 4935 . . . . . . . 8 (((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) ⊆ (𝒫 𝑥 × 𝒫 𝑥) ∧ (𝒫 𝑥 × 𝒫 𝑥) ∈ V) → (𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) ∈ V)
3733, 35, 36sylancl 566 . . . . . . 7 (𝑎 ⊆ (ACS‘𝑥) → (𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) ∈ V)
3820adantlr 686 . . . . . . . . . . . . 13 (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑑𝑎) → 𝑑 ∈ (ACS‘𝑥))
39 elpwi 4305 . . . . . . . . . . . . . 14 (𝑏 ∈ 𝒫 𝑥𝑏𝑥)
4039ad2antlr 698 . . . . . . . . . . . . 13 (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑑𝑎) → 𝑏𝑥)
4122acsfiel2 16522 . . . . . . . . . . . . 13 ((𝑑 ∈ (ACS‘𝑥) ∧ 𝑏𝑥) → (𝑏𝑑 ↔ ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)((mrCls‘𝑑)‘𝑒) ⊆ 𝑏))
4238, 40, 41syl2anc 565 . . . . . . . . . . . 12 (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑑𝑎) → (𝑏𝑑 ↔ ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)((mrCls‘𝑑)‘𝑒) ⊆ 𝑏))
4342ralbidva 3133 . . . . . . . . . . 11 ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → (∀𝑑𝑎 𝑏𝑑 ↔ ∀𝑑𝑎𝑒 ∈ (𝒫 𝑏 ∩ Fin)((mrCls‘𝑑)‘𝑒) ⊆ 𝑏))
44 iunss 4693 . . . . . . . . . . . . 13 ( 𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏 ↔ ∀𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏)
4544ralbii 3128 . . . . . . . . . . . 12 (∀𝑒 ∈ (𝒫 𝑏 ∩ Fin) 𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏 ↔ ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)∀𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏)
46 ralcom 3245 . . . . . . . . . . . 12 (∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)∀𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏 ↔ ∀𝑑𝑎𝑒 ∈ (𝒫 𝑏 ∩ Fin)((mrCls‘𝑑)‘𝑒) ⊆ 𝑏)
4745, 46bitri 264 . . . . . . . . . . 11 (∀𝑒 ∈ (𝒫 𝑏 ∩ Fin) 𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏 ↔ ∀𝑑𝑎𝑒 ∈ (𝒫 𝑏 ∩ Fin)((mrCls‘𝑑)‘𝑒) ⊆ 𝑏)
4843, 47syl6bbr 278 . . . . . . . . . 10 ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → (∀𝑑𝑎 𝑏𝑑 ↔ ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin) 𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏))
49 elrint2 4651 . . . . . . . . . . 11 (𝑏 ∈ 𝒫 𝑥 → (𝑏 ∈ (𝒫 𝑥 𝑎) ↔ ∀𝑑𝑎 𝑏𝑑))
5049adantl 467 . . . . . . . . . 10 ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → (𝑏 ∈ (𝒫 𝑥 𝑎) ↔ ∀𝑑𝑎 𝑏𝑑))
51 funmpt 6069 . . . . . . . . . . . . 13 Fun (𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐))
52 funiunfv 6648 . . . . . . . . . . . . 13 (Fun (𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) → 𝑒 ∈ (𝒫 𝑏 ∩ Fin)((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) = ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)))
5351, 52ax-mp 5 . . . . . . . . . . . 12 𝑒 ∈ (𝒫 𝑏 ∩ Fin)((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) = ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin))
5453sseq1i 3776 . . . . . . . . . . 11 ( 𝑒 ∈ (𝒫 𝑏 ∩ Fin)((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) ⊆ 𝑏 ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏)
55 iunss 4693 . . . . . . . . . . . 12 ( 𝑒 ∈ (𝒫 𝑏 ∩ Fin)((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) ⊆ 𝑏 ↔ ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) ⊆ 𝑏)
56 inss1 3979 . . . . . . . . . . . . . . . . 17 (𝒫 𝑏 ∩ Fin) ⊆ 𝒫 𝑏
57 sspwb 5045 . . . . . . . . . . . . . . . . . . 19 (𝑏𝑥 ↔ 𝒫 𝑏 ⊆ 𝒫 𝑥)
5839, 57sylib 208 . . . . . . . . . . . . . . . . . 18 (𝑏 ∈ 𝒫 𝑥 → 𝒫 𝑏 ⊆ 𝒫 𝑥)
5958adantl 467 . . . . . . . . . . . . . . . . 17 ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → 𝒫 𝑏 ⊆ 𝒫 𝑥)
6056, 59syl5ss 3761 . . . . . . . . . . . . . . . 16 ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → (𝒫 𝑏 ∩ Fin) ⊆ 𝒫 𝑥)
6160sselda 3750 . . . . . . . . . . . . . . 15 (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)) → 𝑒 ∈ 𝒫 𝑥)
6221, 22mrcssvd 16490 . . . . . . . . . . . . . . . . . . 19 ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑑𝑎) → ((mrCls‘𝑑)‘𝑒) ⊆ 𝑥)
6362ralrimiva 3114 . . . . . . . . . . . . . . . . . 18 (𝑎 ⊆ (ACS‘𝑥) → ∀𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑥)
6463ad2antrr 697 . . . . . . . . . . . . . . . . 17 (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)) → ∀𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑥)
65 iunss 4693 . . . . . . . . . . . . . . . . 17 ( 𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑥 ↔ ∀𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑥)
6664, 65sylibr 224 . . . . . . . . . . . . . . . 16 (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)) → 𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑥)
67 ssexg 4935 . . . . . . . . . . . . . . . 16 (( 𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑥𝑥 ∈ V) → 𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ∈ V)
6866, 12, 67sylancl 566 . . . . . . . . . . . . . . 15 (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)) → 𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ∈ V)
69 fveq2 6332 . . . . . . . . . . . . . . . . 17 (𝑐 = 𝑒 → ((mrCls‘𝑑)‘𝑐) = ((mrCls‘𝑑)‘𝑒))
7069iuneq2d 4679 . . . . . . . . . . . . . . . 16 (𝑐 = 𝑒 𝑑𝑎 ((mrCls‘𝑑)‘𝑐) = 𝑑𝑎 ((mrCls‘𝑑)‘𝑒))
7170, 30fvmptg 6422 . . . . . . . . . . . . . . 15 ((𝑒 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ∈ V) → ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) = 𝑑𝑎 ((mrCls‘𝑑)‘𝑒))
7261, 68, 71syl2anc 565 . . . . . . . . . . . . . 14 (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)) → ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) = 𝑑𝑎 ((mrCls‘𝑑)‘𝑒))
7372sseq1d 3779 . . . . . . . . . . . . 13 (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)) → (((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) ⊆ 𝑏 𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏))
7473ralbidva 3133 . . . . . . . . . . . 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 3114 . . . . . . . 8 (𝑎 ⊆ (ACS‘𝑥) → ∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 𝑎) ↔ ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏))
7931, 78jca 495 . . . . . . 7 (𝑎 ⊆ (ACS‘𝑥) → ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)):𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 𝑎) ↔ ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏)))
80 feq1 6166 . . . . . . . . 9 (𝑓 = (𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) → (𝑓:𝒫 𝑥⟶𝒫 𝑥 ↔ (𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)):𝒫 𝑥⟶𝒫 𝑥))
81 imaeq1 5602 . . . . . . . . . . . . 13 (𝑓 = (𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) → (𝑓 “ (𝒫 𝑏 ∩ Fin)) = ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)))
8281unieqd 4582 . . . . . . . . . . . 12 (𝑓 = (𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) → (𝑓 “ (𝒫 𝑏 ∩ Fin)) = ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)))
8382sseq1d 3779 . . . . . . . . . . 11 (𝑓 = (𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) → ( (𝑓 “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏 ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏))
8483bibi2d 331 . . . . . . . . . 10 (𝑓 = (𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) → ((𝑏 ∈ (𝒫 𝑥 𝑎) ↔ (𝑓 “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏) ↔ (𝑏 ∈ (𝒫 𝑥 𝑎) ↔ ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏)))
8584ralbidv 3134 . . . . . . . . 9 (𝑓 = (𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) → (∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 𝑎) ↔ (𝑓 “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏) ↔ ∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 𝑎) ↔ ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏)))
8680, 85anbi12d 608 . . . . . . . 8 (𝑓 = (𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) → ((𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 𝑎) ↔ (𝑓 “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏)) ↔ ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)):𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 𝑎) ↔ ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏))))
8786spcegv 3443 . . . . . . 7 ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) ∈ V → (((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)):𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 𝑎) ↔ ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏)) → ∃𝑓(𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 𝑎) ↔ (𝑓 “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏))))
8837, 79, 87sylc 65 . . . . . 6 (𝑎 ⊆ (ACS‘𝑥) → ∃𝑓(𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 𝑎) ↔ (𝑓 “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏)))
89 isacs 16518 . . . . . 6 ((𝒫 𝑥 𝑎) ∈ (ACS‘𝑥) ↔ ((𝒫 𝑥 𝑎) ∈ (Moore‘𝑥) ∧ ∃𝑓(𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 𝑎) ↔ (𝑓 “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏))))
9019, 88, 89sylanbrc 564 . . . . 5 (𝑎 ⊆ (ACS‘𝑥) → (𝒫 𝑥 𝑎) ∈ (ACS‘𝑥))
9190adantl 467 . . . 4 ((⊤ ∧ 𝑎 ⊆ (ACS‘𝑥)) → (𝒫 𝑥 𝑎) ∈ (ACS‘𝑥))
9211, 91ismred2 16470 . . 3 (⊤ → (ACS‘𝑥) ∈ (Moore‘𝒫 𝑥))
9392trud 1640 . 2 (ACS‘𝑥) ∈ (Moore‘𝒫 𝑥)
944, 93vtoclg 3415 1 (𝑋𝑉 → (ACS‘𝑋) ∈ (Moore‘𝒫 𝑋))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 382   = wceq 1630  wtru 1631  wex 1851  wcel 2144  wral 3060  Vcvv 3349  cin 3720  wss 3721  𝒫 cpw 4295   cuni 4572   cint 4609   ciun 4652  cmpt 4861   × cxp 5247  cima 5252  Fun wfun 6025  wf 6027  cfv 6031  Fincfn 8108  Moorecmre 16449  mrClscmrc 16450  ACScacs 16452
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-8 2146  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750  ax-sep 4912  ax-nul 4920  ax-pow 4971  ax-pr 5034  ax-un 7095
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3an 1072  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-eu 2621  df-mo 2622  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-ne 2943  df-ral 3065  df-rex 3066  df-rab 3069  df-v 3351  df-sbc 3586  df-csb 3681  df-dif 3724  df-un 3726  df-in 3728  df-ss 3735  df-nul 4062  df-if 4224  df-pw 4297  df-sn 4315  df-pr 4317  df-op 4321  df-uni 4573  df-int 4610  df-iun 4654  df-br 4785  df-opab 4845  df-mpt 4862  df-id 5157  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-fv 6039  df-mre 16453  df-mrc 16454  df-acs 16456
This theorem is referenced by:  acsfn1  16528  acsfn1c  16529  acsfn2  16530  submacs  17572  subgacs  17836  nsgacs  17837  lssacs  19179  acsfn1p  38288  subrgacs  38289  sdrgacs  38290
  Copyright terms: Public domain W3C validator