Proof of Theorem acsfn1p
Step | Hyp | Ref
| Expression |
1 | | riinrab 4532 |
. . 3
⊢
(𝒫 𝑋 ∩
∩ 𝑏 ∈ (𝑋 ∩ 𝑌){𝑎 ∈ 𝒫 𝑋 ∣ ({𝑏} ⊆ 𝑎 → 𝐸 ∈ 𝑎)}) = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑏 ∈ (𝑋 ∩ 𝑌)({𝑏} ⊆ 𝑎 → 𝐸 ∈ 𝑎)} |
2 | | elpwi 4117 |
. . . . . . . 8
⊢ (𝑎 ∈ 𝒫 𝑋 → 𝑎 ⊆ 𝑋) |
3 | | ssrin 3800 |
. . . . . . . 8
⊢ (𝑎 ⊆ 𝑋 → (𝑎 ∩ 𝑌) ⊆ (𝑋 ∩ 𝑌)) |
4 | 2, 3 | syl 17 |
. . . . . . 7
⊢ (𝑎 ∈ 𝒫 𝑋 → (𝑎 ∩ 𝑌) ⊆ (𝑋 ∩ 𝑌)) |
5 | 4 | adantl 481 |
. . . . . 6
⊢ (((𝑋 ∈ 𝑉 ∧ ∀𝑏 ∈ 𝑌 𝐸 ∈ 𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) → (𝑎 ∩ 𝑌) ⊆ (𝑋 ∩ 𝑌)) |
6 | | ralss 3631 |
. . . . . 6
⊢ ((𝑎 ∩ 𝑌) ⊆ (𝑋 ∩ 𝑌) → (∀𝑏 ∈ (𝑎 ∩ 𝑌)𝐸 ∈ 𝑎 ↔ ∀𝑏 ∈ (𝑋 ∩ 𝑌)(𝑏 ∈ (𝑎 ∩ 𝑌) → 𝐸 ∈ 𝑎))) |
7 | 5, 6 | syl 17 |
. . . . 5
⊢ (((𝑋 ∈ 𝑉 ∧ ∀𝑏 ∈ 𝑌 𝐸 ∈ 𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) → (∀𝑏 ∈ (𝑎 ∩ 𝑌)𝐸 ∈ 𝑎 ↔ ∀𝑏 ∈ (𝑋 ∩ 𝑌)(𝑏 ∈ (𝑎 ∩ 𝑌) → 𝐸 ∈ 𝑎))) |
8 | | inss2 3796 |
. . . . . . . . . 10
⊢ (𝑋 ∩ 𝑌) ⊆ 𝑌 |
9 | 8 | sseli 3564 |
. . . . . . . . 9
⊢ (𝑏 ∈ (𝑋 ∩ 𝑌) → 𝑏 ∈ 𝑌) |
10 | 9 | biantrud 527 |
. . . . . . . 8
⊢ (𝑏 ∈ (𝑋 ∩ 𝑌) → (𝑏 ∈ 𝑎 ↔ (𝑏 ∈ 𝑎 ∧ 𝑏 ∈ 𝑌))) |
11 | | vex 3176 |
. . . . . . . . . 10
⊢ 𝑏 ∈ V |
12 | 11 | snss 4259 |
. . . . . . . . 9
⊢ (𝑏 ∈ 𝑎 ↔ {𝑏} ⊆ 𝑎) |
13 | 12 | bicomi 213 |
. . . . . . . 8
⊢ ({𝑏} ⊆ 𝑎 ↔ 𝑏 ∈ 𝑎) |
14 | | elin 3758 |
. . . . . . . 8
⊢ (𝑏 ∈ (𝑎 ∩ 𝑌) ↔ (𝑏 ∈ 𝑎 ∧ 𝑏 ∈ 𝑌)) |
15 | 10, 13, 14 | 3bitr4g 302 |
. . . . . . 7
⊢ (𝑏 ∈ (𝑋 ∩ 𝑌) → ({𝑏} ⊆ 𝑎 ↔ 𝑏 ∈ (𝑎 ∩ 𝑌))) |
16 | 15 | imbi1d 330 |
. . . . . 6
⊢ (𝑏 ∈ (𝑋 ∩ 𝑌) → (({𝑏} ⊆ 𝑎 → 𝐸 ∈ 𝑎) ↔ (𝑏 ∈ (𝑎 ∩ 𝑌) → 𝐸 ∈ 𝑎))) |
17 | 16 | ralbiia 2962 |
. . . . 5
⊢
(∀𝑏 ∈
(𝑋 ∩ 𝑌)({𝑏} ⊆ 𝑎 → 𝐸 ∈ 𝑎) ↔ ∀𝑏 ∈ (𝑋 ∩ 𝑌)(𝑏 ∈ (𝑎 ∩ 𝑌) → 𝐸 ∈ 𝑎)) |
18 | 7, 17 | syl6rbbr 278 |
. . . 4
⊢ (((𝑋 ∈ 𝑉 ∧ ∀𝑏 ∈ 𝑌 𝐸 ∈ 𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) → (∀𝑏 ∈ (𝑋 ∩ 𝑌)({𝑏} ⊆ 𝑎 → 𝐸 ∈ 𝑎) ↔ ∀𝑏 ∈ (𝑎 ∩ 𝑌)𝐸 ∈ 𝑎)) |
19 | 18 | rabbidva 3163 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ ∀𝑏 ∈ 𝑌 𝐸 ∈ 𝑋) → {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑏 ∈ (𝑋 ∩ 𝑌)({𝑏} ⊆ 𝑎 → 𝐸 ∈ 𝑎)} = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑏 ∈ (𝑎 ∩ 𝑌)𝐸 ∈ 𝑎}) |
20 | 1, 19 | syl5eq 2656 |
. 2
⊢ ((𝑋 ∈ 𝑉 ∧ ∀𝑏 ∈ 𝑌 𝐸 ∈ 𝑋) → (𝒫 𝑋 ∩ ∩
𝑏 ∈ (𝑋 ∩ 𝑌){𝑎 ∈ 𝒫 𝑋 ∣ ({𝑏} ⊆ 𝑎 → 𝐸 ∈ 𝑎)}) = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑏 ∈ (𝑎 ∩ 𝑌)𝐸 ∈ 𝑎}) |
21 | | mreacs 16142 |
. . . 4
⊢ (𝑋 ∈ 𝑉 → (ACS‘𝑋) ∈ (Moore‘𝒫 𝑋)) |
22 | 21 | adantr 480 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ ∀𝑏 ∈ 𝑌 𝐸 ∈ 𝑋) → (ACS‘𝑋) ∈ (Moore‘𝒫 𝑋)) |
23 | | ssralv 3629 |
. . . . . 6
⊢ ((𝑋 ∩ 𝑌) ⊆ 𝑌 → (∀𝑏 ∈ 𝑌 𝐸 ∈ 𝑋 → ∀𝑏 ∈ (𝑋 ∩ 𝑌)𝐸 ∈ 𝑋)) |
24 | 8, 23 | ax-mp 5 |
. . . . 5
⊢
(∀𝑏 ∈
𝑌 𝐸 ∈ 𝑋 → ∀𝑏 ∈ (𝑋 ∩ 𝑌)𝐸 ∈ 𝑋) |
25 | | simpll 786 |
. . . . . . . 8
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑏 ∈ (𝑋 ∩ 𝑌)) ∧ 𝐸 ∈ 𝑋) → 𝑋 ∈ 𝑉) |
26 | | simpr 476 |
. . . . . . . 8
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑏 ∈ (𝑋 ∩ 𝑌)) ∧ 𝐸 ∈ 𝑋) → 𝐸 ∈ 𝑋) |
27 | | inss1 3795 |
. . . . . . . . . . 11
⊢ (𝑋 ∩ 𝑌) ⊆ 𝑋 |
28 | 27 | sseli 3564 |
. . . . . . . . . 10
⊢ (𝑏 ∈ (𝑋 ∩ 𝑌) → 𝑏 ∈ 𝑋) |
29 | 28 | ad2antlr 759 |
. . . . . . . . 9
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑏 ∈ (𝑋 ∩ 𝑌)) ∧ 𝐸 ∈ 𝑋) → 𝑏 ∈ 𝑋) |
30 | 29 | snssd 4281 |
. . . . . . . 8
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑏 ∈ (𝑋 ∩ 𝑌)) ∧ 𝐸 ∈ 𝑋) → {𝑏} ⊆ 𝑋) |
31 | | snfi 7923 |
. . . . . . . . 9
⊢ {𝑏} ∈ Fin |
32 | 31 | a1i 11 |
. . . . . . . 8
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑏 ∈ (𝑋 ∩ 𝑌)) ∧ 𝐸 ∈ 𝑋) → {𝑏} ∈ Fin) |
33 | | acsfn 16143 |
. . . . . . . 8
⊢ (((𝑋 ∈ 𝑉 ∧ 𝐸 ∈ 𝑋) ∧ ({𝑏} ⊆ 𝑋 ∧ {𝑏} ∈ Fin)) → {𝑎 ∈ 𝒫 𝑋 ∣ ({𝑏} ⊆ 𝑎 → 𝐸 ∈ 𝑎)} ∈ (ACS‘𝑋)) |
34 | 25, 26, 30, 32, 33 | syl22anc 1319 |
. . . . . . 7
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑏 ∈ (𝑋 ∩ 𝑌)) ∧ 𝐸 ∈ 𝑋) → {𝑎 ∈ 𝒫 𝑋 ∣ ({𝑏} ⊆ 𝑎 → 𝐸 ∈ 𝑎)} ∈ (ACS‘𝑋)) |
35 | 34 | ex 449 |
. . . . . 6
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑏 ∈ (𝑋 ∩ 𝑌)) → (𝐸 ∈ 𝑋 → {𝑎 ∈ 𝒫 𝑋 ∣ ({𝑏} ⊆ 𝑎 → 𝐸 ∈ 𝑎)} ∈ (ACS‘𝑋))) |
36 | 35 | ralimdva 2945 |
. . . . 5
⊢ (𝑋 ∈ 𝑉 → (∀𝑏 ∈ (𝑋 ∩ 𝑌)𝐸 ∈ 𝑋 → ∀𝑏 ∈ (𝑋 ∩ 𝑌){𝑎 ∈ 𝒫 𝑋 ∣ ({𝑏} ⊆ 𝑎 → 𝐸 ∈ 𝑎)} ∈ (ACS‘𝑋))) |
37 | 24, 36 | syl5 33 |
. . . 4
⊢ (𝑋 ∈ 𝑉 → (∀𝑏 ∈ 𝑌 𝐸 ∈ 𝑋 → ∀𝑏 ∈ (𝑋 ∩ 𝑌){𝑎 ∈ 𝒫 𝑋 ∣ ({𝑏} ⊆ 𝑎 → 𝐸 ∈ 𝑎)} ∈ (ACS‘𝑋))) |
38 | 37 | imp 444 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ ∀𝑏 ∈ 𝑌 𝐸 ∈ 𝑋) → ∀𝑏 ∈ (𝑋 ∩ 𝑌){𝑎 ∈ 𝒫 𝑋 ∣ ({𝑏} ⊆ 𝑎 → 𝐸 ∈ 𝑎)} ∈ (ACS‘𝑋)) |
39 | | mreriincl 16081 |
. . 3
⊢
(((ACS‘𝑋)
∈ (Moore‘𝒫 𝑋) ∧ ∀𝑏 ∈ (𝑋 ∩ 𝑌){𝑎 ∈ 𝒫 𝑋 ∣ ({𝑏} ⊆ 𝑎 → 𝐸 ∈ 𝑎)} ∈ (ACS‘𝑋)) → (𝒫 𝑋 ∩ ∩
𝑏 ∈ (𝑋 ∩ 𝑌){𝑎 ∈ 𝒫 𝑋 ∣ ({𝑏} ⊆ 𝑎 → 𝐸 ∈ 𝑎)}) ∈ (ACS‘𝑋)) |
40 | 22, 38, 39 | syl2anc 691 |
. 2
⊢ ((𝑋 ∈ 𝑉 ∧ ∀𝑏 ∈ 𝑌 𝐸 ∈ 𝑋) → (𝒫 𝑋 ∩ ∩
𝑏 ∈ (𝑋 ∩ 𝑌){𝑎 ∈ 𝒫 𝑋 ∣ ({𝑏} ⊆ 𝑎 → 𝐸 ∈ 𝑎)}) ∈ (ACS‘𝑋)) |
41 | 20, 40 | eqeltrrd 2689 |
1
⊢ ((𝑋 ∈ 𝑉 ∧ ∀𝑏 ∈ 𝑌 𝐸 ∈ 𝑋) → {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑏 ∈ (𝑎 ∩ 𝑌)𝐸 ∈ 𝑎} ∈ (ACS‘𝑋)) |