Description: Sufficient condition to be a Moore collection. Note that there is no sethood hypothesis on A : it is a consequence of the only hypothesis. (Contributed by BJ, 9-Dec-2021)
Ref | Expression | ||
---|---|---|---|
Hypothesis | bj-ismooredr.1 | |- ( ( ph /\ x C_ A ) -> ( U. A i^i |^| x ) e. A ) |
|
Assertion | bj-ismooredr | |- ( ph -> A e. Moore_ ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bj-ismooredr.1 | |- ( ( ph /\ x C_ A ) -> ( U. A i^i |^| x ) e. A ) |
|
2 | elpwi | |- ( x e. ~P A -> x C_ A ) |
|
3 | 1 | ex | |- ( ph -> ( x C_ A -> ( U. A i^i |^| x ) e. A ) ) |
4 | 2 3 | syl5 | |- ( ph -> ( x e. ~P A -> ( U. A i^i |^| x ) e. A ) ) |
5 | 4 | ralrimiv | |- ( ph -> A. x e. ~P A ( U. A i^i |^| x ) e. A ) |
6 | bj-ismoore | |- ( A e. Moore_ <-> A. x e. ~P A ( U. A i^i |^| x ) e. A ) |
|
7 | 5 6 | sylibr | |- ( ph -> A e. Moore_ ) |