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 bitrdi ( 𝑓 = 𝐹 → ( ∀ 𝑧 ∈ ( 𝒫 𝑡 ∩ 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 bitrdi ( 𝑓 = 𝐹 → ( ∀ 𝑡 ∈ 𝒫 𝑋 ( 𝑡𝐶 ↔ ∀ 𝑧 ∈ ( 𝒫 𝑡 ∩ 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 ) ( 𝐹𝑦 ) ⊆ 𝑠 ) ) )