Proof of Theorem acsfn1p
Step | Hyp | Ref
| Expression |
1 | | riinrab 4997 |
. . 3
⊢
(𝒫 𝑋 ∩
∩ 𝑏 ∈ (𝑋 ∩ 𝑌){𝑎 ∈ 𝒫 𝑋 ∣ ({𝑏} ⊆ 𝑎 → 𝐸 ∈ 𝑎)}) = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑏 ∈ (𝑋 ∩ 𝑌)({𝑏} ⊆ 𝑎 → 𝐸 ∈ 𝑎)} |
2 | | elpwi 4547 |
. . . . . . . 8
⊢ (𝑎 ∈ 𝒫 𝑋 → 𝑎 ⊆ 𝑋) |
3 | 2 | ssrind 4209 |
. . . . . . 7
⊢ (𝑎 ∈ 𝒫 𝑋 → (𝑎 ∩ 𝑌) ⊆ (𝑋 ∩ 𝑌)) |
4 | 3 | adantl 482 |
. . . . . 6
⊢ (((𝑋 ∈ 𝑉 ∧ ∀𝑏 ∈ 𝑌 𝐸 ∈ 𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) → (𝑎 ∩ 𝑌) ⊆ (𝑋 ∩ 𝑌)) |
5 | | ralss 4034 |
. . . . . 6
⊢ ((𝑎 ∩ 𝑌) ⊆ (𝑋 ∩ 𝑌) → (∀𝑏 ∈ (𝑎 ∩ 𝑌)𝐸 ∈ 𝑎 ↔ ∀𝑏 ∈ (𝑋 ∩ 𝑌)(𝑏 ∈ (𝑎 ∩ 𝑌) → 𝐸 ∈ 𝑎))) |
6 | 4, 5 | syl 17 |
. . . . 5
⊢ (((𝑋 ∈ 𝑉 ∧ ∀𝑏 ∈ 𝑌 𝐸 ∈ 𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) → (∀𝑏 ∈ (𝑎 ∩ 𝑌)𝐸 ∈ 𝑎 ↔ ∀𝑏 ∈ (𝑋 ∩ 𝑌)(𝑏 ∈ (𝑎 ∩ 𝑌) → 𝐸 ∈ 𝑎))) |
7 | | inss2 4203 |
. . . . . . . . . 10
⊢ (𝑋 ∩ 𝑌) ⊆ 𝑌 |
8 | 7 | sseli 3960 |
. . . . . . . . 9
⊢ (𝑏 ∈ (𝑋 ∩ 𝑌) → 𝑏 ∈ 𝑌) |
9 | 8 | biantrud 532 |
. . . . . . . 8
⊢ (𝑏 ∈ (𝑋 ∩ 𝑌) → (𝑏 ∈ 𝑎 ↔ (𝑏 ∈ 𝑎 ∧ 𝑏 ∈ 𝑌))) |
10 | | vex 3495 |
. . . . . . . . . 10
⊢ 𝑏 ∈ V |
11 | 10 | snss 4710 |
. . . . . . . . 9
⊢ (𝑏 ∈ 𝑎 ↔ {𝑏} ⊆ 𝑎) |
12 | 11 | bicomi 225 |
. . . . . . . 8
⊢ ({𝑏} ⊆ 𝑎 ↔ 𝑏 ∈ 𝑎) |
13 | | elin 4166 |
. . . . . . . 8
⊢ (𝑏 ∈ (𝑎 ∩ 𝑌) ↔ (𝑏 ∈ 𝑎 ∧ 𝑏 ∈ 𝑌)) |
14 | 9, 12, 13 | 3bitr4g 315 |
. . . . . . 7
⊢ (𝑏 ∈ (𝑋 ∩ 𝑌) → ({𝑏} ⊆ 𝑎 ↔ 𝑏 ∈ (𝑎 ∩ 𝑌))) |
15 | 14 | imbi1d 343 |
. . . . . 6
⊢ (𝑏 ∈ (𝑋 ∩ 𝑌) → (({𝑏} ⊆ 𝑎 → 𝐸 ∈ 𝑎) ↔ (𝑏 ∈ (𝑎 ∩ 𝑌) → 𝐸 ∈ 𝑎))) |
16 | 15 | ralbiia 3161 |
. . . . 5
⊢
(∀𝑏 ∈
(𝑋 ∩ 𝑌)({𝑏} ⊆ 𝑎 → 𝐸 ∈ 𝑎) ↔ ∀𝑏 ∈ (𝑋 ∩ 𝑌)(𝑏 ∈ (𝑎 ∩ 𝑌) → 𝐸 ∈ 𝑎)) |
17 | 6, 16 | syl6rbbr 291 |
. . . 4
⊢ (((𝑋 ∈ 𝑉 ∧ ∀𝑏 ∈ 𝑌 𝐸 ∈ 𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) → (∀𝑏 ∈ (𝑋 ∩ 𝑌)({𝑏} ⊆ 𝑎 → 𝐸 ∈ 𝑎) ↔ ∀𝑏 ∈ (𝑎 ∩ 𝑌)𝐸 ∈ 𝑎)) |
18 | 17 | rabbidva 3476 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ ∀𝑏 ∈ 𝑌 𝐸 ∈ 𝑋) → {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑏 ∈ (𝑋 ∩ 𝑌)({𝑏} ⊆ 𝑎 → 𝐸 ∈ 𝑎)} = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑏 ∈ (𝑎 ∩ 𝑌)𝐸 ∈ 𝑎}) |
19 | 1, 18 | syl5eq 2865 |
. 2
⊢ ((𝑋 ∈ 𝑉 ∧ ∀𝑏 ∈ 𝑌 𝐸 ∈ 𝑋) → (𝒫 𝑋 ∩ ∩
𝑏 ∈ (𝑋 ∩ 𝑌){𝑎 ∈ 𝒫 𝑋 ∣ ({𝑏} ⊆ 𝑎 → 𝐸 ∈ 𝑎)}) = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑏 ∈ (𝑎 ∩ 𝑌)𝐸 ∈ 𝑎}) |
20 | | mreacs 16917 |
. . . 4
⊢ (𝑋 ∈ 𝑉 → (ACS‘𝑋) ∈ (Moore‘𝒫 𝑋)) |
21 | 20 | adantr 481 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ ∀𝑏 ∈ 𝑌 𝐸 ∈ 𝑋) → (ACS‘𝑋) ∈ (Moore‘𝒫 𝑋)) |
22 | | ssralv 4030 |
. . . . . 6
⊢ ((𝑋 ∩ 𝑌) ⊆ 𝑌 → (∀𝑏 ∈ 𝑌 𝐸 ∈ 𝑋 → ∀𝑏 ∈ (𝑋 ∩ 𝑌)𝐸 ∈ 𝑋)) |
23 | 7, 22 | ax-mp 5 |
. . . . 5
⊢
(∀𝑏 ∈
𝑌 𝐸 ∈ 𝑋 → ∀𝑏 ∈ (𝑋 ∩ 𝑌)𝐸 ∈ 𝑋) |
24 | | simpll 763 |
. . . . . . . 8
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑏 ∈ (𝑋 ∩ 𝑌)) ∧ 𝐸 ∈ 𝑋) → 𝑋 ∈ 𝑉) |
25 | | simpr 485 |
. . . . . . . 8
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑏 ∈ (𝑋 ∩ 𝑌)) ∧ 𝐸 ∈ 𝑋) → 𝐸 ∈ 𝑋) |
26 | | inss1 4202 |
. . . . . . . . . . 11
⊢ (𝑋 ∩ 𝑌) ⊆ 𝑋 |
27 | 26 | sseli 3960 |
. . . . . . . . . 10
⊢ (𝑏 ∈ (𝑋 ∩ 𝑌) → 𝑏 ∈ 𝑋) |
28 | 27 | ad2antlr 723 |
. . . . . . . . 9
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑏 ∈ (𝑋 ∩ 𝑌)) ∧ 𝐸 ∈ 𝑋) → 𝑏 ∈ 𝑋) |
29 | 28 | snssd 4734 |
. . . . . . . 8
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑏 ∈ (𝑋 ∩ 𝑌)) ∧ 𝐸 ∈ 𝑋) → {𝑏} ⊆ 𝑋) |
30 | | snfi 8582 |
. . . . . . . . 9
⊢ {𝑏} ∈ Fin |
31 | 30 | a1i 11 |
. . . . . . . 8
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑏 ∈ (𝑋 ∩ 𝑌)) ∧ 𝐸 ∈ 𝑋) → {𝑏} ∈ Fin) |
32 | | acsfn 16918 |
. . . . . . . 8
⊢ (((𝑋 ∈ 𝑉 ∧ 𝐸 ∈ 𝑋) ∧ ({𝑏} ⊆ 𝑋 ∧ {𝑏} ∈ Fin)) → {𝑎 ∈ 𝒫 𝑋 ∣ ({𝑏} ⊆ 𝑎 → 𝐸 ∈ 𝑎)} ∈ (ACS‘𝑋)) |
33 | 24, 25, 29, 31, 32 | syl22anc 834 |
. . . . . . 7
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑏 ∈ (𝑋 ∩ 𝑌)) ∧ 𝐸 ∈ 𝑋) → {𝑎 ∈ 𝒫 𝑋 ∣ ({𝑏} ⊆ 𝑎 → 𝐸 ∈ 𝑎)} ∈ (ACS‘𝑋)) |
34 | 33 | ex 413 |
. . . . . 6
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑏 ∈ (𝑋 ∩ 𝑌)) → (𝐸 ∈ 𝑋 → {𝑎 ∈ 𝒫 𝑋 ∣ ({𝑏} ⊆ 𝑎 → 𝐸 ∈ 𝑎)} ∈ (ACS‘𝑋))) |
35 | 34 | ralimdva 3174 |
. . . . 5
⊢ (𝑋 ∈ 𝑉 → (∀𝑏 ∈ (𝑋 ∩ 𝑌)𝐸 ∈ 𝑋 → ∀𝑏 ∈ (𝑋 ∩ 𝑌){𝑎 ∈ 𝒫 𝑋 ∣ ({𝑏} ⊆ 𝑎 → 𝐸 ∈ 𝑎)} ∈ (ACS‘𝑋))) |
36 | 23, 35 | syl5 34 |
. . . 4
⊢ (𝑋 ∈ 𝑉 → (∀𝑏 ∈ 𝑌 𝐸 ∈ 𝑋 → ∀𝑏 ∈ (𝑋 ∩ 𝑌){𝑎 ∈ 𝒫 𝑋 ∣ ({𝑏} ⊆ 𝑎 → 𝐸 ∈ 𝑎)} ∈ (ACS‘𝑋))) |
37 | 36 | imp 407 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ ∀𝑏 ∈ 𝑌 𝐸 ∈ 𝑋) → ∀𝑏 ∈ (𝑋 ∩ 𝑌){𝑎 ∈ 𝒫 𝑋 ∣ ({𝑏} ⊆ 𝑎 → 𝐸 ∈ 𝑎)} ∈ (ACS‘𝑋)) |
38 | | mreriincl 16857 |
. . 3
⊢
(((ACS‘𝑋)
∈ (Moore‘𝒫 𝑋) ∧ ∀𝑏 ∈ (𝑋 ∩ 𝑌){𝑎 ∈ 𝒫 𝑋 ∣ ({𝑏} ⊆ 𝑎 → 𝐸 ∈ 𝑎)} ∈ (ACS‘𝑋)) → (𝒫 𝑋 ∩ ∩
𝑏 ∈ (𝑋 ∩ 𝑌){𝑎 ∈ 𝒫 𝑋 ∣ ({𝑏} ⊆ 𝑎 → 𝐸 ∈ 𝑎)}) ∈ (ACS‘𝑋)) |
39 | 21, 37, 38 | syl2anc 584 |
. 2
⊢ ((𝑋 ∈ 𝑉 ∧ ∀𝑏 ∈ 𝑌 𝐸 ∈ 𝑋) → (𝒫 𝑋 ∩ ∩
𝑏 ∈ (𝑋 ∩ 𝑌){𝑎 ∈ 𝒫 𝑋 ∣ ({𝑏} ⊆ 𝑎 → 𝐸 ∈ 𝑎)}) ∈ (ACS‘𝑋)) |
40 | 19, 39 | eqeltrrd 2911 |
1
⊢ ((𝑋 ∈ 𝑉 ∧ ∀𝑏 ∈ 𝑌 𝐸 ∈ 𝑋) → {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑏 ∈ (𝑎 ∩ 𝑌)𝐸 ∈ 𝑎} ∈ (ACS‘𝑋)) |