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 ) ) ) )