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

Metamath Proof Explorer

Theorem isacs1i

Description: A closure system determined by a function is a closure system and algebraic. (Contributed by Stefan O'Rear, 3-Apr-2015)

Ref Expression
Assertion isacs1i ( ( 𝑋 ∈ 𝑉 ∧ 𝐹 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ) → { 𝑠 ∈ 𝒫 𝑋 ∣ ∪ ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) ⊆ 𝑠 } ∈ ( ACS ‘ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 ssrab2 ⊢ { 𝑠 ∈ 𝒫 𝑋 ∣ ∪ ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) ⊆ 𝑠 } ⊆ 𝒫 𝑋
2 1 a1i ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐹 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ) → { 𝑠 ∈ 𝒫 𝑋 ∣ ∪ ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) ⊆ 𝑠 } ⊆ 𝒫 𝑋 )
3 pweq ⊢ ( 𝑠 = ( 𝑋 ∩ ∩ 𝑡 ) → 𝒫 𝑠 = 𝒫 ( 𝑋 ∩ ∩ 𝑡 ) )
4 3 ineq1d ⊢ ( 𝑠 = ( 𝑋 ∩ ∩ 𝑡 ) → ( 𝒫 𝑠 ∩ Fin ) = ( 𝒫 ( 𝑋 ∩ ∩ 𝑡 ) ∩ Fin ) )
5 4 imaeq2d ⊢ ( 𝑠 = ( 𝑋 ∩ ∩ 𝑡 ) → ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) = ( 𝐹 “ ( 𝒫 ( 𝑋 ∩ ∩ 𝑡 ) ∩ Fin ) ) )
6 5 unieqd ⊢ ( 𝑠 = ( 𝑋 ∩ ∩ 𝑡 ) → ∪ ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) = ∪ ( 𝐹 “ ( 𝒫 ( 𝑋 ∩ ∩ 𝑡 ) ∩ Fin ) ) )
7 id ⊢ ( 𝑠 = ( 𝑋 ∩ ∩ 𝑡 ) → 𝑠 = ( 𝑋 ∩ ∩ 𝑡 ) )
8 6 7 sseq12d ⊢ ( 𝑠 = ( 𝑋 ∩ ∩ 𝑡 ) → ( ∪ ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) ⊆ 𝑠 ↔ ∪ ( 𝐹 “ ( 𝒫 ( 𝑋 ∩ ∩ 𝑡 ) ∩ Fin ) ) ⊆ ( 𝑋 ∩ ∩ 𝑡 ) ) )
9 inss1 ⊢ ( 𝑋 ∩ ∩ 𝑡 ) ⊆ 𝑋
10 elpw2g ⊢ ( 𝑋 ∈ 𝑉 → ( ( 𝑋 ∩ ∩ 𝑡 ) ∈ 𝒫 𝑋 ↔ ( 𝑋 ∩ ∩ 𝑡 ) ⊆ 𝑋 ) )
11 9 10 mpbiri ⊢ ( 𝑋 ∈ 𝑉 → ( 𝑋 ∩ ∩ 𝑡 ) ∈ 𝒫 𝑋 )
12 11 ad2antrr ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐹 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ) ∧ 𝑡 ⊆ { 𝑠 ∈ 𝒫 𝑋 ∣ ∪ ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) ⊆ 𝑠 } ) → ( 𝑋 ∩ ∩ 𝑡 ) ∈ 𝒫 𝑋 )
13 imassrn ⊢ ( 𝐹 “ ( 𝒫 ( 𝑋 ∩ ∩ 𝑡 ) ∩ Fin ) ) ⊆ ran 𝐹
14 frn ⊢ ( 𝐹 : 𝒫 𝑋 ⟶ 𝒫 𝑋 → ran 𝐹 ⊆ 𝒫 𝑋 )
15 14 adantl ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐹 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ) → ran 𝐹 ⊆ 𝒫 𝑋 )
16 13 15 sstrid ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐹 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ) → ( 𝐹 “ ( 𝒫 ( 𝑋 ∩ ∩ 𝑡 ) ∩ Fin ) ) ⊆ 𝒫 𝑋 )
17 16 unissd ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐹 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ) → ∪ ( 𝐹 “ ( 𝒫 ( 𝑋 ∩ ∩ 𝑡 ) ∩ Fin ) ) ⊆ ∪ 𝒫 𝑋 )
18 unipw ⊢ ∪ 𝒫 𝑋 = 𝑋
19 17 18 sseqtrdi ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐹 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ) → ∪ ( 𝐹 “ ( 𝒫 ( 𝑋 ∩ ∩ 𝑡 ) ∩ Fin ) ) ⊆ 𝑋 )
20 19 adantr ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐹 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ) ∧ 𝑡 ⊆ { 𝑠 ∈ 𝒫 𝑋 ∣ ∪ ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) ⊆ 𝑠 } ) → ∪ ( 𝐹 “ ( 𝒫 ( 𝑋 ∩ ∩ 𝑡 ) ∩ Fin ) ) ⊆ 𝑋 )
21 inss2 ⊢ ( 𝑋 ∩ ∩ 𝑡 ) ⊆ ∩ 𝑡
22 intss1 ⊢ ( 𝑎 ∈ 𝑡 → ∩ 𝑡 ⊆ 𝑎 )
23 21 22 sstrid ⊢ ( 𝑎 ∈ 𝑡 → ( 𝑋 ∩ ∩ 𝑡 ) ⊆ 𝑎 )
24 23 adantl ⊢ ( ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐹 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ) ∧ 𝑡 ⊆ { 𝑠 ∈ 𝒫 𝑋 ∣ ∪ ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) ⊆ 𝑠 } ) ∧ 𝑎 ∈ 𝑡 ) → ( 𝑋 ∩ ∩ 𝑡 ) ⊆ 𝑎 )
25 24 sspwd ⊢ ( ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐹 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ) ∧ 𝑡 ⊆ { 𝑠 ∈ 𝒫 𝑋 ∣ ∪ ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) ⊆ 𝑠 } ) ∧ 𝑎 ∈ 𝑡 ) → 𝒫 ( 𝑋 ∩ ∩ 𝑡 ) ⊆ 𝒫 𝑎 )
26 25 ssrind ⊢ ( ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐹 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ) ∧ 𝑡 ⊆ { 𝑠 ∈ 𝒫 𝑋 ∣ ∪ ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) ⊆ 𝑠 } ) ∧ 𝑎 ∈ 𝑡 ) → ( 𝒫 ( 𝑋 ∩ ∩ 𝑡 ) ∩ Fin ) ⊆ ( 𝒫 𝑎 ∩ Fin ) )
27 imass2 ⊢ ( ( 𝒫 ( 𝑋 ∩ ∩ 𝑡 ) ∩ Fin ) ⊆ ( 𝒫 𝑎 ∩ Fin ) → ( 𝐹 “ ( 𝒫 ( 𝑋 ∩ ∩ 𝑡 ) ∩ Fin ) ) ⊆ ( 𝐹 “ ( 𝒫 𝑎 ∩ Fin ) ) )
28 26 27 syl ⊢ ( ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐹 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ) ∧ 𝑡 ⊆ { 𝑠 ∈ 𝒫 𝑋 ∣ ∪ ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) ⊆ 𝑠 } ) ∧ 𝑎 ∈ 𝑡 ) → ( 𝐹 “ ( 𝒫 ( 𝑋 ∩ ∩ 𝑡 ) ∩ Fin ) ) ⊆ ( 𝐹 “ ( 𝒫 𝑎 ∩ Fin ) ) )
29 28 unissd ⊢ ( ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐹 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ) ∧ 𝑡 ⊆ { 𝑠 ∈ 𝒫 𝑋 ∣ ∪ ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) ⊆ 𝑠 } ) ∧ 𝑎 ∈ 𝑡 ) → ∪ ( 𝐹 “ ( 𝒫 ( 𝑋 ∩ ∩ 𝑡 ) ∩ Fin ) ) ⊆ ∪ ( 𝐹 “ ( 𝒫 𝑎 ∩ Fin ) ) )
30 ssel2 ⊢ ( ( 𝑡 ⊆ { 𝑠 ∈ 𝒫 𝑋 ∣ ∪ ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) ⊆ 𝑠 } ∧ 𝑎 ∈ 𝑡 ) → 𝑎 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ∪ ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) ⊆ 𝑠 } )
31 pweq ⊢ ( 𝑠 = 𝑎 → 𝒫 𝑠 = 𝒫 𝑎 )
32 31 ineq1d ⊢ ( 𝑠 = 𝑎 → ( 𝒫 𝑠 ∩ Fin ) = ( 𝒫 𝑎 ∩ Fin ) )
33 32 imaeq2d ⊢ ( 𝑠 = 𝑎 → ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) = ( 𝐹 “ ( 𝒫 𝑎 ∩ Fin ) ) )
34 33 unieqd ⊢ ( 𝑠 = 𝑎 → ∪ ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) = ∪ ( 𝐹 “ ( 𝒫 𝑎 ∩ Fin ) ) )
35 id ⊢ ( 𝑠 = 𝑎 → 𝑠 = 𝑎 )
36 34 35 sseq12d ⊢ ( 𝑠 = 𝑎 → ( ∪ ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) ⊆ 𝑠 ↔ ∪ ( 𝐹 “ ( 𝒫 𝑎 ∩ Fin ) ) ⊆ 𝑎 ) )
37 36 elrab ⊢ ( 𝑎 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ∪ ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) ⊆ 𝑠 } ↔ ( 𝑎 ∈ 𝒫 𝑋 ∧ ∪ ( 𝐹 “ ( 𝒫 𝑎 ∩ Fin ) ) ⊆ 𝑎 ) )
38 37 simprbi ⊢ ( 𝑎 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ∪ ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) ⊆ 𝑠 } → ∪ ( 𝐹 “ ( 𝒫 𝑎 ∩ Fin ) ) ⊆ 𝑎 )
39 30 38 syl ⊢ ( ( 𝑡 ⊆ { 𝑠 ∈ 𝒫 𝑋 ∣ ∪ ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) ⊆ 𝑠 } ∧ 𝑎 ∈ 𝑡 ) → ∪ ( 𝐹 “ ( 𝒫 𝑎 ∩ Fin ) ) ⊆ 𝑎 )
40 39 adantll ⊢ ( ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐹 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ) ∧ 𝑡 ⊆ { 𝑠 ∈ 𝒫 𝑋 ∣ ∪ ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) ⊆ 𝑠 } ) ∧ 𝑎 ∈ 𝑡 ) → ∪ ( 𝐹 “ ( 𝒫 𝑎 ∩ Fin ) ) ⊆ 𝑎 )
41 29 40 sstrd ⊢ ( ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐹 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ) ∧ 𝑡 ⊆ { 𝑠 ∈ 𝒫 𝑋 ∣ ∪ ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) ⊆ 𝑠 } ) ∧ 𝑎 ∈ 𝑡 ) → ∪ ( 𝐹 “ ( 𝒫 ( 𝑋 ∩ ∩ 𝑡 ) ∩ Fin ) ) ⊆ 𝑎 )
42 41 ralrimiva ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐹 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ) ∧ 𝑡 ⊆ { 𝑠 ∈ 𝒫 𝑋 ∣ ∪ ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) ⊆ 𝑠 } ) → ∀ 𝑎 ∈ 𝑡 ∪ ( 𝐹 “ ( 𝒫 ( 𝑋 ∩ ∩ 𝑡 ) ∩ Fin ) ) ⊆ 𝑎 )
43 ssint ⊢ ( ∪ ( 𝐹 “ ( 𝒫 ( 𝑋 ∩ ∩ 𝑡 ) ∩ Fin ) ) ⊆ ∩ 𝑡 ↔ ∀ 𝑎 ∈ 𝑡 ∪ ( 𝐹 “ ( 𝒫 ( 𝑋 ∩ ∩ 𝑡 ) ∩ Fin ) ) ⊆ 𝑎 )
44 42 43 sylibr ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐹 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ) ∧ 𝑡 ⊆ { 𝑠 ∈ 𝒫 𝑋 ∣ ∪ ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) ⊆ 𝑠 } ) → ∪ ( 𝐹 “ ( 𝒫 ( 𝑋 ∩ ∩ 𝑡 ) ∩ Fin ) ) ⊆ ∩ 𝑡 )
45 20 44 ssind ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐹 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ) ∧ 𝑡 ⊆ { 𝑠 ∈ 𝒫 𝑋 ∣ ∪ ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) ⊆ 𝑠 } ) → ∪ ( 𝐹 “ ( 𝒫 ( 𝑋 ∩ ∩ 𝑡 ) ∩ Fin ) ) ⊆ ( 𝑋 ∩ ∩ 𝑡 ) )
46 8 12 45 elrabd ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐹 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ) ∧ 𝑡 ⊆ { 𝑠 ∈ 𝒫 𝑋 ∣ ∪ ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) ⊆ 𝑠 } ) → ( 𝑋 ∩ ∩ 𝑡 ) ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ∪ ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) ⊆ 𝑠 } )
47 2 46 ismred2 ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐹 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ) → { 𝑠 ∈ 𝒫 𝑋 ∣ ∪ ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) ⊆ 𝑠 } ∈ ( Moore ‘ 𝑋 ) )
48 fssxp ⊢ ( 𝐹 : 𝒫 𝑋 ⟶ 𝒫 𝑋 → 𝐹 ⊆ ( 𝒫 𝑋 × 𝒫 𝑋 ) )
49 pwexg ⊢ ( 𝑋 ∈ 𝑉 → 𝒫 𝑋 ∈ V )
50 49 49 xpexd ⊢ ( 𝑋 ∈ 𝑉 → ( 𝒫 𝑋 × 𝒫 𝑋 ) ∈ V )
51 ssexg ⊢ ( ( 𝐹 ⊆ ( 𝒫 𝑋 × 𝒫 𝑋 ) ∧ ( 𝒫 𝑋 × 𝒫 𝑋 ) ∈ V ) → 𝐹 ∈ V )
52 48 50 51 syl2anr ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐹 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ) → 𝐹 ∈ V )
53 simpr ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐹 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ) → 𝐹 : 𝒫 𝑋 ⟶ 𝒫 𝑋 )
54 pweq ⊢ ( 𝑠 = 𝑡 → 𝒫 𝑠 = 𝒫 𝑡 )
55 54 ineq1d ⊢ ( 𝑠 = 𝑡 → ( 𝒫 𝑠 ∩ Fin ) = ( 𝒫 𝑡 ∩ Fin ) )
56 55 imaeq2d ⊢ ( 𝑠 = 𝑡 → ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) = ( 𝐹 “ ( 𝒫 𝑡 ∩ Fin ) ) )
57 56 unieqd ⊢ ( 𝑠 = 𝑡 → ∪ ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) = ∪ ( 𝐹 “ ( 𝒫 𝑡 ∩ Fin ) ) )
58 id ⊢ ( 𝑠 = 𝑡 → 𝑠 = 𝑡 )
59 57 58 sseq12d ⊢ ( 𝑠 = 𝑡 → ( ∪ ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) ⊆ 𝑠 ↔ ∪ ( 𝐹 “ ( 𝒫 𝑡 ∩ Fin ) ) ⊆ 𝑡 ) )
60 59 elrab3 ⊢ ( 𝑡 ∈ 𝒫 𝑋 → ( 𝑡 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ∪ ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) ⊆ 𝑠 } ↔ ∪ ( 𝐹 “ ( 𝒫 𝑡 ∩ Fin ) ) ⊆ 𝑡 ) )
61 60 rgen ⊢ ∀ 𝑡 ∈ 𝒫 𝑋 ( 𝑡 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ∪ ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) ⊆ 𝑠 } ↔ ∪ ( 𝐹 “ ( 𝒫 𝑡 ∩ Fin ) ) ⊆ 𝑡 )
62 53 61 jctir ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐹 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ) → ( 𝐹 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ∧ ∀ 𝑡 ∈ 𝒫 𝑋 ( 𝑡 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ∪ ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) ⊆ 𝑠 } ↔ ∪ ( 𝐹 “ ( 𝒫 𝑡 ∩ Fin ) ) ⊆ 𝑡 ) ) )
63 feq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ↔ 𝐹 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ) )
64 imaeq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 “ ( 𝒫 𝑡 ∩ Fin ) ) = ( 𝐹 “ ( 𝒫 𝑡 ∩ Fin ) ) )
65 64 unieqd ⊢ ( 𝑓 = 𝐹 → ∪ ( 𝑓 “ ( 𝒫 𝑡 ∩ Fin ) ) = ∪ ( 𝐹 “ ( 𝒫 𝑡 ∩ Fin ) ) )
66 65 sseq1d ⊢ ( 𝑓 = 𝐹 → ( ∪ ( 𝑓 “ ( 𝒫 𝑡 ∩ Fin ) ) ⊆ 𝑡 ↔ ∪ ( 𝐹 “ ( 𝒫 𝑡 ∩ Fin ) ) ⊆ 𝑡 ) )
67 66 bibi2d ⊢ ( 𝑓 = 𝐹 → ( ( 𝑡 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ∪ ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) ⊆ 𝑠 } ↔ ∪ ( 𝑓 “ ( 𝒫 𝑡 ∩ Fin ) ) ⊆ 𝑡 ) ↔ ( 𝑡 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ∪ ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) ⊆ 𝑠 } ↔ ∪ ( 𝐹 “ ( 𝒫 𝑡 ∩ Fin ) ) ⊆ 𝑡 ) ) )
68 67 ralbidv ⊢ ( 𝑓 = 𝐹 → ( ∀ 𝑡 ∈ 𝒫 𝑋 ( 𝑡 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ∪ ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) ⊆ 𝑠 } ↔ ∪ ( 𝑓 “ ( 𝒫 𝑡 ∩ Fin ) ) ⊆ 𝑡 ) ↔ ∀ 𝑡 ∈ 𝒫 𝑋 ( 𝑡 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ∪ ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) ⊆ 𝑠 } ↔ ∪ ( 𝐹 “ ( 𝒫 𝑡 ∩ Fin ) ) ⊆ 𝑡 ) ) )
69 63 68 anbi12d ⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ∧ ∀ 𝑡 ∈ 𝒫 𝑋 ( 𝑡 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ∪ ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) ⊆ 𝑠 } ↔ ∪ ( 𝑓 “ ( 𝒫 𝑡 ∩ Fin ) ) ⊆ 𝑡 ) ) ↔ ( 𝐹 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ∧ ∀ 𝑡 ∈ 𝒫 𝑋 ( 𝑡 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ∪ ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) ⊆ 𝑠 } ↔ ∪ ( 𝐹 “ ( 𝒫 𝑡 ∩ Fin ) ) ⊆ 𝑡 ) ) ) )
70 52 62 69 spcedv ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐹 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ) → ∃ 𝑓 ( 𝑓 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ∧ ∀ 𝑡 ∈ 𝒫 𝑋 ( 𝑡 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ∪ ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) ⊆ 𝑠 } ↔ ∪ ( 𝑓 “ ( 𝒫 𝑡 ∩ Fin ) ) ⊆ 𝑡 ) ) )
71 isacs ⊢ ( { 𝑠 ∈ 𝒫 𝑋 ∣ ∪ ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) ⊆ 𝑠 } ∈ ( ACS ‘ 𝑋 ) ↔ ( { 𝑠 ∈ 𝒫 𝑋 ∣ ∪ ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) ⊆ 𝑠 } ∈ ( Moore ‘ 𝑋 ) ∧ ∃ 𝑓 ( 𝑓 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ∧ ∀ 𝑡 ∈ 𝒫 𝑋 ( 𝑡 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ∪ ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) ⊆ 𝑠 } ↔ ∪ ( 𝑓 “ ( 𝒫 𝑡 ∩ Fin ) ) ⊆ 𝑡 ) ) ) )
72 47 70 71 sylanbrc ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐹 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ) → { 𝑠 ∈ 𝒫 𝑋 ∣ ∪ ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) ⊆ 𝑠 } ∈ ( ACS ‘ 𝑋 ) )