This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mrisval

Description: Value of the set of independent sets of a Moore system. (Contributed by David Moews, 1-May-2017)

Ref Expression
Hypotheses mrisval.1 
|- N = ( mrCls ` A )
mrisval.2 
|- I = ( mrInd ` A )
Assertion mrisval 
|- ( A e. ( Moore ` X ) -> I = { s e. ~P X | A. x e. s -. x e. ( N ` ( s \ { x } ) ) } )

Proof

Step Hyp Ref Expression
1 mrisval.1 
 |-  N = ( mrCls ` A )
2 mrisval.2 
 |-  I = ( mrInd ` A )
3 fvssunirn 
 |-  ( Moore ` X ) C_ U. ran Moore
4 3 sseli 
 |-  ( A e. ( Moore ` X ) -> A e. U. ran Moore )
5 unieq 
 |-  ( c = A -> U. c = U. A )
6 5 pweqd 
 |-  ( c = A -> ~P U. c = ~P U. A )
7 fveq2 
 |-  ( c = A -> ( mrCls ` c ) = ( mrCls ` A ) )
8 7 1 eqtr4di 
 |-  ( c = A -> ( mrCls ` c ) = N )
9 8 fveq1d 
 |-  ( c = A -> ( ( mrCls ` c ) ` ( s \ { x } ) ) = ( N ` ( s \ { x } ) ) )
10 9 eleq2d 
 |-  ( c = A -> ( x e. ( ( mrCls ` c ) ` ( s \ { x } ) ) <-> x e. ( N ` ( s \ { x } ) ) ) )
11 10 notbid 
 |-  ( c = A -> ( -. x e. ( ( mrCls ` c ) ` ( s \ { x } ) ) <-> -. x e. ( N ` ( s \ { x } ) ) ) )
12 11 ralbidv 
 |-  ( c = A -> ( A. x e. s -. x e. ( ( mrCls ` c ) ` ( s \ { x } ) ) <-> A. x e. s -. x e. ( N ` ( s \ { x } ) ) ) )
13 6 12 rabeqbidv 
 |-  ( c = A -> { s e. ~P U. c | A. x e. s -. x e. ( ( mrCls ` c ) ` ( s \ { x } ) ) } = { s e. ~P U. A | A. x e. s -. x e. ( N ` ( s \ { x } ) ) } )
14 df-mri 
 |-  mrInd = ( c e. U. ran Moore |-> { s e. ~P U. c | A. x e. s -. x e. ( ( mrCls ` c ) ` ( s \ { x } ) ) } )
15 vuniex 
 |-  U. c e. _V
16 15 pwex 
 |-  ~P U. c e. _V
17 16 rabex 
 |-  { s e. ~P U. c | A. x e. s -. x e. ( ( mrCls ` c ) ` ( s \ { x } ) ) } e. _V
18 13 14 17 fvmpt3i 
 |-  ( A e. U. ran Moore -> ( mrInd ` A ) = { s e. ~P U. A | A. x e. s -. x e. ( N ` ( s \ { x } ) ) } )
19 4 18 syl 
 |-  ( A e. ( Moore ` X ) -> ( mrInd ` A ) = { s e. ~P U. A | A. x e. s -. x e. ( N ` ( s \ { x } ) ) } )
20 2 19 eqtrid 
 |-  ( A e. ( Moore ` X ) -> I = { s e. ~P U. A | A. x e. s -. x e. ( N ` ( s \ { x } ) ) } )
21 mreuni 
 |-  ( A e. ( Moore ` X ) -> U. A = X )
22 21 pweqd 
 |-  ( A e. ( Moore ` X ) -> ~P U. A = ~P X )
23 22 rabeqdv 
 |-  ( A e. ( Moore ` X ) -> { s e. ~P U. A | A. x e. s -. x e. ( N ` ( s \ { x } ) ) } = { s e. ~P X | A. x e. s -. x e. ( N ` ( s \ { x } ) ) } )
24 20 23 eqtrd 
 |-  ( A e. ( Moore ` X ) -> I = { s e. ~P X | A. x e. s -. x e. ( N ` ( s \ { x } ) ) } )