| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | reldom 8991 | . . . . . 6
⊢ Rel
≼ | 
| 2 | 1 | brrelex2i 5742 | . . . . 5
⊢ (ω
≼ 𝑋 → 𝑋 ∈ V) | 
| 3 |  | numth3 10510 | . . . . 5
⊢ (𝑋 ∈ V → 𝑋 ∈ dom
card) | 
| 4 | 2, 3 | syl 17 | . . . 4
⊢ (ω
≼ 𝑋 → 𝑋 ∈ dom
card) | 
| 5 |  | csdfil 23902 | . . . 4
⊢ ((𝑋 ∈ dom card ∧ ω
≼ 𝑋) → {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑦) ≺ 𝑋} ∈ (Fil‘𝑋)) | 
| 6 | 4, 5 | mpancom 688 | . . 3
⊢ (ω
≼ 𝑋 → {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑦) ≺ 𝑋} ∈ (Fil‘𝑋)) | 
| 7 |  | filssufil 23920 | . . 3
⊢ ({𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑦) ≺ 𝑋} ∈ (Fil‘𝑋) → ∃𝑓 ∈ (UFil‘𝑋){𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑦) ≺ 𝑋} ⊆ 𝑓) | 
| 8 | 6, 7 | syl 17 | . 2
⊢ (ω
≼ 𝑋 →
∃𝑓 ∈
(UFil‘𝑋){𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑦) ≺ 𝑋} ⊆ 𝑓) | 
| 9 |  | elfvex 6944 | . . . . . . 7
⊢ (𝑓 ∈ (UFil‘𝑋) → 𝑋 ∈ V) | 
| 10 | 9 | ad2antlr 727 | . . . . . 6
⊢
(((ω ≼ 𝑋
∧ 𝑓 ∈
(UFil‘𝑋)) ∧ 𝑥 ∈ 𝑓) → 𝑋 ∈ V) | 
| 11 |  | ufilfil 23912 | . . . . . . . 8
⊢ (𝑓 ∈ (UFil‘𝑋) → 𝑓 ∈ (Fil‘𝑋)) | 
| 12 |  | filelss 23860 | . . . . . . . 8
⊢ ((𝑓 ∈ (Fil‘𝑋) ∧ 𝑥 ∈ 𝑓) → 𝑥 ⊆ 𝑋) | 
| 13 | 11, 12 | sylan 580 | . . . . . . 7
⊢ ((𝑓 ∈ (UFil‘𝑋) ∧ 𝑥 ∈ 𝑓) → 𝑥 ⊆ 𝑋) | 
| 14 | 13 | adantll 714 | . . . . . 6
⊢
(((ω ≼ 𝑋
∧ 𝑓 ∈
(UFil‘𝑋)) ∧ 𝑥 ∈ 𝑓) → 𝑥 ⊆ 𝑋) | 
| 15 |  | ssdomg 9040 | . . . . . 6
⊢ (𝑋 ∈ V → (𝑥 ⊆ 𝑋 → 𝑥 ≼ 𝑋)) | 
| 16 | 10, 14, 15 | sylc 65 | . . . . 5
⊢
(((ω ≼ 𝑋
∧ 𝑓 ∈
(UFil‘𝑋)) ∧ 𝑥 ∈ 𝑓) → 𝑥 ≼ 𝑋) | 
| 17 |  | filfbas 23856 | . . . . . . . . 9
⊢ (𝑓 ∈ (Fil‘𝑋) → 𝑓 ∈ (fBas‘𝑋)) | 
| 18 | 11, 17 | syl 17 | . . . . . . . 8
⊢ (𝑓 ∈ (UFil‘𝑋) → 𝑓 ∈ (fBas‘𝑋)) | 
| 19 | 18 | adantl 481 | . . . . . . 7
⊢ ((ω
≼ 𝑋 ∧ 𝑓 ∈ (UFil‘𝑋)) → 𝑓 ∈ (fBas‘𝑋)) | 
| 20 |  | fbncp 23847 | . . . . . . 7
⊢ ((𝑓 ∈ (fBas‘𝑋) ∧ 𝑥 ∈ 𝑓) → ¬ (𝑋 ∖ 𝑥) ∈ 𝑓) | 
| 21 | 19, 20 | sylan 580 | . . . . . 6
⊢
(((ω ≼ 𝑋
∧ 𝑓 ∈
(UFil‘𝑋)) ∧ 𝑥 ∈ 𝑓) → ¬ (𝑋 ∖ 𝑥) ∈ 𝑓) | 
| 22 |  | difeq2 4120 | . . . . . . . . . . . . 13
⊢ (𝑦 = (𝑋 ∖ 𝑥) → (𝑋 ∖ 𝑦) = (𝑋 ∖ (𝑋 ∖ 𝑥))) | 
| 23 | 22 | breq1d 5153 | . . . . . . . . . . . 12
⊢ (𝑦 = (𝑋 ∖ 𝑥) → ((𝑋 ∖ 𝑦) ≺ 𝑋 ↔ (𝑋 ∖ (𝑋 ∖ 𝑥)) ≺ 𝑋)) | 
| 24 |  | difss 4136 | . . . . . . . . . . . . . 14
⊢ (𝑋 ∖ 𝑥) ⊆ 𝑋 | 
| 25 |  | elpw2g 5333 | . . . . . . . . . . . . . 14
⊢ (𝑋 ∈ V → ((𝑋 ∖ 𝑥) ∈ 𝒫 𝑋 ↔ (𝑋 ∖ 𝑥) ⊆ 𝑋)) | 
| 26 | 24, 25 | mpbiri 258 | . . . . . . . . . . . . 13
⊢ (𝑋 ∈ V → (𝑋 ∖ 𝑥) ∈ 𝒫 𝑋) | 
| 27 | 26 | 3ad2ant1 1134 | . . . . . . . . . . . 12
⊢ ((𝑋 ∈ V ∧ 𝑥 ⊆ 𝑋 ∧ 𝑥 ≺ 𝑋) → (𝑋 ∖ 𝑥) ∈ 𝒫 𝑋) | 
| 28 |  | simp2 1138 | . . . . . . . . . . . . . 14
⊢ ((𝑋 ∈ V ∧ 𝑥 ⊆ 𝑋 ∧ 𝑥 ≺ 𝑋) → 𝑥 ⊆ 𝑋) | 
| 29 |  | dfss4 4269 | . . . . . . . . . . . . . 14
⊢ (𝑥 ⊆ 𝑋 ↔ (𝑋 ∖ (𝑋 ∖ 𝑥)) = 𝑥) | 
| 30 | 28, 29 | sylib 218 | . . . . . . . . . . . . 13
⊢ ((𝑋 ∈ V ∧ 𝑥 ⊆ 𝑋 ∧ 𝑥 ≺ 𝑋) → (𝑋 ∖ (𝑋 ∖ 𝑥)) = 𝑥) | 
| 31 |  | simp3 1139 | . . . . . . . . . . . . 13
⊢ ((𝑋 ∈ V ∧ 𝑥 ⊆ 𝑋 ∧ 𝑥 ≺ 𝑋) → 𝑥 ≺ 𝑋) | 
| 32 | 30, 31 | eqbrtrd 5165 | . . . . . . . . . . . 12
⊢ ((𝑋 ∈ V ∧ 𝑥 ⊆ 𝑋 ∧ 𝑥 ≺ 𝑋) → (𝑋 ∖ (𝑋 ∖ 𝑥)) ≺ 𝑋) | 
| 33 | 23, 27, 32 | elrabd 3694 | . . . . . . . . . . 11
⊢ ((𝑋 ∈ V ∧ 𝑥 ⊆ 𝑋 ∧ 𝑥 ≺ 𝑋) → (𝑋 ∖ 𝑥) ∈ {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑦) ≺ 𝑋}) | 
| 34 |  | ssel 3977 | . . . . . . . . . . 11
⊢ ({𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑦) ≺ 𝑋} ⊆ 𝑓 → ((𝑋 ∖ 𝑥) ∈ {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑦) ≺ 𝑋} → (𝑋 ∖ 𝑥) ∈ 𝑓)) | 
| 35 | 33, 34 | syl5com 31 | . . . . . . . . . 10
⊢ ((𝑋 ∈ V ∧ 𝑥 ⊆ 𝑋 ∧ 𝑥 ≺ 𝑋) → ({𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑦) ≺ 𝑋} ⊆ 𝑓 → (𝑋 ∖ 𝑥) ∈ 𝑓)) | 
| 36 | 35 | 3expa 1119 | . . . . . . . . 9
⊢ (((𝑋 ∈ V ∧ 𝑥 ⊆ 𝑋) ∧ 𝑥 ≺ 𝑋) → ({𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑦) ≺ 𝑋} ⊆ 𝑓 → (𝑋 ∖ 𝑥) ∈ 𝑓)) | 
| 37 | 36 | impancom 451 | . . . . . . . 8
⊢ (((𝑋 ∈ V ∧ 𝑥 ⊆ 𝑋) ∧ {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑦) ≺ 𝑋} ⊆ 𝑓) → (𝑥 ≺ 𝑋 → (𝑋 ∖ 𝑥) ∈ 𝑓)) | 
| 38 | 37 | con3d 152 | . . . . . . 7
⊢ (((𝑋 ∈ V ∧ 𝑥 ⊆ 𝑋) ∧ {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑦) ≺ 𝑋} ⊆ 𝑓) → (¬ (𝑋 ∖ 𝑥) ∈ 𝑓 → ¬ 𝑥 ≺ 𝑋)) | 
| 39 | 38 | impancom 451 | . . . . . 6
⊢ (((𝑋 ∈ V ∧ 𝑥 ⊆ 𝑋) ∧ ¬ (𝑋 ∖ 𝑥) ∈ 𝑓) → ({𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑦) ≺ 𝑋} ⊆ 𝑓 → ¬ 𝑥 ≺ 𝑋)) | 
| 40 | 10, 14, 21, 39 | syl21anc 838 | . . . . 5
⊢
(((ω ≼ 𝑋
∧ 𝑓 ∈
(UFil‘𝑋)) ∧ 𝑥 ∈ 𝑓) → ({𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑦) ≺ 𝑋} ⊆ 𝑓 → ¬ 𝑥 ≺ 𝑋)) | 
| 41 |  | bren2 9023 | . . . . . 6
⊢ (𝑥 ≈ 𝑋 ↔ (𝑥 ≼ 𝑋 ∧ ¬ 𝑥 ≺ 𝑋)) | 
| 42 | 41 | simplbi2 500 | . . . . 5
⊢ (𝑥 ≼ 𝑋 → (¬ 𝑥 ≺ 𝑋 → 𝑥 ≈ 𝑋)) | 
| 43 | 16, 40, 42 | sylsyld 61 | . . . 4
⊢
(((ω ≼ 𝑋
∧ 𝑓 ∈
(UFil‘𝑋)) ∧ 𝑥 ∈ 𝑓) → ({𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑦) ≺ 𝑋} ⊆ 𝑓 → 𝑥 ≈ 𝑋)) | 
| 44 | 43 | ralrimdva 3154 | . . 3
⊢ ((ω
≼ 𝑋 ∧ 𝑓 ∈ (UFil‘𝑋)) → ({𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑦) ≺ 𝑋} ⊆ 𝑓 → ∀𝑥 ∈ 𝑓 𝑥 ≈ 𝑋)) | 
| 45 | 44 | reximdva 3168 | . 2
⊢ (ω
≼ 𝑋 →
(∃𝑓 ∈
(UFil‘𝑋){𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑦) ≺ 𝑋} ⊆ 𝑓 → ∃𝑓 ∈ (UFil‘𝑋)∀𝑥 ∈ 𝑓 𝑥 ≈ 𝑋)) | 
| 46 | 8, 45 | mpd 15 | 1
⊢ (ω
≼ 𝑋 →
∃𝑓 ∈
(UFil‘𝑋)∀𝑥 ∈ 𝑓 𝑥 ≈ 𝑋) |