Metamath Proof Explorer

Theorem bj-ismooredr2

Description: Sufficient condition to be a Moore collection (variant of bj-ismooredr singling out the empty intersection). Note that there is no sethood hypothesis on A : it is a consequence of the first hypothesis. (Contributed by BJ, 9-Dec-2021)

Ref Expression
Hypotheses bj-ismooredr2.1 
|- ( ph -> U. A e. A )
bj-ismooredr2.2 
|- ( ( ph /\ ( x C_ A /\ x =/= (/) ) ) -> |^| x e. A )
Assertion bj-ismooredr2 
|- ( ph -> A e. Moore_ )

Proof

Step Hyp Ref Expression
1 bj-ismooredr2.1 
 |-  ( ph -> U. A e. A )
2 bj-ismooredr2.2 
 |-  ( ( ph /\ ( x C_ A /\ x =/= (/) ) ) -> |^| x e. A )
3 2 anassrs 
 |-  ( ( ( ph /\ x C_ A ) /\ x =/= (/) ) -> |^| x e. A )
4 intssuni2 
 |-  ( ( x C_ A /\ x =/= (/) ) -> |^| x C_ U. A )
5 dfss 
 |-  ( |^| x C_ U. A <-> |^| x = ( |^| x i^i U. A ) )
6 incom 
 |-  ( |^| x i^i U. A ) = ( U. A i^i |^| x )
7 6 eqeq2i 
 |-  ( |^| x = ( |^| x i^i U. A ) <-> |^| x = ( U. A i^i |^| x ) )
8 eleq1 
 |-  ( |^| x = ( U. A i^i |^| x ) -> ( |^| x e. A <-> ( U. A i^i |^| x ) e. A ) )
9 7 8 sylbi 
 |-  ( |^| x = ( |^| x i^i U. A ) -> ( |^| x e. A <-> ( U. A i^i |^| x ) e. A ) )
10 9 biimpd 
 |-  ( |^| x = ( |^| x i^i U. A ) -> ( |^| x e. A -> ( U. A i^i |^| x ) e. A ) )
11 5 10 sylbi 
 |-  ( |^| x C_ U. A -> ( |^| x e. A -> ( U. A i^i |^| x ) e. A ) )
12 4 11 syl 
 |-  ( ( x C_ A /\ x =/= (/) ) -> ( |^| x e. A -> ( U. A i^i |^| x ) e. A ) )
13 12 adantll 
 |-  ( ( ( ph /\ x C_ A ) /\ x =/= (/) ) -> ( |^| x e. A -> ( U. A i^i |^| x ) e. A ) )
14 3 13 mpd 
 |-  ( ( ( ph /\ x C_ A ) /\ x =/= (/) ) -> ( U. A i^i |^| x ) e. A )
15 14 ex 
 |-  ( ( ph /\ x C_ A ) -> ( x =/= (/) -> ( U. A i^i |^| x ) e. A ) )
16 nne 
 |-  ( -. x =/= (/) <-> x = (/) )
17 rint0 
 |-  ( x = (/) -> ( U. A i^i |^| x ) = U. A )
18 eleq1a 
 |-  ( U. A e. A -> ( ( U. A i^i |^| x ) = U. A -> ( U. A i^i |^| x ) e. A ) )
19 1 17 18 syl2im 
 |-  ( ph -> ( x = (/) -> ( U. A i^i |^| x ) e. A ) )
20 16 19 biimtrid 
 |-  ( ph -> ( -. x =/= (/) -> ( U. A i^i |^| x ) e. A ) )
21 20 adantr 
 |-  ( ( ph /\ x C_ A ) -> ( -. x =/= (/) -> ( U. A i^i |^| x ) e. A ) )
22 15 21 pm2.61d 
 |-  ( ( ph /\ x C_ A ) -> ( U. A i^i |^| x ) e. A )
23 22 bj-ismooredr 
 |-  ( ph -> A e. Moore_ )