Metamath Proof Explorer


Theorem isacs5lem

Description: If closure commutes with directed unions, then the closure of a set is the closure of its finite subsets. (Contributed by Stefan O'Rear, 2-Apr-2015)

Ref Expression
Hypothesis acsdrscl.f 𝐹 = ( mrCls ‘ 𝐶 )
Assertion isacs5lem ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑡 ∈ 𝒫 𝒫 𝑋 ( ( toInc ‘ 𝑡 ) ∈ Dirset → ( 𝐹 𝑡 ) = ( 𝐹𝑡 ) ) ) → ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝒫 𝑋 ( 𝐹𝑠 ) = ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) ) )

Proof

Step Hyp Ref Expression
1 acsdrscl.f 𝐹 = ( mrCls ‘ 𝐶 )
2 unifpw ( 𝒫 𝑠 ∩ Fin ) = 𝑠
3 2 fveq2i ( 𝐹 ( 𝒫 𝑠 ∩ Fin ) ) = ( 𝐹𝑠 )
4 vex 𝑠 ∈ V
5 fpwipodrs ( 𝑠 ∈ V → ( toInc ‘ ( 𝒫 𝑠 ∩ Fin ) ) ∈ Dirset )
6 4 5 mp1i ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑡 ∈ 𝒫 𝒫 𝑋 ( ( toInc ‘ 𝑡 ) ∈ Dirset → ( 𝐹 𝑡 ) = ( 𝐹𝑡 ) ) ) ∧ 𝑠 ∈ 𝒫 𝑋 ) → ( toInc ‘ ( 𝒫 𝑠 ∩ Fin ) ) ∈ Dirset )
7 fveq2 ( 𝑡 = ( 𝒫 𝑠 ∩ Fin ) → ( toInc ‘ 𝑡 ) = ( toInc ‘ ( 𝒫 𝑠 ∩ Fin ) ) )
8 7 eleq1d ( 𝑡 = ( 𝒫 𝑠 ∩ Fin ) → ( ( toInc ‘ 𝑡 ) ∈ Dirset ↔ ( toInc ‘ ( 𝒫 𝑠 ∩ Fin ) ) ∈ Dirset ) )
9 unieq ( 𝑡 = ( 𝒫 𝑠 ∩ Fin ) → 𝑡 = ( 𝒫 𝑠 ∩ Fin ) )
10 9 fveq2d ( 𝑡 = ( 𝒫 𝑠 ∩ Fin ) → ( 𝐹 𝑡 ) = ( 𝐹 ( 𝒫 𝑠 ∩ Fin ) ) )
11 imaeq2 ( 𝑡 = ( 𝒫 𝑠 ∩ Fin ) → ( 𝐹𝑡 ) = ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) )
12 11 unieqd ( 𝑡 = ( 𝒫 𝑠 ∩ Fin ) → ( 𝐹𝑡 ) = ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) )
13 10 12 eqeq12d ( 𝑡 = ( 𝒫 𝑠 ∩ Fin ) → ( ( 𝐹 𝑡 ) = ( 𝐹𝑡 ) ↔ ( 𝐹 ( 𝒫 𝑠 ∩ Fin ) ) = ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) ) )
14 8 13 imbi12d ( 𝑡 = ( 𝒫 𝑠 ∩ Fin ) → ( ( ( toInc ‘ 𝑡 ) ∈ Dirset → ( 𝐹 𝑡 ) = ( 𝐹𝑡 ) ) ↔ ( ( toInc ‘ ( 𝒫 𝑠 ∩ Fin ) ) ∈ Dirset → ( 𝐹 ( 𝒫 𝑠 ∩ Fin ) ) = ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) ) ) )
15 simplr ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑡 ∈ 𝒫 𝒫 𝑋 ( ( toInc ‘ 𝑡 ) ∈ Dirset → ( 𝐹 𝑡 ) = ( 𝐹𝑡 ) ) ) ∧ 𝑠 ∈ 𝒫 𝑋 ) → ∀ 𝑡 ∈ 𝒫 𝒫 𝑋 ( ( toInc ‘ 𝑡 ) ∈ Dirset → ( 𝐹 𝑡 ) = ( 𝐹𝑡 ) ) )
16 inss1 ( 𝒫 𝑠 ∩ Fin ) ⊆ 𝒫 𝑠
17 elpwi ( 𝑠 ∈ 𝒫 𝑋𝑠𝑋 )
18 17 sspwd ( 𝑠 ∈ 𝒫 𝑋 → 𝒫 𝑠 ⊆ 𝒫 𝑋 )
19 18 adantl ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑠 ∈ 𝒫 𝑋 ) → 𝒫 𝑠 ⊆ 𝒫 𝑋 )
20 16 19 sstrid ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑠 ∈ 𝒫 𝑋 ) → ( 𝒫 𝑠 ∩ Fin ) ⊆ 𝒫 𝑋 )
21 vpwex 𝒫 𝑠 ∈ V
22 21 inex1 ( 𝒫 𝑠 ∩ Fin ) ∈ V
23 22 elpw ( ( 𝒫 𝑠 ∩ Fin ) ∈ 𝒫 𝒫 𝑋 ↔ ( 𝒫 𝑠 ∩ Fin ) ⊆ 𝒫 𝑋 )
24 20 23 sylibr ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑠 ∈ 𝒫 𝑋 ) → ( 𝒫 𝑠 ∩ Fin ) ∈ 𝒫 𝒫 𝑋 )
25 24 adantlr ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑡 ∈ 𝒫 𝒫 𝑋 ( ( toInc ‘ 𝑡 ) ∈ Dirset → ( 𝐹 𝑡 ) = ( 𝐹𝑡 ) ) ) ∧ 𝑠 ∈ 𝒫 𝑋 ) → ( 𝒫 𝑠 ∩ Fin ) ∈ 𝒫 𝒫 𝑋 )
26 14 15 25 rspcdva ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑡 ∈ 𝒫 𝒫 𝑋 ( ( toInc ‘ 𝑡 ) ∈ Dirset → ( 𝐹 𝑡 ) = ( 𝐹𝑡 ) ) ) ∧ 𝑠 ∈ 𝒫 𝑋 ) → ( ( toInc ‘ ( 𝒫 𝑠 ∩ Fin ) ) ∈ Dirset → ( 𝐹 ( 𝒫 𝑠 ∩ Fin ) ) = ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) ) )
27 6 26 mpd ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑡 ∈ 𝒫 𝒫 𝑋 ( ( toInc ‘ 𝑡 ) ∈ Dirset → ( 𝐹 𝑡 ) = ( 𝐹𝑡 ) ) ) ∧ 𝑠 ∈ 𝒫 𝑋 ) → ( 𝐹 ( 𝒫 𝑠 ∩ Fin ) ) = ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) )
28 3 27 eqtr3id ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑡 ∈ 𝒫 𝒫 𝑋 ( ( toInc ‘ 𝑡 ) ∈ Dirset → ( 𝐹 𝑡 ) = ( 𝐹𝑡 ) ) ) ∧ 𝑠 ∈ 𝒫 𝑋 ) → ( 𝐹𝑠 ) = ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) )
29 28 ralrimiva ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑡 ∈ 𝒫 𝒫 𝑋 ( ( toInc ‘ 𝑡 ) ∈ Dirset → ( 𝐹 𝑡 ) = ( 𝐹𝑡 ) ) ) → ∀ 𝑠 ∈ 𝒫 𝑋 ( 𝐹𝑠 ) = ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) )
30 29 ex ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → ( ∀ 𝑡 ∈ 𝒫 𝒫 𝑋 ( ( toInc ‘ 𝑡 ) ∈ Dirset → ( 𝐹 𝑡 ) = ( 𝐹𝑡 ) ) → ∀ 𝑠 ∈ 𝒫 𝑋 ( 𝐹𝑠 ) = ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) ) )
31 30 imdistani ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑡 ∈ 𝒫 𝒫 𝑋 ( ( toInc ‘ 𝑡 ) ∈ Dirset → ( 𝐹 𝑡 ) = ( 𝐹𝑡 ) ) ) → ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝒫 𝑋 ( 𝐹𝑠 ) = ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) ) )