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	⊢ ( 𝜑 → 𝐴 ∈ ( ACS ‘ 𝑋 ) )
	acsexdimd.2	⊢ 𝑁 = ( mrCls ‘ 𝐴 )
	acsexdimd.3	⊢ 𝐼 = ( mrInd ‘ 𝐴 )
	acsexdimd.4	⊢ ( 𝜑 → ∀ 𝑠 ∈ 𝒫 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ ( ( 𝑁 ‘ ( 𝑠 ∪ { 𝑦 } ) ) ∖ ( 𝑁 ‘ 𝑠 ) ) 𝑦 ∈ ( 𝑁 ‘ ( 𝑠 ∪ { 𝑧 } ) ) )
	acsexdimd.5	⊢ ( 𝜑 → 𝑆 ∈ 𝐼 )
	acsexdimd.6	⊢ ( 𝜑 → 𝑇 ∈ 𝐼 )
	acsexdimd.7	⊢ ( 𝜑 → ( 𝑁 ‘ 𝑆 ) = ( 𝑁 ‘ 𝑇 ) )
Assertion	acsexdimd	⊢ ( 𝜑 → 𝑆 ≈ 𝑇 )

Proof

Step	Hyp	Ref	Expression
1		acsexdimd.1	⊢ ( 𝜑 → 𝐴 ∈ ( ACS ‘ 𝑋 ) )
2		acsexdimd.2	⊢ 𝑁 = ( mrCls ‘ 𝐴 )
3		acsexdimd.3	⊢ 𝐼 = ( mrInd ‘ 𝐴 )
4		acsexdimd.4	⊢ ( 𝜑 → ∀ 𝑠 ∈ 𝒫 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ ( ( 𝑁 ‘ ( 𝑠 ∪ { 𝑦 } ) ) ∖ ( 𝑁 ‘ 𝑠 ) ) 𝑦 ∈ ( 𝑁 ‘ ( 𝑠 ∪ { 𝑧 } ) ) )
5		acsexdimd.5	⊢ ( 𝜑 → 𝑆 ∈ 𝐼 )
6		acsexdimd.6	⊢ ( 𝜑 → 𝑇 ∈ 𝐼 )
7		acsexdimd.7	⊢ ( 𝜑 → ( 𝑁 ‘ 𝑆 ) = ( 𝑁 ‘ 𝑇 ) )
8	1	acsmred	⊢ ( 𝜑 → 𝐴 ∈ ( Moore ‘ 𝑋 ) )
9	8	adantr	⊢ ( ( 𝜑 ∧ 𝑆 ∈ Fin ) → 𝐴 ∈ ( Moore ‘ 𝑋 ) )
10	4	adantr	⊢ ( ( 𝜑 ∧ 𝑆 ∈ Fin ) → ∀ 𝑠 ∈ 𝒫 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ ( ( 𝑁 ‘ ( 𝑠 ∪ { 𝑦 } ) ) ∖ ( 𝑁 ‘ 𝑠 ) ) 𝑦 ∈ ( 𝑁 ‘ ( 𝑠 ∪ { 𝑧 } ) ) )
11	5	adantr	⊢ ( ( 𝜑 ∧ 𝑆 ∈ Fin ) → 𝑆 ∈ 𝐼 )
12	6	adantr	⊢ ( ( 𝜑 ∧ 𝑆 ∈ Fin ) → 𝑇 ∈ 𝐼 )
13		simpr	⊢ ( ( 𝜑 ∧ 𝑆 ∈ Fin ) → 𝑆 ∈ Fin )
14	7	adantr	⊢ ( ( 𝜑 ∧ 𝑆 ∈ Fin ) → ( 𝑁 ‘ 𝑆 ) = ( 𝑁 ‘ 𝑇 ) )
15	9 2 3 10 11 12 13 14	mreexfidimd	⊢ ( ( 𝜑 ∧ 𝑆 ∈ Fin ) → 𝑆 ≈ 𝑇 )
16	1	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝑆 ∈ Fin ) → 𝐴 ∈ ( ACS ‘ 𝑋 ) )
17	5	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝑆 ∈ Fin ) → 𝑆 ∈ 𝐼 )
18	6	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝑆 ∈ Fin ) → 𝑇 ∈ 𝐼 )
19	7	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝑆 ∈ Fin ) → ( 𝑁 ‘ 𝑆 ) = ( 𝑁 ‘ 𝑇 ) )
20		simpr	⊢ ( ( 𝜑 ∧ ¬ 𝑆 ∈ Fin ) → ¬ 𝑆 ∈ Fin )
21	16 2 3 17 18 19 20	acsinfdimd	⊢ ( ( 𝜑 ∧ ¬ 𝑆 ∈ Fin ) → 𝑆 ≈ 𝑇 )
22	15 21	pm2.61dan	⊢ ( 𝜑 → 𝑆 ≈ 𝑇 )

Metamath Proof Explorer

Theorem acsexdimd

Proof