Metamath Proof Explorer

Theorem isacs2

Description: In the definition of an algebraic closure system, we may always take the operation being closed over as the Moore closure. (Contributed by Stefan O'Rear, 2-Apr-2015)

Ref Expression
Hypothesis isacs2.f ⊢ 𝐹 = ( mrCls ‘ 𝐶 )
Assertion isacs2 ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ↔ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝒫 𝑋 ( 𝑠 ∈ 𝐶 ↔ ∀ 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) ( 𝐹 ‘ 𝑦 ) ⊆ 𝑠 ) ) )

Proof

Step Hyp Ref Expression
1 isacs2.f ⊢ 𝐹 = ( mrCls ‘ 𝐶 )
2 isacs ⊢ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ↔ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∃ 𝑓 ( 𝑓 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ∧ ∀ 𝑡 ∈ 𝒫 𝑋 ( 𝑡 ∈ 𝐶 ↔ ∪ ( 𝑓 “ ( 𝒫 𝑡 ∩ Fin ) ) ⊆ 𝑡 ) ) ) )
3 ffun ⊢ ( 𝑓 : 𝒫 𝑋 ⟶ 𝒫 𝑋 → Fun 𝑓 )
4 funiunfv ⊢ ( Fun 𝑓 → ∪ 𝑧 ∈ ( 𝒫 𝑡 ∩ Fin ) ( 𝑓 ‘ 𝑧 ) = ∪ ( 𝑓 “ ( 𝒫 𝑡 ∩ Fin ) ) )
5 3 4 syl ⊢ ( 𝑓 : 𝒫 𝑋 ⟶ 𝒫 𝑋 → ∪ 𝑧 ∈ ( 𝒫 𝑡 ∩ Fin ) ( 𝑓 ‘ 𝑧 ) = ∪ ( 𝑓 “ ( 𝒫 𝑡 ∩ Fin ) ) )
6 5 sseq1d ⊢ ( 𝑓 : 𝒫 𝑋 ⟶ 𝒫 𝑋 → ( ∪ 𝑧 ∈ ( 𝒫 𝑡 ∩ Fin ) ( 𝑓 ‘ 𝑧 ) ⊆ 𝑡 ↔ ∪ ( 𝑓 “ ( 𝒫 𝑡 ∩ Fin ) ) ⊆ 𝑡 ) )
7 iunss ⊢ ( ∪ 𝑧 ∈ ( 𝒫 𝑡 ∩ Fin ) ( 𝑓 ‘ 𝑧 ) ⊆ 𝑡 ↔ ∀ 𝑧 ∈ ( 𝒫 𝑡 ∩ Fin ) ( 𝑓 ‘ 𝑧 ) ⊆ 𝑡 )
8 6 7 bitr3di ⊢ ( 𝑓 : 𝒫 𝑋 ⟶ 𝒫 𝑋 → ( ∪ ( 𝑓 “ ( 𝒫 𝑡 ∩ Fin ) ) ⊆ 𝑡 ↔ ∀ 𝑧 ∈ ( 𝒫 𝑡 ∩ Fin ) ( 𝑓 ‘ 𝑧 ) ⊆ 𝑡 ) )
9 8 bibi2d ⊢ ( 𝑓 : 𝒫 𝑋 ⟶ 𝒫 𝑋 → ( ( 𝑡 ∈ 𝐶 ↔ ∪ ( 𝑓 “ ( 𝒫 𝑡 ∩ Fin ) ) ⊆ 𝑡 ) ↔ ( 𝑡 ∈ 𝐶 ↔ ∀ 𝑧 ∈ ( 𝒫 𝑡 ∩ Fin ) ( 𝑓 ‘ 𝑧 ) ⊆ 𝑡 ) ) )
10 9 ralbidv ⊢ ( 𝑓 : 𝒫 𝑋 ⟶ 𝒫 𝑋 → ( ∀ 𝑡 ∈ 𝒫 𝑋 ( 𝑡 ∈ 𝐶 ↔ ∪ ( 𝑓 “ ( 𝒫 𝑡 ∩ Fin ) ) ⊆ 𝑡 ) ↔ ∀ 𝑡 ∈ 𝒫 𝑋 ( 𝑡 ∈ 𝐶 ↔ ∀ 𝑧 ∈ ( 𝒫 𝑡 ∩ Fin ) ( 𝑓 ‘ 𝑧 ) ⊆ 𝑡 ) ) )
11 10 pm5.32i ⊢ ( ( 𝑓 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ∧ ∀ 𝑡 ∈ 𝒫 𝑋 ( 𝑡 ∈ 𝐶 ↔ ∪ ( 𝑓 “ ( 𝒫 𝑡 ∩ Fin ) ) ⊆ 𝑡 ) ) ↔ ( 𝑓 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ∧ ∀ 𝑡 ∈ 𝒫 𝑋 ( 𝑡 ∈ 𝐶 ↔ ∀ 𝑧 ∈ ( 𝒫 𝑡 ∩ Fin ) ( 𝑓 ‘ 𝑧 ) ⊆ 𝑡 ) ) )
12 11 exbii ⊢ ( ∃ 𝑓 ( 𝑓 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ∧ ∀ 𝑡 ∈ 𝒫 𝑋 ( 𝑡 ∈ 𝐶 ↔ ∪ ( 𝑓 “ ( 𝒫 𝑡 ∩ Fin ) ) ⊆ 𝑡 ) ) ↔ ∃ 𝑓 ( 𝑓 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ∧ ∀ 𝑡 ∈ 𝒫 𝑋 ( 𝑡 ∈ 𝐶 ↔ ∀ 𝑧 ∈ ( 𝒫 𝑡 ∩ Fin ) ( 𝑓 ‘ 𝑧 ) ⊆ 𝑡 ) ) )
13 simpll ⊢ ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑠 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) ) → 𝐶 ∈ ( Moore ‘ 𝑋 ) )
14 elinel1 ⊢ ( 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) → 𝑦 ∈ 𝒫 𝑠 )
15 14 elpwid ⊢ ( 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) → 𝑦 ⊆ 𝑠 )
16 15 adantl ⊢ ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑠 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) ) → 𝑦 ⊆ 𝑠 )
17 simplr ⊢ ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑠 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) ) → 𝑠 ∈ 𝐶 )
18 1 mrcsscl ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑦 ⊆ 𝑠 ∧ 𝑠 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑦 ) ⊆ 𝑠 )
19 13 16 17 18 syl3anc ⊢ ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑠 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) ) → ( 𝐹 ‘ 𝑦 ) ⊆ 𝑠 )
20 19 ralrimiva ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑠 ∈ 𝐶 ) → ∀ 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) ( 𝐹 ‘ 𝑦 ) ⊆ 𝑠 )
21 20 ad4ant14 ⊢ ( ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ( 𝑓 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ∧ ∀ 𝑡 ∈ 𝒫 𝑋 ( 𝑡 ∈ 𝐶 ↔ ∀ 𝑧 ∈ ( 𝒫 𝑡 ∩ Fin ) ( 𝑓 ‘ 𝑧 ) ⊆ 𝑡 ) ) ) ∧ 𝑠 ∈ 𝒫 𝑋 ) ∧ 𝑠 ∈ 𝐶 ) → ∀ 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) ( 𝐹 ‘ 𝑦 ) ⊆ 𝑠 )
22 fveq2 ⊢ ( 𝑧 = 𝑦 → ( 𝑓 ‘ 𝑧 ) = ( 𝑓 ‘ 𝑦 ) )
23 22 sseq1d ⊢ ( 𝑧 = 𝑦 → ( ( 𝑓 ‘ 𝑧 ) ⊆ ( 𝐹 ‘ 𝑦 ) ↔ ( 𝑓 ‘ 𝑦 ) ⊆ ( 𝐹 ‘ 𝑦 ) ) )
24 simplll ⊢ ( ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ( 𝑓 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ∧ ∀ 𝑡 ∈ 𝒫 𝑋 ( 𝑡 ∈ 𝐶 ↔ ∀ 𝑧 ∈ ( 𝒫 𝑡 ∩ Fin ) ( 𝑓 ‘ 𝑧 ) ⊆ 𝑡 ) ) ) ∧ 𝑠 ∈ 𝒫 𝑋 ) ∧ 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) ) → 𝐶 ∈ ( Moore ‘ 𝑋 ) )
25 15 adantl ⊢ ( ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ( 𝑓 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ∧ ∀ 𝑡 ∈ 𝒫 𝑋 ( 𝑡 ∈ 𝐶 ↔ ∀ 𝑧 ∈ ( 𝒫 𝑡 ∩ Fin ) ( 𝑓 ‘ 𝑧 ) ⊆ 𝑡 ) ) ) ∧ 𝑠 ∈ 𝒫 𝑋 ) ∧ 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) ) → 𝑦 ⊆ 𝑠 )
26 elpwi ⊢ ( 𝑠 ∈ 𝒫 𝑋 → 𝑠 ⊆ 𝑋 )
27 26 ad2antlr ⊢ ( ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ( 𝑓 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ∧ ∀ 𝑡 ∈ 𝒫 𝑋 ( 𝑡 ∈ 𝐶 ↔ ∀ 𝑧 ∈ ( 𝒫 𝑡 ∩ Fin ) ( 𝑓 ‘ 𝑧 ) ⊆ 𝑡 ) ) ) ∧ 𝑠 ∈ 𝒫 𝑋 ) ∧ 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) ) → 𝑠 ⊆ 𝑋 )
28 25 27 sstrd ⊢ ( ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ( 𝑓 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ∧ ∀ 𝑡 ∈ 𝒫 𝑋 ( 𝑡 ∈ 𝐶 ↔ ∀ 𝑧 ∈ ( 𝒫 𝑡 ∩ Fin ) ( 𝑓 ‘ 𝑧 ) ⊆ 𝑡 ) ) ) ∧ 𝑠 ∈ 𝒫 𝑋 ) ∧ 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) ) → 𝑦 ⊆ 𝑋 )
29 1 mrccl ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑦 ⊆ 𝑋 ) → ( 𝐹 ‘ 𝑦 ) ∈ 𝐶 )
30 24 28 29 syl2anc ⊢ ( ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ( 𝑓 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ∧ ∀ 𝑡 ∈ 𝒫 𝑋 ( 𝑡 ∈ 𝐶 ↔ ∀ 𝑧 ∈ ( 𝒫 𝑡 ∩ Fin ) ( 𝑓 ‘ 𝑧 ) ⊆ 𝑡 ) ) ) ∧ 𝑠 ∈ 𝒫 𝑋 ) ∧ 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) ) → ( 𝐹 ‘ 𝑦 ) ∈ 𝐶 )
31 eleq1 ⊢ ( 𝑡 = ( 𝐹 ‘ 𝑦 ) → ( 𝑡 ∈ 𝐶 ↔ ( 𝐹 ‘ 𝑦 ) ∈ 𝐶 ) )
32 pweq ⊢ ( 𝑡 = ( 𝐹 ‘ 𝑦 ) → 𝒫 𝑡 = 𝒫 ( 𝐹 ‘ 𝑦 ) )
33 32 ineq1d ⊢ ( 𝑡 = ( 𝐹 ‘ 𝑦 ) → ( 𝒫 𝑡 ∩ Fin ) = ( 𝒫 ( 𝐹 ‘ 𝑦 ) ∩ Fin ) )
34 sseq2 ⊢ ( 𝑡 = ( 𝐹 ‘ 𝑦 ) → ( ( 𝑓 ‘ 𝑧 ) ⊆ 𝑡 ↔ ( 𝑓 ‘ 𝑧 ) ⊆ ( 𝐹 ‘ 𝑦 ) ) )
35 33 34 raleqbidv ⊢ ( 𝑡 = ( 𝐹 ‘ 𝑦 ) → ( ∀ 𝑧 ∈ ( 𝒫 𝑡 ∩ Fin ) ( 𝑓 ‘ 𝑧 ) ⊆ 𝑡 ↔ ∀ 𝑧 ∈ ( 𝒫 ( 𝐹 ‘ 𝑦 ) ∩ Fin ) ( 𝑓 ‘ 𝑧 ) ⊆ ( 𝐹 ‘ 𝑦 ) ) )
36 31 35 bibi12d ⊢ ( 𝑡 = ( 𝐹 ‘ 𝑦 ) → ( ( 𝑡 ∈ 𝐶 ↔ ∀ 𝑧 ∈ ( 𝒫 𝑡 ∩ Fin ) ( 𝑓 ‘ 𝑧 ) ⊆ 𝑡 ) ↔ ( ( 𝐹 ‘ 𝑦 ) ∈ 𝐶 ↔ ∀ 𝑧 ∈ ( 𝒫 ( 𝐹 ‘ 𝑦 ) ∩ Fin ) ( 𝑓 ‘ 𝑧 ) ⊆ ( 𝐹 ‘ 𝑦 ) ) ) )
37 simprr ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ( 𝑓 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ∧ ∀ 𝑡 ∈ 𝒫 𝑋 ( 𝑡 ∈ 𝐶 ↔ ∀ 𝑧 ∈ ( 𝒫 𝑡 ∩ Fin ) ( 𝑓 ‘ 𝑧 ) ⊆ 𝑡 ) ) ) → ∀ 𝑡 ∈ 𝒫 𝑋 ( 𝑡 ∈ 𝐶 ↔ ∀ 𝑧 ∈ ( 𝒫 𝑡 ∩ Fin ) ( 𝑓 ‘ 𝑧 ) ⊆ 𝑡 ) )
38 37 ad2antrr ⊢ ( ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ( 𝑓 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ∧ ∀ 𝑡 ∈ 𝒫 𝑋 ( 𝑡 ∈ 𝐶 ↔ ∀ 𝑧 ∈ ( 𝒫 𝑡 ∩ Fin ) ( 𝑓 ‘ 𝑧 ) ⊆ 𝑡 ) ) ) ∧ 𝑠 ∈ 𝒫 𝑋 ) ∧ 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) ) → ∀ 𝑡 ∈ 𝒫 𝑋 ( 𝑡 ∈ 𝐶 ↔ ∀ 𝑧 ∈ ( 𝒫 𝑡 ∩ Fin ) ( 𝑓 ‘ 𝑧 ) ⊆ 𝑡 ) )
39 mresspw ⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → 𝐶 ⊆ 𝒫 𝑋 )
40 39 ad3antrrr ⊢ ( ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ( 𝑓 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ∧ ∀ 𝑡 ∈ 𝒫 𝑋 ( 𝑡 ∈ 𝐶 ↔ ∀ 𝑧 ∈ ( 𝒫 𝑡 ∩ Fin ) ( 𝑓 ‘ 𝑧 ) ⊆ 𝑡 ) ) ) ∧ 𝑠 ∈ 𝒫 𝑋 ) ∧ 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) ) → 𝐶 ⊆ 𝒫 𝑋 )
41 40 30 sseldd ⊢ ( ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ( 𝑓 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ∧ ∀ 𝑡 ∈ 𝒫 𝑋 ( 𝑡 ∈ 𝐶 ↔ ∀ 𝑧 ∈ ( 𝒫 𝑡 ∩ Fin ) ( 𝑓 ‘ 𝑧 ) ⊆ 𝑡 ) ) ) ∧ 𝑠 ∈ 𝒫 𝑋 ) ∧ 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) ) → ( 𝐹 ‘ 𝑦 ) ∈ 𝒫 𝑋 )
42 36 38 41 rspcdva ⊢ ( ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ( 𝑓 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ∧ ∀ 𝑡 ∈ 𝒫 𝑋 ( 𝑡 ∈ 𝐶 ↔ ∀ 𝑧 ∈ ( 𝒫 𝑡 ∩ Fin ) ( 𝑓 ‘ 𝑧 ) ⊆ 𝑡 ) ) ) ∧ 𝑠 ∈ 𝒫 𝑋 ) ∧ 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) ) → ( ( 𝐹 ‘ 𝑦 ) ∈ 𝐶 ↔ ∀ 𝑧 ∈ ( 𝒫 ( 𝐹 ‘ 𝑦 ) ∩ Fin ) ( 𝑓 ‘ 𝑧 ) ⊆ ( 𝐹 ‘ 𝑦 ) ) )
43 30 42 mpbid ⊢ ( ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ( 𝑓 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ∧ ∀ 𝑡 ∈ 𝒫 𝑋 ( 𝑡 ∈ 𝐶 ↔ ∀ 𝑧 ∈ ( 𝒫 𝑡 ∩ Fin ) ( 𝑓 ‘ 𝑧 ) ⊆ 𝑡 ) ) ) ∧ 𝑠 ∈ 𝒫 𝑋 ) ∧ 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) ) → ∀ 𝑧 ∈ ( 𝒫 ( 𝐹 ‘ 𝑦 ) ∩ Fin ) ( 𝑓 ‘ 𝑧 ) ⊆ ( 𝐹 ‘ 𝑦 ) )
44 24 1 28 mrcssidd ⊢ ( ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ( 𝑓 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ∧ ∀ 𝑡 ∈ 𝒫 𝑋 ( 𝑡 ∈ 𝐶 ↔ ∀ 𝑧 ∈ ( 𝒫 𝑡 ∩ Fin ) ( 𝑓 ‘ 𝑧 ) ⊆ 𝑡 ) ) ) ∧ 𝑠 ∈ 𝒫 𝑋 ) ∧ 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) ) → 𝑦 ⊆ ( 𝐹 ‘ 𝑦 ) )
45 vex ⊢ 𝑦 ∈ V
46 45 elpw ⊢ ( 𝑦 ∈ 𝒫 ( 𝐹 ‘ 𝑦 ) ↔ 𝑦 ⊆ ( 𝐹 ‘ 𝑦 ) )
47 44 46 sylibr ⊢ ( ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ( 𝑓 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ∧ ∀ 𝑡 ∈ 𝒫 𝑋 ( 𝑡 ∈ 𝐶 ↔ ∀ 𝑧 ∈ ( 𝒫 𝑡 ∩ Fin ) ( 𝑓 ‘ 𝑧 ) ⊆ 𝑡 ) ) ) ∧ 𝑠 ∈ 𝒫 𝑋 ) ∧ 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) ) → 𝑦 ∈ 𝒫 ( 𝐹 ‘ 𝑦 ) )
48 elinel2 ⊢ ( 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) → 𝑦 ∈ Fin )
49 48 adantl ⊢ ( ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ( 𝑓 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ∧ ∀ 𝑡 ∈ 𝒫 𝑋 ( 𝑡 ∈ 𝐶 ↔ ∀ 𝑧 ∈ ( 𝒫 𝑡 ∩ Fin ) ( 𝑓 ‘ 𝑧 ) ⊆ 𝑡 ) ) ) ∧ 𝑠 ∈ 𝒫 𝑋 ) ∧ 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) ) → 𝑦 ∈ Fin )
50 47 49 elind ⊢ ( ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ( 𝑓 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ∧ ∀ 𝑡 ∈ 𝒫 𝑋 ( 𝑡 ∈ 𝐶 ↔ ∀ 𝑧 ∈ ( 𝒫 𝑡 ∩ Fin ) ( 𝑓 ‘ 𝑧 ) ⊆ 𝑡 ) ) ) ∧ 𝑠 ∈ 𝒫 𝑋 ) ∧ 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) ) → 𝑦 ∈ ( 𝒫 ( 𝐹 ‘ 𝑦 ) ∩ Fin ) )
51 23 43 50 rspcdva ⊢ ( ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ( 𝑓 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ∧ ∀ 𝑡 ∈ 𝒫 𝑋 ( 𝑡 ∈ 𝐶 ↔ ∀ 𝑧 ∈ ( 𝒫 𝑡 ∩ Fin ) ( 𝑓 ‘ 𝑧 ) ⊆ 𝑡 ) ) ) ∧ 𝑠 ∈ 𝒫 𝑋 ) ∧ 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) ) → ( 𝑓 ‘ 𝑦 ) ⊆ ( 𝐹 ‘ 𝑦 ) )
52 sstr2 ⊢ ( ( 𝑓 ‘ 𝑦 ) ⊆ ( 𝐹 ‘ 𝑦 ) → ( ( 𝐹 ‘ 𝑦 ) ⊆ 𝑠 → ( 𝑓 ‘ 𝑦 ) ⊆ 𝑠 ) )
53 51 52 syl ⊢ ( ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ( 𝑓 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ∧ ∀ 𝑡 ∈ 𝒫 𝑋 ( 𝑡 ∈ 𝐶 ↔ ∀ 𝑧 ∈ ( 𝒫 𝑡 ∩ Fin ) ( 𝑓 ‘ 𝑧 ) ⊆ 𝑡 ) ) ) ∧ 𝑠 ∈ 𝒫 𝑋 ) ∧ 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) ) → ( ( 𝐹 ‘ 𝑦 ) ⊆ 𝑠 → ( 𝑓 ‘ 𝑦 ) ⊆ 𝑠 ) )
54 53 ralimdva ⊢ ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ( 𝑓 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ∧ ∀ 𝑡 ∈ 𝒫 𝑋 ( 𝑡 ∈ 𝐶 ↔ ∀ 𝑧 ∈ ( 𝒫 𝑡 ∩ Fin ) ( 𝑓 ‘ 𝑧 ) ⊆ 𝑡 ) ) ) ∧ 𝑠 ∈ 𝒫 𝑋 ) → ( ∀ 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) ( 𝐹 ‘ 𝑦 ) ⊆ 𝑠 → ∀ 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) ( 𝑓 ‘ 𝑦 ) ⊆ 𝑠 ) )
55 54 imp ⊢ ( ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ( 𝑓 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ∧ ∀ 𝑡 ∈ 𝒫 𝑋 ( 𝑡 ∈ 𝐶 ↔ ∀ 𝑧 ∈ ( 𝒫 𝑡 ∩ Fin ) ( 𝑓 ‘ 𝑧 ) ⊆ 𝑡 ) ) ) ∧ 𝑠 ∈ 𝒫 𝑋 ) ∧ ∀ 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) ( 𝐹 ‘ 𝑦 ) ⊆ 𝑠 ) → ∀ 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) ( 𝑓 ‘ 𝑦 ) ⊆ 𝑠 )
56 fveq2 ⊢ ( 𝑦 = 𝑧 → ( 𝑓 ‘ 𝑦 ) = ( 𝑓 ‘ 𝑧 ) )
57 56 sseq1d ⊢ ( 𝑦 = 𝑧 → ( ( 𝑓 ‘ 𝑦 ) ⊆ 𝑠 ↔ ( 𝑓 ‘ 𝑧 ) ⊆ 𝑠 ) )
58 57 cbvralvw ⊢ ( ∀ 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) ( 𝑓 ‘ 𝑦 ) ⊆ 𝑠 ↔ ∀ 𝑧 ∈ ( 𝒫 𝑠 ∩ Fin ) ( 𝑓 ‘ 𝑧 ) ⊆ 𝑠 )
59 55 58 sylib ⊢ ( ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ( 𝑓 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ∧ ∀ 𝑡 ∈ 𝒫 𝑋 ( 𝑡 ∈ 𝐶 ↔ ∀ 𝑧 ∈ ( 𝒫 𝑡 ∩ Fin ) ( 𝑓 ‘ 𝑧 ) ⊆ 𝑡 ) ) ) ∧ 𝑠 ∈ 𝒫 𝑋 ) ∧ ∀ 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) ( 𝐹 ‘ 𝑦 ) ⊆ 𝑠 ) → ∀ 𝑧 ∈ ( 𝒫 𝑠 ∩ Fin ) ( 𝑓 ‘ 𝑧 ) ⊆ 𝑠 )
60 eleq1 ⊢ ( 𝑡 = 𝑠 → ( 𝑡 ∈ 𝐶 ↔ 𝑠 ∈ 𝐶 ) )
61 pweq ⊢ ( 𝑡 = 𝑠 → 𝒫 𝑡 = 𝒫 𝑠 )
62 61 ineq1d ⊢ ( 𝑡 = 𝑠 → ( 𝒫 𝑡 ∩ Fin ) = ( 𝒫 𝑠 ∩ Fin ) )
63 sseq2 ⊢ ( 𝑡 = 𝑠 → ( ( 𝑓 ‘ 𝑧 ) ⊆ 𝑡 ↔ ( 𝑓 ‘ 𝑧 ) ⊆ 𝑠 ) )
64 62 63 raleqbidv ⊢ ( 𝑡 = 𝑠 → ( ∀ 𝑧 ∈ ( 𝒫 𝑡 ∩ Fin ) ( 𝑓 ‘ 𝑧 ) ⊆ 𝑡 ↔ ∀ 𝑧 ∈ ( 𝒫 𝑠 ∩ Fin ) ( 𝑓 ‘ 𝑧 ) ⊆ 𝑠 ) )
65 60 64 bibi12d ⊢ ( 𝑡 = 𝑠 → ( ( 𝑡 ∈ 𝐶 ↔ ∀ 𝑧 ∈ ( 𝒫 𝑡 ∩ Fin ) ( 𝑓 ‘ 𝑧 ) ⊆ 𝑡 ) ↔ ( 𝑠 ∈ 𝐶 ↔ ∀ 𝑧 ∈ ( 𝒫 𝑠 ∩ Fin ) ( 𝑓 ‘ 𝑧 ) ⊆ 𝑠 ) ) )
66 37 ad2antrr ⊢ ( ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ( 𝑓 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ∧ ∀ 𝑡 ∈ 𝒫 𝑋 ( 𝑡 ∈ 𝐶 ↔ ∀ 𝑧 ∈ ( 𝒫 𝑡 ∩ Fin ) ( 𝑓 ‘ 𝑧 ) ⊆ 𝑡 ) ) ) ∧ 𝑠 ∈ 𝒫 𝑋 ) ∧ ∀ 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) ( 𝐹 ‘ 𝑦 ) ⊆ 𝑠 ) → ∀ 𝑡 ∈ 𝒫 𝑋 ( 𝑡 ∈ 𝐶 ↔ ∀ 𝑧 ∈ ( 𝒫 𝑡 ∩ Fin ) ( 𝑓 ‘ 𝑧 ) ⊆ 𝑡 ) )
67 simplr ⊢ ( ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ( 𝑓 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ∧ ∀ 𝑡 ∈ 𝒫 𝑋 ( 𝑡 ∈ 𝐶 ↔ ∀ 𝑧 ∈ ( 𝒫 𝑡 ∩ Fin ) ( 𝑓 ‘ 𝑧 ) ⊆ 𝑡 ) ) ) ∧ 𝑠 ∈ 𝒫 𝑋 ) ∧ ∀ 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) ( 𝐹 ‘ 𝑦 ) ⊆ 𝑠 ) → 𝑠 ∈ 𝒫 𝑋 )
68 65 66 67 rspcdva ⊢ ( ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ( 𝑓 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ∧ ∀ 𝑡 ∈ 𝒫 𝑋 ( 𝑡 ∈ 𝐶 ↔ ∀ 𝑧 ∈ ( 𝒫 𝑡 ∩ Fin ) ( 𝑓 ‘ 𝑧 ) ⊆ 𝑡 ) ) ) ∧ 𝑠 ∈ 𝒫 𝑋 ) ∧ ∀ 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) ( 𝐹 ‘ 𝑦 ) ⊆ 𝑠 ) → ( 𝑠 ∈ 𝐶 ↔ ∀ 𝑧 ∈ ( 𝒫 𝑠 ∩ Fin ) ( 𝑓 ‘ 𝑧 ) ⊆ 𝑠 ) )
69 59 68 mpbird ⊢ ( ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ( 𝑓 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ∧ ∀ 𝑡 ∈ 𝒫 𝑋 ( 𝑡 ∈ 𝐶 ↔ ∀ 𝑧 ∈ ( 𝒫 𝑡 ∩ Fin ) ( 𝑓 ‘ 𝑧 ) ⊆ 𝑡 ) ) ) ∧ 𝑠 ∈ 𝒫 𝑋 ) ∧ ∀ 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) ( 𝐹 ‘ 𝑦 ) ⊆ 𝑠 ) → 𝑠 ∈ 𝐶 )
70 21 69 impbida ⊢ ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ( 𝑓 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ∧ ∀ 𝑡 ∈ 𝒫 𝑋 ( 𝑡 ∈ 𝐶 ↔ ∀ 𝑧 ∈ ( 𝒫 𝑡 ∩ Fin ) ( 𝑓 ‘ 𝑧 ) ⊆ 𝑡 ) ) ) ∧ 𝑠 ∈ 𝒫 𝑋 ) → ( 𝑠 ∈ 𝐶 ↔ ∀ 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) ( 𝐹 ‘ 𝑦 ) ⊆ 𝑠 ) )
71 70 ralrimiva ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ( 𝑓 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ∧ ∀ 𝑡 ∈ 𝒫 𝑋 ( 𝑡 ∈ 𝐶 ↔ ∀ 𝑧 ∈ ( 𝒫 𝑡 ∩ Fin ) ( 𝑓 ‘ 𝑧 ) ⊆ 𝑡 ) ) ) → ∀ 𝑠 ∈ 𝒫 𝑋 ( 𝑠 ∈ 𝐶 ↔ ∀ 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) ( 𝐹 ‘ 𝑦 ) ⊆ 𝑠 ) )
72 71 ex ⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → ( ( 𝑓 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ∧ ∀ 𝑡 ∈ 𝒫 𝑋 ( 𝑡 ∈ 𝐶 ↔ ∀ 𝑧 ∈ ( 𝒫 𝑡 ∩ Fin ) ( 𝑓 ‘ 𝑧 ) ⊆ 𝑡 ) ) → ∀ 𝑠 ∈ 𝒫 𝑋 ( 𝑠 ∈ 𝐶 ↔ ∀ 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) ( 𝐹 ‘ 𝑦 ) ⊆ 𝑠 ) ) )
73 72 exlimdv ⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → ( ∃ 𝑓 ( 𝑓 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ∧ ∀ 𝑡 ∈ 𝒫 𝑋 ( 𝑡 ∈ 𝐶 ↔ ∀ 𝑧 ∈ ( 𝒫 𝑡 ∩ Fin ) ( 𝑓 ‘ 𝑧 ) ⊆ 𝑡 ) ) → ∀ 𝑠 ∈ 𝒫 𝑋 ( 𝑠 ∈ 𝐶 ↔ ∀ 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) ( 𝐹 ‘ 𝑦 ) ⊆ 𝑠 ) ) )
74 1 mrcf ⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → 𝐹 : 𝒫 𝑋 ⟶ 𝐶 )
75 74 39 fssd ⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → 𝐹 : 𝒫 𝑋 ⟶ 𝒫 𝑋 )
76 1 fvexi ⊢ 𝐹 ∈ V
77 feq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ↔ 𝐹 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ) )
78 fveq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑧 ) )
79 78 sseq1d ⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 ‘ 𝑧 ) ⊆ 𝑡 ↔ ( 𝐹 ‘ 𝑧 ) ⊆ 𝑡 ) )
80 79 ralbidv ⊢ ( 𝑓 = 𝐹 → ( ∀ 𝑧 ∈ ( 𝒫 𝑡 ∩ Fin ) ( 𝑓 ‘ 𝑧 ) ⊆ 𝑡 ↔ ∀ 𝑧 ∈ ( 𝒫 𝑡 ∩ Fin ) ( 𝐹 ‘ 𝑧 ) ⊆ 𝑡 ) )
81 fveq2 ⊢ ( 𝑧 = 𝑦 → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑦 ) )
82 81 sseq1d ⊢ ( 𝑧 = 𝑦 → ( ( 𝐹 ‘ 𝑧 ) ⊆ 𝑡 ↔ ( 𝐹 ‘ 𝑦 ) ⊆ 𝑡 ) )
83 82 cbvralvw ⊢ ( ∀ 𝑧 ∈ ( 𝒫 𝑡 ∩ Fin ) ( 𝐹 ‘ 𝑧 ) ⊆ 𝑡 ↔ ∀ 𝑦 ∈ ( 𝒫 𝑡 ∩ Fin ) ( 𝐹 ‘ 𝑦 ) ⊆ 𝑡 )
84 80 83 syl6bb ⊢ ( 𝑓 = 𝐹 → ( ∀ 𝑧 ∈ ( 𝒫 𝑡 ∩ Fin ) ( 𝑓 ‘ 𝑧 ) ⊆ 𝑡 ↔ ∀ 𝑦 ∈ ( 𝒫 𝑡 ∩ Fin ) ( 𝐹 ‘ 𝑦 ) ⊆ 𝑡 ) )
85 84 bibi2d ⊢ ( 𝑓 = 𝐹 → ( ( 𝑡 ∈ 𝐶 ↔ ∀ 𝑧 ∈ ( 𝒫 𝑡 ∩ Fin ) ( 𝑓 ‘ 𝑧 ) ⊆ 𝑡 ) ↔ ( 𝑡 ∈ 𝐶 ↔ ∀ 𝑦 ∈ ( 𝒫 𝑡 ∩ Fin ) ( 𝐹 ‘ 𝑦 ) ⊆ 𝑡 ) ) )
86 85 ralbidv ⊢ ( 𝑓 = 𝐹 → ( ∀ 𝑡 ∈ 𝒫 𝑋 ( 𝑡 ∈ 𝐶 ↔ ∀ 𝑧 ∈ ( 𝒫 𝑡 ∩ Fin ) ( 𝑓 ‘ 𝑧 ) ⊆ 𝑡 ) ↔ ∀ 𝑡 ∈ 𝒫 𝑋 ( 𝑡 ∈ 𝐶 ↔ ∀ 𝑦 ∈ ( 𝒫 𝑡 ∩ Fin ) ( 𝐹 ‘ 𝑦 ) ⊆ 𝑡 ) ) )
87 sseq2 ⊢ ( 𝑡 = 𝑠 → ( ( 𝐹 ‘ 𝑦 ) ⊆ 𝑡 ↔ ( 𝐹 ‘ 𝑦 ) ⊆ 𝑠 ) )
88 62 87 raleqbidv ⊢ ( 𝑡 = 𝑠 → ( ∀ 𝑦 ∈ ( 𝒫 𝑡 ∩ Fin ) ( 𝐹 ‘ 𝑦 ) ⊆ 𝑡 ↔ ∀ 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) ( 𝐹 ‘ 𝑦 ) ⊆ 𝑠 ) )
89 60 88 bibi12d ⊢ ( 𝑡 = 𝑠 → ( ( 𝑡 ∈ 𝐶 ↔ ∀ 𝑦 ∈ ( 𝒫 𝑡 ∩ Fin ) ( 𝐹 ‘ 𝑦 ) ⊆ 𝑡 ) ↔ ( 𝑠 ∈ 𝐶 ↔ ∀ 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) ( 𝐹 ‘ 𝑦 ) ⊆ 𝑠 ) ) )
90 89 cbvralvw ⊢ ( ∀ 𝑡 ∈ 𝒫 𝑋 ( 𝑡 ∈ 𝐶 ↔ ∀ 𝑦 ∈ ( 𝒫 𝑡 ∩ Fin ) ( 𝐹 ‘ 𝑦 ) ⊆ 𝑡 ) ↔ ∀ 𝑠 ∈ 𝒫 𝑋 ( 𝑠 ∈ 𝐶 ↔ ∀ 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) ( 𝐹 ‘ 𝑦 ) ⊆ 𝑠 ) )
91 86 90 syl6bb ⊢ ( 𝑓 = 𝐹 → ( ∀ 𝑡 ∈ 𝒫 𝑋 ( 𝑡 ∈ 𝐶 ↔ ∀ 𝑧 ∈ ( 𝒫 𝑡 ∩ Fin ) ( 𝑓 ‘ 𝑧 ) ⊆ 𝑡 ) ↔ ∀ 𝑠 ∈ 𝒫 𝑋 ( 𝑠 ∈ 𝐶 ↔ ∀ 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) ( 𝐹 ‘ 𝑦 ) ⊆ 𝑠 ) ) )
92 77 91 anbi12d ⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ∧ ∀ 𝑡 ∈ 𝒫 𝑋 ( 𝑡 ∈ 𝐶 ↔ ∀ 𝑧 ∈ ( 𝒫 𝑡 ∩ Fin ) ( 𝑓 ‘ 𝑧 ) ⊆ 𝑡 ) ) ↔ ( 𝐹 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ∧ ∀ 𝑠 ∈ 𝒫 𝑋 ( 𝑠 ∈ 𝐶 ↔ ∀ 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) ( 𝐹 ‘ 𝑦 ) ⊆ 𝑠 ) ) ) )
93 76 92 spcev ⊢ ( ( 𝐹 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ∧ ∀ 𝑠 ∈ 𝒫 𝑋 ( 𝑠 ∈ 𝐶 ↔ ∀ 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) ( 𝐹 ‘ 𝑦 ) ⊆ 𝑠 ) ) → ∃ 𝑓 ( 𝑓 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ∧ ∀ 𝑡 ∈ 𝒫 𝑋 ( 𝑡 ∈ 𝐶 ↔ ∀ 𝑧 ∈ ( 𝒫 𝑡 ∩ Fin ) ( 𝑓 ‘ 𝑧 ) ⊆ 𝑡 ) ) )
94 75 93 sylan ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝒫 𝑋 ( 𝑠 ∈ 𝐶 ↔ ∀ 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) ( 𝐹 ‘ 𝑦 ) ⊆ 𝑠 ) ) → ∃ 𝑓 ( 𝑓 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ∧ ∀ 𝑡 ∈ 𝒫 𝑋 ( 𝑡 ∈ 𝐶 ↔ ∀ 𝑧 ∈ ( 𝒫 𝑡 ∩ Fin ) ( 𝑓 ‘ 𝑧 ) ⊆ 𝑡 ) ) )
95 94 ex ⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → ( ∀ 𝑠 ∈ 𝒫 𝑋 ( 𝑠 ∈ 𝐶 ↔ ∀ 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) ( 𝐹 ‘ 𝑦 ) ⊆ 𝑠 ) → ∃ 𝑓 ( 𝑓 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ∧ ∀ 𝑡 ∈ 𝒫 𝑋 ( 𝑡 ∈ 𝐶 ↔ ∀ 𝑧 ∈ ( 𝒫 𝑡 ∩ Fin ) ( 𝑓 ‘ 𝑧 ) ⊆ 𝑡 ) ) ) )
96 73 95 impbid ⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → ( ∃ 𝑓 ( 𝑓 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ∧ ∀ 𝑡 ∈ 𝒫 𝑋 ( 𝑡 ∈ 𝐶 ↔ ∀ 𝑧 ∈ ( 𝒫 𝑡 ∩ Fin ) ( 𝑓 ‘ 𝑧 ) ⊆ 𝑡 ) ) ↔ ∀ 𝑠 ∈ 𝒫 𝑋 ( 𝑠 ∈ 𝐶 ↔ ∀ 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) ( 𝐹 ‘ 𝑦 ) ⊆ 𝑠 ) ) )
97 12 96 syl5bb ⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → ( ∃ 𝑓 ( 𝑓 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ∧ ∀ 𝑡 ∈ 𝒫 𝑋 ( 𝑡 ∈ 𝐶 ↔ ∪ ( 𝑓 “ ( 𝒫 𝑡 ∩ Fin ) ) ⊆ 𝑡 ) ) ↔ ∀ 𝑠 ∈ 𝒫 𝑋 ( 𝑠 ∈ 𝐶 ↔ ∀ 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) ( 𝐹 ‘ 𝑦 ) ⊆ 𝑠 ) ) )
98 97 pm5.32i ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∃ 𝑓 ( 𝑓 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ∧ ∀ 𝑡 ∈ 𝒫 𝑋 ( 𝑡 ∈ 𝐶 ↔ ∪ ( 𝑓 “ ( 𝒫 𝑡 ∩ Fin ) ) ⊆ 𝑡 ) ) ) ↔ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝒫 𝑋 ( 𝑠 ∈ 𝐶 ↔ ∀ 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) ( 𝐹 ‘ 𝑦 ) ⊆ 𝑠 ) ) )
99 2 98 bitri ⊢ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ↔ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝒫 𝑋 ( 𝑠 ∈ 𝐶 ↔ ∀ 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) ( 𝐹 ‘ 𝑦 ) ⊆ 𝑠 ) ) )