Theorem mreexfidimd

Description: In a Moore system whose closure operator has the exchange property, if two independent sets have equal closure and one is finite, then they are equinumerous. Proven by using mreexdomd twice. This implies a special case of Theorem 4.2.2 in FaureFrolicher p. 87. (Contributed by David Moews, 1-May-2017)

	Ref	Expression
Hypotheses	mreexfidimd.1	⊢ ( 𝜑 → 𝐴 ∈ ( Moore ‘ 𝑋 ) )
	mreexfidimd.2	⊢ 𝑁 = ( mrCls ‘ 𝐴 )
	mreexfidimd.3	⊢ 𝐼 = ( mrInd ‘ 𝐴 )
	mreexfidimd.4	⊢ ( 𝜑 → ∀ 𝑠 ∈ 𝒫 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ ( ( 𝑁 ‘ ( 𝑠 ∪ { 𝑦 } ) ) ∖ ( 𝑁 ‘ 𝑠 ) ) 𝑦 ∈ ( 𝑁 ‘ ( 𝑠 ∪ { 𝑧 } ) ) )
	mreexfidimd.5	⊢ ( 𝜑 → 𝑆 ∈ 𝐼 )
	mreexfidimd.6	⊢ ( 𝜑 → 𝑇 ∈ 𝐼 )
	mreexfidimd.7	⊢ ( 𝜑 → 𝑆 ∈ Fin )
	mreexfidimd.8	⊢ ( 𝜑 → ( 𝑁 ‘ 𝑆 ) = ( 𝑁 ‘ 𝑇 ) )
Assertion	mreexfidimd	⊢ ( 𝜑 → 𝑆 ≈ 𝑇 )

Proof

Step	Hyp	Ref	Expression
1		mreexfidimd.1	⊢ ( 𝜑 → 𝐴 ∈ ( Moore ‘ 𝑋 ) )
2		mreexfidimd.2	⊢ 𝑁 = ( mrCls ‘ 𝐴 )
3		mreexfidimd.3	⊢ 𝐼 = ( mrInd ‘ 𝐴 )
4		mreexfidimd.4	⊢ ( 𝜑 → ∀ 𝑠 ∈ 𝒫 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ ( ( 𝑁 ‘ ( 𝑠 ∪ { 𝑦 } ) ) ∖ ( 𝑁 ‘ 𝑠 ) ) 𝑦 ∈ ( 𝑁 ‘ ( 𝑠 ∪ { 𝑧 } ) ) )
5		mreexfidimd.5	⊢ ( 𝜑 → 𝑆 ∈ 𝐼 )
6		mreexfidimd.6	⊢ ( 𝜑 → 𝑇 ∈ 𝐼 )
7		mreexfidimd.7	⊢ ( 𝜑 → 𝑆 ∈ Fin )
8		mreexfidimd.8	⊢ ( 𝜑 → ( 𝑁 ‘ 𝑆 ) = ( 𝑁 ‘ 𝑇 ) )
9	3 1 5	mrissd	⊢ ( 𝜑 → 𝑆 ⊆ 𝑋 )
10	1 2 9	mrcssidd	⊢ ( 𝜑 → 𝑆 ⊆ ( 𝑁 ‘ 𝑆 ) )
11	10 8	sseqtrd	⊢ ( 𝜑 → 𝑆 ⊆ ( 𝑁 ‘ 𝑇 ) )
12	3 1 6	mrissd	⊢ ( 𝜑 → 𝑇 ⊆ 𝑋 )
13	7	orcd	⊢ ( 𝜑 → ( 𝑆 ∈ Fin ∨ 𝑇 ∈ Fin ) )
14	1 2 3 4 11 12 13 5	mreexdomd	⊢ ( 𝜑 → 𝑆 ≼ 𝑇 )
15	1 2 12	mrcssidd	⊢ ( 𝜑 → 𝑇 ⊆ ( 𝑁 ‘ 𝑇 ) )
16	15 8	sseqtrrd	⊢ ( 𝜑 → 𝑇 ⊆ ( 𝑁 ‘ 𝑆 ) )
17	7	olcd	⊢ ( 𝜑 → ( 𝑇 ∈ Fin ∨ 𝑆 ∈ Fin ) )
18	1 2 3 4 16 9 17 6	mreexdomd	⊢ ( 𝜑 → 𝑇 ≼ 𝑆 )
19		sbth	⊢ ( ( 𝑆 ≼ 𝑇 ∧ 𝑇 ≼ 𝑆 ) → 𝑆 ≈ 𝑇 )
20	14 18 19	syl2anc	⊢ ( 𝜑 → 𝑆 ≈ 𝑇 )