Step | Hyp | Ref
| Expression |
1 | | simpr 476 |
. . . 4
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝒫 𝒫
𝑋 ∈ dom card) →
𝒫 𝒫 𝑋
∈ dom card) |
2 | | rabss 3642 |
. . . . 5
⊢ ({𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔} ⊆ 𝒫 𝒫 𝑋 ↔ ∀𝑔 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑔 → 𝑔 ∈ 𝒫 𝒫 𝑋)) |
3 | | filsspw 21465 |
. . . . . . 7
⊢ (𝑔 ∈ (Fil‘𝑋) → 𝑔 ⊆ 𝒫 𝑋) |
4 | | selpw 4115 |
. . . . . . 7
⊢ (𝑔 ∈ 𝒫 𝒫
𝑋 ↔ 𝑔 ⊆ 𝒫 𝑋) |
5 | 3, 4 | sylibr 223 |
. . . . . 6
⊢ (𝑔 ∈ (Fil‘𝑋) → 𝑔 ∈ 𝒫 𝒫 𝑋) |
6 | 5 | a1d 25 |
. . . . 5
⊢ (𝑔 ∈ (Fil‘𝑋) → (𝐹 ⊆ 𝑔 → 𝑔 ∈ 𝒫 𝒫 𝑋)) |
7 | 2, 6 | mprgbir 2911 |
. . . 4
⊢ {𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔} ⊆ 𝒫 𝒫 𝑋 |
8 | | ssnum 8745 |
. . . 4
⊢
((𝒫 𝒫 𝑋 ∈ dom card ∧ {𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔} ⊆ 𝒫 𝒫 𝑋) → {𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔} ∈ dom card) |
9 | 1, 7, 8 | sylancl 693 |
. . 3
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝒫 𝒫
𝑋 ∈ dom card) →
{𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔} ∈ dom card) |
10 | | ssid 3587 |
. . . . . . 7
⊢ 𝐹 ⊆ 𝐹 |
11 | 10 | jctr 563 |
. . . . . 6
⊢ (𝐹 ∈ (Fil‘𝑋) → (𝐹 ∈ (Fil‘𝑋) ∧ 𝐹 ⊆ 𝐹)) |
12 | | sseq2 3590 |
. . . . . . 7
⊢ (𝑔 = 𝐹 → (𝐹 ⊆ 𝑔 ↔ 𝐹 ⊆ 𝐹)) |
13 | 12 | elrab 3331 |
. . . . . 6
⊢ (𝐹 ∈ {𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔} ↔ (𝐹 ∈ (Fil‘𝑋) ∧ 𝐹 ⊆ 𝐹)) |
14 | 11, 13 | sylibr 223 |
. . . . 5
⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ∈ {𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔}) |
15 | | ne0i 3880 |
. . . . 5
⊢ (𝐹 ∈ {𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔} → {𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔} ≠ ∅) |
16 | 14, 15 | syl 17 |
. . . 4
⊢ (𝐹 ∈ (Fil‘𝑋) → {𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔} ≠ ∅) |
17 | 16 | adantr 480 |
. . 3
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝒫 𝒫
𝑋 ∈ dom card) →
{𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔} ≠ ∅) |
18 | | simpr1 1060 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑥 ⊆ {𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔} ∧ 𝑥 ≠ ∅ ∧ [⊊] Or
𝑥)) → 𝑥 ⊆ {𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔}) |
19 | | ssrab 3643 |
. . . . . . . . . 10
⊢ (𝑥 ⊆ {𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔} ↔ (𝑥 ⊆ (Fil‘𝑋) ∧ ∀𝑔 ∈ 𝑥 𝐹 ⊆ 𝑔)) |
20 | 18, 19 | sylib 207 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑥 ⊆ {𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔} ∧ 𝑥 ≠ ∅ ∧ [⊊] Or
𝑥)) → (𝑥 ⊆ (Fil‘𝑋) ∧ ∀𝑔 ∈ 𝑥 𝐹 ⊆ 𝑔)) |
21 | 20 | simpld 474 |
. . . . . . . 8
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑥 ⊆ {𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔} ∧ 𝑥 ≠ ∅ ∧ [⊊] Or
𝑥)) → 𝑥 ⊆ (Fil‘𝑋)) |
22 | | simpr2 1061 |
. . . . . . . 8
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑥 ⊆ {𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔} ∧ 𝑥 ≠ ∅ ∧ [⊊] Or
𝑥)) → 𝑥 ≠ ∅) |
23 | | simpr3 1062 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑥 ⊆ {𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔} ∧ 𝑥 ≠ ∅ ∧ [⊊] Or
𝑥)) →
[⊊] Or 𝑥) |
24 | | sorpssun 6842 |
. . . . . . . . . 10
⊢ ((
[⊊] Or 𝑥
∧ (𝑔 ∈ 𝑥 ∧ ℎ ∈ 𝑥)) → (𝑔 ∪ ℎ) ∈ 𝑥) |
25 | 24 | ralrimivva 2954 |
. . . . . . . . 9
⊢ (
[⊊] Or 𝑥
→ ∀𝑔 ∈
𝑥 ∀ℎ ∈ 𝑥 (𝑔 ∪ ℎ) ∈ 𝑥) |
26 | 23, 25 | syl 17 |
. . . . . . . 8
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑥 ⊆ {𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔} ∧ 𝑥 ≠ ∅ ∧ [⊊] Or
𝑥)) → ∀𝑔 ∈ 𝑥 ∀ℎ ∈ 𝑥 (𝑔 ∪ ℎ) ∈ 𝑥) |
27 | | filuni 21499 |
. . . . . . . 8
⊢ ((𝑥 ⊆ (Fil‘𝑋) ∧ 𝑥 ≠ ∅ ∧ ∀𝑔 ∈ 𝑥 ∀ℎ ∈ 𝑥 (𝑔 ∪ ℎ) ∈ 𝑥) → ∪ 𝑥 ∈ (Fil‘𝑋)) |
28 | 21, 22, 26, 27 | syl3anc 1318 |
. . . . . . 7
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑥 ⊆ {𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔} ∧ 𝑥 ≠ ∅ ∧ [⊊] Or
𝑥)) → ∪ 𝑥
∈ (Fil‘𝑋)) |
29 | | n0 3890 |
. . . . . . . . 9
⊢ (𝑥 ≠ ∅ ↔
∃ℎ ℎ ∈ 𝑥) |
30 | | ssel2 3563 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ⊆ {𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔} ∧ ℎ ∈ 𝑥) → ℎ ∈ {𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔}) |
31 | | sseq2 3590 |
. . . . . . . . . . . . . . 15
⊢ (𝑔 = ℎ → (𝐹 ⊆ 𝑔 ↔ 𝐹 ⊆ ℎ)) |
32 | 31 | elrab 3331 |
. . . . . . . . . . . . . 14
⊢ (ℎ ∈ {𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔} ↔ (ℎ ∈ (Fil‘𝑋) ∧ 𝐹 ⊆ ℎ)) |
33 | 30, 32 | sylib 207 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ⊆ {𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔} ∧ ℎ ∈ 𝑥) → (ℎ ∈ (Fil‘𝑋) ∧ 𝐹 ⊆ ℎ)) |
34 | 33 | simprd 478 |
. . . . . . . . . . . 12
⊢ ((𝑥 ⊆ {𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔} ∧ ℎ ∈ 𝑥) → 𝐹 ⊆ ℎ) |
35 | | ssuni 4395 |
. . . . . . . . . . . 12
⊢ ((𝐹 ⊆ ℎ ∧ ℎ ∈ 𝑥) → 𝐹 ⊆ ∪ 𝑥) |
36 | 34, 35 | sylancom 698 |
. . . . . . . . . . 11
⊢ ((𝑥 ⊆ {𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔} ∧ ℎ ∈ 𝑥) → 𝐹 ⊆ ∪ 𝑥) |
37 | 36 | ex 449 |
. . . . . . . . . 10
⊢ (𝑥 ⊆ {𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔} → (ℎ ∈ 𝑥 → 𝐹 ⊆ ∪ 𝑥)) |
38 | 37 | exlimdv 1848 |
. . . . . . . . 9
⊢ (𝑥 ⊆ {𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔} → (∃ℎ ℎ ∈ 𝑥 → 𝐹 ⊆ ∪ 𝑥)) |
39 | 29, 38 | syl5bi 231 |
. . . . . . . 8
⊢ (𝑥 ⊆ {𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔} → (𝑥 ≠ ∅ → 𝐹 ⊆ ∪ 𝑥)) |
40 | 18, 22, 39 | sylc 63 |
. . . . . . 7
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑥 ⊆ {𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔} ∧ 𝑥 ≠ ∅ ∧ [⊊] Or
𝑥)) → 𝐹 ⊆ ∪ 𝑥) |
41 | | sseq2 3590 |
. . . . . . . 8
⊢ (𝑔 = ∪
𝑥 → (𝐹 ⊆ 𝑔 ↔ 𝐹 ⊆ ∪ 𝑥)) |
42 | 41 | elrab 3331 |
. . . . . . 7
⊢ (∪ 𝑥
∈ {𝑔 ∈
(Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔} ↔ (∪ 𝑥 ∈ (Fil‘𝑋) ∧ 𝐹 ⊆ ∪ 𝑥)) |
43 | 28, 40, 42 | sylanbrc 695 |
. . . . . 6
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑥 ⊆ {𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔} ∧ 𝑥 ≠ ∅ ∧ [⊊] Or
𝑥)) → ∪ 𝑥
∈ {𝑔 ∈
(Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔}) |
44 | 43 | ex 449 |
. . . . 5
⊢ (𝐹 ∈ (Fil‘𝑋) → ((𝑥 ⊆ {𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔} ∧ 𝑥 ≠ ∅ ∧ [⊊] Or
𝑥) → ∪ 𝑥
∈ {𝑔 ∈
(Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔})) |
45 | 44 | alrimiv 1842 |
. . . 4
⊢ (𝐹 ∈ (Fil‘𝑋) → ∀𝑥((𝑥 ⊆ {𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔} ∧ 𝑥 ≠ ∅ ∧ [⊊] Or
𝑥) → ∪ 𝑥
∈ {𝑔 ∈
(Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔})) |
46 | 45 | adantr 480 |
. . 3
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝒫 𝒫
𝑋 ∈ dom card) →
∀𝑥((𝑥 ⊆ {𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔} ∧ 𝑥 ≠ ∅ ∧ [⊊] Or
𝑥) → ∪ 𝑥
∈ {𝑔 ∈
(Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔})) |
47 | | zornn0g 9210 |
. . 3
⊢ (({𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔} ∈ dom card ∧ {𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔} ≠ ∅ ∧ ∀𝑥((𝑥 ⊆ {𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔} ∧ 𝑥 ≠ ∅ ∧ [⊊] Or
𝑥) → ∪ 𝑥
∈ {𝑔 ∈
(Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔})) → ∃𝑓 ∈ {𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔}∀ℎ ∈ {𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔} ¬ 𝑓 ⊊ ℎ) |
48 | 9, 17, 46, 47 | syl3anc 1318 |
. 2
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝒫 𝒫
𝑋 ∈ dom card) →
∃𝑓 ∈ {𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔}∀ℎ ∈ {𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔} ¬ 𝑓 ⊊ ℎ) |
49 | | sseq2 3590 |
. . . . 5
⊢ (𝑔 = 𝑓 → (𝐹 ⊆ 𝑔 ↔ 𝐹 ⊆ 𝑓)) |
50 | 49 | elrab 3331 |
. . . 4
⊢ (𝑓 ∈ {𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔} ↔ (𝑓 ∈ (Fil‘𝑋) ∧ 𝐹 ⊆ 𝑓)) |
51 | 31 | ralrab 3335 |
. . . 4
⊢
(∀ℎ ∈
{𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔} ¬ 𝑓 ⊊ ℎ ↔ ∀ℎ ∈ (Fil‘𝑋)(𝐹 ⊆ ℎ → ¬ 𝑓 ⊊ ℎ)) |
52 | | simpll 786 |
. . . . . 6
⊢ (((𝑓 ∈ (Fil‘𝑋) ∧ 𝐹 ⊆ 𝑓) ∧ ∀ℎ ∈ (Fil‘𝑋)(𝐹 ⊆ ℎ → ¬ 𝑓 ⊊ ℎ)) → 𝑓 ∈ (Fil‘𝑋)) |
53 | | sstr2 3575 |
. . . . . . . . . . 11
⊢ (𝐹 ⊆ 𝑓 → (𝑓 ⊆ ℎ → 𝐹 ⊆ ℎ)) |
54 | 53 | imim1d 80 |
. . . . . . . . . 10
⊢ (𝐹 ⊆ 𝑓 → ((𝐹 ⊆ ℎ → ¬ 𝑓 ⊊ ℎ) → (𝑓 ⊆ ℎ → ¬ 𝑓 ⊊ ℎ))) |
55 | | df-pss 3556 |
. . . . . . . . . . . . 13
⊢ (𝑓 ⊊ ℎ ↔ (𝑓 ⊆ ℎ ∧ 𝑓 ≠ ℎ)) |
56 | 55 | simplbi2 653 |
. . . . . . . . . . . 12
⊢ (𝑓 ⊆ ℎ → (𝑓 ≠ ℎ → 𝑓 ⊊ ℎ)) |
57 | 56 | necon1bd 2800 |
. . . . . . . . . . 11
⊢ (𝑓 ⊆ ℎ → (¬ 𝑓 ⊊ ℎ → 𝑓 = ℎ)) |
58 | 57 | a2i 14 |
. . . . . . . . . 10
⊢ ((𝑓 ⊆ ℎ → ¬ 𝑓 ⊊ ℎ) → (𝑓 ⊆ ℎ → 𝑓 = ℎ)) |
59 | 54, 58 | syl6 34 |
. . . . . . . . 9
⊢ (𝐹 ⊆ 𝑓 → ((𝐹 ⊆ ℎ → ¬ 𝑓 ⊊ ℎ) → (𝑓 ⊆ ℎ → 𝑓 = ℎ))) |
60 | 59 | ralimdv 2946 |
. . . . . . . 8
⊢ (𝐹 ⊆ 𝑓 → (∀ℎ ∈ (Fil‘𝑋)(𝐹 ⊆ ℎ → ¬ 𝑓 ⊊ ℎ) → ∀ℎ ∈ (Fil‘𝑋)(𝑓 ⊆ ℎ → 𝑓 = ℎ))) |
61 | 60 | imp 444 |
. . . . . . 7
⊢ ((𝐹 ⊆ 𝑓 ∧ ∀ℎ ∈ (Fil‘𝑋)(𝐹 ⊆ ℎ → ¬ 𝑓 ⊊ ℎ)) → ∀ℎ ∈ (Fil‘𝑋)(𝑓 ⊆ ℎ → 𝑓 = ℎ)) |
62 | 61 | adantll 746 |
. . . . . 6
⊢ (((𝑓 ∈ (Fil‘𝑋) ∧ 𝐹 ⊆ 𝑓) ∧ ∀ℎ ∈ (Fil‘𝑋)(𝐹 ⊆ ℎ → ¬ 𝑓 ⊊ ℎ)) → ∀ℎ ∈ (Fil‘𝑋)(𝑓 ⊆ ℎ → 𝑓 = ℎ)) |
63 | | isufil2 21522 |
. . . . . 6
⊢ (𝑓 ∈ (UFil‘𝑋) ↔ (𝑓 ∈ (Fil‘𝑋) ∧ ∀ℎ ∈ (Fil‘𝑋)(𝑓 ⊆ ℎ → 𝑓 = ℎ))) |
64 | 52, 62, 63 | sylanbrc 695 |
. . . . 5
⊢ (((𝑓 ∈ (Fil‘𝑋) ∧ 𝐹 ⊆ 𝑓) ∧ ∀ℎ ∈ (Fil‘𝑋)(𝐹 ⊆ ℎ → ¬ 𝑓 ⊊ ℎ)) → 𝑓 ∈ (UFil‘𝑋)) |
65 | | simplr 788 |
. . . . 5
⊢ (((𝑓 ∈ (Fil‘𝑋) ∧ 𝐹 ⊆ 𝑓) ∧ ∀ℎ ∈ (Fil‘𝑋)(𝐹 ⊆ ℎ → ¬ 𝑓 ⊊ ℎ)) → 𝐹 ⊆ 𝑓) |
66 | 64, 65 | jca 553 |
. . . 4
⊢ (((𝑓 ∈ (Fil‘𝑋) ∧ 𝐹 ⊆ 𝑓) ∧ ∀ℎ ∈ (Fil‘𝑋)(𝐹 ⊆ ℎ → ¬ 𝑓 ⊊ ℎ)) → (𝑓 ∈ (UFil‘𝑋) ∧ 𝐹 ⊆ 𝑓)) |
67 | 50, 51, 66 | syl2anb 495 |
. . 3
⊢ ((𝑓 ∈ {𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔} ∧ ∀ℎ ∈ {𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔} ¬ 𝑓 ⊊ ℎ) → (𝑓 ∈ (UFil‘𝑋) ∧ 𝐹 ⊆ 𝑓)) |
68 | 67 | reximi2 2993 |
. 2
⊢
(∃𝑓 ∈
{𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔}∀ℎ ∈ {𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔} ¬ 𝑓 ⊊ ℎ → ∃𝑓 ∈ (UFil‘𝑋)𝐹 ⊆ 𝑓) |
69 | 48, 68 | syl 17 |
1
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝒫 𝒫
𝑋 ∈ dom card) →
∃𝑓 ∈
(UFil‘𝑋)𝐹 ⊆ 𝑓) |