Step | Hyp | Ref
| Expression |
1 | | ominf 8057 |
. . . . 5
⊢ ¬
ω ∈ Fin |
2 | | domfi 8066 |
. . . . . 6
⊢ ((𝐴 ∈ Fin ∧ ω
≼ 𝐴) → ω
∈ Fin) |
3 | 2 | expcom 450 |
. . . . 5
⊢ (ω
≼ 𝐴 → (𝐴 ∈ Fin → ω
∈ Fin)) |
4 | 1, 3 | mtoi 189 |
. . . 4
⊢ (ω
≼ 𝐴 → ¬
𝐴 ∈
Fin) |
5 | | cfinfil 21507 |
. . . 4
⊢ ((𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ¬ 𝐴 ∈ Fin) → {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∖ 𝑥) ∈ Fin} ∈ (Fil‘𝑋)) |
6 | 4, 5 | syl3an3 1353 |
. . 3
⊢ ((𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ω ≼ 𝐴) → {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∖ 𝑥) ∈ Fin} ∈ (Fil‘𝑋)) |
7 | | filssufil 21526 |
. . 3
⊢ ({𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∖ 𝑥) ∈ Fin} ∈ (Fil‘𝑋) → ∃𝑓 ∈ (UFil‘𝑋){𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∖ 𝑥) ∈ Fin} ⊆ 𝑓) |
8 | 6, 7 | syl 17 |
. 2
⊢ ((𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ω ≼ 𝐴) → ∃𝑓 ∈ (UFil‘𝑋){𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∖ 𝑥) ∈ Fin} ⊆ 𝑓) |
9 | | elpw2g 4754 |
. . . . . . . 8
⊢ (𝑋 ∈ 𝐵 → (𝐴 ∈ 𝒫 𝑋 ↔ 𝐴 ⊆ 𝑋)) |
10 | 9 | biimpar 501 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋) → 𝐴 ∈ 𝒫 𝑋) |
11 | 10 | 3adant3 1074 |
. . . . . 6
⊢ ((𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ω ≼ 𝐴) → 𝐴 ∈ 𝒫 𝑋) |
12 | | 0fin 8073 |
. . . . . . 7
⊢ ∅
∈ Fin |
13 | 12 | a1i 11 |
. . . . . 6
⊢ ((𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ω ≼ 𝐴) → ∅ ∈
Fin) |
14 | | difeq2 3684 |
. . . . . . . . 9
⊢ (𝑥 = 𝐴 → (𝐴 ∖ 𝑥) = (𝐴 ∖ 𝐴)) |
15 | | difid 3902 |
. . . . . . . . 9
⊢ (𝐴 ∖ 𝐴) = ∅ |
16 | 14, 15 | syl6eq 2660 |
. . . . . . . 8
⊢ (𝑥 = 𝐴 → (𝐴 ∖ 𝑥) = ∅) |
17 | 16 | eleq1d 2672 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → ((𝐴 ∖ 𝑥) ∈ Fin ↔ ∅ ∈
Fin)) |
18 | 17 | elrab 3331 |
. . . . . 6
⊢ (𝐴 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∖ 𝑥) ∈ Fin} ↔ (𝐴 ∈ 𝒫 𝑋 ∧ ∅ ∈ Fin)) |
19 | 11, 13, 18 | sylanbrc 695 |
. . . . 5
⊢ ((𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ω ≼ 𝐴) → 𝐴 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∖ 𝑥) ∈ Fin}) |
20 | | ssel 3562 |
. . . . 5
⊢ ({𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∖ 𝑥) ∈ Fin} ⊆ 𝑓 → (𝐴 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∖ 𝑥) ∈ Fin} → 𝐴 ∈ 𝑓)) |
21 | 19, 20 | syl5com 31 |
. . . 4
⊢ ((𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ω ≼ 𝐴) → ({𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∖ 𝑥) ∈ Fin} ⊆ 𝑓 → 𝐴 ∈ 𝑓)) |
22 | | intss 4433 |
. . . . . 6
⊢ ({𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∖ 𝑥) ∈ Fin} ⊆ 𝑓 → ∩ 𝑓 ⊆ ∩ {𝑥
∈ 𝒫 𝑋 ∣
(𝐴 ∖ 𝑥) ∈ Fin}) |
23 | | neldifsn 4262 |
. . . . . . . . . 10
⊢ ¬
𝑦 ∈ (𝐴 ∖ {𝑦}) |
24 | | elinti 4420 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ∩ {𝑥
∈ 𝒫 𝑋 ∣
(𝐴 ∖ 𝑥) ∈ Fin} → ((𝐴 ∖ {𝑦}) ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∖ 𝑥) ∈ Fin} → 𝑦 ∈ (𝐴 ∖ {𝑦}))) |
25 | 23, 24 | mtoi 189 |
. . . . . . . . 9
⊢ (𝑦 ∈ ∩ {𝑥
∈ 𝒫 𝑋 ∣
(𝐴 ∖ 𝑥) ∈ Fin} → ¬
(𝐴 ∖ {𝑦}) ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∖ 𝑥) ∈ Fin}) |
26 | | simp2 1055 |
. . . . . . . . . . . 12
⊢ ((𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ω ≼ 𝐴) → 𝐴 ⊆ 𝑋) |
27 | 26 | ssdifssd 3710 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ω ≼ 𝐴) → (𝐴 ∖ {𝑦}) ⊆ 𝑋) |
28 | | elpw2g 4754 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ 𝐵 → ((𝐴 ∖ {𝑦}) ∈ 𝒫 𝑋 ↔ (𝐴 ∖ {𝑦}) ⊆ 𝑋)) |
29 | 28 | 3ad2ant1 1075 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ω ≼ 𝐴) → ((𝐴 ∖ {𝑦}) ∈ 𝒫 𝑋 ↔ (𝐴 ∖ {𝑦}) ⊆ 𝑋)) |
30 | 27, 29 | mpbird 246 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ω ≼ 𝐴) → (𝐴 ∖ {𝑦}) ∈ 𝒫 𝑋) |
31 | | snfi 7923 |
. . . . . . . . . . . 12
⊢ {𝑦} ∈ Fin |
32 | | eldif 3550 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (𝐴 ∖ (𝐴 ∖ {𝑦})) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ (𝐴 ∖ {𝑦}))) |
33 | | eldif 3550 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ (𝐴 ∖ {𝑦}) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ {𝑦})) |
34 | 33 | notbii 309 |
. . . . . . . . . . . . . . . . 17
⊢ (¬
𝑥 ∈ (𝐴 ∖ {𝑦}) ↔ ¬ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ {𝑦})) |
35 | | iman 439 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ {𝑦}) ↔ ¬ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ {𝑦})) |
36 | 34, 35 | bitr4i 266 |
. . . . . . . . . . . . . . . 16
⊢ (¬
𝑥 ∈ (𝐴 ∖ {𝑦}) ↔ (𝑥 ∈ 𝐴 → 𝑥 ∈ {𝑦})) |
37 | 36 | anbi2i 726 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ (𝐴 ∖ {𝑦})) ↔ (𝑥 ∈ 𝐴 ∧ (𝑥 ∈ 𝐴 → 𝑥 ∈ {𝑦}))) |
38 | 32, 37 | bitri 263 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (𝐴 ∖ (𝐴 ∖ {𝑦})) ↔ (𝑥 ∈ 𝐴 ∧ (𝑥 ∈ 𝐴 → 𝑥 ∈ {𝑦}))) |
39 | | pm3.35 609 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ 𝐴 ∧ (𝑥 ∈ 𝐴 → 𝑥 ∈ {𝑦})) → 𝑥 ∈ {𝑦}) |
40 | 38, 39 | sylbi 206 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (𝐴 ∖ (𝐴 ∖ {𝑦})) → 𝑥 ∈ {𝑦}) |
41 | 40 | ssriv 3572 |
. . . . . . . . . . . 12
⊢ (𝐴 ∖ (𝐴 ∖ {𝑦})) ⊆ {𝑦} |
42 | | ssfi 8065 |
. . . . . . . . . . . 12
⊢ (({𝑦} ∈ Fin ∧ (𝐴 ∖ (𝐴 ∖ {𝑦})) ⊆ {𝑦}) → (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin) |
43 | 31, 41, 42 | mp2an 704 |
. . . . . . . . . . 11
⊢ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin |
44 | 43 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ω ≼ 𝐴) → (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin) |
45 | | difeq2 3684 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝐴 ∖ {𝑦}) → (𝐴 ∖ 𝑥) = (𝐴 ∖ (𝐴 ∖ {𝑦}))) |
46 | 45 | eleq1d 2672 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝐴 ∖ {𝑦}) → ((𝐴 ∖ 𝑥) ∈ Fin ↔ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin)) |
47 | 46 | elrab 3331 |
. . . . . . . . . 10
⊢ ((𝐴 ∖ {𝑦}) ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∖ 𝑥) ∈ Fin} ↔ ((𝐴 ∖ {𝑦}) ∈ 𝒫 𝑋 ∧ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin)) |
48 | 30, 44, 47 | sylanbrc 695 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ω ≼ 𝐴) → (𝐴 ∖ {𝑦}) ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∖ 𝑥) ∈ Fin}) |
49 | 25, 48 | nsyl3 132 |
. . . . . . . 8
⊢ ((𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ω ≼ 𝐴) → ¬ 𝑦 ∈ ∩ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∖ 𝑥) ∈ Fin}) |
50 | 49 | eq0rdv 3931 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ω ≼ 𝐴) → ∩ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∖ 𝑥) ∈ Fin} = ∅) |
51 | 50 | sseq2d 3596 |
. . . . . 6
⊢ ((𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ω ≼ 𝐴) → (∩ 𝑓 ⊆ ∩ {𝑥
∈ 𝒫 𝑋 ∣
(𝐴 ∖ 𝑥) ∈ Fin} ↔ ∩ 𝑓
⊆ ∅)) |
52 | 22, 51 | syl5ib 233 |
. . . . 5
⊢ ((𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ω ≼ 𝐴) → ({𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∖ 𝑥) ∈ Fin} ⊆ 𝑓 → ∩ 𝑓 ⊆
∅)) |
53 | | ss0 3926 |
. . . . 5
⊢ (∩ 𝑓
⊆ ∅ → ∩ 𝑓 = ∅) |
54 | 52, 53 | syl6 34 |
. . . 4
⊢ ((𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ω ≼ 𝐴) → ({𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∖ 𝑥) ∈ Fin} ⊆ 𝑓 → ∩ 𝑓 = ∅)) |
55 | 21, 54 | jcad 554 |
. . 3
⊢ ((𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ω ≼ 𝐴) → ({𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∖ 𝑥) ∈ Fin} ⊆ 𝑓 → (𝐴 ∈ 𝑓 ∧ ∩ 𝑓 = ∅))) |
56 | 55 | reximdv 2999 |
. 2
⊢ ((𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ω ≼ 𝐴) → (∃𝑓 ∈ (UFil‘𝑋){𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∖ 𝑥) ∈ Fin} ⊆ 𝑓 → ∃𝑓 ∈ (UFil‘𝑋)(𝐴 ∈ 𝑓 ∧ ∩ 𝑓 = ∅))) |
57 | 8, 56 | mpd 15 |
1
⊢ ((𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ω ≼ 𝐴) → ∃𝑓 ∈ (UFil‘𝑋)(𝐴 ∈ 𝑓 ∧ ∩ 𝑓 = ∅)) |