| Step | Hyp | Ref
| Expression |
| 1 | | elpwi 4607 |
. . . . 5
⊢ (𝑥 ∈ 𝒫 𝑋 → 𝑥 ⊆ 𝑋) |
| 2 | | ufilb 23914 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑥 ⊆ 𝑋) → (¬ 𝑥 ∈ 𝐹 ↔ (𝑋 ∖ 𝑥) ∈ 𝐹)) |
| 3 | 2 | adantr 480 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (UFil‘𝑋) ∧ 𝑥 ⊆ 𝑋) ∧ (𝑋 ∖ 𝑥) ∈ Fin) → (¬ 𝑥 ∈ 𝐹 ↔ (𝑋 ∖ 𝑥) ∈ 𝐹)) |
| 4 | | ufilfil 23912 |
. . . . . . . . . . . 12
⊢ (𝐹 ∈ (UFil‘𝑋) → 𝐹 ∈ (Fil‘𝑋)) |
| 5 | 4 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑥 ⊆ 𝑋) → 𝐹 ∈ (Fil‘𝑋)) |
| 6 | | filfinnfr 23885 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑋 ∖ 𝑥) ∈ 𝐹 ∧ (𝑋 ∖ 𝑥) ∈ Fin) → ∩ 𝐹
≠ ∅) |
| 7 | 6 | 3exp 1120 |
. . . . . . . . . . . 12
⊢ (𝐹 ∈ (Fil‘𝑋) → ((𝑋 ∖ 𝑥) ∈ 𝐹 → ((𝑋 ∖ 𝑥) ∈ Fin → ∩ 𝐹
≠ ∅))) |
| 8 | 7 | com23 86 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ (Fil‘𝑋) → ((𝑋 ∖ 𝑥) ∈ Fin → ((𝑋 ∖ 𝑥) ∈ 𝐹 → ∩ 𝐹 ≠
∅))) |
| 9 | 5, 8 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑥 ⊆ 𝑋) → ((𝑋 ∖ 𝑥) ∈ Fin → ((𝑋 ∖ 𝑥) ∈ 𝐹 → ∩ 𝐹 ≠
∅))) |
| 10 | 9 | imp 406 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (UFil‘𝑋) ∧ 𝑥 ⊆ 𝑋) ∧ (𝑋 ∖ 𝑥) ∈ Fin) → ((𝑋 ∖ 𝑥) ∈ 𝐹 → ∩ 𝐹 ≠ ∅)) |
| 11 | 3, 10 | sylbid 240 |
. . . . . . . 8
⊢ (((𝐹 ∈ (UFil‘𝑋) ∧ 𝑥 ⊆ 𝑋) ∧ (𝑋 ∖ 𝑥) ∈ Fin) → (¬ 𝑥 ∈ 𝐹 → ∩ 𝐹 ≠ ∅)) |
| 12 | 11 | necon4bd 2960 |
. . . . . . 7
⊢ (((𝐹 ∈ (UFil‘𝑋) ∧ 𝑥 ⊆ 𝑋) ∧ (𝑋 ∖ 𝑥) ∈ Fin) → (∩ 𝐹 =
∅ → 𝑥 ∈
𝐹)) |
| 13 | 12 | ex 412 |
. . . . . 6
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑥 ⊆ 𝑋) → ((𝑋 ∖ 𝑥) ∈ Fin → (∩ 𝐹 =
∅ → 𝑥 ∈
𝐹))) |
| 14 | 13 | com23 86 |
. . . . 5
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑥 ⊆ 𝑋) → (∩ 𝐹 = ∅ → ((𝑋 ∖ 𝑥) ∈ Fin → 𝑥 ∈ 𝐹))) |
| 15 | 1, 14 | sylan2 593 |
. . . 4
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑥 ∈ 𝒫 𝑋) → (∩ 𝐹 = ∅ → ((𝑋 ∖ 𝑥) ∈ Fin → 𝑥 ∈ 𝐹))) |
| 16 | 15 | ralrimdva 3154 |
. . 3
⊢ (𝐹 ∈ (UFil‘𝑋) → (∩ 𝐹 =
∅ → ∀𝑥
∈ 𝒫 𝑋((𝑋 ∖ 𝑥) ∈ Fin → 𝑥 ∈ 𝐹))) |
| 17 | 4 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑦 ∈ ∩ 𝐹) → 𝐹 ∈ (Fil‘𝑋)) |
| 18 | | uffixsn 23933 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑦 ∈ ∩ 𝐹) → {𝑦} ∈ 𝐹) |
| 19 | | filelss 23860 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ {𝑦} ∈ 𝐹) → {𝑦} ⊆ 𝑋) |
| 20 | 17, 18, 19 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑦 ∈ ∩ 𝐹) → {𝑦} ⊆ 𝑋) |
| 21 | | dfss4 4269 |
. . . . . . . . . . 11
⊢ ({𝑦} ⊆ 𝑋 ↔ (𝑋 ∖ (𝑋 ∖ {𝑦})) = {𝑦}) |
| 22 | 20, 21 | sylib 218 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑦 ∈ ∩ 𝐹) → (𝑋 ∖ (𝑋 ∖ {𝑦})) = {𝑦}) |
| 23 | | snfi 9083 |
. . . . . . . . . 10
⊢ {𝑦} ∈ Fin |
| 24 | 22, 23 | eqeltrdi 2849 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑦 ∈ ∩ 𝐹) → (𝑋 ∖ (𝑋 ∖ {𝑦})) ∈ Fin) |
| 25 | | difss 4136 |
. . . . . . . . . . 11
⊢ (𝑋 ∖ {𝑦}) ⊆ 𝑋 |
| 26 | | filtop 23863 |
. . . . . . . . . . . 12
⊢ (𝐹 ∈ (Fil‘𝑋) → 𝑋 ∈ 𝐹) |
| 27 | | elpw2g 5333 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ 𝐹 → ((𝑋 ∖ {𝑦}) ∈ 𝒫 𝑋 ↔ (𝑋 ∖ {𝑦}) ⊆ 𝑋)) |
| 28 | 17, 26, 27 | 3syl 18 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑦 ∈ ∩ 𝐹) → ((𝑋 ∖ {𝑦}) ∈ 𝒫 𝑋 ↔ (𝑋 ∖ {𝑦}) ⊆ 𝑋)) |
| 29 | 25, 28 | mpbiri 258 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑦 ∈ ∩ 𝐹) → (𝑋 ∖ {𝑦}) ∈ 𝒫 𝑋) |
| 30 | | difeq2 4120 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝑋 ∖ {𝑦}) → (𝑋 ∖ 𝑥) = (𝑋 ∖ (𝑋 ∖ {𝑦}))) |
| 31 | 30 | eleq1d 2826 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑋 ∖ {𝑦}) → ((𝑋 ∖ 𝑥) ∈ Fin ↔ (𝑋 ∖ (𝑋 ∖ {𝑦})) ∈ Fin)) |
| 32 | | eleq1 2829 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑋 ∖ {𝑦}) → (𝑥 ∈ 𝐹 ↔ (𝑋 ∖ {𝑦}) ∈ 𝐹)) |
| 33 | 31, 32 | imbi12d 344 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑋 ∖ {𝑦}) → (((𝑋 ∖ 𝑥) ∈ Fin → 𝑥 ∈ 𝐹) ↔ ((𝑋 ∖ (𝑋 ∖ {𝑦})) ∈ Fin → (𝑋 ∖ {𝑦}) ∈ 𝐹))) |
| 34 | 33 | rspcv 3618 |
. . . . . . . . . 10
⊢ ((𝑋 ∖ {𝑦}) ∈ 𝒫 𝑋 → (∀𝑥 ∈ 𝒫 𝑋((𝑋 ∖ 𝑥) ∈ Fin → 𝑥 ∈ 𝐹) → ((𝑋 ∖ (𝑋 ∖ {𝑦})) ∈ Fin → (𝑋 ∖ {𝑦}) ∈ 𝐹))) |
| 35 | 29, 34 | syl 17 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑦 ∈ ∩ 𝐹) → (∀𝑥 ∈ 𝒫 𝑋((𝑋 ∖ 𝑥) ∈ Fin → 𝑥 ∈ 𝐹) → ((𝑋 ∖ (𝑋 ∖ {𝑦})) ∈ Fin → (𝑋 ∖ {𝑦}) ∈ 𝐹))) |
| 36 | 24, 35 | mpid 44 |
. . . . . . . 8
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑦 ∈ ∩ 𝐹) → (∀𝑥 ∈ 𝒫 𝑋((𝑋 ∖ 𝑥) ∈ Fin → 𝑥 ∈ 𝐹) → (𝑋 ∖ {𝑦}) ∈ 𝐹)) |
| 37 | | ufilb 23914 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ {𝑦} ⊆ 𝑋) → (¬ {𝑦} ∈ 𝐹 ↔ (𝑋 ∖ {𝑦}) ∈ 𝐹)) |
| 38 | 20, 37 | syldan 591 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑦 ∈ ∩ 𝐹) → (¬ {𝑦} ∈ 𝐹 ↔ (𝑋 ∖ {𝑦}) ∈ 𝐹)) |
| 39 | 18 | pm2.24d 151 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑦 ∈ ∩ 𝐹) → (¬ {𝑦} ∈ 𝐹 → ¬ 𝑦 ∈ ∩ 𝐹)) |
| 40 | 38, 39 | sylbird 260 |
. . . . . . . 8
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑦 ∈ ∩ 𝐹) → ((𝑋 ∖ {𝑦}) ∈ 𝐹 → ¬ 𝑦 ∈ ∩ 𝐹)) |
| 41 | 36, 40 | syld 47 |
. . . . . . 7
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑦 ∈ ∩ 𝐹) → (∀𝑥 ∈ 𝒫 𝑋((𝑋 ∖ 𝑥) ∈ Fin → 𝑥 ∈ 𝐹) → ¬ 𝑦 ∈ ∩ 𝐹)) |
| 42 | 41 | impancom 451 |
. . . . . 6
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ ∀𝑥 ∈ 𝒫 𝑋((𝑋 ∖ 𝑥) ∈ Fin → 𝑥 ∈ 𝐹)) → (𝑦 ∈ ∩ 𝐹 → ¬ 𝑦 ∈ ∩ 𝐹)) |
| 43 | 42 | pm2.01d 190 |
. . . . 5
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ ∀𝑥 ∈ 𝒫 𝑋((𝑋 ∖ 𝑥) ∈ Fin → 𝑥 ∈ 𝐹)) → ¬ 𝑦 ∈ ∩ 𝐹) |
| 44 | 43 | eq0rdv 4407 |
. . . 4
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ ∀𝑥 ∈ 𝒫 𝑋((𝑋 ∖ 𝑥) ∈ Fin → 𝑥 ∈ 𝐹)) → ∩ 𝐹 = ∅) |
| 45 | 44 | ex 412 |
. . 3
⊢ (𝐹 ∈ (UFil‘𝑋) → (∀𝑥 ∈ 𝒫 𝑋((𝑋 ∖ 𝑥) ∈ Fin → 𝑥 ∈ 𝐹) → ∩ 𝐹 = ∅)) |
| 46 | 16, 45 | impbid 212 |
. 2
⊢ (𝐹 ∈ (UFil‘𝑋) → (∩ 𝐹 =
∅ ↔ ∀𝑥
∈ 𝒫 𝑋((𝑋 ∖ 𝑥) ∈ Fin → 𝑥 ∈ 𝐹))) |
| 47 | | rabss 4072 |
. 2
⊢ ({𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ∈ Fin} ⊆ 𝐹 ↔ ∀𝑥 ∈ 𝒫 𝑋((𝑋 ∖ 𝑥) ∈ Fin → 𝑥 ∈ 𝐹)) |
| 48 | 46, 47 | bitr4di 289 |
1
⊢ (𝐹 ∈ (UFil‘𝑋) → (∩ 𝐹 =
∅ ↔ {𝑥 ∈
𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ∈ Fin} ⊆ 𝐹)) |