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

Theorem mreacs 17606
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 6890 . . 3 (π‘₯ = 𝑋 β†’ (ACSβ€˜π‘₯) = (ACSβ€˜π‘‹))
2 pweq 4615 . . . 4 (π‘₯ = 𝑋 β†’ 𝒫 π‘₯ = 𝒫 𝑋)
32fveq2d 6894 . . 3 (π‘₯ = 𝑋 β†’ (Mooreβ€˜π’« π‘₯) = (Mooreβ€˜π’« 𝑋))
41, 3eleq12d 2825 . 2 (π‘₯ = 𝑋 β†’ ((ACSβ€˜π‘₯) ∈ (Mooreβ€˜π’« π‘₯) ↔ (ACSβ€˜π‘‹) ∈ (Mooreβ€˜π’« 𝑋)))
5 acsmre 17600 . . . . . . 7 (π‘Ž ∈ (ACSβ€˜π‘₯) β†’ π‘Ž ∈ (Mooreβ€˜π‘₯))
6 mresspw 17540 . . . . . . . 8 (π‘Ž ∈ (Mooreβ€˜π‘₯) β†’ π‘Ž βŠ† 𝒫 π‘₯)
75, 6syl 17 . . . . . . 7 (π‘Ž ∈ (ACSβ€˜π‘₯) β†’ π‘Ž βŠ† 𝒫 π‘₯)
85, 7elpwd 4607 . . . . . 6 (π‘Ž ∈ (ACSβ€˜π‘₯) β†’ π‘Ž ∈ 𝒫 𝒫 π‘₯)
98ssriv 3985 . . . . 5 (ACSβ€˜π‘₯) βŠ† 𝒫 𝒫 π‘₯
109a1i 11 . . . 4 (⊀ β†’ (ACSβ€˜π‘₯) βŠ† 𝒫 𝒫 π‘₯)
11 vex 3476 . . . . . . . 8 π‘₯ ∈ V
12 mremre 17552 . . . . . . . 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 687 . . . . . . 7 (π‘Ž βŠ† (ACSβ€˜π‘₯) β†’ π‘Ž βŠ† (Mooreβ€˜π‘₯))
17 mrerintcl 17545 . . . . . . 7 (((Mooreβ€˜π‘₯) ∈ (Mooreβ€˜π’« π‘₯) ∧ π‘Ž βŠ† (Mooreβ€˜π‘₯)) β†’ (𝒫 π‘₯ ∩ ∩ π‘Ž) ∈ (Mooreβ€˜π‘₯))
1813, 16, 17syl2anc 582 . . . . . 6 (π‘Ž βŠ† (ACSβ€˜π‘₯) β†’ (𝒫 π‘₯ ∩ ∩ π‘Ž) ∈ (Mooreβ€˜π‘₯))
19 ssel2 3976 . . . . . . . . . . . . . . . 16 ((π‘Ž βŠ† (ACSβ€˜π‘₯) ∧ 𝑑 ∈ π‘Ž) β†’ 𝑑 ∈ (ACSβ€˜π‘₯))
2019acsmred 17604 . . . . . . . . . . . . . . 15 ((π‘Ž βŠ† (ACSβ€˜π‘₯) ∧ 𝑑 ∈ π‘Ž) β†’ 𝑑 ∈ (Mooreβ€˜π‘₯))
21 eqid 2730 . . . . . . . . . . . . . . 15 (mrClsβ€˜π‘‘) = (mrClsβ€˜π‘‘)
2220, 21mrcssvd 17571 . . . . . . . . . . . . . 14 ((π‘Ž βŠ† (ACSβ€˜π‘₯) ∧ 𝑑 ∈ π‘Ž) β†’ ((mrClsβ€˜π‘‘)β€˜π‘) βŠ† π‘₯)
2322ralrimiva 3144 . . . . . . . . . . . . 13 (π‘Ž βŠ† (ACSβ€˜π‘₯) β†’ βˆ€π‘‘ ∈ π‘Ž ((mrClsβ€˜π‘‘)β€˜π‘) βŠ† π‘₯)
2423adantr 479 . . . . . . . . . . . 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 7115 . . . . . . . . 9 (π‘Ž βŠ† (ACSβ€˜π‘₯) β†’ (𝑐 ∈ 𝒫 π‘₯ ↦ βˆͺ 𝑑 ∈ π‘Ž ((mrClsβ€˜π‘‘)β€˜π‘)):𝒫 π‘₯βŸΆπ’« π‘₯)
30 fssxp 6744 . . . . . . . . 9 ((𝑐 ∈ 𝒫 π‘₯ ↦ βˆͺ 𝑑 ∈ π‘Ž ((mrClsβ€˜π‘‘)β€˜π‘)):𝒫 π‘₯βŸΆπ’« π‘₯ β†’ (𝑐 ∈ 𝒫 π‘₯ ↦ βˆͺ 𝑑 ∈ π‘Ž ((mrClsβ€˜π‘‘)β€˜π‘)) βŠ† (𝒫 π‘₯ Γ— 𝒫 π‘₯))
3129, 30syl 17 . . . . . . . 8 (π‘Ž βŠ† (ACSβ€˜π‘₯) β†’ (𝑐 ∈ 𝒫 π‘₯ ↦ βˆͺ 𝑑 ∈ π‘Ž ((mrClsβ€˜π‘‘)β€˜π‘)) βŠ† (𝒫 π‘₯ Γ— 𝒫 π‘₯))
32 vpwex 5374 . . . . . . . . 9 𝒫 π‘₯ ∈ V
3332, 32xpex 7742 . . . . . . . 8 (𝒫 π‘₯ Γ— 𝒫 π‘₯) ∈ V
34 ssexg 5322 . . . . . . . 8 (((𝑐 ∈ 𝒫 π‘₯ ↦ βˆͺ 𝑑 ∈ π‘Ž ((mrClsβ€˜π‘‘)β€˜π‘)) βŠ† (𝒫 π‘₯ Γ— 𝒫 π‘₯) ∧ (𝒫 π‘₯ Γ— 𝒫 π‘₯) ∈ V) β†’ (𝑐 ∈ 𝒫 π‘₯ ↦ βˆͺ 𝑑 ∈ π‘Ž ((mrClsβ€˜π‘‘)β€˜π‘)) ∈ V)
3531, 33, 34sylancl 584 . . . . . . 7 (π‘Ž βŠ† (ACSβ€˜π‘₯) β†’ (𝑐 ∈ 𝒫 π‘₯ ↦ βˆͺ 𝑑 ∈ π‘Ž ((mrClsβ€˜π‘‘)β€˜π‘)) ∈ V)
3619adantlr 711 . . . . . . . . . . . . 13 (((π‘Ž βŠ† (ACSβ€˜π‘₯) ∧ 𝑏 ∈ 𝒫 π‘₯) ∧ 𝑑 ∈ π‘Ž) β†’ 𝑑 ∈ (ACSβ€˜π‘₯))
37 elpwi 4608 . . . . . . . . . . . . . 14 (𝑏 ∈ 𝒫 π‘₯ β†’ 𝑏 βŠ† π‘₯)
3837ad2antlr 723 . . . . . . . . . . . . 13 (((π‘Ž βŠ† (ACSβ€˜π‘₯) ∧ 𝑏 ∈ 𝒫 π‘₯) ∧ 𝑑 ∈ π‘Ž) β†’ 𝑏 βŠ† π‘₯)
3921acsfiel2 17603 . . . . . . . . . . . . 13 ((𝑑 ∈ (ACSβ€˜π‘₯) ∧ 𝑏 βŠ† π‘₯) β†’ (𝑏 ∈ 𝑑 ↔ βˆ€π‘’ ∈ (𝒫 𝑏 ∩ Fin)((mrClsβ€˜π‘‘)β€˜π‘’) βŠ† 𝑏))
4036, 38, 39syl2anc 582 . . . . . . . . . . . 12 (((π‘Ž βŠ† (ACSβ€˜π‘₯) ∧ 𝑏 ∈ 𝒫 π‘₯) ∧ 𝑑 ∈ π‘Ž) β†’ (𝑏 ∈ 𝑑 ↔ βˆ€π‘’ ∈ (𝒫 𝑏 ∩ Fin)((mrClsβ€˜π‘‘)β€˜π‘’) βŠ† 𝑏))
4140ralbidva 3173 . . . . . . . . . . 11 ((π‘Ž βŠ† (ACSβ€˜π‘₯) ∧ 𝑏 ∈ 𝒫 π‘₯) β†’ (βˆ€π‘‘ ∈ π‘Ž 𝑏 ∈ 𝑑 ↔ βˆ€π‘‘ ∈ π‘Ž βˆ€π‘’ ∈ (𝒫 𝑏 ∩ Fin)((mrClsβ€˜π‘‘)β€˜π‘’) βŠ† 𝑏))
42 iunss 5047 . . . . . . . . . . . . 13 (βˆͺ 𝑑 ∈ π‘Ž ((mrClsβ€˜π‘‘)β€˜π‘’) βŠ† 𝑏 ↔ βˆ€π‘‘ ∈ π‘Ž ((mrClsβ€˜π‘‘)β€˜π‘’) βŠ† 𝑏)
4342ralbii 3091 . . . . . . . . . . . 12 (βˆ€π‘’ ∈ (𝒫 𝑏 ∩ Fin)βˆͺ 𝑑 ∈ π‘Ž ((mrClsβ€˜π‘‘)β€˜π‘’) βŠ† 𝑏 ↔ βˆ€π‘’ ∈ (𝒫 𝑏 ∩ Fin)βˆ€π‘‘ ∈ π‘Ž ((mrClsβ€˜π‘‘)β€˜π‘’) βŠ† 𝑏)
44 ralcom 3284 . . . . . . . . . . . 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 480 . . . . . . . . . 10 ((π‘Ž βŠ† (ACSβ€˜π‘₯) ∧ 𝑏 ∈ 𝒫 π‘₯) β†’ (𝑏 ∈ (𝒫 π‘₯ ∩ ∩ π‘Ž) ↔ βˆ€π‘‘ ∈ π‘Ž 𝑏 ∈ 𝑑))
49 funmpt 6585 . . . . . . . . . . . . 13 Fun (𝑐 ∈ 𝒫 π‘₯ ↦ βˆͺ 𝑑 ∈ π‘Ž ((mrClsβ€˜π‘‘)β€˜π‘))
50 funiunfv 7249 . . . . . . . . . . . . 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 2730 . . . . . . . . . . . . . . 15 (𝑐 ∈ 𝒫 π‘₯ ↦ βˆͺ 𝑑 ∈ π‘Ž ((mrClsβ€˜π‘‘)β€˜π‘)) = (𝑐 ∈ 𝒫 π‘₯ ↦ βˆͺ 𝑑 ∈ π‘Ž ((mrClsβ€˜π‘‘)β€˜π‘))
55 fveq2 6890 . . . . . . . . . . . . . . . 16 (𝑐 = 𝑒 β†’ ((mrClsβ€˜π‘‘)β€˜π‘) = ((mrClsβ€˜π‘‘)β€˜π‘’))
5655iuneq2d 5025 . . . . . . . . . . . . . . 15 (𝑐 = 𝑒 β†’ βˆͺ 𝑑 ∈ π‘Ž ((mrClsβ€˜π‘‘)β€˜π‘) = βˆͺ 𝑑 ∈ π‘Ž ((mrClsβ€˜π‘‘)β€˜π‘’))
57 inss1 4227 . . . . . . . . . . . . . . . . 17 (𝒫 𝑏 ∩ Fin) βŠ† 𝒫 𝑏
5837sspwd 4614 . . . . . . . . . . . . . . . . . 18 (𝑏 ∈ 𝒫 π‘₯ β†’ 𝒫 𝑏 βŠ† 𝒫 π‘₯)
5958adantl 480 . . . . . . . . . . . . . . . . 17 ((π‘Ž βŠ† (ACSβ€˜π‘₯) ∧ 𝑏 ∈ 𝒫 π‘₯) β†’ 𝒫 𝑏 βŠ† 𝒫 π‘₯)
6057, 59sstrid 3992 . . . . . . . . . . . . . . . 16 ((π‘Ž βŠ† (ACSβ€˜π‘₯) ∧ 𝑏 ∈ 𝒫 π‘₯) β†’ (𝒫 𝑏 ∩ Fin) βŠ† 𝒫 π‘₯)
6160sselda 3981 . . . . . . . . . . . . . . 15 (((π‘Ž βŠ† (ACSβ€˜π‘₯) ∧ 𝑏 ∈ 𝒫 π‘₯) ∧ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)) β†’ 𝑒 ∈ 𝒫 π‘₯)
6220, 21mrcssvd 17571 . . . . . . . . . . . . . . . . . . 19 ((π‘Ž βŠ† (ACSβ€˜π‘₯) ∧ 𝑑 ∈ π‘Ž) β†’ ((mrClsβ€˜π‘‘)β€˜π‘’) βŠ† π‘₯)
6362ralrimiva 3144 . . . . . . . . . . . . . . . . . 18 (π‘Ž βŠ† (ACSβ€˜π‘₯) β†’ βˆ€π‘‘ ∈ π‘Ž ((mrClsβ€˜π‘‘)β€˜π‘’) βŠ† π‘₯)
6463ad2antrr 722 . . . . . . . . . . . . . . . . 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 584 . . . . . . . . . . . . . . 15 (((π‘Ž βŠ† (ACSβ€˜π‘₯) ∧ 𝑏 ∈ 𝒫 π‘₯) ∧ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)) β†’ βˆͺ 𝑑 ∈ π‘Ž ((mrClsβ€˜π‘‘)β€˜π‘’) ∈ V)
6954, 56, 61, 68fvmptd3 7020 . . . . . . . . . . . . . 14 (((π‘Ž βŠ† (ACSβ€˜π‘₯) ∧ 𝑏 ∈ 𝒫 π‘₯) ∧ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)) β†’ ((𝑐 ∈ 𝒫 π‘₯ ↦ βˆͺ 𝑑 ∈ π‘Ž ((mrClsβ€˜π‘‘)β€˜π‘))β€˜π‘’) = βˆͺ 𝑑 ∈ π‘Ž ((mrClsβ€˜π‘‘)β€˜π‘’))
7069sseq1d 4012 . . . . . . . . . . . . 13 (((π‘Ž βŠ† (ACSβ€˜π‘₯) ∧ 𝑏 ∈ 𝒫 π‘₯) ∧ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)) β†’ (((𝑐 ∈ 𝒫 π‘₯ ↦ βˆͺ 𝑑 ∈ π‘Ž ((mrClsβ€˜π‘‘)β€˜π‘))β€˜π‘’) βŠ† 𝑏 ↔ βˆͺ 𝑑 ∈ π‘Ž ((mrClsβ€˜π‘‘)β€˜π‘’) βŠ† 𝑏))
7170ralbidva 3173 . . . . . . . . . . . 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 3144 . . . . . . . 8 (π‘Ž βŠ† (ACSβ€˜π‘₯) β†’ βˆ€π‘ ∈ 𝒫 π‘₯(𝑏 ∈ (𝒫 π‘₯ ∩ ∩ π‘Ž) ↔ βˆͺ ((𝑐 ∈ 𝒫 π‘₯ ↦ βˆͺ 𝑑 ∈ π‘Ž ((mrClsβ€˜π‘‘)β€˜π‘)) β€œ (𝒫 𝑏 ∩ Fin)) βŠ† 𝑏))
7629, 75jca 510 . . . . . . 7 (π‘Ž βŠ† (ACSβ€˜π‘₯) β†’ ((𝑐 ∈ 𝒫 π‘₯ ↦ βˆͺ 𝑑 ∈ π‘Ž ((mrClsβ€˜π‘‘)β€˜π‘)):𝒫 π‘₯βŸΆπ’« π‘₯ ∧ βˆ€π‘ ∈ 𝒫 π‘₯(𝑏 ∈ (𝒫 π‘₯ ∩ ∩ π‘Ž) ↔ βˆͺ ((𝑐 ∈ 𝒫 π‘₯ ↦ βˆͺ 𝑑 ∈ π‘Ž ((mrClsβ€˜π‘‘)β€˜π‘)) β€œ (𝒫 𝑏 ∩ Fin)) βŠ† 𝑏)))
77 feq1 6697 . . . . . . . 8 (𝑓 = (𝑐 ∈ 𝒫 π‘₯ ↦ βˆͺ 𝑑 ∈ π‘Ž ((mrClsβ€˜π‘‘)β€˜π‘)) β†’ (𝑓:𝒫 π‘₯βŸΆπ’« π‘₯ ↔ (𝑐 ∈ 𝒫 π‘₯ ↦ βˆͺ 𝑑 ∈ π‘Ž ((mrClsβ€˜π‘‘)β€˜π‘)):𝒫 π‘₯βŸΆπ’« π‘₯))
78 imaeq1 6053 . . . . . . . . . . . 12 (𝑓 = (𝑐 ∈ 𝒫 π‘₯ ↦ βˆͺ 𝑑 ∈ π‘Ž ((mrClsβ€˜π‘‘)β€˜π‘)) β†’ (𝑓 β€œ (𝒫 𝑏 ∩ Fin)) = ((𝑐 ∈ 𝒫 π‘₯ ↦ βˆͺ 𝑑 ∈ π‘Ž ((mrClsβ€˜π‘‘)β€˜π‘)) β€œ (𝒫 𝑏 ∩ Fin)))
7978unieqd 4921 . . . . . . . . . . 11 (𝑓 = (𝑐 ∈ 𝒫 π‘₯ ↦ βˆͺ 𝑑 ∈ π‘Ž ((mrClsβ€˜π‘‘)β€˜π‘)) β†’ βˆͺ (𝑓 β€œ (𝒫 𝑏 ∩ Fin)) = βˆͺ ((𝑐 ∈ 𝒫 π‘₯ ↦ βˆͺ 𝑑 ∈ π‘Ž ((mrClsβ€˜π‘‘)β€˜π‘)) β€œ (𝒫 𝑏 ∩ Fin)))
8079sseq1d 4012 . . . . . . . . . 10 (𝑓 = (𝑐 ∈ 𝒫 π‘₯ ↦ βˆͺ 𝑑 ∈ π‘Ž ((mrClsβ€˜π‘‘)β€˜π‘)) β†’ (βˆͺ (𝑓 β€œ (𝒫 𝑏 ∩ Fin)) βŠ† 𝑏 ↔ βˆͺ ((𝑐 ∈ 𝒫 π‘₯ ↦ βˆͺ 𝑑 ∈ π‘Ž ((mrClsβ€˜π‘‘)β€˜π‘)) β€œ (𝒫 𝑏 ∩ Fin)) βŠ† 𝑏))
8180bibi2d 341 . . . . . . . . 9 (𝑓 = (𝑐 ∈ 𝒫 π‘₯ ↦ βˆͺ 𝑑 ∈ π‘Ž ((mrClsβ€˜π‘‘)β€˜π‘)) β†’ ((𝑏 ∈ (𝒫 π‘₯ ∩ ∩ π‘Ž) ↔ βˆͺ (𝑓 β€œ (𝒫 𝑏 ∩ Fin)) βŠ† 𝑏) ↔ (𝑏 ∈ (𝒫 π‘₯ ∩ ∩ π‘Ž) ↔ βˆͺ ((𝑐 ∈ 𝒫 π‘₯ ↦ βˆͺ 𝑑 ∈ π‘Ž ((mrClsβ€˜π‘‘)β€˜π‘)) β€œ (𝒫 𝑏 ∩ Fin)) βŠ† 𝑏)))
8281ralbidv 3175 . . . . . . . 8 (𝑓 = (𝑐 ∈ 𝒫 π‘₯ ↦ βˆͺ 𝑑 ∈ π‘Ž ((mrClsβ€˜π‘‘)β€˜π‘)) β†’ (βˆ€π‘ ∈ 𝒫 π‘₯(𝑏 ∈ (𝒫 π‘₯ ∩ ∩ π‘Ž) ↔ βˆͺ (𝑓 β€œ (𝒫 𝑏 ∩ Fin)) βŠ† 𝑏) ↔ βˆ€π‘ ∈ 𝒫 π‘₯(𝑏 ∈ (𝒫 π‘₯ ∩ ∩ π‘Ž) ↔ βˆͺ ((𝑐 ∈ 𝒫 π‘₯ ↦ βˆͺ 𝑑 ∈ π‘Ž ((mrClsβ€˜π‘‘)β€˜π‘)) β€œ (𝒫 𝑏 ∩ Fin)) βŠ† 𝑏)))
8377, 82anbi12d 629 . . . . . . 7 (𝑓 = (𝑐 ∈ 𝒫 π‘₯ ↦ βˆͺ 𝑑 ∈ π‘Ž ((mrClsβ€˜π‘‘)β€˜π‘)) β†’ ((𝑓:𝒫 π‘₯βŸΆπ’« π‘₯ ∧ βˆ€π‘ ∈ 𝒫 π‘₯(𝑏 ∈ (𝒫 π‘₯ ∩ ∩ π‘Ž) ↔ βˆͺ (𝑓 β€œ (𝒫 𝑏 ∩ Fin)) βŠ† 𝑏)) ↔ ((𝑐 ∈ 𝒫 π‘₯ ↦ βˆͺ 𝑑 ∈ π‘Ž ((mrClsβ€˜π‘‘)β€˜π‘)):𝒫 π‘₯βŸΆπ’« π‘₯ ∧ βˆ€π‘ ∈ 𝒫 π‘₯(𝑏 ∈ (𝒫 π‘₯ ∩ ∩ π‘Ž) ↔ βˆͺ ((𝑐 ∈ 𝒫 π‘₯ ↦ βˆͺ 𝑑 ∈ π‘Ž ((mrClsβ€˜π‘‘)β€˜π‘)) β€œ (𝒫 𝑏 ∩ Fin)) βŠ† 𝑏))))
8435, 76, 83spcedv 3587 . . . . . 6 (π‘Ž βŠ† (ACSβ€˜π‘₯) β†’ βˆƒπ‘“(𝑓:𝒫 π‘₯βŸΆπ’« π‘₯ ∧ βˆ€π‘ ∈ 𝒫 π‘₯(𝑏 ∈ (𝒫 π‘₯ ∩ ∩ π‘Ž) ↔ βˆͺ (𝑓 β€œ (𝒫 𝑏 ∩ Fin)) βŠ† 𝑏)))
85 isacs 17599 . . . . . 6 ((𝒫 π‘₯ ∩ ∩ π‘Ž) ∈ (ACSβ€˜π‘₯) ↔ ((𝒫 π‘₯ ∩ ∩ π‘Ž) ∈ (Mooreβ€˜π‘₯) ∧ βˆƒπ‘“(𝑓:𝒫 π‘₯βŸΆπ’« π‘₯ ∧ βˆ€π‘ ∈ 𝒫 π‘₯(𝑏 ∈ (𝒫 π‘₯ ∩ ∩ π‘Ž) ↔ βˆͺ (𝑓 β€œ (𝒫 𝑏 ∩ Fin)) βŠ† 𝑏))))
8618, 84, 85sylanbrc 581 . . . . 5 (π‘Ž βŠ† (ACSβ€˜π‘₯) β†’ (𝒫 π‘₯ ∩ ∩ π‘Ž) ∈ (ACSβ€˜π‘₯))
8786adantl 480 . . . 4 ((⊀ ∧ π‘Ž βŠ† (ACSβ€˜π‘₯)) β†’ (𝒫 π‘₯ ∩ ∩ π‘Ž) ∈ (ACSβ€˜π‘₯))
8810, 87ismred2 17551 . . 3 (⊀ β†’ (ACSβ€˜π‘₯) ∈ (Mooreβ€˜π’« π‘₯))
8988mptru 1546 . 2 (ACSβ€˜π‘₯) ∈ (Mooreβ€˜π’« π‘₯)
904, 89vtoclg 3541 1 (𝑋 ∈ 𝑉 β†’ (ACSβ€˜π‘‹) ∈ (Mooreβ€˜π’« 𝑋))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 394   = wceq 1539  βŠ€wtru 1540  βˆƒwex 1779   ∈ wcel 2104  βˆ€wral 3059  Vcvv 3472   ∩ cin 3946   βŠ† wss 3947  π’« cpw 4601  βˆͺ cuni 4907  βˆ© cint 4949  βˆͺ ciun 4996   ↦ cmpt 5230   Γ— cxp 5673   β€œ cima 5678  Fun wfun 6536  βŸΆwf 6538  β€˜cfv 6542  Fincfn 8941  Moorecmre 17530  mrClscmrc 17531  ACScacs 17533
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  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 6494  df-fun 6544  df-fn 6545  df-f 6546  df-fv 6550  df-mre 17534  df-mrc 17535  df-acs 17537
This theorem is referenced by:  acsfn1  17609  acsfn1c  17610  acsfn2  17611  submacs  18744  subgacs  19077  nsgacs  19078  acsfn1p  20558  subrgacs  20559  sdrgacs  20560  lssacs  20722
  Copyright terms: Public domain W3C validator