| Step | Hyp | Ref
| Expression |
| 1 | | ominf 9294 |
. . . . 5
⊢ ¬
ω ∈ Fin |
| 2 | | domfi 9229 |
. . . . . 6
⊢ ((𝐴 ∈ Fin ∧ ω
≼ 𝐴) → ω
∈ Fin) |
| 3 | 2 | expcom 413 |
. . . . 5
⊢ (ω
≼ 𝐴 → (𝐴 ∈ Fin → ω
∈ Fin)) |
| 4 | 1, 3 | mtoi 199 |
. . . 4
⊢ (ω
≼ 𝐴 → ¬
𝐴 ∈
Fin) |
| 5 | | cfinfil 23901 |
. . . 4
⊢ ((𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ¬ 𝐴 ∈ Fin) → {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∖ 𝑥) ∈ Fin} ∈ (Fil‘𝑋)) |
| 6 | 4, 5 | syl3an3 1166 |
. . 3
⊢ ((𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ω ≼ 𝐴) → {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∖ 𝑥) ∈ Fin} ∈ (Fil‘𝑋)) |
| 7 | | filssufil 23920 |
. . 3
⊢ ({𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∖ 𝑥) ∈ Fin} ∈ (Fil‘𝑋) → ∃𝑓 ∈ (UFil‘𝑋){𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∖ 𝑥) ∈ Fin} ⊆ 𝑓) |
| 8 | 6, 7 | syl 17 |
. 2
⊢ ((𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ω ≼ 𝐴) → ∃𝑓 ∈ (UFil‘𝑋){𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∖ 𝑥) ∈ Fin} ⊆ 𝑓) |
| 9 | | difeq2 4120 |
. . . . . . . 8
⊢ (𝑥 = 𝐴 → (𝐴 ∖ 𝑥) = (𝐴 ∖ 𝐴)) |
| 10 | | difid 4376 |
. . . . . . . 8
⊢ (𝐴 ∖ 𝐴) = ∅ |
| 11 | 9, 10 | eqtrdi 2793 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → (𝐴 ∖ 𝑥) = ∅) |
| 12 | 11 | eleq1d 2826 |
. . . . . 6
⊢ (𝑥 = 𝐴 → ((𝐴 ∖ 𝑥) ∈ Fin ↔ ∅ ∈
Fin)) |
| 13 | | elpw2g 5333 |
. . . . . . . 8
⊢ (𝑋 ∈ 𝐵 → (𝐴 ∈ 𝒫 𝑋 ↔ 𝐴 ⊆ 𝑋)) |
| 14 | 13 | biimpar 477 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋) → 𝐴 ∈ 𝒫 𝑋) |
| 15 | 14 | 3adant3 1133 |
. . . . . 6
⊢ ((𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ω ≼ 𝐴) → 𝐴 ∈ 𝒫 𝑋) |
| 16 | | 0fi 9082 |
. . . . . . 7
⊢ ∅
∈ Fin |
| 17 | 16 | a1i 11 |
. . . . . 6
⊢ ((𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ω ≼ 𝐴) → ∅ ∈
Fin) |
| 18 | 12, 15, 17 | elrabd 3694 |
. . . . 5
⊢ ((𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ω ≼ 𝐴) → 𝐴 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∖ 𝑥) ∈ Fin}) |
| 19 | | ssel 3977 |
. . . . 5
⊢ ({𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∖ 𝑥) ∈ Fin} ⊆ 𝑓 → (𝐴 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∖ 𝑥) ∈ Fin} → 𝐴 ∈ 𝑓)) |
| 20 | 18, 19 | syl5com 31 |
. . . 4
⊢ ((𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ω ≼ 𝐴) → ({𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∖ 𝑥) ∈ Fin} ⊆ 𝑓 → 𝐴 ∈ 𝑓)) |
| 21 | | intss 4969 |
. . . . . 6
⊢ ({𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∖ 𝑥) ∈ Fin} ⊆ 𝑓 → ∩ 𝑓 ⊆ ∩ {𝑥
∈ 𝒫 𝑋 ∣
(𝐴 ∖ 𝑥) ∈ Fin}) |
| 22 | | neldifsn 4792 |
. . . . . . . . . 10
⊢ ¬
𝑦 ∈ (𝐴 ∖ {𝑦}) |
| 23 | | elinti 4955 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ∩ {𝑥
∈ 𝒫 𝑋 ∣
(𝐴 ∖ 𝑥) ∈ Fin} → ((𝐴 ∖ {𝑦}) ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∖ 𝑥) ∈ Fin} → 𝑦 ∈ (𝐴 ∖ {𝑦}))) |
| 24 | 22, 23 | mtoi 199 |
. . . . . . . . 9
⊢ (𝑦 ∈ ∩ {𝑥
∈ 𝒫 𝑋 ∣
(𝐴 ∖ 𝑥) ∈ Fin} → ¬
(𝐴 ∖ {𝑦}) ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∖ 𝑥) ∈ Fin}) |
| 25 | | difeq2 4120 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝐴 ∖ {𝑦}) → (𝐴 ∖ 𝑥) = (𝐴 ∖ (𝐴 ∖ {𝑦}))) |
| 26 | 25 | eleq1d 2826 |
. . . . . . . . . 10
⊢ (𝑥 = (𝐴 ∖ {𝑦}) → ((𝐴 ∖ 𝑥) ∈ Fin ↔ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin)) |
| 27 | | simp2 1138 |
. . . . . . . . . . . 12
⊢ ((𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ω ≼ 𝐴) → 𝐴 ⊆ 𝑋) |
| 28 | 27 | ssdifssd 4147 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ω ≼ 𝐴) → (𝐴 ∖ {𝑦}) ⊆ 𝑋) |
| 29 | | elpw2g 5333 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ 𝐵 → ((𝐴 ∖ {𝑦}) ∈ 𝒫 𝑋 ↔ (𝐴 ∖ {𝑦}) ⊆ 𝑋)) |
| 30 | 29 | 3ad2ant1 1134 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ω ≼ 𝐴) → ((𝐴 ∖ {𝑦}) ∈ 𝒫 𝑋 ↔ (𝐴 ∖ {𝑦}) ⊆ 𝑋)) |
| 31 | 28, 30 | mpbird 257 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ω ≼ 𝐴) → (𝐴 ∖ {𝑦}) ∈ 𝒫 𝑋) |
| 32 | | snfi 9083 |
. . . . . . . . . . . 12
⊢ {𝑦} ∈ Fin |
| 33 | | eldif 3961 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (𝐴 ∖ (𝐴 ∖ {𝑦})) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ (𝐴 ∖ {𝑦}))) |
| 34 | | eldif 3961 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ (𝐴 ∖ {𝑦}) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ {𝑦})) |
| 35 | 34 | notbii 320 |
. . . . . . . . . . . . . . . . 17
⊢ (¬
𝑥 ∈ (𝐴 ∖ {𝑦}) ↔ ¬ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ {𝑦})) |
| 36 | | iman 401 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ {𝑦}) ↔ ¬ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ {𝑦})) |
| 37 | 35, 36 | bitr4i 278 |
. . . . . . . . . . . . . . . 16
⊢ (¬
𝑥 ∈ (𝐴 ∖ {𝑦}) ↔ (𝑥 ∈ 𝐴 → 𝑥 ∈ {𝑦})) |
| 38 | 37 | anbi2i 623 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ (𝐴 ∖ {𝑦})) ↔ (𝑥 ∈ 𝐴 ∧ (𝑥 ∈ 𝐴 → 𝑥 ∈ {𝑦}))) |
| 39 | 33, 38 | bitri 275 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (𝐴 ∖ (𝐴 ∖ {𝑦})) ↔ (𝑥 ∈ 𝐴 ∧ (𝑥 ∈ 𝐴 → 𝑥 ∈ {𝑦}))) |
| 40 | | pm3.35 803 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ 𝐴 ∧ (𝑥 ∈ 𝐴 → 𝑥 ∈ {𝑦})) → 𝑥 ∈ {𝑦}) |
| 41 | 39, 40 | sylbi 217 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (𝐴 ∖ (𝐴 ∖ {𝑦})) → 𝑥 ∈ {𝑦}) |
| 42 | 41 | ssriv 3987 |
. . . . . . . . . . . 12
⊢ (𝐴 ∖ (𝐴 ∖ {𝑦})) ⊆ {𝑦} |
| 43 | | ssfi 9213 |
. . . . . . . . . . . 12
⊢ (({𝑦} ∈ Fin ∧ (𝐴 ∖ (𝐴 ∖ {𝑦})) ⊆ {𝑦}) → (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin) |
| 44 | 32, 42, 43 | mp2an 692 |
. . . . . . . . . . 11
⊢ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin |
| 45 | 44 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ω ≼ 𝐴) → (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin) |
| 46 | 26, 31, 45 | elrabd 3694 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ω ≼ 𝐴) → (𝐴 ∖ {𝑦}) ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∖ 𝑥) ∈ Fin}) |
| 47 | 24, 46 | nsyl3 138 |
. . . . . . . 8
⊢ ((𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ω ≼ 𝐴) → ¬ 𝑦 ∈ ∩ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∖ 𝑥) ∈ Fin}) |
| 48 | 47 | eq0rdv 4407 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ω ≼ 𝐴) → ∩ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∖ 𝑥) ∈ Fin} = ∅) |
| 49 | 48 | sseq2d 4016 |
. . . . . 6
⊢ ((𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ω ≼ 𝐴) → (∩ 𝑓 ⊆ ∩ {𝑥
∈ 𝒫 𝑋 ∣
(𝐴 ∖ 𝑥) ∈ Fin} ↔ ∩ 𝑓
⊆ ∅)) |
| 50 | 21, 49 | imbitrid 244 |
. . . . 5
⊢ ((𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ω ≼ 𝐴) → ({𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∖ 𝑥) ∈ Fin} ⊆ 𝑓 → ∩ 𝑓 ⊆
∅)) |
| 51 | | ss0 4402 |
. . . . 5
⊢ (∩ 𝑓
⊆ ∅ → ∩ 𝑓 = ∅) |
| 52 | 50, 51 | syl6 35 |
. . . 4
⊢ ((𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ω ≼ 𝐴) → ({𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∖ 𝑥) ∈ Fin} ⊆ 𝑓 → ∩ 𝑓 = ∅)) |
| 53 | 20, 52 | jcad 512 |
. . 3
⊢ ((𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ω ≼ 𝐴) → ({𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∖ 𝑥) ∈ Fin} ⊆ 𝑓 → (𝐴 ∈ 𝑓 ∧ ∩ 𝑓 = ∅))) |
| 54 | 53 | reximdv 3170 |
. 2
⊢ ((𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ω ≼ 𝐴) → (∃𝑓 ∈ (UFil‘𝑋){𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∖ 𝑥) ∈ Fin} ⊆ 𝑓 → ∃𝑓 ∈ (UFil‘𝑋)(𝐴 ∈ 𝑓 ∧ ∩ 𝑓 = ∅))) |
| 55 | 8, 54 | mpd 15 |
1
⊢ ((𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ω ≼ 𝐴) → ∃𝑓 ∈ (UFil‘𝑋)(𝐴 ∈ 𝑓 ∧ ∩ 𝑓 = ∅)) |