Step |
Hyp |
Ref |
Expression |
1 |
|
acsficld.1 |
⊢ ( 𝜑 → 𝐴 ∈ ( ACS ‘ 𝑋 ) ) |
2 |
|
acsficld.2 |
⊢ 𝑁 = ( mrCls ‘ 𝐴 ) |
3 |
|
acsficld.3 |
⊢ ( 𝜑 → 𝑆 ⊆ 𝑋 ) |
4 |
1 2 3
|
acsficld |
⊢ ( 𝜑 → ( 𝑁 ‘ 𝑆 ) = ∪ ( 𝑁 “ ( 𝒫 𝑆 ∩ Fin ) ) ) |
5 |
4
|
eleq2d |
⊢ ( 𝜑 → ( 𝑌 ∈ ( 𝑁 ‘ 𝑆 ) ↔ 𝑌 ∈ ∪ ( 𝑁 “ ( 𝒫 𝑆 ∩ Fin ) ) ) ) |
6 |
1
|
acsmred |
⊢ ( 𝜑 → 𝐴 ∈ ( Moore ‘ 𝑋 ) ) |
7 |
|
funmpt |
⊢ Fun ( 𝑧 ∈ 𝒫 𝑋 ↦ ∩ { 𝑤 ∈ 𝐴 ∣ 𝑧 ⊆ 𝑤 } ) |
8 |
2
|
mrcfval |
⊢ ( 𝐴 ∈ ( Moore ‘ 𝑋 ) → 𝑁 = ( 𝑧 ∈ 𝒫 𝑋 ↦ ∩ { 𝑤 ∈ 𝐴 ∣ 𝑧 ⊆ 𝑤 } ) ) |
9 |
8
|
funeqd |
⊢ ( 𝐴 ∈ ( Moore ‘ 𝑋 ) → ( Fun 𝑁 ↔ Fun ( 𝑧 ∈ 𝒫 𝑋 ↦ ∩ { 𝑤 ∈ 𝐴 ∣ 𝑧 ⊆ 𝑤 } ) ) ) |
10 |
7 9
|
mpbiri |
⊢ ( 𝐴 ∈ ( Moore ‘ 𝑋 ) → Fun 𝑁 ) |
11 |
|
eluniima |
⊢ ( Fun 𝑁 → ( 𝑌 ∈ ∪ ( 𝑁 “ ( 𝒫 𝑆 ∩ Fin ) ) ↔ ∃ 𝑥 ∈ ( 𝒫 𝑆 ∩ Fin ) 𝑌 ∈ ( 𝑁 ‘ 𝑥 ) ) ) |
12 |
6 10 11
|
3syl |
⊢ ( 𝜑 → ( 𝑌 ∈ ∪ ( 𝑁 “ ( 𝒫 𝑆 ∩ Fin ) ) ↔ ∃ 𝑥 ∈ ( 𝒫 𝑆 ∩ Fin ) 𝑌 ∈ ( 𝑁 ‘ 𝑥 ) ) ) |
13 |
5 12
|
bitrd |
⊢ ( 𝜑 → ( 𝑌 ∈ ( 𝑁 ‘ 𝑆 ) ↔ ∃ 𝑥 ∈ ( 𝒫 𝑆 ∩ Fin ) 𝑌 ∈ ( 𝑁 ‘ 𝑥 ) ) ) |