Proof of Theorem acsfn1p
Step | Hyp | Ref
| Expression |
1 | | riinrab 5008 |
. . 3
⊢
(𝒫 𝑋 ∩
∩ 𝑏 ∈ (𝑋 ∩ 𝑌){𝑎 ∈ 𝒫 𝑋 ∣ ({𝑏} ⊆ 𝑎 → 𝐸 ∈ 𝑎)}) = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑏 ∈ (𝑋 ∩ 𝑌)({𝑏} ⊆ 𝑎 → 𝐸 ∈ 𝑎)} |
2 | | elpwi 4550 |
. . . . . . . 8
⊢ (𝑎 ∈ 𝒫 𝑋 → 𝑎 ⊆ 𝑋) |
3 | 2 | ssrind 4214 |
. . . . . . 7
⊢ (𝑎 ∈ 𝒫 𝑋 → (𝑎 ∩ 𝑌) ⊆ (𝑋 ∩ 𝑌)) |
4 | 3 | adantl 484 |
. . . . . 6
⊢ (((𝑋 ∈ 𝑉 ∧ ∀𝑏 ∈ 𝑌 𝐸 ∈ 𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) → (𝑎 ∩ 𝑌) ⊆ (𝑋 ∩ 𝑌)) |
5 | | ralss 4039 |
. . . . . 6
⊢ ((𝑎 ∩ 𝑌) ⊆ (𝑋 ∩ 𝑌) → (∀𝑏 ∈ (𝑎 ∩ 𝑌)𝐸 ∈ 𝑎 ↔ ∀𝑏 ∈ (𝑋 ∩ 𝑌)(𝑏 ∈ (𝑎 ∩ 𝑌) → 𝐸 ∈ 𝑎))) |
6 | 4, 5 | syl 17 |
. . . . 5
⊢ (((𝑋 ∈ 𝑉 ∧ ∀𝑏 ∈ 𝑌 𝐸 ∈ 𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) → (∀𝑏 ∈ (𝑎 ∩ 𝑌)𝐸 ∈ 𝑎 ↔ ∀𝑏 ∈ (𝑋 ∩ 𝑌)(𝑏 ∈ (𝑎 ∩ 𝑌) → 𝐸 ∈ 𝑎))) |
7 | | inss2 4208 |
. . . . . . . . . 10
⊢ (𝑋 ∩ 𝑌) ⊆ 𝑌 |
8 | 7 | sseli 3965 |
. . . . . . . . 9
⊢ (𝑏 ∈ (𝑋 ∩ 𝑌) → 𝑏 ∈ 𝑌) |
9 | 8 | biantrud 534 |
. . . . . . . 8
⊢ (𝑏 ∈ (𝑋 ∩ 𝑌) → (𝑏 ∈ 𝑎 ↔ (𝑏 ∈ 𝑎 ∧ 𝑏 ∈ 𝑌))) |
10 | | vex 3499 |
. . . . . . . . . 10
⊢ 𝑏 ∈ V |
11 | 10 | snss 4720 |
. . . . . . . . 9
⊢ (𝑏 ∈ 𝑎 ↔ {𝑏} ⊆ 𝑎) |
12 | 11 | bicomi 226 |
. . . . . . . 8
⊢ ({𝑏} ⊆ 𝑎 ↔ 𝑏 ∈ 𝑎) |
13 | | elin 4171 |
. . . . . . . 8
⊢ (𝑏 ∈ (𝑎 ∩ 𝑌) ↔ (𝑏 ∈ 𝑎 ∧ 𝑏 ∈ 𝑌)) |
14 | 9, 12, 13 | 3bitr4g 316 |
. . . . . . 7
⊢ (𝑏 ∈ (𝑋 ∩ 𝑌) → ({𝑏} ⊆ 𝑎 ↔ 𝑏 ∈ (𝑎 ∩ 𝑌))) |
15 | 14 | imbi1d 344 |
. . . . . 6
⊢ (𝑏 ∈ (𝑋 ∩ 𝑌) → (({𝑏} ⊆ 𝑎 → 𝐸 ∈ 𝑎) ↔ (𝑏 ∈ (𝑎 ∩ 𝑌) → 𝐸 ∈ 𝑎))) |
16 | 15 | ralbiia 3166 |
. . . . 5
⊢
(∀𝑏 ∈
(𝑋 ∩ 𝑌)({𝑏} ⊆ 𝑎 → 𝐸 ∈ 𝑎) ↔ ∀𝑏 ∈ (𝑋 ∩ 𝑌)(𝑏 ∈ (𝑎 ∩ 𝑌) → 𝐸 ∈ 𝑎)) |
17 | 6, 16 | syl6rbbr 292 |
. . . 4
⊢ (((𝑋 ∈ 𝑉 ∧ ∀𝑏 ∈ 𝑌 𝐸 ∈ 𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) → (∀𝑏 ∈ (𝑋 ∩ 𝑌)({𝑏} ⊆ 𝑎 → 𝐸 ∈ 𝑎) ↔ ∀𝑏 ∈ (𝑎 ∩ 𝑌)𝐸 ∈ 𝑎)) |
18 | 17 | rabbidva 3480 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ ∀𝑏 ∈ 𝑌 𝐸 ∈ 𝑋) → {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑏 ∈ (𝑋 ∩ 𝑌)({𝑏} ⊆ 𝑎 → 𝐸 ∈ 𝑎)} = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑏 ∈ (𝑎 ∩ 𝑌)𝐸 ∈ 𝑎}) |
19 | 1, 18 | syl5eq 2870 |
. 2
⊢ ((𝑋 ∈ 𝑉 ∧ ∀𝑏 ∈ 𝑌 𝐸 ∈ 𝑋) → (𝒫 𝑋 ∩ ∩
𝑏 ∈ (𝑋 ∩ 𝑌){𝑎 ∈ 𝒫 𝑋 ∣ ({𝑏} ⊆ 𝑎 → 𝐸 ∈ 𝑎)}) = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑏 ∈ (𝑎 ∩ 𝑌)𝐸 ∈ 𝑎}) |
20 | | mreacs 16931 |
. . . 4
⊢ (𝑋 ∈ 𝑉 → (ACS‘𝑋) ∈ (Moore‘𝒫 𝑋)) |
21 | 20 | adantr 483 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ ∀𝑏 ∈ 𝑌 𝐸 ∈ 𝑋) → (ACS‘𝑋) ∈ (Moore‘𝒫 𝑋)) |
22 | | ssralv 4035 |
. . . . . 6
⊢ ((𝑋 ∩ 𝑌) ⊆ 𝑌 → (∀𝑏 ∈ 𝑌 𝐸 ∈ 𝑋 → ∀𝑏 ∈ (𝑋 ∩ 𝑌)𝐸 ∈ 𝑋)) |
23 | 7, 22 | ax-mp 5 |
. . . . 5
⊢
(∀𝑏 ∈
𝑌 𝐸 ∈ 𝑋 → ∀𝑏 ∈ (𝑋 ∩ 𝑌)𝐸 ∈ 𝑋) |
24 | | simpll 765 |
. . . . . . . 8
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑏 ∈ (𝑋 ∩ 𝑌)) ∧ 𝐸 ∈ 𝑋) → 𝑋 ∈ 𝑉) |
25 | | simpr 487 |
. . . . . . . 8
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑏 ∈ (𝑋 ∩ 𝑌)) ∧ 𝐸 ∈ 𝑋) → 𝐸 ∈ 𝑋) |
26 | | inss1 4207 |
. . . . . . . . . . 11
⊢ (𝑋 ∩ 𝑌) ⊆ 𝑋 |
27 | 26 | sseli 3965 |
. . . . . . . . . 10
⊢ (𝑏 ∈ (𝑋 ∩ 𝑌) → 𝑏 ∈ 𝑋) |
28 | 27 | ad2antlr 725 |
. . . . . . . . 9
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑏 ∈ (𝑋 ∩ 𝑌)) ∧ 𝐸 ∈ 𝑋) → 𝑏 ∈ 𝑋) |
29 | 28 | snssd 4744 |
. . . . . . . 8
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑏 ∈ (𝑋 ∩ 𝑌)) ∧ 𝐸 ∈ 𝑋) → {𝑏} ⊆ 𝑋) |
30 | | snfi 8596 |
. . . . . . . . 9
⊢ {𝑏} ∈ Fin |
31 | 30 | a1i 11 |
. . . . . . . 8
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑏 ∈ (𝑋 ∩ 𝑌)) ∧ 𝐸 ∈ 𝑋) → {𝑏} ∈ Fin) |
32 | | acsfn 16932 |
. . . . . . . 8
⊢ (((𝑋 ∈ 𝑉 ∧ 𝐸 ∈ 𝑋) ∧ ({𝑏} ⊆ 𝑋 ∧ {𝑏} ∈ Fin)) → {𝑎 ∈ 𝒫 𝑋 ∣ ({𝑏} ⊆ 𝑎 → 𝐸 ∈ 𝑎)} ∈ (ACS‘𝑋)) |
33 | 24, 25, 29, 31, 32 | syl22anc 836 |
. . . . . . 7
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑏 ∈ (𝑋 ∩ 𝑌)) ∧ 𝐸 ∈ 𝑋) → {𝑎 ∈ 𝒫 𝑋 ∣ ({𝑏} ⊆ 𝑎 → 𝐸 ∈ 𝑎)} ∈ (ACS‘𝑋)) |
34 | 33 | ex 415 |
. . . . . 6
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑏 ∈ (𝑋 ∩ 𝑌)) → (𝐸 ∈ 𝑋 → {𝑎 ∈ 𝒫 𝑋 ∣ ({𝑏} ⊆ 𝑎 → 𝐸 ∈ 𝑎)} ∈ (ACS‘𝑋))) |
35 | 34 | ralimdva 3179 |
. . . . 5
⊢ (𝑋 ∈ 𝑉 → (∀𝑏 ∈ (𝑋 ∩ 𝑌)𝐸 ∈ 𝑋 → ∀𝑏 ∈ (𝑋 ∩ 𝑌){𝑎 ∈ 𝒫 𝑋 ∣ ({𝑏} ⊆ 𝑎 → 𝐸 ∈ 𝑎)} ∈ (ACS‘𝑋))) |
36 | 23, 35 | syl5 34 |
. . . 4
⊢ (𝑋 ∈ 𝑉 → (∀𝑏 ∈ 𝑌 𝐸 ∈ 𝑋 → ∀𝑏 ∈ (𝑋 ∩ 𝑌){𝑎 ∈ 𝒫 𝑋 ∣ ({𝑏} ⊆ 𝑎 → 𝐸 ∈ 𝑎)} ∈ (ACS‘𝑋))) |
37 | 36 | imp 409 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ ∀𝑏 ∈ 𝑌 𝐸 ∈ 𝑋) → ∀𝑏 ∈ (𝑋 ∩ 𝑌){𝑎 ∈ 𝒫 𝑋 ∣ ({𝑏} ⊆ 𝑎 → 𝐸 ∈ 𝑎)} ∈ (ACS‘𝑋)) |
38 | | mreriincl 16871 |
. . 3
⊢
(((ACS‘𝑋)
∈ (Moore‘𝒫 𝑋) ∧ ∀𝑏 ∈ (𝑋 ∩ 𝑌){𝑎 ∈ 𝒫 𝑋 ∣ ({𝑏} ⊆ 𝑎 → 𝐸 ∈ 𝑎)} ∈ (ACS‘𝑋)) → (𝒫 𝑋 ∩ ∩
𝑏 ∈ (𝑋 ∩ 𝑌){𝑎 ∈ 𝒫 𝑋 ∣ ({𝑏} ⊆ 𝑎 → 𝐸 ∈ 𝑎)}) ∈ (ACS‘𝑋)) |
39 | 21, 37, 38 | syl2anc 586 |
. 2
⊢ ((𝑋 ∈ 𝑉 ∧ ∀𝑏 ∈ 𝑌 𝐸 ∈ 𝑋) → (𝒫 𝑋 ∩ ∩
𝑏 ∈ (𝑋 ∩ 𝑌){𝑎 ∈ 𝒫 𝑋 ∣ ({𝑏} ⊆ 𝑎 → 𝐸 ∈ 𝑎)}) ∈ (ACS‘𝑋)) |
40 | 19, 39 | eqeltrrd 2916 |
1
⊢ ((𝑋 ∈ 𝑉 ∧ ∀𝑏 ∈ 𝑌 𝐸 ∈ 𝑋) → {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑏 ∈ (𝑎 ∩ 𝑌)𝐸 ∈ 𝑎} ∈ (ACS‘𝑋)) |