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

Metamath Proof Explorer

Theorem acsexdimd

Description: In an algebraic closure system whose closure operator has the exchange property, if two independent sets have equal closure, they are equinumerous. See mreexfidimd for the finite case and acsinfdimd for the infinite case. This is a special case of Theorem 4.2.2 in FaureFrolicher p. 87. (Contributed by David Moews, 1-May-2017)

Ref Expression
Hypotheses acsexdimd.1 
|- ( ph -> A e. ( ACS ` X ) )
acsexdimd.2 
|- N = ( mrCls ` A )
acsexdimd.3 
|- I = ( mrInd ` A )
acsexdimd.4 
|- ( ph -> A. s e. ~P X A. y e. X A. z e. ( ( N ` ( s u. { y } ) ) \ ( N ` s ) ) y e. ( N ` ( s u. { z } ) ) )
acsexdimd.5 
|- ( ph -> S e. I )
acsexdimd.6 
|- ( ph -> T e. I )
acsexdimd.7 
|- ( ph -> ( N ` S ) = ( N ` T ) )
Assertion acsexdimd 
|- ( ph -> S ~~ T )

Proof

Step Hyp Ref Expression
1 acsexdimd.1 
 |-  ( ph -> A e. ( ACS ` X ) )
2 acsexdimd.2 
 |-  N = ( mrCls ` A )
3 acsexdimd.3 
 |-  I = ( mrInd ` A )
4 acsexdimd.4 
 |-  ( ph -> A. s e. ~P X A. y e. X A. z e. ( ( N ` ( s u. { y } ) ) \ ( N ` s ) ) y e. ( N ` ( s u. { z } ) ) )
5 acsexdimd.5 
 |-  ( ph -> S e. I )
6 acsexdimd.6 
 |-  ( ph -> T e. I )
7 acsexdimd.7 
 |-  ( ph -> ( N ` S ) = ( N ` T ) )
8 1 acsmred 
 |-  ( ph -> A e. ( Moore ` X ) )
9 8 adantr 
 |-  ( ( ph /\ S e. Fin ) -> A e. ( Moore ` X ) )
10 4 adantr 
 |-  ( ( ph /\ S e. Fin ) -> A. s e. ~P X A. y e. X A. z e. ( ( N ` ( s u. { y } ) ) \ ( N ` s ) ) y e. ( N ` ( s u. { z } ) ) )
11 5 adantr 
 |-  ( ( ph /\ S e. Fin ) -> S e. I )
12 6 adantr 
 |-  ( ( ph /\ S e. Fin ) -> T e. I )
13 simpr 
 |-  ( ( ph /\ S e. Fin ) -> S e. Fin )
14 7 adantr 
 |-  ( ( ph /\ S e. Fin ) -> ( N ` S ) = ( N ` T ) )
15 9 2 3 10 11 12 13 14 mreexfidimd 
 |-  ( ( ph /\ S e. Fin ) -> S ~~ T )
16 1 adantr 
 |-  ( ( ph /\ -. S e. Fin ) -> A e. ( ACS ` X ) )
17 5 adantr 
 |-  ( ( ph /\ -. S e. Fin ) -> S e. I )
18 6 adantr 
 |-  ( ( ph /\ -. S e. Fin ) -> T e. I )
19 7 adantr 
 |-  ( ( ph /\ -. S e. Fin ) -> ( N ` S ) = ( N ` T ) )
20 simpr 
 |-  ( ( ph /\ -. S e. Fin ) -> -. S e. Fin )
21 16 2 3 17 18 19 20 acsinfdimd 
 |-  ( ( ph /\ -. S e. Fin ) -> S ~~ T )
22 15 21 pm2.61dan 
 |-  ( ph -> S ~~ T )