Metamath Proof Explorer

Theorem isacs5

Description: A closure system is algebraic iff the closure of a generating set is the union of the closures of its finite subsets. (Contributed by Stefan O'Rear, 2-Apr-2015)

Ref Expression
Hypothesis acsdrscl.f ⊢ 𝐹 = ( mrCls ‘ 𝐶 )
Assertion isacs5 ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ↔ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝒫 𝑋 ( 𝐹 ‘ 𝑠 ) = ∪ ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) ) )

Proof

Step Hyp Ref Expression
1 acsdrscl.f ⊢ 𝐹 = ( mrCls ‘ 𝐶 )
2 isacs3lem ⊢ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) → ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝒫 𝐶 ( ( toInc ‘ 𝑠 ) ∈ Dirset → ∪ 𝑠 ∈ 𝐶 ) ) )
3 1 isacs4lem ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝒫 𝐶 ( ( toInc ‘ 𝑠 ) ∈ Dirset → ∪ 𝑠 ∈ 𝐶 ) ) → ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑡 ∈ 𝒫 𝒫 𝑋 ( ( toInc ‘ 𝑡 ) ∈ Dirset → ( 𝐹 ‘ ∪ 𝑡 ) = ∪ ( 𝐹 “ 𝑡 ) ) ) )
4 1 isacs5lem ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑡 ∈ 𝒫 𝒫 𝑋 ( ( toInc ‘ 𝑡 ) ∈ Dirset → ( 𝐹 ‘ ∪ 𝑡 ) = ∪ ( 𝐹 “ 𝑡 ) ) ) → ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝒫 𝑋 ( 𝐹 ‘ 𝑠 ) = ∪ ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) ) )
5 2 3 4 3syl ⊢ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) → ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝒫 𝑋 ( 𝐹 ‘ 𝑠 ) = ∪ ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) ) )
6 simpl ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝒫 𝑋 ( 𝐹 ‘ 𝑠 ) = ∪ ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) ) → 𝐶 ∈ ( Moore ‘ 𝑋 ) )
7 elpwi ⊢ ( 𝑠 ∈ 𝒫 𝑋 → 𝑠 ⊆ 𝑋 )
8 1 mrcidb2 ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑠 ⊆ 𝑋 ) → ( 𝑠 ∈ 𝐶 ↔ ( 𝐹 ‘ 𝑠 ) ⊆ 𝑠 ) )
9 7 8 sylan2 ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑠 ∈ 𝒫 𝑋 ) → ( 𝑠 ∈ 𝐶 ↔ ( 𝐹 ‘ 𝑠 ) ⊆ 𝑠 ) )
10 9 adantr ⊢ ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑠 ∈ 𝒫 𝑋 ) ∧ ( 𝐹 ‘ 𝑠 ) = ∪ ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) ) → ( 𝑠 ∈ 𝐶 ↔ ( 𝐹 ‘ 𝑠 ) ⊆ 𝑠 ) )
11 simpr ⊢ ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑠 ∈ 𝒫 𝑋 ) ∧ ( 𝐹 ‘ 𝑠 ) = ∪ ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) ) → ( 𝐹 ‘ 𝑠 ) = ∪ ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) )
12 1 mrcf ⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → 𝐹 : 𝒫 𝑋 ⟶ 𝐶 )
13 ffun ⊢ ( 𝐹 : 𝒫 𝑋 ⟶ 𝐶 → Fun 𝐹 )
14 funiunfv ⊢ ( Fun 𝐹 → ∪ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) ( 𝐹 ‘ 𝑡 ) = ∪ ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) )
15 12 13 14 3syl ⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → ∪ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) ( 𝐹 ‘ 𝑡 ) = ∪ ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) )
16 15 ad2antrr ⊢ ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑠 ∈ 𝒫 𝑋 ) ∧ ( 𝐹 ‘ 𝑠 ) = ∪ ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) ) → ∪ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) ( 𝐹 ‘ 𝑡 ) = ∪ ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) )
17 11 16 eqtr4d ⊢ ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑠 ∈ 𝒫 𝑋 ) ∧ ( 𝐹 ‘ 𝑠 ) = ∪ ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) ) → ( 𝐹 ‘ 𝑠 ) = ∪ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) ( 𝐹 ‘ 𝑡 ) )
18 17 sseq1d ⊢ ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑠 ∈ 𝒫 𝑋 ) ∧ ( 𝐹 ‘ 𝑠 ) = ∪ ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) ) → ( ( 𝐹 ‘ 𝑠 ) ⊆ 𝑠 ↔ ∪ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) ( 𝐹 ‘ 𝑡 ) ⊆ 𝑠 ) )
19 iunss ⊢ ( ∪ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) ( 𝐹 ‘ 𝑡 ) ⊆ 𝑠 ↔ ∀ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) ( 𝐹 ‘ 𝑡 ) ⊆ 𝑠 )
20 18 19 bitrdi ⊢ ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑠 ∈ 𝒫 𝑋 ) ∧ ( 𝐹 ‘ 𝑠 ) = ∪ ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) ) → ( ( 𝐹 ‘ 𝑠 ) ⊆ 𝑠 ↔ ∀ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) ( 𝐹 ‘ 𝑡 ) ⊆ 𝑠 ) )
21 10 20 bitrd ⊢ ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑠 ∈ 𝒫 𝑋 ) ∧ ( 𝐹 ‘ 𝑠 ) = ∪ ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) ) → ( 𝑠 ∈ 𝐶 ↔ ∀ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) ( 𝐹 ‘ 𝑡 ) ⊆ 𝑠 ) )
22 21 ex ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑠 ∈ 𝒫 𝑋 ) → ( ( 𝐹 ‘ 𝑠 ) = ∪ ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) → ( 𝑠 ∈ 𝐶 ↔ ∀ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) ( 𝐹 ‘ 𝑡 ) ⊆ 𝑠 ) ) )
23 22 ralimdva ⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → ( ∀ 𝑠 ∈ 𝒫 𝑋 ( 𝐹 ‘ 𝑠 ) = ∪ ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) → ∀ 𝑠 ∈ 𝒫 𝑋 ( 𝑠 ∈ 𝐶 ↔ ∀ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) ( 𝐹 ‘ 𝑡 ) ⊆ 𝑠 ) ) )
24 23 imp ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝒫 𝑋 ( 𝐹 ‘ 𝑠 ) = ∪ ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) ) → ∀ 𝑠 ∈ 𝒫 𝑋 ( 𝑠 ∈ 𝐶 ↔ ∀ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) ( 𝐹 ‘ 𝑡 ) ⊆ 𝑠 ) )
25 1 isacs2 ⊢ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ↔ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝒫 𝑋 ( 𝑠 ∈ 𝐶 ↔ ∀ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) ( 𝐹 ‘ 𝑡 ) ⊆ 𝑠 ) ) )
26 6 24 25 sylanbrc ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝒫 𝑋 ( 𝐹 ‘ 𝑠 ) = ∪ ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) ) → 𝐶 ∈ ( ACS ‘ 𝑋 ) )
27 5 26 impbii ⊢ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ↔ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝒫 𝑋 ( 𝐹 ‘ 𝑠 ) = ∪ ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) ) )