Step |
Hyp |
Ref |
Expression |
1 |
|
mrcfval.f |
|- F = ( mrCls ` C ) |
2 |
1
|
mrcid |
|- ( ( C e. ( Moore ` X ) /\ U e. C ) -> ( F ` U ) = U ) |
3 |
|
simpr |
|- ( ( C e. ( Moore ` X ) /\ ( F ` U ) = U ) -> ( F ` U ) = U ) |
4 |
1
|
mrcssv |
|- ( C e. ( Moore ` X ) -> ( F ` U ) C_ X ) |
5 |
4
|
adantr |
|- ( ( C e. ( Moore ` X ) /\ ( F ` U ) = U ) -> ( F ` U ) C_ X ) |
6 |
3 5
|
eqsstrrd |
|- ( ( C e. ( Moore ` X ) /\ ( F ` U ) = U ) -> U C_ X ) |
7 |
1
|
mrccl |
|- ( ( C e. ( Moore ` X ) /\ U C_ X ) -> ( F ` U ) e. C ) |
8 |
6 7
|
syldan |
|- ( ( C e. ( Moore ` X ) /\ ( F ` U ) = U ) -> ( F ` U ) e. C ) |
9 |
3 8
|
eqeltrrd |
|- ( ( C e. ( Moore ` X ) /\ ( F ` U ) = U ) -> U e. C ) |
10 |
2 9
|
impbida |
|- ( C e. ( Moore ` X ) -> ( U e. C <-> ( F ` U ) = U ) ) |