Theorem mreexdomd

Description: In a Moore system whose closure operator has the exchange property, if S is independent and contained in the closure of T , and either S or T is finite, then T dominates S . This is an immediate consequence of mreexexd . (Contributed by David Moews, 1-May-2017)

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

Proof

Step	Hyp	Ref	Expression
1		mreexdomd.1	⊢ ( 𝜑 → 𝐴 ∈ ( Moore ‘ 𝑋 ) )
2		mreexdomd.2	⊢ 𝑁 = ( mrCls ‘ 𝐴 )
3		mreexdomd.3	⊢ 𝐼 = ( mrInd ‘ 𝐴 )
4		mreexdomd.4	⊢ ( 𝜑 → ∀ 𝑠 ∈ 𝒫 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ ( ( 𝑁 ‘ ( 𝑠 ∪ { 𝑦 } ) ) ∖ ( 𝑁 ‘ 𝑠 ) ) 𝑦 ∈ ( 𝑁 ‘ ( 𝑠 ∪ { 𝑧 } ) ) )
5		mreexdomd.5	⊢ ( 𝜑 → 𝑆 ⊆ ( 𝑁 ‘ 𝑇 ) )
6		mreexdomd.6	⊢ ( 𝜑 → 𝑇 ⊆ 𝑋 )
7		mreexdomd.7	⊢ ( 𝜑 → ( 𝑆 ∈ Fin ∨ 𝑇 ∈ Fin ) )
8		mreexdomd.8	⊢ ( 𝜑 → 𝑆 ∈ 𝐼 )
9	3 1 8	mrissd	⊢ ( 𝜑 → 𝑆 ⊆ 𝑋 )
10		dif0	⊢ ( 𝑋 ∖ ∅ ) = 𝑋
11	9 10	sseqtrrdi	⊢ ( 𝜑 → 𝑆 ⊆ ( 𝑋 ∖ ∅ ) )
12	6 10	sseqtrrdi	⊢ ( 𝜑 → 𝑇 ⊆ ( 𝑋 ∖ ∅ ) )
13		un0	⊢ ( 𝑇 ∪ ∅ ) = 𝑇
14	13	fveq2i	⊢ ( 𝑁 ‘ ( 𝑇 ∪ ∅ ) ) = ( 𝑁 ‘ 𝑇 )
15	5 14	sseqtrrdi	⊢ ( 𝜑 → 𝑆 ⊆ ( 𝑁 ‘ ( 𝑇 ∪ ∅ ) ) )
16		un0	⊢ ( 𝑆 ∪ ∅ ) = 𝑆
17	16 8	eqeltrid	⊢ ( 𝜑 → ( 𝑆 ∪ ∅ ) ∈ 𝐼 )
18	1 2 3 4 11 12 15 17 7	mreexexd	⊢ ( 𝜑 → ∃ 𝑖 ∈ 𝒫 𝑇 ( 𝑆 ≈ 𝑖 ∧ ( 𝑖 ∪ ∅ ) ∈ 𝐼 ) )
19		simprrl	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝒫 𝑇 ∧ ( 𝑆 ≈ 𝑖 ∧ ( 𝑖 ∪ ∅ ) ∈ 𝐼 ) ) ) → 𝑆 ≈ 𝑖 )
20		simprl	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝒫 𝑇 ∧ ( 𝑆 ≈ 𝑖 ∧ ( 𝑖 ∪ ∅ ) ∈ 𝐼 ) ) ) → 𝑖 ∈ 𝒫 𝑇 )
21	20	elpwid	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝒫 𝑇 ∧ ( 𝑆 ≈ 𝑖 ∧ ( 𝑖 ∪ ∅ ) ∈ 𝐼 ) ) ) → 𝑖 ⊆ 𝑇 )
22	1	elfvexd	⊢ ( 𝜑 → 𝑋 ∈ V )
23	22 6	ssexd	⊢ ( 𝜑 → 𝑇 ∈ V )
24		ssdomg	⊢ ( 𝑇 ∈ V → ( 𝑖 ⊆ 𝑇 → 𝑖 ≼ 𝑇 ) )
25	23 24	syl	⊢ ( 𝜑 → ( 𝑖 ⊆ 𝑇 → 𝑖 ≼ 𝑇 ) )
26	25	adantr	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝒫 𝑇 ∧ ( 𝑆 ≈ 𝑖 ∧ ( 𝑖 ∪ ∅ ) ∈ 𝐼 ) ) ) → ( 𝑖 ⊆ 𝑇 → 𝑖 ≼ 𝑇 ) )
27	21 26	mpd	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝒫 𝑇 ∧ ( 𝑆 ≈ 𝑖 ∧ ( 𝑖 ∪ ∅ ) ∈ 𝐼 ) ) ) → 𝑖 ≼ 𝑇 )
28		endomtr	⊢ ( ( 𝑆 ≈ 𝑖 ∧ 𝑖 ≼ 𝑇 ) → 𝑆 ≼ 𝑇 )
29	19 27 28	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝒫 𝑇 ∧ ( 𝑆 ≈ 𝑖 ∧ ( 𝑖 ∪ ∅ ) ∈ 𝐼 ) ) ) → 𝑆 ≼ 𝑇 )
30	18 29	rexlimddv	⊢ ( 𝜑 → 𝑆 ≼ 𝑇 )