Step | Hyp | Ref
| Expression |
1 | | reldom 8632 |
. . . . . 6
⊢ Rel
≼ |
2 | 1 | brrelex2i 5606 |
. . . . 5
⊢ (ω
≼ 𝑋 → 𝑋 ∈ V) |
3 | | numth3 10084 |
. . . . 5
⊢ (𝑋 ∈ V → 𝑋 ∈ dom
card) |
4 | 2, 3 | syl 17 |
. . . 4
⊢ (ω
≼ 𝑋 → 𝑋 ∈ dom
card) |
5 | | csdfil 22791 |
. . . 4
⊢ ((𝑋 ∈ dom card ∧ ω
≼ 𝑋) → {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑦) ≺ 𝑋} ∈ (Fil‘𝑋)) |
6 | 4, 5 | mpancom 688 |
. . 3
⊢ (ω
≼ 𝑋 → {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑦) ≺ 𝑋} ∈ (Fil‘𝑋)) |
7 | | filssufil 22809 |
. . 3
⊢ ({𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑦) ≺ 𝑋} ∈ (Fil‘𝑋) → ∃𝑓 ∈ (UFil‘𝑋){𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑦) ≺ 𝑋} ⊆ 𝑓) |
8 | 6, 7 | syl 17 |
. 2
⊢ (ω
≼ 𝑋 →
∃𝑓 ∈
(UFil‘𝑋){𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑦) ≺ 𝑋} ⊆ 𝑓) |
9 | | elfvex 6750 |
. . . . . . 7
⊢ (𝑓 ∈ (UFil‘𝑋) → 𝑋 ∈ V) |
10 | 9 | ad2antlr 727 |
. . . . . 6
⊢
(((ω ≼ 𝑋
∧ 𝑓 ∈
(UFil‘𝑋)) ∧ 𝑥 ∈ 𝑓) → 𝑋 ∈ V) |
11 | | ufilfil 22801 |
. . . . . . . 8
⊢ (𝑓 ∈ (UFil‘𝑋) → 𝑓 ∈ (Fil‘𝑋)) |
12 | | filelss 22749 |
. . . . . . . 8
⊢ ((𝑓 ∈ (Fil‘𝑋) ∧ 𝑥 ∈ 𝑓) → 𝑥 ⊆ 𝑋) |
13 | 11, 12 | sylan 583 |
. . . . . . 7
⊢ ((𝑓 ∈ (UFil‘𝑋) ∧ 𝑥 ∈ 𝑓) → 𝑥 ⊆ 𝑋) |
14 | 13 | adantll 714 |
. . . . . 6
⊢
(((ω ≼ 𝑋
∧ 𝑓 ∈
(UFil‘𝑋)) ∧ 𝑥 ∈ 𝑓) → 𝑥 ⊆ 𝑋) |
15 | | ssdomg 8674 |
. . . . . 6
⊢ (𝑋 ∈ V → (𝑥 ⊆ 𝑋 → 𝑥 ≼ 𝑋)) |
16 | 10, 14, 15 | sylc 65 |
. . . . 5
⊢
(((ω ≼ 𝑋
∧ 𝑓 ∈
(UFil‘𝑋)) ∧ 𝑥 ∈ 𝑓) → 𝑥 ≼ 𝑋) |
17 | | filfbas 22745 |
. . . . . . . . 9
⊢ (𝑓 ∈ (Fil‘𝑋) → 𝑓 ∈ (fBas‘𝑋)) |
18 | 11, 17 | syl 17 |
. . . . . . . 8
⊢ (𝑓 ∈ (UFil‘𝑋) → 𝑓 ∈ (fBas‘𝑋)) |
19 | 18 | adantl 485 |
. . . . . . 7
⊢ ((ω
≼ 𝑋 ∧ 𝑓 ∈ (UFil‘𝑋)) → 𝑓 ∈ (fBas‘𝑋)) |
20 | | fbncp 22736 |
. . . . . . 7
⊢ ((𝑓 ∈ (fBas‘𝑋) ∧ 𝑥 ∈ 𝑓) → ¬ (𝑋 ∖ 𝑥) ∈ 𝑓) |
21 | 19, 20 | sylan 583 |
. . . . . 6
⊢
(((ω ≼ 𝑋
∧ 𝑓 ∈
(UFil‘𝑋)) ∧ 𝑥 ∈ 𝑓) → ¬ (𝑋 ∖ 𝑥) ∈ 𝑓) |
22 | | difeq2 4031 |
. . . . . . . . . . . . 13
⊢ (𝑦 = (𝑋 ∖ 𝑥) → (𝑋 ∖ 𝑦) = (𝑋 ∖ (𝑋 ∖ 𝑥))) |
23 | 22 | breq1d 5063 |
. . . . . . . . . . . 12
⊢ (𝑦 = (𝑋 ∖ 𝑥) → ((𝑋 ∖ 𝑦) ≺ 𝑋 ↔ (𝑋 ∖ (𝑋 ∖ 𝑥)) ≺ 𝑋)) |
24 | | difss 4046 |
. . . . . . . . . . . . . 14
⊢ (𝑋 ∖ 𝑥) ⊆ 𝑋 |
25 | | elpw2g 5237 |
. . . . . . . . . . . . . 14
⊢ (𝑋 ∈ V → ((𝑋 ∖ 𝑥) ∈ 𝒫 𝑋 ↔ (𝑋 ∖ 𝑥) ⊆ 𝑋)) |
26 | 24, 25 | mpbiri 261 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∈ V → (𝑋 ∖ 𝑥) ∈ 𝒫 𝑋) |
27 | 26 | 3ad2ant1 1135 |
. . . . . . . . . . . 12
⊢ ((𝑋 ∈ V ∧ 𝑥 ⊆ 𝑋 ∧ 𝑥 ≺ 𝑋) → (𝑋 ∖ 𝑥) ∈ 𝒫 𝑋) |
28 | | simp2 1139 |
. . . . . . . . . . . . . 14
⊢ ((𝑋 ∈ V ∧ 𝑥 ⊆ 𝑋 ∧ 𝑥 ≺ 𝑋) → 𝑥 ⊆ 𝑋) |
29 | | dfss4 4173 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ⊆ 𝑋 ↔ (𝑋 ∖ (𝑋 ∖ 𝑥)) = 𝑥) |
30 | 28, 29 | sylib 221 |
. . . . . . . . . . . . 13
⊢ ((𝑋 ∈ V ∧ 𝑥 ⊆ 𝑋 ∧ 𝑥 ≺ 𝑋) → (𝑋 ∖ (𝑋 ∖ 𝑥)) = 𝑥) |
31 | | simp3 1140 |
. . . . . . . . . . . . 13
⊢ ((𝑋 ∈ V ∧ 𝑥 ⊆ 𝑋 ∧ 𝑥 ≺ 𝑋) → 𝑥 ≺ 𝑋) |
32 | 30, 31 | eqbrtrd 5075 |
. . . . . . . . . . . 12
⊢ ((𝑋 ∈ V ∧ 𝑥 ⊆ 𝑋 ∧ 𝑥 ≺ 𝑋) → (𝑋 ∖ (𝑋 ∖ 𝑥)) ≺ 𝑋) |
33 | 23, 27, 32 | elrabd 3604 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ V ∧ 𝑥 ⊆ 𝑋 ∧ 𝑥 ≺ 𝑋) → (𝑋 ∖ 𝑥) ∈ {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑦) ≺ 𝑋}) |
34 | | ssel 3893 |
. . . . . . . . . . 11
⊢ ({𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑦) ≺ 𝑋} ⊆ 𝑓 → ((𝑋 ∖ 𝑥) ∈ {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑦) ≺ 𝑋} → (𝑋 ∖ 𝑥) ∈ 𝑓)) |
35 | 33, 34 | syl5com 31 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ V ∧ 𝑥 ⊆ 𝑋 ∧ 𝑥 ≺ 𝑋) → ({𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑦) ≺ 𝑋} ⊆ 𝑓 → (𝑋 ∖ 𝑥) ∈ 𝑓)) |
36 | 35 | 3expa 1120 |
. . . . . . . . 9
⊢ (((𝑋 ∈ V ∧ 𝑥 ⊆ 𝑋) ∧ 𝑥 ≺ 𝑋) → ({𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑦) ≺ 𝑋} ⊆ 𝑓 → (𝑋 ∖ 𝑥) ∈ 𝑓)) |
37 | 36 | impancom 455 |
. . . . . . . 8
⊢ (((𝑋 ∈ V ∧ 𝑥 ⊆ 𝑋) ∧ {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑦) ≺ 𝑋} ⊆ 𝑓) → (𝑥 ≺ 𝑋 → (𝑋 ∖ 𝑥) ∈ 𝑓)) |
38 | 37 | con3d 155 |
. . . . . . 7
⊢ (((𝑋 ∈ V ∧ 𝑥 ⊆ 𝑋) ∧ {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑦) ≺ 𝑋} ⊆ 𝑓) → (¬ (𝑋 ∖ 𝑥) ∈ 𝑓 → ¬ 𝑥 ≺ 𝑋)) |
39 | 38 | impancom 455 |
. . . . . 6
⊢ (((𝑋 ∈ V ∧ 𝑥 ⊆ 𝑋) ∧ ¬ (𝑋 ∖ 𝑥) ∈ 𝑓) → ({𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑦) ≺ 𝑋} ⊆ 𝑓 → ¬ 𝑥 ≺ 𝑋)) |
40 | 10, 14, 21, 39 | syl21anc 838 |
. . . . 5
⊢
(((ω ≼ 𝑋
∧ 𝑓 ∈
(UFil‘𝑋)) ∧ 𝑥 ∈ 𝑓) → ({𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑦) ≺ 𝑋} ⊆ 𝑓 → ¬ 𝑥 ≺ 𝑋)) |
41 | | bren2 8659 |
. . . . . 6
⊢ (𝑥 ≈ 𝑋 ↔ (𝑥 ≼ 𝑋 ∧ ¬ 𝑥 ≺ 𝑋)) |
42 | 41 | simplbi2 504 |
. . . . 5
⊢ (𝑥 ≼ 𝑋 → (¬ 𝑥 ≺ 𝑋 → 𝑥 ≈ 𝑋)) |
43 | 16, 40, 42 | sylsyld 61 |
. . . 4
⊢
(((ω ≼ 𝑋
∧ 𝑓 ∈
(UFil‘𝑋)) ∧ 𝑥 ∈ 𝑓) → ({𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑦) ≺ 𝑋} ⊆ 𝑓 → 𝑥 ≈ 𝑋)) |
44 | 43 | ralrimdva 3110 |
. . 3
⊢ ((ω
≼ 𝑋 ∧ 𝑓 ∈ (UFil‘𝑋)) → ({𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑦) ≺ 𝑋} ⊆ 𝑓 → ∀𝑥 ∈ 𝑓 𝑥 ≈ 𝑋)) |
45 | 44 | reximdva 3193 |
. 2
⊢ (ω
≼ 𝑋 →
(∃𝑓 ∈
(UFil‘𝑋){𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑦) ≺ 𝑋} ⊆ 𝑓 → ∃𝑓 ∈ (UFil‘𝑋)∀𝑥 ∈ 𝑓 𝑥 ≈ 𝑋)) |
46 | 8, 45 | mpd 15 |
1
⊢ (ω
≼ 𝑋 →
∃𝑓 ∈
(UFil‘𝑋)∀𝑥 ∈ 𝑓 𝑥 ≈ 𝑋) |