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 ) |