Step |
Hyp |
Ref |
Expression |
1 |
|
acsdrscl.f |
⊢ 𝐹 = ( mrCls ‘ 𝐶 ) |
2 |
|
fveq2 |
⊢ ( 𝑠 = 𝑆 → ( 𝐹 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑆 ) ) |
3 |
|
pweq |
⊢ ( 𝑠 = 𝑆 → 𝒫 𝑠 = 𝒫 𝑆 ) |
4 |
3
|
ineq1d |
⊢ ( 𝑠 = 𝑆 → ( 𝒫 𝑠 ∩ Fin ) = ( 𝒫 𝑆 ∩ Fin ) ) |
5 |
4
|
imaeq2d |
⊢ ( 𝑠 = 𝑆 → ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) = ( 𝐹 “ ( 𝒫 𝑆 ∩ Fin ) ) ) |
6 |
5
|
unieqd |
⊢ ( 𝑠 = 𝑆 → ∪ ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) = ∪ ( 𝐹 “ ( 𝒫 𝑆 ∩ Fin ) ) ) |
7 |
2 6
|
eqeq12d |
⊢ ( 𝑠 = 𝑆 → ( ( 𝐹 ‘ 𝑠 ) = ∪ ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) ↔ ( 𝐹 ‘ 𝑆 ) = ∪ ( 𝐹 “ ( 𝒫 𝑆 ∩ Fin ) ) ) ) |
8 |
|
isacs3lem |
⊢ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) → ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝒫 𝐶 ( ( toInc ‘ 𝑠 ) ∈ Dirset → ∪ 𝑠 ∈ 𝐶 ) ) ) |
9 |
1
|
isacs4lem |
⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝒫 𝐶 ( ( toInc ‘ 𝑠 ) ∈ Dirset → ∪ 𝑠 ∈ 𝐶 ) ) → ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑡 ∈ 𝒫 𝒫 𝑋 ( ( toInc ‘ 𝑡 ) ∈ Dirset → ( 𝐹 ‘ ∪ 𝑡 ) = ∪ ( 𝐹 “ 𝑡 ) ) ) ) |
10 |
1
|
isacs5lem |
⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑡 ∈ 𝒫 𝒫 𝑋 ( ( toInc ‘ 𝑡 ) ∈ Dirset → ( 𝐹 ‘ ∪ 𝑡 ) = ∪ ( 𝐹 “ 𝑡 ) ) ) → ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝒫 𝑋 ( 𝐹 ‘ 𝑠 ) = ∪ ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) ) ) |
11 |
8 9 10
|
3syl |
⊢ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) → ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝒫 𝑋 ( 𝐹 ‘ 𝑠 ) = ∪ ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) ) ) |
12 |
11
|
simprd |
⊢ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) → ∀ 𝑠 ∈ 𝒫 𝑋 ( 𝐹 ‘ 𝑠 ) = ∪ ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) ) |
13 |
12
|
adantr |
⊢ ( ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → ∀ 𝑠 ∈ 𝒫 𝑋 ( 𝐹 ‘ 𝑠 ) = ∪ ( 𝐹 “ ( 𝒫 𝑠 ∩ Fin ) ) ) |
14 |
|
elfvdm |
⊢ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) → 𝑋 ∈ dom ACS ) |
15 |
|
elpw2g |
⊢ ( 𝑋 ∈ dom ACS → ( 𝑆 ∈ 𝒫 𝑋 ↔ 𝑆 ⊆ 𝑋 ) ) |
16 |
14 15
|
syl |
⊢ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) → ( 𝑆 ∈ 𝒫 𝑋 ↔ 𝑆 ⊆ 𝑋 ) ) |
17 |
16
|
biimpar |
⊢ ( ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → 𝑆 ∈ 𝒫 𝑋 ) |
18 |
7 13 17
|
rspcdva |
⊢ ( ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → ( 𝐹 ‘ 𝑆 ) = ∪ ( 𝐹 “ ( 𝒫 𝑆 ∩ Fin ) ) ) |