This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )