This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 → ( 𝐹 ‘ ∪ 𝑡 ) = ∪ ( 𝐹 “ 𝑡 ) ) ) )