Metamath Proof Explorer


Theorem mreexdomd

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
|- ( ph -> A e. ( Moore ` X ) )
mreexdomd.2
|- N = ( mrCls ` A )
mreexdomd.3
|- I = ( mrInd ` A )
mreexdomd.4
|- ( ph -> A. s e. ~P X A. y e. X A. z e. ( ( N ` ( s u. { y } ) ) \ ( N ` s ) ) y e. ( N ` ( s u. { z } ) ) )
mreexdomd.5
|- ( ph -> S C_ ( N ` T ) )
mreexdomd.6
|- ( ph -> T C_ X )
mreexdomd.7
|- ( ph -> ( S e. Fin \/ T e. Fin ) )
mreexdomd.8
|- ( ph -> S e. I )
Assertion mreexdomd
|- ( ph -> S ~<_ T )

Proof

Step Hyp Ref Expression
1 mreexdomd.1
 |-  ( ph -> A e. ( Moore ` X ) )
2 mreexdomd.2
 |-  N = ( mrCls ` A )
3 mreexdomd.3
 |-  I = ( mrInd ` A )
4 mreexdomd.4
 |-  ( ph -> A. s e. ~P X A. y e. X A. z e. ( ( N ` ( s u. { y } ) ) \ ( N ` s ) ) y e. ( N ` ( s u. { z } ) ) )
5 mreexdomd.5
 |-  ( ph -> S C_ ( N ` T ) )
6 mreexdomd.6
 |-  ( ph -> T C_ X )
7 mreexdomd.7
 |-  ( ph -> ( S e. Fin \/ T e. Fin ) )
8 mreexdomd.8
 |-  ( ph -> S e. I )
9 3 1 8 mrissd
 |-  ( ph -> S C_ X )
10 dif0
 |-  ( X \ (/) ) = X
11 9 10 sseqtrrdi
 |-  ( ph -> S C_ ( X \ (/) ) )
12 6 10 sseqtrrdi
 |-  ( ph -> T C_ ( X \ (/) ) )
13 un0
 |-  ( T u. (/) ) = T
14 13 fveq2i
 |-  ( N ` ( T u. (/) ) ) = ( N ` T )
15 5 14 sseqtrrdi
 |-  ( ph -> S C_ ( N ` ( T u. (/) ) ) )
16 un0
 |-  ( S u. (/) ) = S
17 16 8 eqeltrid
 |-  ( ph -> ( S u. (/) ) e. I )
18 1 2 3 4 11 12 15 17 7 mreexexd
 |-  ( ph -> E. i e. ~P T ( S ~~ i /\ ( i u. (/) ) e. I ) )
19 simprrl
 |-  ( ( ph /\ ( i e. ~P T /\ ( S ~~ i /\ ( i u. (/) ) e. I ) ) ) -> S ~~ i )
20 simprl
 |-  ( ( ph /\ ( i e. ~P T /\ ( S ~~ i /\ ( i u. (/) ) e. I ) ) ) -> i e. ~P T )
21 20 elpwid
 |-  ( ( ph /\ ( i e. ~P T /\ ( S ~~ i /\ ( i u. (/) ) e. I ) ) ) -> i C_ T )
22 1 elfvexd
 |-  ( ph -> X e. _V )
23 22 6 ssexd
 |-  ( ph -> T e. _V )
24 ssdomg
 |-  ( T e. _V -> ( i C_ T -> i ~<_ T ) )
25 23 24 syl
 |-  ( ph -> ( i C_ T -> i ~<_ T ) )
26 25 adantr
 |-  ( ( ph /\ ( i e. ~P T /\ ( S ~~ i /\ ( i u. (/) ) e. I ) ) ) -> ( i C_ T -> i ~<_ T ) )
27 21 26 mpd
 |-  ( ( ph /\ ( i e. ~P T /\ ( S ~~ i /\ ( i u. (/) ) e. I ) ) ) -> i ~<_ T )
28 endomtr
 |-  ( ( S ~~ i /\ i ~<_ T ) -> S ~<_ T )
29 19 27 28 syl2anc
 |-  ( ( ph /\ ( i e. ~P T /\ ( S ~~ i /\ ( i u. (/) ) e. I ) ) ) -> S ~<_ T )
30 18 29 rexlimddv
 |-  ( ph -> S ~<_ T )