Step |
Hyp |
Ref |
Expression |
1 |
|
isnacs.f |
⊢ 𝐹 = ( mrCls ‘ 𝐶 ) |
2 |
1
|
isnacs |
⊢ ( 𝐶 ∈ ( NoeACS ‘ 𝑋 ) ↔ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝐶 ∃ 𝑔 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑠 = ( 𝐹 ‘ 𝑔 ) ) ) |
3 |
|
eqcom |
⊢ ( 𝑠 = ( 𝐹 ‘ 𝑔 ) ↔ ( 𝐹 ‘ 𝑔 ) = 𝑠 ) |
4 |
3
|
rexbii |
⊢ ( ∃ 𝑔 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑠 = ( 𝐹 ‘ 𝑔 ) ↔ ∃ 𝑔 ∈ ( 𝒫 𝑋 ∩ Fin ) ( 𝐹 ‘ 𝑔 ) = 𝑠 ) |
5 |
|
acsmre |
⊢ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) → 𝐶 ∈ ( Moore ‘ 𝑋 ) ) |
6 |
1
|
mrcf |
⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → 𝐹 : 𝒫 𝑋 ⟶ 𝐶 ) |
7 |
|
ffn |
⊢ ( 𝐹 : 𝒫 𝑋 ⟶ 𝐶 → 𝐹 Fn 𝒫 𝑋 ) |
8 |
5 6 7
|
3syl |
⊢ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) → 𝐹 Fn 𝒫 𝑋 ) |
9 |
|
inss1 |
⊢ ( 𝒫 𝑋 ∩ Fin ) ⊆ 𝒫 𝑋 |
10 |
|
fvelimab |
⊢ ( ( 𝐹 Fn 𝒫 𝑋 ∧ ( 𝒫 𝑋 ∩ Fin ) ⊆ 𝒫 𝑋 ) → ( 𝑠 ∈ ( 𝐹 “ ( 𝒫 𝑋 ∩ Fin ) ) ↔ ∃ 𝑔 ∈ ( 𝒫 𝑋 ∩ Fin ) ( 𝐹 ‘ 𝑔 ) = 𝑠 ) ) |
11 |
8 9 10
|
sylancl |
⊢ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) → ( 𝑠 ∈ ( 𝐹 “ ( 𝒫 𝑋 ∩ Fin ) ) ↔ ∃ 𝑔 ∈ ( 𝒫 𝑋 ∩ Fin ) ( 𝐹 ‘ 𝑔 ) = 𝑠 ) ) |
12 |
4 11
|
bitr4id |
⊢ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) → ( ∃ 𝑔 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑠 = ( 𝐹 ‘ 𝑔 ) ↔ 𝑠 ∈ ( 𝐹 “ ( 𝒫 𝑋 ∩ Fin ) ) ) ) |
13 |
12
|
ralbidv |
⊢ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) → ( ∀ 𝑠 ∈ 𝐶 ∃ 𝑔 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑠 = ( 𝐹 ‘ 𝑔 ) ↔ ∀ 𝑠 ∈ 𝐶 𝑠 ∈ ( 𝐹 “ ( 𝒫 𝑋 ∩ Fin ) ) ) ) |
14 |
|
dfss3 |
⊢ ( 𝐶 ⊆ ( 𝐹 “ ( 𝒫 𝑋 ∩ Fin ) ) ↔ ∀ 𝑠 ∈ 𝐶 𝑠 ∈ ( 𝐹 “ ( 𝒫 𝑋 ∩ Fin ) ) ) |
15 |
13 14
|
bitr4di |
⊢ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) → ( ∀ 𝑠 ∈ 𝐶 ∃ 𝑔 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑠 = ( 𝐹 ‘ 𝑔 ) ↔ 𝐶 ⊆ ( 𝐹 “ ( 𝒫 𝑋 ∩ Fin ) ) ) ) |
16 |
|
imassrn |
⊢ ( 𝐹 “ ( 𝒫 𝑋 ∩ Fin ) ) ⊆ ran 𝐹 |
17 |
|
frn |
⊢ ( 𝐹 : 𝒫 𝑋 ⟶ 𝐶 → ran 𝐹 ⊆ 𝐶 ) |
18 |
5 6 17
|
3syl |
⊢ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) → ran 𝐹 ⊆ 𝐶 ) |
19 |
16 18
|
sstrid |
⊢ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) → ( 𝐹 “ ( 𝒫 𝑋 ∩ Fin ) ) ⊆ 𝐶 ) |
20 |
19
|
biantrurd |
⊢ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) → ( 𝐶 ⊆ ( 𝐹 “ ( 𝒫 𝑋 ∩ Fin ) ) ↔ ( ( 𝐹 “ ( 𝒫 𝑋 ∩ Fin ) ) ⊆ 𝐶 ∧ 𝐶 ⊆ ( 𝐹 “ ( 𝒫 𝑋 ∩ Fin ) ) ) ) ) |
21 |
|
eqss |
⊢ ( ( 𝐹 “ ( 𝒫 𝑋 ∩ Fin ) ) = 𝐶 ↔ ( ( 𝐹 “ ( 𝒫 𝑋 ∩ Fin ) ) ⊆ 𝐶 ∧ 𝐶 ⊆ ( 𝐹 “ ( 𝒫 𝑋 ∩ Fin ) ) ) ) |
22 |
20 21
|
bitr4di |
⊢ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) → ( 𝐶 ⊆ ( 𝐹 “ ( 𝒫 𝑋 ∩ Fin ) ) ↔ ( 𝐹 “ ( 𝒫 𝑋 ∩ Fin ) ) = 𝐶 ) ) |
23 |
15 22
|
bitrd |
⊢ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) → ( ∀ 𝑠 ∈ 𝐶 ∃ 𝑔 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑠 = ( 𝐹 ‘ 𝑔 ) ↔ ( 𝐹 “ ( 𝒫 𝑋 ∩ Fin ) ) = 𝐶 ) ) |
24 |
23
|
pm5.32i |
⊢ ( ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝐶 ∃ 𝑔 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑠 = ( 𝐹 ‘ 𝑔 ) ) ↔ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ∧ ( 𝐹 “ ( 𝒫 𝑋 ∩ Fin ) ) = 𝐶 ) ) |
25 |
2 24
|
bitri |
⊢ ( 𝐶 ∈ ( NoeACS ‘ 𝑋 ) ↔ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ∧ ( 𝐹 “ ( 𝒫 𝑋 ∩ Fin ) ) = 𝐶 ) ) |