| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simpr 484 | . . . 4
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝒫 𝒫
𝑋 ∈ dom card) →
𝒫 𝒫 𝑋
∈ dom card) | 
| 2 |  | rabss 4071 | . . . . 5
⊢ ({𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔} ⊆ 𝒫 𝒫 𝑋 ↔ ∀𝑔 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑔 → 𝑔 ∈ 𝒫 𝒫 𝑋)) | 
| 3 |  | filsspw 23860 | . . . . . . 7
⊢ (𝑔 ∈ (Fil‘𝑋) → 𝑔 ⊆ 𝒫 𝑋) | 
| 4 |  | velpw 4604 | . . . . . . 7
⊢ (𝑔 ∈ 𝒫 𝒫
𝑋 ↔ 𝑔 ⊆ 𝒫 𝑋) | 
| 5 | 3, 4 | sylibr 234 | . . . . . 6
⊢ (𝑔 ∈ (Fil‘𝑋) → 𝑔 ∈ 𝒫 𝒫 𝑋) | 
| 6 | 5 | a1d 25 | . . . . 5
⊢ (𝑔 ∈ (Fil‘𝑋) → (𝐹 ⊆ 𝑔 → 𝑔 ∈ 𝒫 𝒫 𝑋)) | 
| 7 | 2, 6 | mprgbir 3067 | . . . 4
⊢ {𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔} ⊆ 𝒫 𝒫 𝑋 | 
| 8 |  | ssnum 10080 | . . . 4
⊢
((𝒫 𝒫 𝑋 ∈ dom card ∧ {𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔} ⊆ 𝒫 𝒫 𝑋) → {𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔} ∈ dom card) | 
| 9 | 1, 7, 8 | sylancl 586 | . . 3
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝒫 𝒫
𝑋 ∈ dom card) →
{𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔} ∈ dom card) | 
| 10 |  | ssid 4005 | . . . . . . 7
⊢ 𝐹 ⊆ 𝐹 | 
| 11 | 10 | jctr 524 | . . . . . 6
⊢ (𝐹 ∈ (Fil‘𝑋) → (𝐹 ∈ (Fil‘𝑋) ∧ 𝐹 ⊆ 𝐹)) | 
| 12 |  | sseq2 4009 | . . . . . . 7
⊢ (𝑔 = 𝐹 → (𝐹 ⊆ 𝑔 ↔ 𝐹 ⊆ 𝐹)) | 
| 13 | 12 | elrab 3691 | . . . . . 6
⊢ (𝐹 ∈ {𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔} ↔ (𝐹 ∈ (Fil‘𝑋) ∧ 𝐹 ⊆ 𝐹)) | 
| 14 | 11, 13 | sylibr 234 | . . . . 5
⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ∈ {𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔}) | 
| 15 | 14 | ne0d 4341 | . . . 4
⊢ (𝐹 ∈ (Fil‘𝑋) → {𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔} ≠ ∅) | 
| 16 | 15 | adantr 480 | . . 3
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝒫 𝒫
𝑋 ∈ dom card) →
{𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔} ≠ ∅) | 
| 17 |  | sseq2 4009 | . . . . . . 7
⊢ (𝑔 = ∪
𝑥 → (𝐹 ⊆ 𝑔 ↔ 𝐹 ⊆ ∪ 𝑥)) | 
| 18 |  | simpr1 1194 | . . . . . . . . . 10
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑥 ⊆ {𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔} ∧ 𝑥 ≠ ∅ ∧ [⊊] Or
𝑥)) → 𝑥 ⊆ {𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔}) | 
| 19 |  | ssrab 4072 | . . . . . . . . . 10
⊢ (𝑥 ⊆ {𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔} ↔ (𝑥 ⊆ (Fil‘𝑋) ∧ ∀𝑔 ∈ 𝑥 𝐹 ⊆ 𝑔)) | 
| 20 | 18, 19 | sylib 218 | . . . . . . . . 9
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑥 ⊆ {𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔} ∧ 𝑥 ≠ ∅ ∧ [⊊] Or
𝑥)) → (𝑥 ⊆ (Fil‘𝑋) ∧ ∀𝑔 ∈ 𝑥 𝐹 ⊆ 𝑔)) | 
| 21 | 20 | simpld 494 | . . . . . . . 8
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑥 ⊆ {𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔} ∧ 𝑥 ≠ ∅ ∧ [⊊] Or
𝑥)) → 𝑥 ⊆ (Fil‘𝑋)) | 
| 22 |  | simpr2 1195 | . . . . . . . 8
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑥 ⊆ {𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔} ∧ 𝑥 ≠ ∅ ∧ [⊊] Or
𝑥)) → 𝑥 ≠ ∅) | 
| 23 |  | simpr3 1196 | . . . . . . . . 9
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑥 ⊆ {𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔} ∧ 𝑥 ≠ ∅ ∧ [⊊] Or
𝑥)) →
[⊊] Or 𝑥) | 
| 24 |  | sorpssun 7751 | . . . . . . . . . 10
⊢ ((
[⊊] Or 𝑥
∧ (𝑔 ∈ 𝑥 ∧ ℎ ∈ 𝑥)) → (𝑔 ∪ ℎ) ∈ 𝑥) | 
| 25 | 24 | ralrimivva 3201 | . . . . . . . . 9
⊢ (
[⊊] Or 𝑥
→ ∀𝑔 ∈
𝑥 ∀ℎ ∈ 𝑥 (𝑔 ∪ ℎ) ∈ 𝑥) | 
| 26 | 23, 25 | syl 17 | . . . . . . . 8
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑥 ⊆ {𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔} ∧ 𝑥 ≠ ∅ ∧ [⊊] Or
𝑥)) → ∀𝑔 ∈ 𝑥 ∀ℎ ∈ 𝑥 (𝑔 ∪ ℎ) ∈ 𝑥) | 
| 27 |  | filuni 23894 | . . . . . . . 8
⊢ ((𝑥 ⊆ (Fil‘𝑋) ∧ 𝑥 ≠ ∅ ∧ ∀𝑔 ∈ 𝑥 ∀ℎ ∈ 𝑥 (𝑔 ∪ ℎ) ∈ 𝑥) → ∪ 𝑥 ∈ (Fil‘𝑋)) | 
| 28 | 21, 22, 26, 27 | syl3anc 1372 | . . . . . . 7
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑥 ⊆ {𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔} ∧ 𝑥 ≠ ∅ ∧ [⊊] Or
𝑥)) → ∪ 𝑥
∈ (Fil‘𝑋)) | 
| 29 |  | n0 4352 | . . . . . . . . 9
⊢ (𝑥 ≠ ∅ ↔
∃ℎ ℎ ∈ 𝑥) | 
| 30 |  | ssel2 3977 | . . . . . . . . . . . . . 14
⊢ ((𝑥 ⊆ {𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔} ∧ ℎ ∈ 𝑥) → ℎ ∈ {𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔}) | 
| 31 |  | sseq2 4009 | . . . . . . . . . . . . . . 15
⊢ (𝑔 = ℎ → (𝐹 ⊆ 𝑔 ↔ 𝐹 ⊆ ℎ)) | 
| 32 | 31 | elrab 3691 | . . . . . . . . . . . . . 14
⊢ (ℎ ∈ {𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔} ↔ (ℎ ∈ (Fil‘𝑋) ∧ 𝐹 ⊆ ℎ)) | 
| 33 | 30, 32 | sylib 218 | . . . . . . . . . . . . 13
⊢ ((𝑥 ⊆ {𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔} ∧ ℎ ∈ 𝑥) → (ℎ ∈ (Fil‘𝑋) ∧ 𝐹 ⊆ ℎ)) | 
| 34 | 33 | simprd 495 | . . . . . . . . . . . 12
⊢ ((𝑥 ⊆ {𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔} ∧ ℎ ∈ 𝑥) → 𝐹 ⊆ ℎ) | 
| 35 |  | ssuni 4931 | . . . . . . . . . . . 12
⊢ ((𝐹 ⊆ ℎ ∧ ℎ ∈ 𝑥) → 𝐹 ⊆ ∪ 𝑥) | 
| 36 | 34, 35 | sylancom 588 | . . . . . . . . . . 11
⊢ ((𝑥 ⊆ {𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔} ∧ ℎ ∈ 𝑥) → 𝐹 ⊆ ∪ 𝑥) | 
| 37 | 36 | ex 412 | . . . . . . . . . 10
⊢ (𝑥 ⊆ {𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔} → (ℎ ∈ 𝑥 → 𝐹 ⊆ ∪ 𝑥)) | 
| 38 | 37 | exlimdv 1932 | . . . . . . . . 9
⊢ (𝑥 ⊆ {𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔} → (∃ℎ ℎ ∈ 𝑥 → 𝐹 ⊆ ∪ 𝑥)) | 
| 39 | 29, 38 | biimtrid 242 | . . . . . . . 8
⊢ (𝑥 ⊆ {𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔} → (𝑥 ≠ ∅ → 𝐹 ⊆ ∪ 𝑥)) | 
| 40 | 18, 22, 39 | sylc 65 | . . . . . . 7
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑥 ⊆ {𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔} ∧ 𝑥 ≠ ∅ ∧ [⊊] Or
𝑥)) → 𝐹 ⊆ ∪ 𝑥) | 
| 41 | 17, 28, 40 | elrabd 3693 | . . . . . 6
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑥 ⊆ {𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔} ∧ 𝑥 ≠ ∅ ∧ [⊊] Or
𝑥)) → ∪ 𝑥
∈ {𝑔 ∈
(Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔}) | 
| 42 | 41 | ex 412 | . . . . 5
⊢ (𝐹 ∈ (Fil‘𝑋) → ((𝑥 ⊆ {𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔} ∧ 𝑥 ≠ ∅ ∧ [⊊] Or
𝑥) → ∪ 𝑥
∈ {𝑔 ∈
(Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔})) | 
| 43 | 42 | alrimiv 1926 | . . . 4
⊢ (𝐹 ∈ (Fil‘𝑋) → ∀𝑥((𝑥 ⊆ {𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔} ∧ 𝑥 ≠ ∅ ∧ [⊊] Or
𝑥) → ∪ 𝑥
∈ {𝑔 ∈
(Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔})) | 
| 44 | 43 | adantr 480 | . . 3
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝒫 𝒫
𝑋 ∈ dom card) →
∀𝑥((𝑥 ⊆ {𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔} ∧ 𝑥 ≠ ∅ ∧ [⊊] Or
𝑥) → ∪ 𝑥
∈ {𝑔 ∈
(Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔})) | 
| 45 |  | zornn0g 10546 | . . 3
⊢ (({𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔} ∈ dom card ∧ {𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔} ≠ ∅ ∧ ∀𝑥((𝑥 ⊆ {𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔} ∧ 𝑥 ≠ ∅ ∧ [⊊] Or
𝑥) → ∪ 𝑥
∈ {𝑔 ∈
(Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔})) → ∃𝑓 ∈ {𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔}∀ℎ ∈ {𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔} ¬ 𝑓 ⊊ ℎ) | 
| 46 | 9, 16, 44, 45 | syl3anc 1372 | . 2
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝒫 𝒫
𝑋 ∈ dom card) →
∃𝑓 ∈ {𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔}∀ℎ ∈ {𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔} ¬ 𝑓 ⊊ ℎ) | 
| 47 |  | sseq2 4009 | . . . . 5
⊢ (𝑔 = 𝑓 → (𝐹 ⊆ 𝑔 ↔ 𝐹 ⊆ 𝑓)) | 
| 48 | 47 | elrab 3691 | . . . 4
⊢ (𝑓 ∈ {𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔} ↔ (𝑓 ∈ (Fil‘𝑋) ∧ 𝐹 ⊆ 𝑓)) | 
| 49 | 31 | ralrab 3698 | . . . 4
⊢
(∀ℎ ∈
{𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔} ¬ 𝑓 ⊊ ℎ ↔ ∀ℎ ∈ (Fil‘𝑋)(𝐹 ⊆ ℎ → ¬ 𝑓 ⊊ ℎ)) | 
| 50 |  | simpll 766 | . . . . . 6
⊢ (((𝑓 ∈ (Fil‘𝑋) ∧ 𝐹 ⊆ 𝑓) ∧ ∀ℎ ∈ (Fil‘𝑋)(𝐹 ⊆ ℎ → ¬ 𝑓 ⊊ ℎ)) → 𝑓 ∈ (Fil‘𝑋)) | 
| 51 |  | sstr2 3989 | . . . . . . . . . . 11
⊢ (𝐹 ⊆ 𝑓 → (𝑓 ⊆ ℎ → 𝐹 ⊆ ℎ)) | 
| 52 | 51 | imim1d 82 | . . . . . . . . . 10
⊢ (𝐹 ⊆ 𝑓 → ((𝐹 ⊆ ℎ → ¬ 𝑓 ⊊ ℎ) → (𝑓 ⊆ ℎ → ¬ 𝑓 ⊊ ℎ))) | 
| 53 |  | df-pss 3970 | . . . . . . . . . . . . 13
⊢ (𝑓 ⊊ ℎ ↔ (𝑓 ⊆ ℎ ∧ 𝑓 ≠ ℎ)) | 
| 54 | 53 | simplbi2 500 | . . . . . . . . . . . 12
⊢ (𝑓 ⊆ ℎ → (𝑓 ≠ ℎ → 𝑓 ⊊ ℎ)) | 
| 55 | 54 | necon1bd 2957 | . . . . . . . . . . 11
⊢ (𝑓 ⊆ ℎ → (¬ 𝑓 ⊊ ℎ → 𝑓 = ℎ)) | 
| 56 | 55 | a2i 14 | . . . . . . . . . 10
⊢ ((𝑓 ⊆ ℎ → ¬ 𝑓 ⊊ ℎ) → (𝑓 ⊆ ℎ → 𝑓 = ℎ)) | 
| 57 | 52, 56 | syl6 35 | . . . . . . . . 9
⊢ (𝐹 ⊆ 𝑓 → ((𝐹 ⊆ ℎ → ¬ 𝑓 ⊊ ℎ) → (𝑓 ⊆ ℎ → 𝑓 = ℎ))) | 
| 58 | 57 | ralimdv 3168 | . . . . . . . 8
⊢ (𝐹 ⊆ 𝑓 → (∀ℎ ∈ (Fil‘𝑋)(𝐹 ⊆ ℎ → ¬ 𝑓 ⊊ ℎ) → ∀ℎ ∈ (Fil‘𝑋)(𝑓 ⊆ ℎ → 𝑓 = ℎ))) | 
| 59 | 58 | imp 406 | . . . . . . 7
⊢ ((𝐹 ⊆ 𝑓 ∧ ∀ℎ ∈ (Fil‘𝑋)(𝐹 ⊆ ℎ → ¬ 𝑓 ⊊ ℎ)) → ∀ℎ ∈ (Fil‘𝑋)(𝑓 ⊆ ℎ → 𝑓 = ℎ)) | 
| 60 | 59 | adantll 714 | . . . . . 6
⊢ (((𝑓 ∈ (Fil‘𝑋) ∧ 𝐹 ⊆ 𝑓) ∧ ∀ℎ ∈ (Fil‘𝑋)(𝐹 ⊆ ℎ → ¬ 𝑓 ⊊ ℎ)) → ∀ℎ ∈ (Fil‘𝑋)(𝑓 ⊆ ℎ → 𝑓 = ℎ)) | 
| 61 |  | isufil2 23917 | . . . . . 6
⊢ (𝑓 ∈ (UFil‘𝑋) ↔ (𝑓 ∈ (Fil‘𝑋) ∧ ∀ℎ ∈ (Fil‘𝑋)(𝑓 ⊆ ℎ → 𝑓 = ℎ))) | 
| 62 | 50, 60, 61 | sylanbrc 583 | . . . . 5
⊢ (((𝑓 ∈ (Fil‘𝑋) ∧ 𝐹 ⊆ 𝑓) ∧ ∀ℎ ∈ (Fil‘𝑋)(𝐹 ⊆ ℎ → ¬ 𝑓 ⊊ ℎ)) → 𝑓 ∈ (UFil‘𝑋)) | 
| 63 |  | simplr 768 | . . . . 5
⊢ (((𝑓 ∈ (Fil‘𝑋) ∧ 𝐹 ⊆ 𝑓) ∧ ∀ℎ ∈ (Fil‘𝑋)(𝐹 ⊆ ℎ → ¬ 𝑓 ⊊ ℎ)) → 𝐹 ⊆ 𝑓) | 
| 64 | 62, 63 | jca 511 | . . . 4
⊢ (((𝑓 ∈ (Fil‘𝑋) ∧ 𝐹 ⊆ 𝑓) ∧ ∀ℎ ∈ (Fil‘𝑋)(𝐹 ⊆ ℎ → ¬ 𝑓 ⊊ ℎ)) → (𝑓 ∈ (UFil‘𝑋) ∧ 𝐹 ⊆ 𝑓)) | 
| 65 | 48, 49, 64 | syl2anb 598 | . . 3
⊢ ((𝑓 ∈ {𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔} ∧ ∀ℎ ∈ {𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔} ¬ 𝑓 ⊊ ℎ) → (𝑓 ∈ (UFil‘𝑋) ∧ 𝐹 ⊆ 𝑓)) | 
| 66 | 65 | reximi2 3078 | . 2
⊢
(∃𝑓 ∈
{𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔}∀ℎ ∈ {𝑔 ∈ (Fil‘𝑋) ∣ 𝐹 ⊆ 𝑔} ¬ 𝑓 ⊊ ℎ → ∃𝑓 ∈ (UFil‘𝑋)𝐹 ⊆ 𝑓) | 
| 67 | 46, 66 | syl 17 | 1
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝒫 𝒫
𝑋 ∈ dom card) →
∃𝑓 ∈
(UFil‘𝑋)𝐹 ⊆ 𝑓) |