Metamath Proof Explorer


Theorem acsfn

Description: Algebraicity of a conditional point closure condition. (Contributed by Stefan O'Rear, 3-Apr-2015)

Ref Expression
Assertion acsfn ( ( ( 𝑋𝑉𝐾𝑋 ) ∧ ( 𝑇𝑋𝑇 ∈ Fin ) ) → { 𝑎 ∈ 𝒫 𝑋 ∣ ( 𝑇𝑎𝐾𝑎 ) } ∈ ( ACS ‘ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 funmpt Fun ( 𝑏 ∈ 𝒫 𝑋 ↦ if ( 𝑏 = 𝑇 , { 𝐾 } , ∅ ) )
2 funiunfv ( Fun ( 𝑏 ∈ 𝒫 𝑋 ↦ if ( 𝑏 = 𝑇 , { 𝐾 } , ∅ ) ) → 𝑐 ∈ ( 𝒫 𝑎 ∩ Fin ) ( ( 𝑏 ∈ 𝒫 𝑋 ↦ if ( 𝑏 = 𝑇 , { 𝐾 } , ∅ ) ) ‘ 𝑐 ) = ( ( 𝑏 ∈ 𝒫 𝑋 ↦ if ( 𝑏 = 𝑇 , { 𝐾 } , ∅ ) ) “ ( 𝒫 𝑎 ∩ Fin ) ) )
3 1 2 mp1i ( ( ( ( 𝑋𝑉𝐾𝑋 ) ∧ ( 𝑇𝑋𝑇 ∈ Fin ) ) ∧ 𝑎 ∈ 𝒫 𝑋 ) → 𝑐 ∈ ( 𝒫 𝑎 ∩ Fin ) ( ( 𝑏 ∈ 𝒫 𝑋 ↦ if ( 𝑏 = 𝑇 , { 𝐾 } , ∅ ) ) ‘ 𝑐 ) = ( ( 𝑏 ∈ 𝒫 𝑋 ↦ if ( 𝑏 = 𝑇 , { 𝐾 } , ∅ ) ) “ ( 𝒫 𝑎 ∩ Fin ) ) )
4 elinel1 ( 𝑐 ∈ ( 𝒫 𝑎 ∩ Fin ) → 𝑐 ∈ 𝒫 𝑎 )
5 4 elpwid ( 𝑐 ∈ ( 𝒫 𝑎 ∩ Fin ) → 𝑐𝑎 )
6 elpwi ( 𝑎 ∈ 𝒫 𝑋𝑎𝑋 )
7 5 6 sylan9ssr ( ( 𝑎 ∈ 𝒫 𝑋𝑐 ∈ ( 𝒫 𝑎 ∩ Fin ) ) → 𝑐𝑋 )
8 velpw ( 𝑐 ∈ 𝒫 𝑋𝑐𝑋 )
9 7 8 sylibr ( ( 𝑎 ∈ 𝒫 𝑋𝑐 ∈ ( 𝒫 𝑎 ∩ Fin ) ) → 𝑐 ∈ 𝒫 𝑋 )
10 9 adantll ( ( ( ( ( 𝑋𝑉𝐾𝑋 ) ∧ ( 𝑇𝑋𝑇 ∈ Fin ) ) ∧ 𝑎 ∈ 𝒫 𝑋 ) ∧ 𝑐 ∈ ( 𝒫 𝑎 ∩ Fin ) ) → 𝑐 ∈ 𝒫 𝑋 )
11 eqeq1 ( 𝑏 = 𝑐 → ( 𝑏 = 𝑇𝑐 = 𝑇 ) )
12 11 ifbid ( 𝑏 = 𝑐 → if ( 𝑏 = 𝑇 , { 𝐾 } , ∅ ) = if ( 𝑐 = 𝑇 , { 𝐾 } , ∅ ) )
13 eqid ( 𝑏 ∈ 𝒫 𝑋 ↦ if ( 𝑏 = 𝑇 , { 𝐾 } , ∅ ) ) = ( 𝑏 ∈ 𝒫 𝑋 ↦ if ( 𝑏 = 𝑇 , { 𝐾 } , ∅ ) )
14 snex { 𝐾 } ∈ V
15 0ex ∅ ∈ V
16 14 15 ifex if ( 𝑐 = 𝑇 , { 𝐾 } , ∅ ) ∈ V
17 12 13 16 fvmpt ( 𝑐 ∈ 𝒫 𝑋 → ( ( 𝑏 ∈ 𝒫 𝑋 ↦ if ( 𝑏 = 𝑇 , { 𝐾 } , ∅ ) ) ‘ 𝑐 ) = if ( 𝑐 = 𝑇 , { 𝐾 } , ∅ ) )
18 10 17 syl ( ( ( ( ( 𝑋𝑉𝐾𝑋 ) ∧ ( 𝑇𝑋𝑇 ∈ Fin ) ) ∧ 𝑎 ∈ 𝒫 𝑋 ) ∧ 𝑐 ∈ ( 𝒫 𝑎 ∩ Fin ) ) → ( ( 𝑏 ∈ 𝒫 𝑋 ↦ if ( 𝑏 = 𝑇 , { 𝐾 } , ∅ ) ) ‘ 𝑐 ) = if ( 𝑐 = 𝑇 , { 𝐾 } , ∅ ) )
19 18 iuneq2dv ( ( ( ( 𝑋𝑉𝐾𝑋 ) ∧ ( 𝑇𝑋𝑇 ∈ Fin ) ) ∧ 𝑎 ∈ 𝒫 𝑋 ) → 𝑐 ∈ ( 𝒫 𝑎 ∩ Fin ) ( ( 𝑏 ∈ 𝒫 𝑋 ↦ if ( 𝑏 = 𝑇 , { 𝐾 } , ∅ ) ) ‘ 𝑐 ) = 𝑐 ∈ ( 𝒫 𝑎 ∩ Fin ) if ( 𝑐 = 𝑇 , { 𝐾 } , ∅ ) )
20 3 19 eqtr3d ( ( ( ( 𝑋𝑉𝐾𝑋 ) ∧ ( 𝑇𝑋𝑇 ∈ Fin ) ) ∧ 𝑎 ∈ 𝒫 𝑋 ) → ( ( 𝑏 ∈ 𝒫 𝑋 ↦ if ( 𝑏 = 𝑇 , { 𝐾 } , ∅ ) ) “ ( 𝒫 𝑎 ∩ Fin ) ) = 𝑐 ∈ ( 𝒫 𝑎 ∩ Fin ) if ( 𝑐 = 𝑇 , { 𝐾 } , ∅ ) )
21 20 sseq1d ( ( ( ( 𝑋𝑉𝐾𝑋 ) ∧ ( 𝑇𝑋𝑇 ∈ Fin ) ) ∧ 𝑎 ∈ 𝒫 𝑋 ) → ( ( ( 𝑏 ∈ 𝒫 𝑋 ↦ if ( 𝑏 = 𝑇 , { 𝐾 } , ∅ ) ) “ ( 𝒫 𝑎 ∩ Fin ) ) ⊆ 𝑎 𝑐 ∈ ( 𝒫 𝑎 ∩ Fin ) if ( 𝑐 = 𝑇 , { 𝐾 } , ∅ ) ⊆ 𝑎 ) )
22 iunss ( 𝑐 ∈ ( 𝒫 𝑎 ∩ Fin ) if ( 𝑐 = 𝑇 , { 𝐾 } , ∅ ) ⊆ 𝑎 ↔ ∀ 𝑐 ∈ ( 𝒫 𝑎 ∩ Fin ) if ( 𝑐 = 𝑇 , { 𝐾 } , ∅ ) ⊆ 𝑎 )
23 sseq1 ( { 𝐾 } = if ( 𝑐 = 𝑇 , { 𝐾 } , ∅ ) → ( { 𝐾 } ⊆ 𝑎 ↔ if ( 𝑐 = 𝑇 , { 𝐾 } , ∅ ) ⊆ 𝑎 ) )
24 23 bibi1d ( { 𝐾 } = if ( 𝑐 = 𝑇 , { 𝐾 } , ∅ ) → ( ( { 𝐾 } ⊆ 𝑎 ↔ ( 𝑐 = 𝑇𝐾𝑎 ) ) ↔ ( if ( 𝑐 = 𝑇 , { 𝐾 } , ∅ ) ⊆ 𝑎 ↔ ( 𝑐 = 𝑇𝐾𝑎 ) ) ) )
25 sseq1 ( ∅ = if ( 𝑐 = 𝑇 , { 𝐾 } , ∅ ) → ( ∅ ⊆ 𝑎 ↔ if ( 𝑐 = 𝑇 , { 𝐾 } , ∅ ) ⊆ 𝑎 ) )
26 25 bibi1d ( ∅ = if ( 𝑐 = 𝑇 , { 𝐾 } , ∅ ) → ( ( ∅ ⊆ 𝑎 ↔ ( 𝑐 = 𝑇𝐾𝑎 ) ) ↔ ( if ( 𝑐 = 𝑇 , { 𝐾 } , ∅ ) ⊆ 𝑎 ↔ ( 𝑐 = 𝑇𝐾𝑎 ) ) ) )
27 snssg ( 𝐾𝑋 → ( 𝐾𝑎 ↔ { 𝐾 } ⊆ 𝑎 ) )
28 27 adantr ( ( 𝐾𝑋𝑐 = 𝑇 ) → ( 𝐾𝑎 ↔ { 𝐾 } ⊆ 𝑎 ) )
29 biimt ( 𝑐 = 𝑇 → ( 𝐾𝑎 ↔ ( 𝑐 = 𝑇𝐾𝑎 ) ) )
30 29 adantl ( ( 𝐾𝑋𝑐 = 𝑇 ) → ( 𝐾𝑎 ↔ ( 𝑐 = 𝑇𝐾𝑎 ) ) )
31 28 30 bitr3d ( ( 𝐾𝑋𝑐 = 𝑇 ) → ( { 𝐾 } ⊆ 𝑎 ↔ ( 𝑐 = 𝑇𝐾𝑎 ) ) )
32 0ss ∅ ⊆ 𝑎
33 32 a1i ( ¬ 𝑐 = 𝑇 → ∅ ⊆ 𝑎 )
34 pm2.21 ( ¬ 𝑐 = 𝑇 → ( 𝑐 = 𝑇𝐾𝑎 ) )
35 33 34 2thd ( ¬ 𝑐 = 𝑇 → ( ∅ ⊆ 𝑎 ↔ ( 𝑐 = 𝑇𝐾𝑎 ) ) )
36 35 adantl ( ( 𝐾𝑋 ∧ ¬ 𝑐 = 𝑇 ) → ( ∅ ⊆ 𝑎 ↔ ( 𝑐 = 𝑇𝐾𝑎 ) ) )
37 24 26 31 36 ifbothda ( 𝐾𝑋 → ( if ( 𝑐 = 𝑇 , { 𝐾 } , ∅ ) ⊆ 𝑎 ↔ ( 𝑐 = 𝑇𝐾𝑎 ) ) )
38 37 ralbidv ( 𝐾𝑋 → ( ∀ 𝑐 ∈ ( 𝒫 𝑎 ∩ Fin ) if ( 𝑐 = 𝑇 , { 𝐾 } , ∅ ) ⊆ 𝑎 ↔ ∀ 𝑐 ∈ ( 𝒫 𝑎 ∩ Fin ) ( 𝑐 = 𝑇𝐾𝑎 ) ) )
39 38 ad3antlr ( ( ( ( 𝑋𝑉𝐾𝑋 ) ∧ ( 𝑇𝑋𝑇 ∈ Fin ) ) ∧ 𝑎 ∈ 𝒫 𝑋 ) → ( ∀ 𝑐 ∈ ( 𝒫 𝑎 ∩ Fin ) if ( 𝑐 = 𝑇 , { 𝐾 } , ∅ ) ⊆ 𝑎 ↔ ∀ 𝑐 ∈ ( 𝒫 𝑎 ∩ Fin ) ( 𝑐 = 𝑇𝐾𝑎 ) ) )
40 22 39 syl5bb ( ( ( ( 𝑋𝑉𝐾𝑋 ) ∧ ( 𝑇𝑋𝑇 ∈ Fin ) ) ∧ 𝑎 ∈ 𝒫 𝑋 ) → ( 𝑐 ∈ ( 𝒫 𝑎 ∩ Fin ) if ( 𝑐 = 𝑇 , { 𝐾 } , ∅ ) ⊆ 𝑎 ↔ ∀ 𝑐 ∈ ( 𝒫 𝑎 ∩ Fin ) ( 𝑐 = 𝑇𝐾𝑎 ) ) )
41 inss1 ( 𝒫 𝑎 ∩ Fin ) ⊆ 𝒫 𝑎
42 6 sspwd ( 𝑎 ∈ 𝒫 𝑋 → 𝒫 𝑎 ⊆ 𝒫 𝑋 )
43 41 42 sstrid ( 𝑎 ∈ 𝒫 𝑋 → ( 𝒫 𝑎 ∩ Fin ) ⊆ 𝒫 𝑋 )
44 43 adantl ( ( ( ( 𝑋𝑉𝐾𝑋 ) ∧ ( 𝑇𝑋𝑇 ∈ Fin ) ) ∧ 𝑎 ∈ 𝒫 𝑋 ) → ( 𝒫 𝑎 ∩ Fin ) ⊆ 𝒫 𝑋 )
45 ralss ( ( 𝒫 𝑎 ∩ Fin ) ⊆ 𝒫 𝑋 → ( ∀ 𝑐 ∈ ( 𝒫 𝑎 ∩ Fin ) ( 𝑐 = 𝑇𝐾𝑎 ) ↔ ∀ 𝑐 ∈ 𝒫 𝑋 ( 𝑐 ∈ ( 𝒫 𝑎 ∩ Fin ) → ( 𝑐 = 𝑇𝐾𝑎 ) ) ) )
46 44 45 syl ( ( ( ( 𝑋𝑉𝐾𝑋 ) ∧ ( 𝑇𝑋𝑇 ∈ Fin ) ) ∧ 𝑎 ∈ 𝒫 𝑋 ) → ( ∀ 𝑐 ∈ ( 𝒫 𝑎 ∩ Fin ) ( 𝑐 = 𝑇𝐾𝑎 ) ↔ ∀ 𝑐 ∈ 𝒫 𝑋 ( 𝑐 ∈ ( 𝒫 𝑎 ∩ Fin ) → ( 𝑐 = 𝑇𝐾𝑎 ) ) ) )
47 bi2.04 ( ( 𝑐 ∈ ( 𝒫 𝑎 ∩ Fin ) → ( 𝑐 = 𝑇𝐾𝑎 ) ) ↔ ( 𝑐 = 𝑇 → ( 𝑐 ∈ ( 𝒫 𝑎 ∩ Fin ) → 𝐾𝑎 ) ) )
48 47 ralbii ( ∀ 𝑐 ∈ 𝒫 𝑋 ( 𝑐 ∈ ( 𝒫 𝑎 ∩ Fin ) → ( 𝑐 = 𝑇𝐾𝑎 ) ) ↔ ∀ 𝑐 ∈ 𝒫 𝑋 ( 𝑐 = 𝑇 → ( 𝑐 ∈ ( 𝒫 𝑎 ∩ Fin ) → 𝐾𝑎 ) ) )
49 elpwg ( 𝑇 ∈ Fin → ( 𝑇 ∈ 𝒫 𝑋𝑇𝑋 ) )
50 49 biimparc ( ( 𝑇𝑋𝑇 ∈ Fin ) → 𝑇 ∈ 𝒫 𝑋 )
51 50 ad2antlr ( ( ( ( 𝑋𝑉𝐾𝑋 ) ∧ ( 𝑇𝑋𝑇 ∈ Fin ) ) ∧ 𝑎 ∈ 𝒫 𝑋 ) → 𝑇 ∈ 𝒫 𝑋 )
52 eleq1 ( 𝑐 = 𝑇 → ( 𝑐 ∈ ( 𝒫 𝑎 ∩ Fin ) ↔ 𝑇 ∈ ( 𝒫 𝑎 ∩ Fin ) ) )
53 52 imbi1d ( 𝑐 = 𝑇 → ( ( 𝑐 ∈ ( 𝒫 𝑎 ∩ Fin ) → 𝐾𝑎 ) ↔ ( 𝑇 ∈ ( 𝒫 𝑎 ∩ Fin ) → 𝐾𝑎 ) ) )
54 53 ceqsralv ( 𝑇 ∈ 𝒫 𝑋 → ( ∀ 𝑐 ∈ 𝒫 𝑋 ( 𝑐 = 𝑇 → ( 𝑐 ∈ ( 𝒫 𝑎 ∩ Fin ) → 𝐾𝑎 ) ) ↔ ( 𝑇 ∈ ( 𝒫 𝑎 ∩ Fin ) → 𝐾𝑎 ) ) )
55 51 54 syl ( ( ( ( 𝑋𝑉𝐾𝑋 ) ∧ ( 𝑇𝑋𝑇 ∈ Fin ) ) ∧ 𝑎 ∈ 𝒫 𝑋 ) → ( ∀ 𝑐 ∈ 𝒫 𝑋 ( 𝑐 = 𝑇 → ( 𝑐 ∈ ( 𝒫 𝑎 ∩ Fin ) → 𝐾𝑎 ) ) ↔ ( 𝑇 ∈ ( 𝒫 𝑎 ∩ Fin ) → 𝐾𝑎 ) ) )
56 48 55 syl5bb ( ( ( ( 𝑋𝑉𝐾𝑋 ) ∧ ( 𝑇𝑋𝑇 ∈ Fin ) ) ∧ 𝑎 ∈ 𝒫 𝑋 ) → ( ∀ 𝑐 ∈ 𝒫 𝑋 ( 𝑐 ∈ ( 𝒫 𝑎 ∩ Fin ) → ( 𝑐 = 𝑇𝐾𝑎 ) ) ↔ ( 𝑇 ∈ ( 𝒫 𝑎 ∩ Fin ) → 𝐾𝑎 ) ) )
57 simplrr ( ( ( ( 𝑋𝑉𝐾𝑋 ) ∧ ( 𝑇𝑋𝑇 ∈ Fin ) ) ∧ 𝑎 ∈ 𝒫 𝑋 ) → 𝑇 ∈ Fin )
58 57 biantrud ( ( ( ( 𝑋𝑉𝐾𝑋 ) ∧ ( 𝑇𝑋𝑇 ∈ Fin ) ) ∧ 𝑎 ∈ 𝒫 𝑋 ) → ( 𝑇 ∈ 𝒫 𝑎 ↔ ( 𝑇 ∈ 𝒫 𝑎𝑇 ∈ Fin ) ) )
59 elin ( 𝑇 ∈ ( 𝒫 𝑎 ∩ Fin ) ↔ ( 𝑇 ∈ 𝒫 𝑎𝑇 ∈ Fin ) )
60 58 59 bitr4di ( ( ( ( 𝑋𝑉𝐾𝑋 ) ∧ ( 𝑇𝑋𝑇 ∈ Fin ) ) ∧ 𝑎 ∈ 𝒫 𝑋 ) → ( 𝑇 ∈ 𝒫 𝑎𝑇 ∈ ( 𝒫 𝑎 ∩ Fin ) ) )
61 vex 𝑎 ∈ V
62 61 elpw2 ( 𝑇 ∈ 𝒫 𝑎𝑇𝑎 )
63 60 62 bitr3di ( ( ( ( 𝑋𝑉𝐾𝑋 ) ∧ ( 𝑇𝑋𝑇 ∈ Fin ) ) ∧ 𝑎 ∈ 𝒫 𝑋 ) → ( 𝑇 ∈ ( 𝒫 𝑎 ∩ Fin ) ↔ 𝑇𝑎 ) )
64 63 imbi1d ( ( ( ( 𝑋𝑉𝐾𝑋 ) ∧ ( 𝑇𝑋𝑇 ∈ Fin ) ) ∧ 𝑎 ∈ 𝒫 𝑋 ) → ( ( 𝑇 ∈ ( 𝒫 𝑎 ∩ Fin ) → 𝐾𝑎 ) ↔ ( 𝑇𝑎𝐾𝑎 ) ) )
65 46 56 64 3bitrd ( ( ( ( 𝑋𝑉𝐾𝑋 ) ∧ ( 𝑇𝑋𝑇 ∈ Fin ) ) ∧ 𝑎 ∈ 𝒫 𝑋 ) → ( ∀ 𝑐 ∈ ( 𝒫 𝑎 ∩ Fin ) ( 𝑐 = 𝑇𝐾𝑎 ) ↔ ( 𝑇𝑎𝐾𝑎 ) ) )
66 21 40 65 3bitrrd ( ( ( ( 𝑋𝑉𝐾𝑋 ) ∧ ( 𝑇𝑋𝑇 ∈ Fin ) ) ∧ 𝑎 ∈ 𝒫 𝑋 ) → ( ( 𝑇𝑎𝐾𝑎 ) ↔ ( ( 𝑏 ∈ 𝒫 𝑋 ↦ if ( 𝑏 = 𝑇 , { 𝐾 } , ∅ ) ) “ ( 𝒫 𝑎 ∩ Fin ) ) ⊆ 𝑎 ) )
67 66 rabbidva ( ( ( 𝑋𝑉𝐾𝑋 ) ∧ ( 𝑇𝑋𝑇 ∈ Fin ) ) → { 𝑎 ∈ 𝒫 𝑋 ∣ ( 𝑇𝑎𝐾𝑎 ) } = { 𝑎 ∈ 𝒫 𝑋 ( ( 𝑏 ∈ 𝒫 𝑋 ↦ if ( 𝑏 = 𝑇 , { 𝐾 } , ∅ ) ) “ ( 𝒫 𝑎 ∩ Fin ) ) ⊆ 𝑎 } )
68 simpll ( ( ( 𝑋𝑉𝐾𝑋 ) ∧ ( 𝑇𝑋𝑇 ∈ Fin ) ) → 𝑋𝑉 )
69 snelpwi ( 𝐾𝑋 → { 𝐾 } ∈ 𝒫 𝑋 )
70 69 ad2antlr ( ( ( 𝑋𝑉𝐾𝑋 ) ∧ ( 𝑇𝑋𝑇 ∈ Fin ) ) → { 𝐾 } ∈ 𝒫 𝑋 )
71 0elpw ∅ ∈ 𝒫 𝑋
72 ifcl ( ( { 𝐾 } ∈ 𝒫 𝑋 ∧ ∅ ∈ 𝒫 𝑋 ) → if ( 𝑏 = 𝑇 , { 𝐾 } , ∅ ) ∈ 𝒫 𝑋 )
73 70 71 72 sylancl ( ( ( 𝑋𝑉𝐾𝑋 ) ∧ ( 𝑇𝑋𝑇 ∈ Fin ) ) → if ( 𝑏 = 𝑇 , { 𝐾 } , ∅ ) ∈ 𝒫 𝑋 )
74 73 adantr ( ( ( ( 𝑋𝑉𝐾𝑋 ) ∧ ( 𝑇𝑋𝑇 ∈ Fin ) ) ∧ 𝑏 ∈ 𝒫 𝑋 ) → if ( 𝑏 = 𝑇 , { 𝐾 } , ∅ ) ∈ 𝒫 𝑋 )
75 74 fmpttd ( ( ( 𝑋𝑉𝐾𝑋 ) ∧ ( 𝑇𝑋𝑇 ∈ Fin ) ) → ( 𝑏 ∈ 𝒫 𝑋 ↦ if ( 𝑏 = 𝑇 , { 𝐾 } , ∅ ) ) : 𝒫 𝑋 ⟶ 𝒫 𝑋 )
76 isacs1i ( ( 𝑋𝑉 ∧ ( 𝑏 ∈ 𝒫 𝑋 ↦ if ( 𝑏 = 𝑇 , { 𝐾 } , ∅ ) ) : 𝒫 𝑋 ⟶ 𝒫 𝑋 ) → { 𝑎 ∈ 𝒫 𝑋 ( ( 𝑏 ∈ 𝒫 𝑋 ↦ if ( 𝑏 = 𝑇 , { 𝐾 } , ∅ ) ) “ ( 𝒫 𝑎 ∩ Fin ) ) ⊆ 𝑎 } ∈ ( ACS ‘ 𝑋 ) )
77 68 75 76 syl2anc ( ( ( 𝑋𝑉𝐾𝑋 ) ∧ ( 𝑇𝑋𝑇 ∈ Fin ) ) → { 𝑎 ∈ 𝒫 𝑋 ( ( 𝑏 ∈ 𝒫 𝑋 ↦ if ( 𝑏 = 𝑇 , { 𝐾 } , ∅ ) ) “ ( 𝒫 𝑎 ∩ Fin ) ) ⊆ 𝑎 } ∈ ( ACS ‘ 𝑋 ) )
78 67 77 eqeltrd ( ( ( 𝑋𝑉𝐾𝑋 ) ∧ ( 𝑇𝑋𝑇 ∈ Fin ) ) → { 𝑎 ∈ 𝒫 𝑋 ∣ ( 𝑇𝑎𝐾𝑎 ) } ∈ ( ACS ‘ 𝑋 ) )