Step |
Hyp |
Ref |
Expression |
1 |
|
breq1 |
|- ( |^| F = (/) -> ( |^| F ~<_ 1o <-> (/) ~<_ 1o ) ) |
2 |
|
uffixsn |
|- ( ( F e. ( UFil ` X ) /\ x e. |^| F ) -> { x } e. F ) |
3 |
|
intss1 |
|- ( { x } e. F -> |^| F C_ { x } ) |
4 |
2 3
|
syl |
|- ( ( F e. ( UFil ` X ) /\ x e. |^| F ) -> |^| F C_ { x } ) |
5 |
|
simpr |
|- ( ( F e. ( UFil ` X ) /\ x e. |^| F ) -> x e. |^| F ) |
6 |
5
|
snssd |
|- ( ( F e. ( UFil ` X ) /\ x e. |^| F ) -> { x } C_ |^| F ) |
7 |
4 6
|
eqssd |
|- ( ( F e. ( UFil ` X ) /\ x e. |^| F ) -> |^| F = { x } ) |
8 |
7
|
ex |
|- ( F e. ( UFil ` X ) -> ( x e. |^| F -> |^| F = { x } ) ) |
9 |
8
|
eximdv |
|- ( F e. ( UFil ` X ) -> ( E. x x e. |^| F -> E. x |^| F = { x } ) ) |
10 |
|
n0 |
|- ( |^| F =/= (/) <-> E. x x e. |^| F ) |
11 |
|
en1 |
|- ( |^| F ~~ 1o <-> E. x |^| F = { x } ) |
12 |
9 10 11
|
3imtr4g |
|- ( F e. ( UFil ` X ) -> ( |^| F =/= (/) -> |^| F ~~ 1o ) ) |
13 |
12
|
imp |
|- ( ( F e. ( UFil ` X ) /\ |^| F =/= (/) ) -> |^| F ~~ 1o ) |
14 |
|
endom |
|- ( |^| F ~~ 1o -> |^| F ~<_ 1o ) |
15 |
13 14
|
syl |
|- ( ( F e. ( UFil ` X ) /\ |^| F =/= (/) ) -> |^| F ~<_ 1o ) |
16 |
|
1on |
|- 1o e. On |
17 |
|
0domg |
|- ( 1o e. On -> (/) ~<_ 1o ) |
18 |
16 17
|
mp1i |
|- ( F e. ( UFil ` X ) -> (/) ~<_ 1o ) |
19 |
1 15 18
|
pm2.61ne |
|- ( F e. ( UFil ` X ) -> |^| F ~<_ 1o ) |