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

Theorem mreacs 17598
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 6888 . . 3 (𝑥 = 𝑋 → (ACS‘𝑥) = (ACS‘𝑋))
2 pweq 4615 . . . 4 (𝑥 = 𝑋 → 𝒫 𝑥 = 𝒫 𝑋)
32fveq2d 6892 . . 3 (𝑥 = 𝑋 → (Moore‘𝒫 𝑥) = (Moore‘𝒫 𝑋))
41, 3eleq12d 2827 . 2 (𝑥 = 𝑋 → ((ACS‘𝑥) ∈ (Moore‘𝒫 𝑥) ↔ (ACS‘𝑋) ∈ (Moore‘𝒫 𝑋)))
5 acsmre 17592 . . . . . . 7 (𝑎 ∈ (ACS‘𝑥) → 𝑎 ∈ (Moore‘𝑥))
6 mresspw 17532 . . . . . . . 8 (𝑎 ∈ (Moore‘𝑥) → 𝑎 ⊆ 𝒫 𝑥)
75, 6syl 17 . . . . . . 7 (𝑎 ∈ (ACS‘𝑥) → 𝑎 ⊆ 𝒫 𝑥)
85, 7elpwd 4607 . . . . . 6 (𝑎 ∈ (ACS‘𝑥) → 𝑎 ∈ 𝒫 𝒫 𝑥)
98ssriv 3985 . . . . 5 (ACS‘𝑥) ⊆ 𝒫 𝒫 𝑥
109a1i 11 . . . 4 (⊤ → (ACS‘𝑥) ⊆ 𝒫 𝒫 𝑥)
11 vex 3478 . . . . . . . 8 𝑥 ∈ V
12 mremre 17544 . . . . . . . 8 (𝑥 ∈ V → (Moore‘𝑥) ∈ (Moore‘𝒫 𝑥))
1311, 12mp1i 13 . . . . . . 7 (𝑎 ⊆ (ACS‘𝑥) → (Moore‘𝑥) ∈ (Moore‘𝒫 𝑥))
145ssriv 3985 . . . . . . . 8 (ACS‘𝑥) ⊆ (Moore‘𝑥)
15 sstr 3989 . . . . . . . 8 ((𝑎 ⊆ (ACS‘𝑥) ∧ (ACS‘𝑥) ⊆ (Moore‘𝑥)) → 𝑎 ⊆ (Moore‘𝑥))
1614, 15mpan2 689 . . . . . . 7 (𝑎 ⊆ (ACS‘𝑥) → 𝑎 ⊆ (Moore‘𝑥))
17 mrerintcl 17537 . . . . . . 7 (((Moore‘𝑥) ∈ (Moore‘𝒫 𝑥) ∧ 𝑎 ⊆ (Moore‘𝑥)) → (𝒫 𝑥 𝑎) ∈ (Moore‘𝑥))
1813, 16, 17syl2anc 584 . . . . . 6 (𝑎 ⊆ (ACS‘𝑥) → (𝒫 𝑥 𝑎) ∈ (Moore‘𝑥))
19 ssel2 3976 . . . . . . . . . . . . . . . 16 ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑑𝑎) → 𝑑 ∈ (ACS‘𝑥))
2019acsmred 17596 . . . . . . . . . . . . . . 15 ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑑𝑎) → 𝑑 ∈ (Moore‘𝑥))
21 eqid 2732 . . . . . . . . . . . . . . 15 (mrCls‘𝑑) = (mrCls‘𝑑)
2220, 21mrcssvd 17563 . . . . . . . . . . . . . 14 ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑑𝑎) → ((mrCls‘𝑑)‘𝑐) ⊆ 𝑥)
2322ralrimiva 3146 . . . . . . . . . . . . 13 (𝑎 ⊆ (ACS‘𝑥) → ∀𝑑𝑎 ((mrCls‘𝑑)‘𝑐) ⊆ 𝑥)
2423adantr 481 . . . . . . . . . . . 12 ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑐 ∈ 𝒫 𝑥) → ∀𝑑𝑎 ((mrCls‘𝑑)‘𝑐) ⊆ 𝑥)
25 iunss 5047 . . . . . . . . . . . 12 ( 𝑑𝑎 ((mrCls‘𝑑)‘𝑐) ⊆ 𝑥 ↔ ∀𝑑𝑎 ((mrCls‘𝑑)‘𝑐) ⊆ 𝑥)
2624, 25sylibr 233 . . . . . . . . . . 11 ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑐 ∈ 𝒫 𝑥) → 𝑑𝑎 ((mrCls‘𝑑)‘𝑐) ⊆ 𝑥)
2711elpw2 5344 . . . . . . . . . . 11 ( 𝑑𝑎 ((mrCls‘𝑑)‘𝑐) ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐) ⊆ 𝑥)
2826, 27sylibr 233 . . . . . . . . . 10 ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑐 ∈ 𝒫 𝑥) → 𝑑𝑎 ((mrCls‘𝑑)‘𝑐) ∈ 𝒫 𝑥)
2928fmpttd 7111 . . . . . . . . 9 (𝑎 ⊆ (ACS‘𝑥) → (𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)):𝒫 𝑥⟶𝒫 𝑥)
30 fssxp 6742 . . . . . . . . 9 ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)):𝒫 𝑥⟶𝒫 𝑥 → (𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) ⊆ (𝒫 𝑥 × 𝒫 𝑥))
3129, 30syl 17 . . . . . . . 8 (𝑎 ⊆ (ACS‘𝑥) → (𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) ⊆ (𝒫 𝑥 × 𝒫 𝑥))
32 vpwex 5374 . . . . . . . . 9 𝒫 𝑥 ∈ V
3332, 32xpex 7736 . . . . . . . 8 (𝒫 𝑥 × 𝒫 𝑥) ∈ V
34 ssexg 5322 . . . . . . . 8 (((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) ⊆ (𝒫 𝑥 × 𝒫 𝑥) ∧ (𝒫 𝑥 × 𝒫 𝑥) ∈ V) → (𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) ∈ V)
3531, 33, 34sylancl 586 . . . . . . 7 (𝑎 ⊆ (ACS‘𝑥) → (𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) ∈ V)
3619adantlr 713 . . . . . . . . . . . . 13 (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑑𝑎) → 𝑑 ∈ (ACS‘𝑥))
37 elpwi 4608 . . . . . . . . . . . . . 14 (𝑏 ∈ 𝒫 𝑥𝑏𝑥)
3837ad2antlr 725 . . . . . . . . . . . . 13 (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑑𝑎) → 𝑏𝑥)
3921acsfiel2 17595 . . . . . . . . . . . . 13 ((𝑑 ∈ (ACS‘𝑥) ∧ 𝑏𝑥) → (𝑏𝑑 ↔ ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)((mrCls‘𝑑)‘𝑒) ⊆ 𝑏))
4036, 38, 39syl2anc 584 . . . . . . . . . . . 12 (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑑𝑎) → (𝑏𝑑 ↔ ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)((mrCls‘𝑑)‘𝑒) ⊆ 𝑏))
4140ralbidva 3175 . . . . . . . . . . 11 ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → (∀𝑑𝑎 𝑏𝑑 ↔ ∀𝑑𝑎𝑒 ∈ (𝒫 𝑏 ∩ Fin)((mrCls‘𝑑)‘𝑒) ⊆ 𝑏))
42 iunss 5047 . . . . . . . . . . . . 13 ( 𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏 ↔ ∀𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏)
4342ralbii 3093 . . . . . . . . . . . 12 (∀𝑒 ∈ (𝒫 𝑏 ∩ Fin) 𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏 ↔ ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)∀𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏)
44 ralcom 3286 . . . . . . . . . . . 12 (∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)∀𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏 ↔ ∀𝑑𝑎𝑒 ∈ (𝒫 𝑏 ∩ Fin)((mrCls‘𝑑)‘𝑒) ⊆ 𝑏)
4543, 44bitri 274 . . . . . . . . . . 11 (∀𝑒 ∈ (𝒫 𝑏 ∩ Fin) 𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏 ↔ ∀𝑑𝑎𝑒 ∈ (𝒫 𝑏 ∩ Fin)((mrCls‘𝑑)‘𝑒) ⊆ 𝑏)
4641, 45bitr4di 288 . . . . . . . . . 10 ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → (∀𝑑𝑎 𝑏𝑑 ↔ ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin) 𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏))
47 elrint2 4995 . . . . . . . . . . 11 (𝑏 ∈ 𝒫 𝑥 → (𝑏 ∈ (𝒫 𝑥 𝑎) ↔ ∀𝑑𝑎 𝑏𝑑))
4847adantl 482 . . . . . . . . . 10 ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → (𝑏 ∈ (𝒫 𝑥 𝑎) ↔ ∀𝑑𝑎 𝑏𝑑))
49 funmpt 6583 . . . . . . . . . . . . 13 Fun (𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐))
50 funiunfv 7243 . . . . . . . . . . . . 13 (Fun (𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) → 𝑒 ∈ (𝒫 𝑏 ∩ Fin)((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) = ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)))
5149, 50ax-mp 5 . . . . . . . . . . . 12 𝑒 ∈ (𝒫 𝑏 ∩ Fin)((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) = ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin))
5251sseq1i 4009 . . . . . . . . . . 11 ( 𝑒 ∈ (𝒫 𝑏 ∩ Fin)((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) ⊆ 𝑏 ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏)
53 iunss 5047 . . . . . . . . . . . 12 ( 𝑒 ∈ (𝒫 𝑏 ∩ Fin)((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) ⊆ 𝑏 ↔ ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) ⊆ 𝑏)
54 eqid 2732 . . . . . . . . . . . . . . 15 (𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) = (𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐))
55 fveq2 6888 . . . . . . . . . . . . . . . 16 (𝑐 = 𝑒 → ((mrCls‘𝑑)‘𝑐) = ((mrCls‘𝑑)‘𝑒))
5655iuneq2d 5025 . . . . . . . . . . . . . . 15 (𝑐 = 𝑒 𝑑𝑎 ((mrCls‘𝑑)‘𝑐) = 𝑑𝑎 ((mrCls‘𝑑)‘𝑒))
57 inss1 4227 . . . . . . . . . . . . . . . . 17 (𝒫 𝑏 ∩ Fin) ⊆ 𝒫 𝑏
5837sspwd 4614 . . . . . . . . . . . . . . . . . 18 (𝑏 ∈ 𝒫 𝑥 → 𝒫 𝑏 ⊆ 𝒫 𝑥)
5958adantl 482 . . . . . . . . . . . . . . . . 17 ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → 𝒫 𝑏 ⊆ 𝒫 𝑥)
6057, 59sstrid 3992 . . . . . . . . . . . . . . . 16 ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → (𝒫 𝑏 ∩ Fin) ⊆ 𝒫 𝑥)
6160sselda 3981 . . . . . . . . . . . . . . 15 (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)) → 𝑒 ∈ 𝒫 𝑥)
6220, 21mrcssvd 17563 . . . . . . . . . . . . . . . . . . 19 ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑑𝑎) → ((mrCls‘𝑑)‘𝑒) ⊆ 𝑥)
6362ralrimiva 3146 . . . . . . . . . . . . . . . . . 18 (𝑎 ⊆ (ACS‘𝑥) → ∀𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑥)
6463ad2antrr 724 . . . . . . . . . . . . . . . . 17 (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)) → ∀𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑥)
65 iunss 5047 . . . . . . . . . . . . . . . . 17 ( 𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑥 ↔ ∀𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑥)
6664, 65sylibr 233 . . . . . . . . . . . . . . . 16 (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)) → 𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑥)
67 ssexg 5322 . . . . . . . . . . . . . . . 16 (( 𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑥𝑥 ∈ V) → 𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ∈ V)
6866, 11, 67sylancl 586 . . . . . . . . . . . . . . 15 (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)) → 𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ∈ V)
6954, 56, 61, 68fvmptd3 7018 . . . . . . . . . . . . . 14 (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)) → ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) = 𝑑𝑎 ((mrCls‘𝑑)‘𝑒))
7069sseq1d 4012 . . . . . . . . . . . . 13 (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)) → (((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) ⊆ 𝑏 𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏))
7170ralbidva 3175 . . . . . . . . . . . 12 ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → (∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) ⊆ 𝑏 ↔ ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin) 𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏))
7253, 71bitrid 282 . . . . . . . . . . 11 ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → ( 𝑒 ∈ (𝒫 𝑏 ∩ Fin)((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) ⊆ 𝑏 ↔ ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin) 𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏))
7352, 72bitr3id 284 . . . . . . . . . 10 ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → ( ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏 ↔ ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin) 𝑑𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏))
7446, 48, 733bitr4d 310 . . . . . . . . 9 ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → (𝑏 ∈ (𝒫 𝑥 𝑎) ↔ ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏))
7574ralrimiva 3146 . . . . . . . 8 (𝑎 ⊆ (ACS‘𝑥) → ∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 𝑎) ↔ ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏))
7629, 75jca 512 . . . . . . 7 (𝑎 ⊆ (ACS‘𝑥) → ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)):𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 𝑎) ↔ ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏)))
77 feq1 6695 . . . . . . . 8 (𝑓 = (𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) → (𝑓:𝒫 𝑥⟶𝒫 𝑥 ↔ (𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)):𝒫 𝑥⟶𝒫 𝑥))
78 imaeq1 6052 . . . . . . . . . . . 12 (𝑓 = (𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) → (𝑓 “ (𝒫 𝑏 ∩ Fin)) = ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)))
7978unieqd 4921 . . . . . . . . . . 11 (𝑓 = (𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) → (𝑓 “ (𝒫 𝑏 ∩ Fin)) = ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)))
8079sseq1d 4012 . . . . . . . . . 10 (𝑓 = (𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) → ( (𝑓 “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏 ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏))
8180bibi2d 342 . . . . . . . . 9 (𝑓 = (𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) → ((𝑏 ∈ (𝒫 𝑥 𝑎) ↔ (𝑓 “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏) ↔ (𝑏 ∈ (𝒫 𝑥 𝑎) ↔ ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏)))
8281ralbidv 3177 . . . . . . . 8 (𝑓 = (𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) → (∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 𝑎) ↔ (𝑓 “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏) ↔ ∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 𝑎) ↔ ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏)))
8377, 82anbi12d 631 . . . . . . 7 (𝑓 = (𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) → ((𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 𝑎) ↔ (𝑓 “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏)) ↔ ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)):𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 𝑎) ↔ ((𝑐 ∈ 𝒫 𝑥 𝑑𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏))))
8435, 76, 83spcedv 3588 . . . . . 6 (𝑎 ⊆ (ACS‘𝑥) → ∃𝑓(𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 𝑎) ↔ (𝑓 “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏)))
85 isacs 17591 . . . . . 6 ((𝒫 𝑥 𝑎) ∈ (ACS‘𝑥) ↔ ((𝒫 𝑥 𝑎) ∈ (Moore‘𝑥) ∧ ∃𝑓(𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 𝑎) ↔ (𝑓 “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏))))
8618, 84, 85sylanbrc 583 . . . . 5 (𝑎 ⊆ (ACS‘𝑥) → (𝒫 𝑥 𝑎) ∈ (ACS‘𝑥))
8786adantl 482 . . . 4 ((⊤ ∧ 𝑎 ⊆ (ACS‘𝑥)) → (𝒫 𝑥 𝑎) ∈ (ACS‘𝑥))
8810, 87ismred2 17543 . . 3 (⊤ → (ACS‘𝑥) ∈ (Moore‘𝒫 𝑥))
8988mptru 1548 . 2 (ACS‘𝑥) ∈ (Moore‘𝒫 𝑥)
904, 89vtoclg 3556 1 (𝑋𝑉 → (ACS‘𝑋) ∈ (Moore‘𝒫 𝑋))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396   = wceq 1541  wtru 1542  wex 1781  wcel 2106  wral 3061  Vcvv 3474  cin 3946  wss 3947  𝒫 cpw 4601   cuni 4907   cint 4949   ciun 4996  cmpt 5230   × cxp 5673  cima 5678  Fun wfun 6534  wf 6536  cfv 6540  Fincfn 8935  Moorecmre 17522  mrClscmrc 17523  ACScacs 17525
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-fv 6548  df-mre 17526  df-mrc 17527  df-acs 17529
This theorem is referenced by:  acsfn1  17601  acsfn1c  17602  acsfn2  17603  submacs  18704  subgacs  19035  nsgacs  19036  acsfn1p  20407  subrgacs  20408  sdrgacs  20409  lssacs  20570
  Copyright terms: Public domain W3C validator