Step | Hyp | Ref
| Expression |
1 | | acsfiindd.1 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ (ACS‘𝑋)) |
2 | 1 | acsmred 17159 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋)) |
3 | 2 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ 𝑆 ∈ 𝐼) ∧ 𝑠 ∈ (𝒫 𝑆 ∩ Fin)) → 𝐴 ∈ (Moore‘𝑋)) |
4 | | acsfiindd.2 |
. . . . 5
⊢ 𝑁 = (mrCls‘𝐴) |
5 | | acsfiindd.3 |
. . . . 5
⊢ 𝐼 = (mrInd‘𝐴) |
6 | | simplr 769 |
. . . . 5
⊢ (((𝜑 ∧ 𝑆 ∈ 𝐼) ∧ 𝑠 ∈ (𝒫 𝑆 ∩ Fin)) → 𝑆 ∈ 𝐼) |
7 | | simpr 488 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑆 ∈ 𝐼) ∧ 𝑠 ∈ (𝒫 𝑆 ∩ Fin)) → 𝑠 ∈ (𝒫 𝑆 ∩ Fin)) |
8 | 7 | elin1d 4112 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑆 ∈ 𝐼) ∧ 𝑠 ∈ (𝒫 𝑆 ∩ Fin)) → 𝑠 ∈ 𝒫 𝑆) |
9 | 8 | elpwid 4524 |
. . . . 5
⊢ (((𝜑 ∧ 𝑆 ∈ 𝐼) ∧ 𝑠 ∈ (𝒫 𝑆 ∩ Fin)) → 𝑠 ⊆ 𝑆) |
10 | 3, 4, 5, 6, 9 | mrissmrid 17144 |
. . . 4
⊢ (((𝜑 ∧ 𝑆 ∈ 𝐼) ∧ 𝑠 ∈ (𝒫 𝑆 ∩ Fin)) → 𝑠 ∈ 𝐼) |
11 | 10 | ralrimiva 3105 |
. . 3
⊢ ((𝜑 ∧ 𝑆 ∈ 𝐼) → ∀𝑠 ∈ (𝒫 𝑆 ∩ Fin)𝑠 ∈ 𝐼) |
12 | | dfss3 3888 |
. . 3
⊢
((𝒫 𝑆 ∩
Fin) ⊆ 𝐼 ↔
∀𝑠 ∈ (𝒫
𝑆 ∩ Fin)𝑠 ∈ 𝐼) |
13 | 11, 12 | sylibr 237 |
. 2
⊢ ((𝜑 ∧ 𝑆 ∈ 𝐼) → (𝒫 𝑆 ∩ Fin) ⊆ 𝐼) |
14 | 2 | adantr 484 |
. . 3
⊢ ((𝜑 ∧ (𝒫 𝑆 ∩ Fin) ⊆ 𝐼) → 𝐴 ∈ (Moore‘𝑋)) |
15 | | acsfiindd.4 |
. . . 4
⊢ (𝜑 → 𝑆 ⊆ 𝑋) |
16 | 15 | adantr 484 |
. . 3
⊢ ((𝜑 ∧ (𝒫 𝑆 ∩ Fin) ⊆ 𝐼) → 𝑆 ⊆ 𝑋) |
17 | | simpr 488 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑡 ∈ (𝒫 (𝑆 ∖ {𝑥}) ∩ Fin)) → 𝑡 ∈ (𝒫 (𝑆 ∖ {𝑥}) ∩ Fin)) |
18 | | elfpw 8978 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 ∈ (𝒫 (𝑆 ∖ {𝑥}) ∩ Fin) ↔ (𝑡 ⊆ (𝑆 ∖ {𝑥}) ∧ 𝑡 ∈ Fin)) |
19 | 17, 18 | sylib 221 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑡 ∈ (𝒫 (𝑆 ∖ {𝑥}) ∩ Fin)) → (𝑡 ⊆ (𝑆 ∖ {𝑥}) ∧ 𝑡 ∈ Fin)) |
20 | 19 | simpld 498 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑡 ∈ (𝒫 (𝑆 ∖ {𝑥}) ∩ Fin)) → 𝑡 ⊆ (𝑆 ∖ {𝑥})) |
21 | 20 | difss2d 4049 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑡 ∈ (𝒫 (𝑆 ∖ {𝑥}) ∩ Fin)) → 𝑡 ⊆ 𝑆) |
22 | | simplr 769 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑡 ∈ (𝒫 (𝑆 ∖ {𝑥}) ∩ Fin)) → 𝑥 ∈ 𝑆) |
23 | 22 | snssd 4722 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑡 ∈ (𝒫 (𝑆 ∖ {𝑥}) ∩ Fin)) → {𝑥} ⊆ 𝑆) |
24 | 21, 23 | unssd 4100 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑡 ∈ (𝒫 (𝑆 ∖ {𝑥}) ∩ Fin)) → (𝑡 ∪ {𝑥}) ⊆ 𝑆) |
25 | 19 | simprd 499 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑡 ∈ (𝒫 (𝑆 ∖ {𝑥}) ∩ Fin)) → 𝑡 ∈ Fin) |
26 | | snfi 8721 |
. . . . . . . . . . . 12
⊢ {𝑥} ∈ Fin |
27 | | unfi 8850 |
. . . . . . . . . . . 12
⊢ ((𝑡 ∈ Fin ∧ {𝑥} ∈ Fin) → (𝑡 ∪ {𝑥}) ∈ Fin) |
28 | 25, 26, 27 | sylancl 589 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑡 ∈ (𝒫 (𝑆 ∖ {𝑥}) ∩ Fin)) → (𝑡 ∪ {𝑥}) ∈ Fin) |
29 | | elfpw 8978 |
. . . . . . . . . . 11
⊢ ((𝑡 ∪ {𝑥}) ∈ (𝒫 𝑆 ∩ Fin) ↔ ((𝑡 ∪ {𝑥}) ⊆ 𝑆 ∧ (𝑡 ∪ {𝑥}) ∈ Fin)) |
30 | 24, 28, 29 | sylanbrc 586 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑡 ∈ (𝒫 (𝑆 ∖ {𝑥}) ∩ Fin)) → (𝑡 ∪ {𝑥}) ∈ (𝒫 𝑆 ∩ Fin)) |
31 | 2 | ad4antr 732 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑡 ∈ (𝒫 (𝑆 ∖ {𝑥}) ∩ Fin)) ∧ 𝑠 = (𝑡 ∪ {𝑥})) ∧ 𝑠 ∈ 𝐼) → 𝐴 ∈ (Moore‘𝑋)) |
32 | | simpr 488 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑡 ∈ (𝒫 (𝑆 ∖ {𝑥}) ∩ Fin)) ∧ 𝑠 = (𝑡 ∪ {𝑥})) ∧ 𝑠 ∈ 𝐼) → 𝑠 ∈ 𝐼) |
33 | | simpllr 776 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑡 ∈ (𝒫 (𝑆 ∖ {𝑥}) ∩ Fin)) ∧ 𝑠 = (𝑡 ∪ {𝑥})) → 𝑥 ∈ 𝑆) |
34 | | snidg 4575 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ 𝑆 → 𝑥 ∈ {𝑥}) |
35 | | elun2 4091 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ {𝑥} → 𝑥 ∈ (𝑡 ∪ {𝑥})) |
36 | 33, 34, 35 | 3syl 18 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑡 ∈ (𝒫 (𝑆 ∖ {𝑥}) ∩ Fin)) ∧ 𝑠 = (𝑡 ∪ {𝑥})) → 𝑥 ∈ (𝑡 ∪ {𝑥})) |
37 | | simpr 488 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑡 ∈ (𝒫 (𝑆 ∖ {𝑥}) ∩ Fin)) ∧ 𝑠 = (𝑡 ∪ {𝑥})) → 𝑠 = (𝑡 ∪ {𝑥})) |
38 | 36, 37 | eleqtrrd 2841 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑡 ∈ (𝒫 (𝑆 ∖ {𝑥}) ∩ Fin)) ∧ 𝑠 = (𝑡 ∪ {𝑥})) → 𝑥 ∈ 𝑠) |
39 | 38 | adantr 484 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑡 ∈ (𝒫 (𝑆 ∖ {𝑥}) ∩ Fin)) ∧ 𝑠 = (𝑡 ∪ {𝑥})) ∧ 𝑠 ∈ 𝐼) → 𝑥 ∈ 𝑠) |
40 | 4, 5, 31, 32, 39 | ismri2dad 17140 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑡 ∈ (𝒫 (𝑆 ∖ {𝑥}) ∩ Fin)) ∧ 𝑠 = (𝑡 ∪ {𝑥})) ∧ 𝑠 ∈ 𝐼) → ¬ 𝑥 ∈ (𝑁‘(𝑠 ∖ {𝑥}))) |
41 | 2 | ad3antrrr 730 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑡 ∈ (𝒫 (𝑆 ∖ {𝑥}) ∩ Fin)) ∧ 𝑠 = (𝑡 ∪ {𝑥})) → 𝐴 ∈ (Moore‘𝑋)) |
42 | 20 | adantr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑡 ∈ (𝒫 (𝑆 ∖ {𝑥}) ∩ Fin)) ∧ 𝑠 = (𝑡 ∪ {𝑥})) → 𝑡 ⊆ (𝑆 ∖ {𝑥})) |
43 | | neldifsnd 4706 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑡 ∈ (𝒫 (𝑆 ∖ {𝑥}) ∩ Fin)) ∧ 𝑠 = (𝑡 ∪ {𝑥})) → ¬ 𝑥 ∈ (𝑆 ∖ {𝑥})) |
44 | 42, 43 | ssneldd 3904 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑡 ∈ (𝒫 (𝑆 ∖ {𝑥}) ∩ Fin)) ∧ 𝑠 = (𝑡 ∪ {𝑥})) → ¬ 𝑥 ∈ 𝑡) |
45 | | difsnb 4719 |
. . . . . . . . . . . . . . . . 17
⊢ (¬
𝑥 ∈ 𝑡 ↔ (𝑡 ∖ {𝑥}) = 𝑡) |
46 | 44, 45 | sylib 221 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑡 ∈ (𝒫 (𝑆 ∖ {𝑥}) ∩ Fin)) ∧ 𝑠 = (𝑡 ∪ {𝑥})) → (𝑡 ∖ {𝑥}) = 𝑡) |
47 | | ssun1 4086 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑡 ⊆ (𝑡 ∪ {𝑥}) |
48 | 47, 37 | sseqtrrid 3954 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑡 ∈ (𝒫 (𝑆 ∖ {𝑥}) ∩ Fin)) ∧ 𝑠 = (𝑡 ∪ {𝑥})) → 𝑡 ⊆ 𝑠) |
49 | 48 | ssdifd 4055 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑡 ∈ (𝒫 (𝑆 ∖ {𝑥}) ∩ Fin)) ∧ 𝑠 = (𝑡 ∪ {𝑥})) → (𝑡 ∖ {𝑥}) ⊆ (𝑠 ∖ {𝑥})) |
50 | 46, 49 | eqsstrrd 3940 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑡 ∈ (𝒫 (𝑆 ∖ {𝑥}) ∩ Fin)) ∧ 𝑠 = (𝑡 ∪ {𝑥})) → 𝑡 ⊆ (𝑠 ∖ {𝑥})) |
51 | 24 | adantr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑡 ∈ (𝒫 (𝑆 ∖ {𝑥}) ∩ Fin)) ∧ 𝑠 = (𝑡 ∪ {𝑥})) → (𝑡 ∪ {𝑥}) ⊆ 𝑆) |
52 | 15 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑡 ∈ (𝒫 (𝑆 ∖ {𝑥}) ∩ Fin)) ∧ 𝑠 = (𝑡 ∪ {𝑥})) → 𝑆 ⊆ 𝑋) |
53 | 51, 52 | sstrd 3911 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑡 ∈ (𝒫 (𝑆 ∖ {𝑥}) ∩ Fin)) ∧ 𝑠 = (𝑡 ∪ {𝑥})) → (𝑡 ∪ {𝑥}) ⊆ 𝑋) |
54 | 37, 53 | eqsstrd 3939 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑡 ∈ (𝒫 (𝑆 ∖ {𝑥}) ∩ Fin)) ∧ 𝑠 = (𝑡 ∪ {𝑥})) → 𝑠 ⊆ 𝑋) |
55 | 54 | ssdifssd 4057 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑡 ∈ (𝒫 (𝑆 ∖ {𝑥}) ∩ Fin)) ∧ 𝑠 = (𝑡 ∪ {𝑥})) → (𝑠 ∖ {𝑥}) ⊆ 𝑋) |
56 | 41, 4, 50, 55 | mrcssd 17127 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑡 ∈ (𝒫 (𝑆 ∖ {𝑥}) ∩ Fin)) ∧ 𝑠 = (𝑡 ∪ {𝑥})) → (𝑁‘𝑡) ⊆ (𝑁‘(𝑠 ∖ {𝑥}))) |
57 | 56 | sseld 3900 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑡 ∈ (𝒫 (𝑆 ∖ {𝑥}) ∩ Fin)) ∧ 𝑠 = (𝑡 ∪ {𝑥})) → (𝑥 ∈ (𝑁‘𝑡) → 𝑥 ∈ (𝑁‘(𝑠 ∖ {𝑥})))) |
58 | 57 | adantr 484 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑡 ∈ (𝒫 (𝑆 ∖ {𝑥}) ∩ Fin)) ∧ 𝑠 = (𝑡 ∪ {𝑥})) ∧ 𝑠 ∈ 𝐼) → (𝑥 ∈ (𝑁‘𝑡) → 𝑥 ∈ (𝑁‘(𝑠 ∖ {𝑥})))) |
59 | 40, 58 | mtod 201 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑡 ∈ (𝒫 (𝑆 ∖ {𝑥}) ∩ Fin)) ∧ 𝑠 = (𝑡 ∪ {𝑥})) ∧ 𝑠 ∈ 𝐼) → ¬ 𝑥 ∈ (𝑁‘𝑡)) |
60 | 59 | ex 416 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑡 ∈ (𝒫 (𝑆 ∖ {𝑥}) ∩ Fin)) ∧ 𝑠 = (𝑡 ∪ {𝑥})) → (𝑠 ∈ 𝐼 → ¬ 𝑥 ∈ (𝑁‘𝑡))) |
61 | 30, 60 | rspcimdv 3527 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑡 ∈ (𝒫 (𝑆 ∖ {𝑥}) ∩ Fin)) → (∀𝑠 ∈ (𝒫 𝑆 ∩ Fin)𝑠 ∈ 𝐼 → ¬ 𝑥 ∈ (𝑁‘𝑡))) |
62 | 12, 61 | syl5bi 245 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑡 ∈ (𝒫 (𝑆 ∖ {𝑥}) ∩ Fin)) → ((𝒫 𝑆 ∩ Fin) ⊆ 𝐼 → ¬ 𝑥 ∈ (𝑁‘𝑡))) |
63 | 62 | impancom 455 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ (𝒫 𝑆 ∩ Fin) ⊆ 𝐼) → (𝑡 ∈ (𝒫 (𝑆 ∖ {𝑥}) ∩ Fin) → ¬ 𝑥 ∈ (𝑁‘𝑡))) |
64 | 63 | ralrimiv 3104 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ (𝒫 𝑆 ∩ Fin) ⊆ 𝐼) → ∀𝑡 ∈ (𝒫 (𝑆 ∖ {𝑥}) ∩ Fin) ¬ 𝑥 ∈ (𝑁‘𝑡)) |
65 | 15 | ssdifssd 4057 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑆 ∖ {𝑥}) ⊆ 𝑋) |
66 | 1, 4, 65 | acsficl2d 18058 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ (𝑁‘(𝑆 ∖ {𝑥})) ↔ ∃𝑡 ∈ (𝒫 (𝑆 ∖ {𝑥}) ∩ Fin)𝑥 ∈ (𝑁‘𝑡))) |
67 | 66 | notbid 321 |
. . . . . . . 8
⊢ (𝜑 → (¬ 𝑥 ∈ (𝑁‘(𝑆 ∖ {𝑥})) ↔ ¬ ∃𝑡 ∈ (𝒫 (𝑆 ∖ {𝑥}) ∩ Fin)𝑥 ∈ (𝑁‘𝑡))) |
68 | | ralnex 3158 |
. . . . . . . 8
⊢
(∀𝑡 ∈
(𝒫 (𝑆 ∖
{𝑥}) ∩ Fin) ¬ 𝑥 ∈ (𝑁‘𝑡) ↔ ¬ ∃𝑡 ∈ (𝒫 (𝑆 ∖ {𝑥}) ∩ Fin)𝑥 ∈ (𝑁‘𝑡)) |
69 | 67, 68 | bitr4di 292 |
. . . . . . 7
⊢ (𝜑 → (¬ 𝑥 ∈ (𝑁‘(𝑆 ∖ {𝑥})) ↔ ∀𝑡 ∈ (𝒫 (𝑆 ∖ {𝑥}) ∩ Fin) ¬ 𝑥 ∈ (𝑁‘𝑡))) |
70 | 69 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ (𝒫 𝑆 ∩ Fin) ⊆ 𝐼) → (¬ 𝑥 ∈ (𝑁‘(𝑆 ∖ {𝑥})) ↔ ∀𝑡 ∈ (𝒫 (𝑆 ∖ {𝑥}) ∩ Fin) ¬ 𝑥 ∈ (𝑁‘𝑡))) |
71 | 64, 70 | mpbird 260 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ (𝒫 𝑆 ∩ Fin) ⊆ 𝐼) → ¬ 𝑥 ∈ (𝑁‘(𝑆 ∖ {𝑥}))) |
72 | 71 | an32s 652 |
. . . 4
⊢ (((𝜑 ∧ (𝒫 𝑆 ∩ Fin) ⊆ 𝐼) ∧ 𝑥 ∈ 𝑆) → ¬ 𝑥 ∈ (𝑁‘(𝑆 ∖ {𝑥}))) |
73 | 72 | ralrimiva 3105 |
. . 3
⊢ ((𝜑 ∧ (𝒫 𝑆 ∩ Fin) ⊆ 𝐼) → ∀𝑥 ∈ 𝑆 ¬ 𝑥 ∈ (𝑁‘(𝑆 ∖ {𝑥}))) |
74 | 4, 5, 14, 16, 73 | ismri2dd 17137 |
. 2
⊢ ((𝜑 ∧ (𝒫 𝑆 ∩ Fin) ⊆ 𝐼) → 𝑆 ∈ 𝐼) |
75 | 13, 74 | impbida 801 |
1
⊢ (𝜑 → (𝑆 ∈ 𝐼 ↔ (𝒫 𝑆 ∩ Fin) ⊆ 𝐼)) |