Step |
Hyp |
Ref |
Expression |
1 |
|
simpr |
⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝒫 𝒫 𝑋 ∈ dom card ) → 𝒫 𝒫 𝑋 ∈ dom card ) |
2 |
|
rabss |
⊢ ( { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹 ⊆ 𝑔 } ⊆ 𝒫 𝒫 𝑋 ↔ ∀ 𝑔 ∈ ( Fil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑔 → 𝑔 ∈ 𝒫 𝒫 𝑋 ) ) |
3 |
|
filsspw |
⊢ ( 𝑔 ∈ ( Fil ‘ 𝑋 ) → 𝑔 ⊆ 𝒫 𝑋 ) |
4 |
|
velpw |
⊢ ( 𝑔 ∈ 𝒫 𝒫 𝑋 ↔ 𝑔 ⊆ 𝒫 𝑋 ) |
5 |
3 4
|
sylibr |
⊢ ( 𝑔 ∈ ( Fil ‘ 𝑋 ) → 𝑔 ∈ 𝒫 𝒫 𝑋 ) |
6 |
5
|
a1d |
⊢ ( 𝑔 ∈ ( Fil ‘ 𝑋 ) → ( 𝐹 ⊆ 𝑔 → 𝑔 ∈ 𝒫 𝒫 𝑋 ) ) |
7 |
2 6
|
mprgbir |
⊢ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹 ⊆ 𝑔 } ⊆ 𝒫 𝒫 𝑋 |
8 |
|
ssnum |
⊢ ( ( 𝒫 𝒫 𝑋 ∈ dom card ∧ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹 ⊆ 𝑔 } ⊆ 𝒫 𝒫 𝑋 ) → { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹 ⊆ 𝑔 } ∈ dom card ) |
9 |
1 7 8
|
sylancl |
⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝒫 𝒫 𝑋 ∈ dom card ) → { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹 ⊆ 𝑔 } ∈ dom card ) |
10 |
|
ssid |
⊢ 𝐹 ⊆ 𝐹 |
11 |
10
|
jctr |
⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 ⊆ 𝐹 ) ) |
12 |
|
sseq2 |
⊢ ( 𝑔 = 𝐹 → ( 𝐹 ⊆ 𝑔 ↔ 𝐹 ⊆ 𝐹 ) ) |
13 |
12
|
elrab |
⊢ ( 𝐹 ∈ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹 ⊆ 𝑔 } ↔ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 ⊆ 𝐹 ) ) |
14 |
11 13
|
sylibr |
⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝐹 ∈ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹 ⊆ 𝑔 } ) |
15 |
14
|
ne0d |
⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹 ⊆ 𝑔 } ≠ ∅ ) |
16 |
15
|
adantr |
⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝒫 𝒫 𝑋 ∈ dom card ) → { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹 ⊆ 𝑔 } ≠ ∅ ) |
17 |
|
sseq2 |
⊢ ( 𝑔 = ∪ 𝑥 → ( 𝐹 ⊆ 𝑔 ↔ 𝐹 ⊆ ∪ 𝑥 ) ) |
18 |
|
simpr1 |
⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑥 ⊆ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹 ⊆ 𝑔 } ∧ 𝑥 ≠ ∅ ∧ [⊊] Or 𝑥 ) ) → 𝑥 ⊆ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹 ⊆ 𝑔 } ) |
19 |
|
ssrab |
⊢ ( 𝑥 ⊆ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹 ⊆ 𝑔 } ↔ ( 𝑥 ⊆ ( Fil ‘ 𝑋 ) ∧ ∀ 𝑔 ∈ 𝑥 𝐹 ⊆ 𝑔 ) ) |
20 |
18 19
|
sylib |
⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑥 ⊆ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹 ⊆ 𝑔 } ∧ 𝑥 ≠ ∅ ∧ [⊊] Or 𝑥 ) ) → ( 𝑥 ⊆ ( Fil ‘ 𝑋 ) ∧ ∀ 𝑔 ∈ 𝑥 𝐹 ⊆ 𝑔 ) ) |
21 |
20
|
simpld |
⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑥 ⊆ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹 ⊆ 𝑔 } ∧ 𝑥 ≠ ∅ ∧ [⊊] Or 𝑥 ) ) → 𝑥 ⊆ ( Fil ‘ 𝑋 ) ) |
22 |
|
simpr2 |
⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑥 ⊆ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹 ⊆ 𝑔 } ∧ 𝑥 ≠ ∅ ∧ [⊊] Or 𝑥 ) ) → 𝑥 ≠ ∅ ) |
23 |
|
simpr3 |
⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑥 ⊆ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹 ⊆ 𝑔 } ∧ 𝑥 ≠ ∅ ∧ [⊊] Or 𝑥 ) ) → [⊊] Or 𝑥 ) |
24 |
|
sorpssun |
⊢ ( ( [⊊] Or 𝑥 ∧ ( 𝑔 ∈ 𝑥 ∧ ℎ ∈ 𝑥 ) ) → ( 𝑔 ∪ ℎ ) ∈ 𝑥 ) |
25 |
24
|
ralrimivva |
⊢ ( [⊊] Or 𝑥 → ∀ 𝑔 ∈ 𝑥 ∀ ℎ ∈ 𝑥 ( 𝑔 ∪ ℎ ) ∈ 𝑥 ) |
26 |
23 25
|
syl |
⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑥 ⊆ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹 ⊆ 𝑔 } ∧ 𝑥 ≠ ∅ ∧ [⊊] Or 𝑥 ) ) → ∀ 𝑔 ∈ 𝑥 ∀ ℎ ∈ 𝑥 ( 𝑔 ∪ ℎ ) ∈ 𝑥 ) |
27 |
|
filuni |
⊢ ( ( 𝑥 ⊆ ( Fil ‘ 𝑋 ) ∧ 𝑥 ≠ ∅ ∧ ∀ 𝑔 ∈ 𝑥 ∀ ℎ ∈ 𝑥 ( 𝑔 ∪ ℎ ) ∈ 𝑥 ) → ∪ 𝑥 ∈ ( Fil ‘ 𝑋 ) ) |
28 |
21 22 26 27
|
syl3anc |
⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑥 ⊆ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹 ⊆ 𝑔 } ∧ 𝑥 ≠ ∅ ∧ [⊊] Or 𝑥 ) ) → ∪ 𝑥 ∈ ( Fil ‘ 𝑋 ) ) |
29 |
|
n0 |
⊢ ( 𝑥 ≠ ∅ ↔ ∃ ℎ ℎ ∈ 𝑥 ) |
30 |
|
ssel2 |
⊢ ( ( 𝑥 ⊆ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹 ⊆ 𝑔 } ∧ ℎ ∈ 𝑥 ) → ℎ ∈ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹 ⊆ 𝑔 } ) |
31 |
|
sseq2 |
⊢ ( 𝑔 = ℎ → ( 𝐹 ⊆ 𝑔 ↔ 𝐹 ⊆ ℎ ) ) |
32 |
31
|
elrab |
⊢ ( ℎ ∈ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹 ⊆ 𝑔 } ↔ ( ℎ ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 ⊆ ℎ ) ) |
33 |
30 32
|
sylib |
⊢ ( ( 𝑥 ⊆ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹 ⊆ 𝑔 } ∧ ℎ ∈ 𝑥 ) → ( ℎ ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 ⊆ ℎ ) ) |
34 |
33
|
simprd |
⊢ ( ( 𝑥 ⊆ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹 ⊆ 𝑔 } ∧ ℎ ∈ 𝑥 ) → 𝐹 ⊆ ℎ ) |
35 |
|
ssuni |
⊢ ( ( 𝐹 ⊆ ℎ ∧ ℎ ∈ 𝑥 ) → 𝐹 ⊆ ∪ 𝑥 ) |
36 |
34 35
|
sylancom |
⊢ ( ( 𝑥 ⊆ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹 ⊆ 𝑔 } ∧ ℎ ∈ 𝑥 ) → 𝐹 ⊆ ∪ 𝑥 ) |
37 |
36
|
ex |
⊢ ( 𝑥 ⊆ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹 ⊆ 𝑔 } → ( ℎ ∈ 𝑥 → 𝐹 ⊆ ∪ 𝑥 ) ) |
38 |
37
|
exlimdv |
⊢ ( 𝑥 ⊆ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹 ⊆ 𝑔 } → ( ∃ ℎ ℎ ∈ 𝑥 → 𝐹 ⊆ ∪ 𝑥 ) ) |
39 |
29 38
|
syl5bi |
⊢ ( 𝑥 ⊆ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹 ⊆ 𝑔 } → ( 𝑥 ≠ ∅ → 𝐹 ⊆ ∪ 𝑥 ) ) |
40 |
18 22 39
|
sylc |
⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑥 ⊆ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹 ⊆ 𝑔 } ∧ 𝑥 ≠ ∅ ∧ [⊊] Or 𝑥 ) ) → 𝐹 ⊆ ∪ 𝑥 ) |
41 |
17 28 40
|
elrabd |
⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑥 ⊆ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹 ⊆ 𝑔 } ∧ 𝑥 ≠ ∅ ∧ [⊊] Or 𝑥 ) ) → ∪ 𝑥 ∈ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹 ⊆ 𝑔 } ) |
42 |
41
|
ex |
⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( ( 𝑥 ⊆ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹 ⊆ 𝑔 } ∧ 𝑥 ≠ ∅ ∧ [⊊] Or 𝑥 ) → ∪ 𝑥 ∈ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹 ⊆ 𝑔 } ) ) |
43 |
42
|
alrimiv |
⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ∀ 𝑥 ( ( 𝑥 ⊆ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹 ⊆ 𝑔 } ∧ 𝑥 ≠ ∅ ∧ [⊊] Or 𝑥 ) → ∪ 𝑥 ∈ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹 ⊆ 𝑔 } ) ) |
44 |
43
|
adantr |
⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝒫 𝒫 𝑋 ∈ dom card ) → ∀ 𝑥 ( ( 𝑥 ⊆ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹 ⊆ 𝑔 } ∧ 𝑥 ≠ ∅ ∧ [⊊] Or 𝑥 ) → ∪ 𝑥 ∈ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹 ⊆ 𝑔 } ) ) |
45 |
|
zornn0g |
⊢ ( ( { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹 ⊆ 𝑔 } ∈ dom card ∧ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹 ⊆ 𝑔 } ≠ ∅ ∧ ∀ 𝑥 ( ( 𝑥 ⊆ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹 ⊆ 𝑔 } ∧ 𝑥 ≠ ∅ ∧ [⊊] Or 𝑥 ) → ∪ 𝑥 ∈ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹 ⊆ 𝑔 } ) ) → ∃ 𝑓 ∈ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹 ⊆ 𝑔 } ∀ ℎ ∈ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹 ⊆ 𝑔 } ¬ 𝑓 ⊊ ℎ ) |
46 |
9 16 44 45
|
syl3anc |
⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝒫 𝒫 𝑋 ∈ dom card ) → ∃ 𝑓 ∈ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹 ⊆ 𝑔 } ∀ ℎ ∈ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹 ⊆ 𝑔 } ¬ 𝑓 ⊊ ℎ ) |
47 |
|
sseq2 |
⊢ ( 𝑔 = 𝑓 → ( 𝐹 ⊆ 𝑔 ↔ 𝐹 ⊆ 𝑓 ) ) |
48 |
47
|
elrab |
⊢ ( 𝑓 ∈ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹 ⊆ 𝑔 } ↔ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 ⊆ 𝑓 ) ) |
49 |
31
|
ralrab |
⊢ ( ∀ ℎ ∈ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹 ⊆ 𝑔 } ¬ 𝑓 ⊊ ℎ ↔ ∀ ℎ ∈ ( Fil ‘ 𝑋 ) ( 𝐹 ⊆ ℎ → ¬ 𝑓 ⊊ ℎ ) ) |
50 |
|
simpll |
⊢ ( ( ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 ⊆ 𝑓 ) ∧ ∀ ℎ ∈ ( Fil ‘ 𝑋 ) ( 𝐹 ⊆ ℎ → ¬ 𝑓 ⊊ ℎ ) ) → 𝑓 ∈ ( Fil ‘ 𝑋 ) ) |
51 |
|
sstr2 |
⊢ ( 𝐹 ⊆ 𝑓 → ( 𝑓 ⊆ ℎ → 𝐹 ⊆ ℎ ) ) |
52 |
51
|
imim1d |
⊢ ( 𝐹 ⊆ 𝑓 → ( ( 𝐹 ⊆ ℎ → ¬ 𝑓 ⊊ ℎ ) → ( 𝑓 ⊆ ℎ → ¬ 𝑓 ⊊ ℎ ) ) ) |
53 |
|
df-pss |
⊢ ( 𝑓 ⊊ ℎ ↔ ( 𝑓 ⊆ ℎ ∧ 𝑓 ≠ ℎ ) ) |
54 |
53
|
simplbi2 |
⊢ ( 𝑓 ⊆ ℎ → ( 𝑓 ≠ ℎ → 𝑓 ⊊ ℎ ) ) |
55 |
54
|
necon1bd |
⊢ ( 𝑓 ⊆ ℎ → ( ¬ 𝑓 ⊊ ℎ → 𝑓 = ℎ ) ) |
56 |
55
|
a2i |
⊢ ( ( 𝑓 ⊆ ℎ → ¬ 𝑓 ⊊ ℎ ) → ( 𝑓 ⊆ ℎ → 𝑓 = ℎ ) ) |
57 |
52 56
|
syl6 |
⊢ ( 𝐹 ⊆ 𝑓 → ( ( 𝐹 ⊆ ℎ → ¬ 𝑓 ⊊ ℎ ) → ( 𝑓 ⊆ ℎ → 𝑓 = ℎ ) ) ) |
58 |
57
|
ralimdv |
⊢ ( 𝐹 ⊆ 𝑓 → ( ∀ ℎ ∈ ( Fil ‘ 𝑋 ) ( 𝐹 ⊆ ℎ → ¬ 𝑓 ⊊ ℎ ) → ∀ ℎ ∈ ( Fil ‘ 𝑋 ) ( 𝑓 ⊆ ℎ → 𝑓 = ℎ ) ) ) |
59 |
58
|
imp |
⊢ ( ( 𝐹 ⊆ 𝑓 ∧ ∀ ℎ ∈ ( Fil ‘ 𝑋 ) ( 𝐹 ⊆ ℎ → ¬ 𝑓 ⊊ ℎ ) ) → ∀ ℎ ∈ ( Fil ‘ 𝑋 ) ( 𝑓 ⊆ ℎ → 𝑓 = ℎ ) ) |
60 |
59
|
adantll |
⊢ ( ( ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 ⊆ 𝑓 ) ∧ ∀ ℎ ∈ ( Fil ‘ 𝑋 ) ( 𝐹 ⊆ ℎ → ¬ 𝑓 ⊊ ℎ ) ) → ∀ ℎ ∈ ( Fil ‘ 𝑋 ) ( 𝑓 ⊆ ℎ → 𝑓 = ℎ ) ) |
61 |
|
isufil2 |
⊢ ( 𝑓 ∈ ( UFil ‘ 𝑋 ) ↔ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ ∀ ℎ ∈ ( Fil ‘ 𝑋 ) ( 𝑓 ⊆ ℎ → 𝑓 = ℎ ) ) ) |
62 |
50 60 61
|
sylanbrc |
⊢ ( ( ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 ⊆ 𝑓 ) ∧ ∀ ℎ ∈ ( Fil ‘ 𝑋 ) ( 𝐹 ⊆ ℎ → ¬ 𝑓 ⊊ ℎ ) ) → 𝑓 ∈ ( UFil ‘ 𝑋 ) ) |
63 |
|
simplr |
⊢ ( ( ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 ⊆ 𝑓 ) ∧ ∀ ℎ ∈ ( Fil ‘ 𝑋 ) ( 𝐹 ⊆ ℎ → ¬ 𝑓 ⊊ ℎ ) ) → 𝐹 ⊆ 𝑓 ) |
64 |
62 63
|
jca |
⊢ ( ( ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 ⊆ 𝑓 ) ∧ ∀ ℎ ∈ ( Fil ‘ 𝑋 ) ( 𝐹 ⊆ ℎ → ¬ 𝑓 ⊊ ℎ ) ) → ( 𝑓 ∈ ( UFil ‘ 𝑋 ) ∧ 𝐹 ⊆ 𝑓 ) ) |
65 |
48 49 64
|
syl2anb |
⊢ ( ( 𝑓 ∈ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹 ⊆ 𝑔 } ∧ ∀ ℎ ∈ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹 ⊆ 𝑔 } ¬ 𝑓 ⊊ ℎ ) → ( 𝑓 ∈ ( UFil ‘ 𝑋 ) ∧ 𝐹 ⊆ 𝑓 ) ) |
66 |
65
|
reximi2 |
⊢ ( ∃ 𝑓 ∈ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹 ⊆ 𝑔 } ∀ ℎ ∈ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹 ⊆ 𝑔 } ¬ 𝑓 ⊊ ℎ → ∃ 𝑓 ∈ ( UFil ‘ 𝑋 ) 𝐹 ⊆ 𝑓 ) |
67 |
46 66
|
syl |
⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝒫 𝒫 𝑋 ∈ dom card ) → ∃ 𝑓 ∈ ( UFil ‘ 𝑋 ) 𝐹 ⊆ 𝑓 ) |