This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 bitrid ⊢ ( ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐾 ∈ 𝑋 ) ∧ ( 𝑇 ⊆ 𝑋 ∧ 𝑇 ∈ 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 bitrid ⊢ ( ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐾 ∈ 𝑋 ) ∧ ( 𝑇 ⊆ 𝑋 ∧ 𝑇 ∈ 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 ‘ 𝑋 ) )