Step | Hyp | Ref
| Expression |
1 | | reldom 7961 |
. . . . . 6
⊢ Rel
≼ |
2 | 1 | brrelex2i 5159 |
. . . . 5
⊢ (ω
≼ 𝑋 → 𝑋 ∈ V) |
3 | | numth3 9292 |
. . . . 5
⊢ (𝑋 ∈ V → 𝑋 ∈ dom
card) |
4 | 2, 3 | syl 17 |
. . . 4
⊢ (ω
≼ 𝑋 → 𝑋 ∈ dom
card) |
5 | | csdfil 21698 |
. . . 4
⊢ ((𝑋 ∈ dom card ∧ ω
≼ 𝑋) → {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑦) ≺ 𝑋} ∈ (Fil‘𝑋)) |
6 | 4, 5 | mpancom 703 |
. . 3
⊢ (ω
≼ 𝑋 → {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑦) ≺ 𝑋} ∈ (Fil‘𝑋)) |
7 | | filssufil 21716 |
. . 3
⊢ ({𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑦) ≺ 𝑋} ∈ (Fil‘𝑋) → ∃𝑓 ∈ (UFil‘𝑋){𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑦) ≺ 𝑋} ⊆ 𝑓) |
8 | 6, 7 | syl 17 |
. 2
⊢ (ω
≼ 𝑋 →
∃𝑓 ∈
(UFil‘𝑋){𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑦) ≺ 𝑋} ⊆ 𝑓) |
9 | | elfvex 6221 |
. . . . . . 7
⊢ (𝑓 ∈ (UFil‘𝑋) → 𝑋 ∈ V) |
10 | 9 | ad2antlr 763 |
. . . . . 6
⊢
(((ω ≼ 𝑋
∧ 𝑓 ∈
(UFil‘𝑋)) ∧ 𝑥 ∈ 𝑓) → 𝑋 ∈ V) |
11 | | ufilfil 21708 |
. . . . . . . 8
⊢ (𝑓 ∈ (UFil‘𝑋) → 𝑓 ∈ (Fil‘𝑋)) |
12 | | filelss 21656 |
. . . . . . . 8
⊢ ((𝑓 ∈ (Fil‘𝑋) ∧ 𝑥 ∈ 𝑓) → 𝑥 ⊆ 𝑋) |
13 | 11, 12 | sylan 488 |
. . . . . . 7
⊢ ((𝑓 ∈ (UFil‘𝑋) ∧ 𝑥 ∈ 𝑓) → 𝑥 ⊆ 𝑋) |
14 | 13 | adantll 750 |
. . . . . 6
⊢
(((ω ≼ 𝑋
∧ 𝑓 ∈
(UFil‘𝑋)) ∧ 𝑥 ∈ 𝑓) → 𝑥 ⊆ 𝑋) |
15 | | ssdomg 8001 |
. . . . . 6
⊢ (𝑋 ∈ V → (𝑥 ⊆ 𝑋 → 𝑥 ≼ 𝑋)) |
16 | 10, 14, 15 | sylc 65 |
. . . . 5
⊢
(((ω ≼ 𝑋
∧ 𝑓 ∈
(UFil‘𝑋)) ∧ 𝑥 ∈ 𝑓) → 𝑥 ≼ 𝑋) |
17 | | filfbas 21652 |
. . . . . . . . 9
⊢ (𝑓 ∈ (Fil‘𝑋) → 𝑓 ∈ (fBas‘𝑋)) |
18 | 11, 17 | syl 17 |
. . . . . . . 8
⊢ (𝑓 ∈ (UFil‘𝑋) → 𝑓 ∈ (fBas‘𝑋)) |
19 | 18 | adantl 482 |
. . . . . . 7
⊢ ((ω
≼ 𝑋 ∧ 𝑓 ∈ (UFil‘𝑋)) → 𝑓 ∈ (fBas‘𝑋)) |
20 | | fbncp 21643 |
. . . . . . 7
⊢ ((𝑓 ∈ (fBas‘𝑋) ∧ 𝑥 ∈ 𝑓) → ¬ (𝑋 ∖ 𝑥) ∈ 𝑓) |
21 | 19, 20 | sylan 488 |
. . . . . 6
⊢
(((ω ≼ 𝑋
∧ 𝑓 ∈
(UFil‘𝑋)) ∧ 𝑥 ∈ 𝑓) → ¬ (𝑋 ∖ 𝑥) ∈ 𝑓) |
22 | | difss 3737 |
. . . . . . . . . . . . . 14
⊢ (𝑋 ∖ 𝑥) ⊆ 𝑋 |
23 | | elpw2g 4827 |
. . . . . . . . . . . . . 14
⊢ (𝑋 ∈ V → ((𝑋 ∖ 𝑥) ∈ 𝒫 𝑋 ↔ (𝑋 ∖ 𝑥) ⊆ 𝑋)) |
24 | 22, 23 | mpbiri 248 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∈ V → (𝑋 ∖ 𝑥) ∈ 𝒫 𝑋) |
25 | 24 | 3ad2ant1 1082 |
. . . . . . . . . . . 12
⊢ ((𝑋 ∈ V ∧ 𝑥 ⊆ 𝑋 ∧ 𝑥 ≺ 𝑋) → (𝑋 ∖ 𝑥) ∈ 𝒫 𝑋) |
26 | | simp2 1062 |
. . . . . . . . . . . . . 14
⊢ ((𝑋 ∈ V ∧ 𝑥 ⊆ 𝑋 ∧ 𝑥 ≺ 𝑋) → 𝑥 ⊆ 𝑋) |
27 | | dfss4 3858 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ⊆ 𝑋 ↔ (𝑋 ∖ (𝑋 ∖ 𝑥)) = 𝑥) |
28 | 26, 27 | sylib 208 |
. . . . . . . . . . . . 13
⊢ ((𝑋 ∈ V ∧ 𝑥 ⊆ 𝑋 ∧ 𝑥 ≺ 𝑋) → (𝑋 ∖ (𝑋 ∖ 𝑥)) = 𝑥) |
29 | | simp3 1063 |
. . . . . . . . . . . . 13
⊢ ((𝑋 ∈ V ∧ 𝑥 ⊆ 𝑋 ∧ 𝑥 ≺ 𝑋) → 𝑥 ≺ 𝑋) |
30 | 28, 29 | eqbrtrd 4675 |
. . . . . . . . . . . 12
⊢ ((𝑋 ∈ V ∧ 𝑥 ⊆ 𝑋 ∧ 𝑥 ≺ 𝑋) → (𝑋 ∖ (𝑋 ∖ 𝑥)) ≺ 𝑋) |
31 | | difeq2 3722 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = (𝑋 ∖ 𝑥) → (𝑋 ∖ 𝑦) = (𝑋 ∖ (𝑋 ∖ 𝑥))) |
32 | 31 | breq1d 4663 |
. . . . . . . . . . . . 13
⊢ (𝑦 = (𝑋 ∖ 𝑥) → ((𝑋 ∖ 𝑦) ≺ 𝑋 ↔ (𝑋 ∖ (𝑋 ∖ 𝑥)) ≺ 𝑋)) |
33 | 32 | elrab 3363 |
. . . . . . . . . . . 12
⊢ ((𝑋 ∖ 𝑥) ∈ {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑦) ≺ 𝑋} ↔ ((𝑋 ∖ 𝑥) ∈ 𝒫 𝑋 ∧ (𝑋 ∖ (𝑋 ∖ 𝑥)) ≺ 𝑋)) |
34 | 25, 30, 33 | sylanbrc 698 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ V ∧ 𝑥 ⊆ 𝑋 ∧ 𝑥 ≺ 𝑋) → (𝑋 ∖ 𝑥) ∈ {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑦) ≺ 𝑋}) |
35 | | ssel 3597 |
. . . . . . . . . . 11
⊢ ({𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑦) ≺ 𝑋} ⊆ 𝑓 → ((𝑋 ∖ 𝑥) ∈ {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑦) ≺ 𝑋} → (𝑋 ∖ 𝑥) ∈ 𝑓)) |
36 | 34, 35 | syl5com 31 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ V ∧ 𝑥 ⊆ 𝑋 ∧ 𝑥 ≺ 𝑋) → ({𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑦) ≺ 𝑋} ⊆ 𝑓 → (𝑋 ∖ 𝑥) ∈ 𝑓)) |
37 | 36 | 3expa 1265 |
. . . . . . . . 9
⊢ (((𝑋 ∈ V ∧ 𝑥 ⊆ 𝑋) ∧ 𝑥 ≺ 𝑋) → ({𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑦) ≺ 𝑋} ⊆ 𝑓 → (𝑋 ∖ 𝑥) ∈ 𝑓)) |
38 | 37 | impancom 456 |
. . . . . . . 8
⊢ (((𝑋 ∈ V ∧ 𝑥 ⊆ 𝑋) ∧ {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑦) ≺ 𝑋} ⊆ 𝑓) → (𝑥 ≺ 𝑋 → (𝑋 ∖ 𝑥) ∈ 𝑓)) |
39 | 38 | con3d 148 |
. . . . . . 7
⊢ (((𝑋 ∈ V ∧ 𝑥 ⊆ 𝑋) ∧ {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑦) ≺ 𝑋} ⊆ 𝑓) → (¬ (𝑋 ∖ 𝑥) ∈ 𝑓 → ¬ 𝑥 ≺ 𝑋)) |
40 | 39 | impancom 456 |
. . . . . 6
⊢ (((𝑋 ∈ V ∧ 𝑥 ⊆ 𝑋) ∧ ¬ (𝑋 ∖ 𝑥) ∈ 𝑓) → ({𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑦) ≺ 𝑋} ⊆ 𝑓 → ¬ 𝑥 ≺ 𝑋)) |
41 | 10, 14, 21, 40 | syl21anc 1325 |
. . . . 5
⊢
(((ω ≼ 𝑋
∧ 𝑓 ∈
(UFil‘𝑋)) ∧ 𝑥 ∈ 𝑓) → ({𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑦) ≺ 𝑋} ⊆ 𝑓 → ¬ 𝑥 ≺ 𝑋)) |
42 | | bren2 7986 |
. . . . . 6
⊢ (𝑥 ≈ 𝑋 ↔ (𝑥 ≼ 𝑋 ∧ ¬ 𝑥 ≺ 𝑋)) |
43 | 42 | simplbi2 655 |
. . . . 5
⊢ (𝑥 ≼ 𝑋 → (¬ 𝑥 ≺ 𝑋 → 𝑥 ≈ 𝑋)) |
44 | 16, 41, 43 | sylsyld 61 |
. . . 4
⊢
(((ω ≼ 𝑋
∧ 𝑓 ∈
(UFil‘𝑋)) ∧ 𝑥 ∈ 𝑓) → ({𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑦) ≺ 𝑋} ⊆ 𝑓 → 𝑥 ≈ 𝑋)) |
45 | 44 | ralrimdva 2969 |
. . 3
⊢ ((ω
≼ 𝑋 ∧ 𝑓 ∈ (UFil‘𝑋)) → ({𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑦) ≺ 𝑋} ⊆ 𝑓 → ∀𝑥 ∈ 𝑓 𝑥 ≈ 𝑋)) |
46 | 45 | reximdva 3017 |
. 2
⊢ (ω
≼ 𝑋 →
(∃𝑓 ∈
(UFil‘𝑋){𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑦) ≺ 𝑋} ⊆ 𝑓 → ∃𝑓 ∈ (UFil‘𝑋)∀𝑥 ∈ 𝑓 𝑥 ≈ 𝑋)) |
47 | 8, 46 | mpd 15 |
1
⊢ (ω
≼ 𝑋 →
∃𝑓 ∈
(UFil‘𝑋)∀𝑥 ∈ 𝑓 𝑥 ≈ 𝑋) |