Metamath Proof Explorer


Theorem isacs4lem

Description: In a closure system in which directed unions of closed sets are closed, closure commutes with directed unions. (Contributed by Stefan O'Rear, 2-Apr-2015)

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

Proof

Step Hyp Ref Expression
1 acsdrscl.f 𝐹 = ( mrCls ‘ 𝐶 )
2 simpll ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝒫 𝐶 ( ( toInc ‘ 𝑠 ) ∈ Dirset → 𝑠𝐶 ) ) ∧ ( 𝑡 ∈ 𝒫 𝒫 𝑋 ∧ ( toInc ‘ 𝑡 ) ∈ Dirset ) ) → 𝐶 ∈ ( Moore ‘ 𝑋 ) )
3 elpwi ( 𝑡 ∈ 𝒫 𝒫 𝑋𝑡 ⊆ 𝒫 𝑋 )
4 3 ad2antrl ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝒫 𝐶 ( ( toInc ‘ 𝑠 ) ∈ Dirset → 𝑠𝐶 ) ) ∧ ( 𝑡 ∈ 𝒫 𝒫 𝑋 ∧ ( toInc ‘ 𝑡 ) ∈ Dirset ) ) → 𝑡 ⊆ 𝒫 𝑋 )
5 1 mrcuni ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑡 ⊆ 𝒫 𝑋 ) → ( 𝐹 𝑡 ) = ( 𝐹 ( 𝐹𝑡 ) ) )
6 2 4 5 syl2anc ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝒫 𝐶 ( ( toInc ‘ 𝑠 ) ∈ Dirset → 𝑠𝐶 ) ) ∧ ( 𝑡 ∈ 𝒫 𝒫 𝑋 ∧ ( toInc ‘ 𝑡 ) ∈ Dirset ) ) → ( 𝐹 𝑡 ) = ( 𝐹 ( 𝐹𝑡 ) ) )
7 1 mrcf ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → 𝐹 : 𝒫 𝑋𝐶 )
8 7 ffnd ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → 𝐹 Fn 𝒫 𝑋 )
9 8 adantr ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ( 𝑡 ∈ 𝒫 𝒫 𝑋 ∧ ( toInc ‘ 𝑡 ) ∈ Dirset ) ) → 𝐹 Fn 𝒫 𝑋 )
10 simpll ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ( 𝑡 ∈ 𝒫 𝒫 𝑋 ∧ ( toInc ‘ 𝑡 ) ∈ Dirset ) ) ∧ ( 𝑥𝑦𝑦𝑋 ) ) → 𝐶 ∈ ( Moore ‘ 𝑋 ) )
11 simprl ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ( 𝑡 ∈ 𝒫 𝒫 𝑋 ∧ ( toInc ‘ 𝑡 ) ∈ Dirset ) ) ∧ ( 𝑥𝑦𝑦𝑋 ) ) → 𝑥𝑦 )
12 simprr ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ( 𝑡 ∈ 𝒫 𝒫 𝑋 ∧ ( toInc ‘ 𝑡 ) ∈ Dirset ) ) ∧ ( 𝑥𝑦𝑦𝑋 ) ) → 𝑦𝑋 )
13 10 1 11 12 mrcssd ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ( 𝑡 ∈ 𝒫 𝒫 𝑋 ∧ ( toInc ‘ 𝑡 ) ∈ Dirset ) ) ∧ ( 𝑥𝑦𝑦𝑋 ) ) → ( 𝐹𝑥 ) ⊆ ( 𝐹𝑦 ) )
14 simprr ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ( 𝑡 ∈ 𝒫 𝒫 𝑋 ∧ ( toInc ‘ 𝑡 ) ∈ Dirset ) ) → ( toInc ‘ 𝑡 ) ∈ Dirset )
15 3 ad2antrl ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ( 𝑡 ∈ 𝒫 𝒫 𝑋 ∧ ( toInc ‘ 𝑡 ) ∈ Dirset ) ) → 𝑡 ⊆ 𝒫 𝑋 )
16 1 fvexi 𝐹 ∈ V
17 16 imaex ( 𝐹𝑡 ) ∈ V
18 17 a1i ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ( 𝑡 ∈ 𝒫 𝒫 𝑋 ∧ ( toInc ‘ 𝑡 ) ∈ Dirset ) ) → ( 𝐹𝑡 ) ∈ V )
19 9 13 14 15 18 ipodrsima ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ( 𝑡 ∈ 𝒫 𝒫 𝑋 ∧ ( toInc ‘ 𝑡 ) ∈ Dirset ) ) → ( toInc ‘ ( 𝐹𝑡 ) ) ∈ Dirset )
20 19 adantlr ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝒫 𝐶 ( ( toInc ‘ 𝑠 ) ∈ Dirset → 𝑠𝐶 ) ) ∧ ( 𝑡 ∈ 𝒫 𝒫 𝑋 ∧ ( toInc ‘ 𝑡 ) ∈ Dirset ) ) → ( toInc ‘ ( 𝐹𝑡 ) ) ∈ Dirset )
21 fveq2 ( 𝑠 = ( 𝐹𝑡 ) → ( toInc ‘ 𝑠 ) = ( toInc ‘ ( 𝐹𝑡 ) ) )
22 21 eleq1d ( 𝑠 = ( 𝐹𝑡 ) → ( ( toInc ‘ 𝑠 ) ∈ Dirset ↔ ( toInc ‘ ( 𝐹𝑡 ) ) ∈ Dirset ) )
23 unieq ( 𝑠 = ( 𝐹𝑡 ) → 𝑠 = ( 𝐹𝑡 ) )
24 23 eleq1d ( 𝑠 = ( 𝐹𝑡 ) → ( 𝑠𝐶 ( 𝐹𝑡 ) ∈ 𝐶 ) )
25 22 24 imbi12d ( 𝑠 = ( 𝐹𝑡 ) → ( ( ( toInc ‘ 𝑠 ) ∈ Dirset → 𝑠𝐶 ) ↔ ( ( toInc ‘ ( 𝐹𝑡 ) ) ∈ Dirset → ( 𝐹𝑡 ) ∈ 𝐶 ) ) )
26 simplr ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝒫 𝐶 ( ( toInc ‘ 𝑠 ) ∈ Dirset → 𝑠𝐶 ) ) ∧ ( 𝑡 ∈ 𝒫 𝒫 𝑋 ∧ ( toInc ‘ 𝑡 ) ∈ Dirset ) ) → ∀ 𝑠 ∈ 𝒫 𝐶 ( ( toInc ‘ 𝑠 ) ∈ Dirset → 𝑠𝐶 ) )
27 imassrn ( 𝐹𝑡 ) ⊆ ran 𝐹
28 7 frnd ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → ran 𝐹𝐶 )
29 27 28 sstrid ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → ( 𝐹𝑡 ) ⊆ 𝐶 )
30 17 elpw ( ( 𝐹𝑡 ) ∈ 𝒫 𝐶 ↔ ( 𝐹𝑡 ) ⊆ 𝐶 )
31 29 30 sylibr ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → ( 𝐹𝑡 ) ∈ 𝒫 𝐶 )
32 31 ad2antrr ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝒫 𝐶 ( ( toInc ‘ 𝑠 ) ∈ Dirset → 𝑠𝐶 ) ) ∧ ( 𝑡 ∈ 𝒫 𝒫 𝑋 ∧ ( toInc ‘ 𝑡 ) ∈ Dirset ) ) → ( 𝐹𝑡 ) ∈ 𝒫 𝐶 )
33 25 26 32 rspcdva ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝒫 𝐶 ( ( toInc ‘ 𝑠 ) ∈ Dirset → 𝑠𝐶 ) ) ∧ ( 𝑡 ∈ 𝒫 𝒫 𝑋 ∧ ( toInc ‘ 𝑡 ) ∈ Dirset ) ) → ( ( toInc ‘ ( 𝐹𝑡 ) ) ∈ Dirset → ( 𝐹𝑡 ) ∈ 𝐶 ) )
34 20 33 mpd ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝒫 𝐶 ( ( toInc ‘ 𝑠 ) ∈ Dirset → 𝑠𝐶 ) ) ∧ ( 𝑡 ∈ 𝒫 𝒫 𝑋 ∧ ( toInc ‘ 𝑡 ) ∈ Dirset ) ) → ( 𝐹𝑡 ) ∈ 𝐶 )
35 1 mrcid ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ( 𝐹𝑡 ) ∈ 𝐶 ) → ( 𝐹 ( 𝐹𝑡 ) ) = ( 𝐹𝑡 ) )
36 2 34 35 syl2anc ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝒫 𝐶 ( ( toInc ‘ 𝑠 ) ∈ Dirset → 𝑠𝐶 ) ) ∧ ( 𝑡 ∈ 𝒫 𝒫 𝑋 ∧ ( toInc ‘ 𝑡 ) ∈ Dirset ) ) → ( 𝐹 ( 𝐹𝑡 ) ) = ( 𝐹𝑡 ) )
37 6 36 eqtrd ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝒫 𝐶 ( ( toInc ‘ 𝑠 ) ∈ Dirset → 𝑠𝐶 ) ) ∧ ( 𝑡 ∈ 𝒫 𝒫 𝑋 ∧ ( toInc ‘ 𝑡 ) ∈ Dirset ) ) → ( 𝐹 𝑡 ) = ( 𝐹𝑡 ) )
38 37 exp32 ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝒫 𝐶 ( ( toInc ‘ 𝑠 ) ∈ Dirset → 𝑠𝐶 ) ) → ( 𝑡 ∈ 𝒫 𝒫 𝑋 → ( ( toInc ‘ 𝑡 ) ∈ Dirset → ( 𝐹 𝑡 ) = ( 𝐹𝑡 ) ) ) )
39 38 ralrimiv ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝒫 𝐶 ( ( toInc ‘ 𝑠 ) ∈ Dirset → 𝑠𝐶 ) ) → ∀ 𝑡 ∈ 𝒫 𝒫 𝑋 ( ( toInc ‘ 𝑡 ) ∈ Dirset → ( 𝐹 𝑡 ) = ( 𝐹𝑡 ) ) )
40 39 ex ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → ( ∀ 𝑠 ∈ 𝒫 𝐶 ( ( toInc ‘ 𝑠 ) ∈ Dirset → 𝑠𝐶 ) → ∀ 𝑡 ∈ 𝒫 𝒫 𝑋 ( ( toInc ‘ 𝑡 ) ∈ Dirset → ( 𝐹 𝑡 ) = ( 𝐹𝑡 ) ) ) )
41 40 imdistani ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝒫 𝐶 ( ( toInc ‘ 𝑠 ) ∈ Dirset → 𝑠𝐶 ) ) → ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑡 ∈ 𝒫 𝒫 𝑋 ( ( toInc ‘ 𝑡 ) ∈ Dirset → ( 𝐹 𝑡 ) = ( 𝐹𝑡 ) ) ) )