Description: In a Moore system whose closure operator has the exchange property, if S is independent and contained in the closure of T , and either S or T is finite, then T dominates S . This is an immediate consequence of mreexexd . (Contributed by David Moews, 1-May-2017)
Ref | Expression | ||
---|---|---|---|
Hypotheses | mreexdomd.1 | |
|
mreexdomd.2 | |
||
mreexdomd.3 | |
||
mreexdomd.4 | |
||
mreexdomd.5 | |
||
mreexdomd.6 | |
||
mreexdomd.7 | |
||
mreexdomd.8 | |
||
Assertion | mreexdomd | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mreexdomd.1 | |
|
2 | mreexdomd.2 | |
|
3 | mreexdomd.3 | |
|
4 | mreexdomd.4 | |
|
5 | mreexdomd.5 | |
|
6 | mreexdomd.6 | |
|
7 | mreexdomd.7 | |
|
8 | mreexdomd.8 | |
|
9 | 3 1 8 | mrissd | |
10 | dif0 | |
|
11 | 9 10 | sseqtrrdi | |
12 | 6 10 | sseqtrrdi | |
13 | un0 | |
|
14 | 13 | fveq2i | |
15 | 5 14 | sseqtrrdi | |
16 | un0 | |
|
17 | 16 8 | eqeltrid | |
18 | 1 2 3 4 11 12 15 17 7 | mreexexd | |
19 | simprrl | |
|
20 | simprl | |
|
21 | 20 | elpwid | |
22 | 1 | elfvexd | |
23 | 22 6 | ssexd | |
24 | ssdomg | |
|
25 | 23 24 | syl | |
26 | 25 | adantr | |
27 | 21 26 | mpd | |
28 | endomtr | |
|
29 | 19 27 28 | syl2anc | |
30 | 18 29 | rexlimddv | |