Metamath Proof Explorer

Theorem ismre

Description: Property of being a Moore collection on some base set. (Contributed by Stefan O'Rear, 30-Jan-2015)

Ref Expression
Assertion ismre 
|- ( C e. ( Moore ` X ) <-> ( C C_ ~P X /\ X e. C /\ A. s e. ~P C ( s =/= (/) -> |^| s e. C ) ) )

Proof

Step Hyp Ref Expression
1 elfvex 
 |-  ( C e. ( Moore ` X ) -> X e. _V )
2 elex 
 |-  ( X e. C -> X e. _V )
3 2 3ad2ant2 
 |-  ( ( C C_ ~P X /\ X e. C /\ A. s e. ~P C ( s =/= (/) -> |^| s e. C ) ) -> X e. _V )
4 pweq 
 |-  ( x = X -> ~P x = ~P X )
5 4 pweqd 
 |-  ( x = X -> ~P ~P x = ~P ~P X )
6 eleq1 
 |-  ( x = X -> ( x e. c <-> X e. c ) )
7 6 anbi1d 
 |-  ( x = X -> ( ( x e. c /\ A. s e. ~P c ( s =/= (/) -> |^| s e. c ) ) <-> ( X e. c /\ A. s e. ~P c ( s =/= (/) -> |^| s e. c ) ) ) )
8 5 7 rabeqbidv 
 |-  ( x = X -> { c e. ~P ~P x | ( x e. c /\ A. s e. ~P c ( s =/= (/) -> |^| s e. c ) ) } = { c e. ~P ~P X | ( X e. c /\ A. s e. ~P c ( s =/= (/) -> |^| s e. c ) ) } )
9 df-mre 
 |-  Moore = ( x e. _V |-> { c e. ~P ~P x | ( x e. c /\ A. s e. ~P c ( s =/= (/) -> |^| s e. c ) ) } )
10 vpwex 
 |-  ~P x e. _V
11 10 pwex 
 |-  ~P ~P x e. _V
12 11 rabex 
 |-  { c e. ~P ~P x | ( x e. c /\ A. s e. ~P c ( s =/= (/) -> |^| s e. c ) ) } e. _V
13 8 9 12 fvmpt3i 
 |-  ( X e. _V -> ( Moore ` X ) = { c e. ~P ~P X | ( X e. c /\ A. s e. ~P c ( s =/= (/) -> |^| s e. c ) ) } )
14 13 eleq2d 
 |-  ( X e. _V -> ( C e. ( Moore ` X ) <-> C e. { c e. ~P ~P X | ( X e. c /\ A. s e. ~P c ( s =/= (/) -> |^| s e. c ) ) } ) )
15 eleq2 
 |-  ( c = C -> ( X e. c <-> X e. C ) )
16 pweq 
 |-  ( c = C -> ~P c = ~P C )
17 eleq2 
 |-  ( c = C -> ( |^| s e. c <-> |^| s e. C ) )
18 17 imbi2d 
 |-  ( c = C -> ( ( s =/= (/) -> |^| s e. c ) <-> ( s =/= (/) -> |^| s e. C ) ) )
19 16 18 raleqbidv 
 |-  ( c = C -> ( A. s e. ~P c ( s =/= (/) -> |^| s e. c ) <-> A. s e. ~P C ( s =/= (/) -> |^| s e. C ) ) )
20 15 19 anbi12d 
 |-  ( c = C -> ( ( X e. c /\ A. s e. ~P c ( s =/= (/) -> |^| s e. c ) ) <-> ( X e. C /\ A. s e. ~P C ( s =/= (/) -> |^| s e. C ) ) ) )
21 20 elrab 
 |-  ( C e. { c e. ~P ~P X | ( X e. c /\ A. s e. ~P c ( s =/= (/) -> |^| s e. c ) ) } <-> ( C e. ~P ~P X /\ ( X e. C /\ A. s e. ~P C ( s =/= (/) -> |^| s e. C ) ) ) )
22 21 a1i 
 |-  ( X e. _V -> ( C e. { c e. ~P ~P X | ( X e. c /\ A. s e. ~P c ( s =/= (/) -> |^| s e. c ) ) } <-> ( C e. ~P ~P X /\ ( X e. C /\ A. s e. ~P C ( s =/= (/) -> |^| s e. C ) ) ) ) )
23 pwexg 
 |-  ( X e. _V -> ~P X e. _V )
24 elpw2g 
 |-  ( ~P X e. _V -> ( C e. ~P ~P X <-> C C_ ~P X ) )
25 23 24 syl 
 |-  ( X e. _V -> ( C e. ~P ~P X <-> C C_ ~P X ) )
26 25 anbi1d 
 |-  ( X e. _V -> ( ( C e. ~P ~P X /\ ( X e. C /\ A. s e. ~P C ( s =/= (/) -> |^| s e. C ) ) ) <-> ( C C_ ~P X /\ ( X e. C /\ A. s e. ~P C ( s =/= (/) -> |^| s e. C ) ) ) ) )
27 3anass 
 |-  ( ( C C_ ~P X /\ X e. C /\ A. s e. ~P C ( s =/= (/) -> |^| s e. C ) ) <-> ( C C_ ~P X /\ ( X e. C /\ A. s e. ~P C ( s =/= (/) -> |^| s e. C ) ) ) )
28 26 27 bitr4di 
 |-  ( X e. _V -> ( ( C e. ~P ~P X /\ ( X e. C /\ A. s e. ~P C ( s =/= (/) -> |^| s e. C ) ) ) <-> ( C C_ ~P X /\ X e. C /\ A. s e. ~P C ( s =/= (/) -> |^| s e. C ) ) ) )
29 14 22 28 3bitrd 
 |-  ( X e. _V -> ( C e. ( Moore ` X ) <-> ( C C_ ~P X /\ X e. C /\ A. s e. ~P C ( s =/= (/) -> |^| s e. C ) ) ) )
30 1 3 29 pm5.21nii 
 |-  ( C e. ( Moore ` X ) <-> ( C C_ ~P X /\ X e. C /\ A. s e. ~P C ( s =/= (/) -> |^| s e. C ) ) )