Step | Hyp | Ref
| Expression |
1 | | isnacs.f |
. . 3
⊢ 𝐹 = (mrCls‘𝐶) |
2 | 1 | isnacs 40526 |
. 2
⊢ (𝐶 ∈ (NoeACS‘𝑋) ↔ (𝐶 ∈ (ACS‘𝑋) ∧ ∀𝑠 ∈ 𝐶 ∃𝑔 ∈ (𝒫 𝑋 ∩ Fin)𝑠 = (𝐹‘𝑔))) |
3 | | eqcom 2745 |
. . . . . . . 8
⊢ (𝑠 = (𝐹‘𝑔) ↔ (𝐹‘𝑔) = 𝑠) |
4 | 3 | rexbii 3181 |
. . . . . . 7
⊢
(∃𝑔 ∈
(𝒫 𝑋 ∩
Fin)𝑠 = (𝐹‘𝑔) ↔ ∃𝑔 ∈ (𝒫 𝑋 ∩ Fin)(𝐹‘𝑔) = 𝑠) |
5 | | acsmre 17361 |
. . . . . . . . 9
⊢ (𝐶 ∈ (ACS‘𝑋) → 𝐶 ∈ (Moore‘𝑋)) |
6 | 1 | mrcf 17318 |
. . . . . . . . 9
⊢ (𝐶 ∈ (Moore‘𝑋) → 𝐹:𝒫 𝑋⟶𝐶) |
7 | | ffn 6600 |
. . . . . . . . 9
⊢ (𝐹:𝒫 𝑋⟶𝐶 → 𝐹 Fn 𝒫 𝑋) |
8 | 5, 6, 7 | 3syl 18 |
. . . . . . . 8
⊢ (𝐶 ∈ (ACS‘𝑋) → 𝐹 Fn 𝒫 𝑋) |
9 | | inss1 4162 |
. . . . . . . 8
⊢
(𝒫 𝑋 ∩
Fin) ⊆ 𝒫 𝑋 |
10 | | fvelimab 6841 |
. . . . . . . 8
⊢ ((𝐹 Fn 𝒫 𝑋 ∧ (𝒫 𝑋 ∩ Fin) ⊆ 𝒫 𝑋) → (𝑠 ∈ (𝐹 “ (𝒫 𝑋 ∩ Fin)) ↔ ∃𝑔 ∈ (𝒫 𝑋 ∩ Fin)(𝐹‘𝑔) = 𝑠)) |
11 | 8, 9, 10 | sylancl 586 |
. . . . . . 7
⊢ (𝐶 ∈ (ACS‘𝑋) → (𝑠 ∈ (𝐹 “ (𝒫 𝑋 ∩ Fin)) ↔ ∃𝑔 ∈ (𝒫 𝑋 ∩ Fin)(𝐹‘𝑔) = 𝑠)) |
12 | 4, 11 | bitr4id 290 |
. . . . . 6
⊢ (𝐶 ∈ (ACS‘𝑋) → (∃𝑔 ∈ (𝒫 𝑋 ∩ Fin)𝑠 = (𝐹‘𝑔) ↔ 𝑠 ∈ (𝐹 “ (𝒫 𝑋 ∩ Fin)))) |
13 | 12 | ralbidv 3112 |
. . . . 5
⊢ (𝐶 ∈ (ACS‘𝑋) → (∀𝑠 ∈ 𝐶 ∃𝑔 ∈ (𝒫 𝑋 ∩ Fin)𝑠 = (𝐹‘𝑔) ↔ ∀𝑠 ∈ 𝐶 𝑠 ∈ (𝐹 “ (𝒫 𝑋 ∩ Fin)))) |
14 | | dfss3 3909 |
. . . . 5
⊢ (𝐶 ⊆ (𝐹 “ (𝒫 𝑋 ∩ Fin)) ↔ ∀𝑠 ∈ 𝐶 𝑠 ∈ (𝐹 “ (𝒫 𝑋 ∩ Fin))) |
15 | 13, 14 | bitr4di 289 |
. . . 4
⊢ (𝐶 ∈ (ACS‘𝑋) → (∀𝑠 ∈ 𝐶 ∃𝑔 ∈ (𝒫 𝑋 ∩ Fin)𝑠 = (𝐹‘𝑔) ↔ 𝐶 ⊆ (𝐹 “ (𝒫 𝑋 ∩ Fin)))) |
16 | | imassrn 5980 |
. . . . . . 7
⊢ (𝐹 “ (𝒫 𝑋 ∩ Fin)) ⊆ ran 𝐹 |
17 | | frn 6607 |
. . . . . . . 8
⊢ (𝐹:𝒫 𝑋⟶𝐶 → ran 𝐹 ⊆ 𝐶) |
18 | 5, 6, 17 | 3syl 18 |
. . . . . . 7
⊢ (𝐶 ∈ (ACS‘𝑋) → ran 𝐹 ⊆ 𝐶) |
19 | 16, 18 | sstrid 3932 |
. . . . . 6
⊢ (𝐶 ∈ (ACS‘𝑋) → (𝐹 “ (𝒫 𝑋 ∩ Fin)) ⊆ 𝐶) |
20 | 19 | biantrurd 533 |
. . . . 5
⊢ (𝐶 ∈ (ACS‘𝑋) → (𝐶 ⊆ (𝐹 “ (𝒫 𝑋 ∩ Fin)) ↔ ((𝐹 “ (𝒫 𝑋 ∩ Fin)) ⊆ 𝐶 ∧ 𝐶 ⊆ (𝐹 “ (𝒫 𝑋 ∩ Fin))))) |
21 | | eqss 3936 |
. . . . 5
⊢ ((𝐹 “ (𝒫 𝑋 ∩ Fin)) = 𝐶 ↔ ((𝐹 “ (𝒫 𝑋 ∩ Fin)) ⊆ 𝐶 ∧ 𝐶 ⊆ (𝐹 “ (𝒫 𝑋 ∩ Fin)))) |
22 | 20, 21 | bitr4di 289 |
. . . 4
⊢ (𝐶 ∈ (ACS‘𝑋) → (𝐶 ⊆ (𝐹 “ (𝒫 𝑋 ∩ Fin)) ↔ (𝐹 “ (𝒫 𝑋 ∩ Fin)) = 𝐶)) |
23 | 15, 22 | bitrd 278 |
. . 3
⊢ (𝐶 ∈ (ACS‘𝑋) → (∀𝑠 ∈ 𝐶 ∃𝑔 ∈ (𝒫 𝑋 ∩ Fin)𝑠 = (𝐹‘𝑔) ↔ (𝐹 “ (𝒫 𝑋 ∩ Fin)) = 𝐶)) |
24 | 23 | pm5.32i 575 |
. 2
⊢ ((𝐶 ∈ (ACS‘𝑋) ∧ ∀𝑠 ∈ 𝐶 ∃𝑔 ∈ (𝒫 𝑋 ∩ Fin)𝑠 = (𝐹‘𝑔)) ↔ (𝐶 ∈ (ACS‘𝑋) ∧ (𝐹 “ (𝒫 𝑋 ∩ Fin)) = 𝐶)) |
25 | 2, 24 | bitri 274 |
1
⊢ (𝐶 ∈ (NoeACS‘𝑋) ↔ (𝐶 ∈ (ACS‘𝑋) ∧ (𝐹 “ (𝒫 𝑋 ∩ Fin)) = 𝐶)) |