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