Step | Hyp | Ref
| Expression |
1 | | isnacs.f |
. . 3
⊢ 𝐹 = (mrCls‘𝐶) |
2 | 1 | isnacs 39308 |
. 2
⊢ (𝐶 ∈ (NoeACS‘𝑋) ↔ (𝐶 ∈ (ACS‘𝑋) ∧ ∀𝑠 ∈ 𝐶 ∃𝑔 ∈ (𝒫 𝑋 ∩ Fin)𝑠 = (𝐹‘𝑔))) |
3 | | acsmre 16925 |
. . . . . . . . 9
⊢ (𝐶 ∈ (ACS‘𝑋) → 𝐶 ∈ (Moore‘𝑋)) |
4 | 1 | mrcf 16882 |
. . . . . . . . 9
⊢ (𝐶 ∈ (Moore‘𝑋) → 𝐹:𝒫 𝑋⟶𝐶) |
5 | | ffn 6516 |
. . . . . . . . 9
⊢ (𝐹:𝒫 𝑋⟶𝐶 → 𝐹 Fn 𝒫 𝑋) |
6 | 3, 4, 5 | 3syl 18 |
. . . . . . . 8
⊢ (𝐶 ∈ (ACS‘𝑋) → 𝐹 Fn 𝒫 𝑋) |
7 | | inss1 4207 |
. . . . . . . 8
⊢
(𝒫 𝑋 ∩
Fin) ⊆ 𝒫 𝑋 |
8 | | fvelimab 6739 |
. . . . . . . 8
⊢ ((𝐹 Fn 𝒫 𝑋 ∧ (𝒫 𝑋 ∩ Fin) ⊆ 𝒫 𝑋) → (𝑠 ∈ (𝐹 “ (𝒫 𝑋 ∩ Fin)) ↔ ∃𝑔 ∈ (𝒫 𝑋 ∩ Fin)(𝐹‘𝑔) = 𝑠)) |
9 | 6, 7, 8 | sylancl 588 |
. . . . . . 7
⊢ (𝐶 ∈ (ACS‘𝑋) → (𝑠 ∈ (𝐹 “ (𝒫 𝑋 ∩ Fin)) ↔ ∃𝑔 ∈ (𝒫 𝑋 ∩ Fin)(𝐹‘𝑔) = 𝑠)) |
10 | | eqcom 2830 |
. . . . . . . 8
⊢ (𝑠 = (𝐹‘𝑔) ↔ (𝐹‘𝑔) = 𝑠) |
11 | 10 | rexbii 3249 |
. . . . . . 7
⊢
(∃𝑔 ∈
(𝒫 𝑋 ∩
Fin)𝑠 = (𝐹‘𝑔) ↔ ∃𝑔 ∈ (𝒫 𝑋 ∩ Fin)(𝐹‘𝑔) = 𝑠) |
12 | 9, 11 | syl6rbbr 292 |
. . . . . 6
⊢ (𝐶 ∈ (ACS‘𝑋) → (∃𝑔 ∈ (𝒫 𝑋 ∩ Fin)𝑠 = (𝐹‘𝑔) ↔ 𝑠 ∈ (𝐹 “ (𝒫 𝑋 ∩ Fin)))) |
13 | 12 | ralbidv 3199 |
. . . . 5
⊢ (𝐶 ∈ (ACS‘𝑋) → (∀𝑠 ∈ 𝐶 ∃𝑔 ∈ (𝒫 𝑋 ∩ Fin)𝑠 = (𝐹‘𝑔) ↔ ∀𝑠 ∈ 𝐶 𝑠 ∈ (𝐹 “ (𝒫 𝑋 ∩ Fin)))) |
14 | | dfss3 3958 |
. . . . 5
⊢ (𝐶 ⊆ (𝐹 “ (𝒫 𝑋 ∩ Fin)) ↔ ∀𝑠 ∈ 𝐶 𝑠 ∈ (𝐹 “ (𝒫 𝑋 ∩ Fin))) |
15 | 13, 14 | syl6bbr 291 |
. . . 4
⊢ (𝐶 ∈ (ACS‘𝑋) → (∀𝑠 ∈ 𝐶 ∃𝑔 ∈ (𝒫 𝑋 ∩ Fin)𝑠 = (𝐹‘𝑔) ↔ 𝐶 ⊆ (𝐹 “ (𝒫 𝑋 ∩ Fin)))) |
16 | | imassrn 5942 |
. . . . . . 7
⊢ (𝐹 “ (𝒫 𝑋 ∩ Fin)) ⊆ ran 𝐹 |
17 | | frn 6522 |
. . . . . . . 8
⊢ (𝐹:𝒫 𝑋⟶𝐶 → ran 𝐹 ⊆ 𝐶) |
18 | 3, 4, 17 | 3syl 18 |
. . . . . . 7
⊢ (𝐶 ∈ (ACS‘𝑋) → ran 𝐹 ⊆ 𝐶) |
19 | 16, 18 | sstrid 3980 |
. . . . . 6
⊢ (𝐶 ∈ (ACS‘𝑋) → (𝐹 “ (𝒫 𝑋 ∩ Fin)) ⊆ 𝐶) |
20 | 19 | biantrurd 535 |
. . . . 5
⊢ (𝐶 ∈ (ACS‘𝑋) → (𝐶 ⊆ (𝐹 “ (𝒫 𝑋 ∩ Fin)) ↔ ((𝐹 “ (𝒫 𝑋 ∩ Fin)) ⊆ 𝐶 ∧ 𝐶 ⊆ (𝐹 “ (𝒫 𝑋 ∩ Fin))))) |
21 | | eqss 3984 |
. . . . 5
⊢ ((𝐹 “ (𝒫 𝑋 ∩ Fin)) = 𝐶 ↔ ((𝐹 “ (𝒫 𝑋 ∩ Fin)) ⊆ 𝐶 ∧ 𝐶 ⊆ (𝐹 “ (𝒫 𝑋 ∩ Fin)))) |
22 | 20, 21 | syl6bbr 291 |
. . . 4
⊢ (𝐶 ∈ (ACS‘𝑋) → (𝐶 ⊆ (𝐹 “ (𝒫 𝑋 ∩ Fin)) ↔ (𝐹 “ (𝒫 𝑋 ∩ Fin)) = 𝐶)) |
23 | 15, 22 | bitrd 281 |
. . 3
⊢ (𝐶 ∈ (ACS‘𝑋) → (∀𝑠 ∈ 𝐶 ∃𝑔 ∈ (𝒫 𝑋 ∩ Fin)𝑠 = (𝐹‘𝑔) ↔ (𝐹 “ (𝒫 𝑋 ∩ Fin)) = 𝐶)) |
24 | 23 | pm5.32i 577 |
. 2
⊢ ((𝐶 ∈ (ACS‘𝑋) ∧ ∀𝑠 ∈ 𝐶 ∃𝑔 ∈ (𝒫 𝑋 ∩ Fin)𝑠 = (𝐹‘𝑔)) ↔ (𝐶 ∈ (ACS‘𝑋) ∧ (𝐹 “ (𝒫 𝑋 ∩ Fin)) = 𝐶)) |
25 | 2, 24 | bitri 277 |
1
⊢ (𝐶 ∈ (NoeACS‘𝑋) ↔ (𝐶 ∈ (ACS‘𝑋) ∧ (𝐹 “ (𝒫 𝑋 ∩ Fin)) = 𝐶)) |