mrissmrcd

Description: In a Moore system, if an independent set is between a set and its closure, the two sets are equal (since the two sets must have equal closures by mressmrcd , and so are equal by mrieqv2d .) (Contributed by David Moews, 1-May-2017)

	Ref	Expression
Hypotheses	mrissmrcd.1	⊢ ( 𝜑 → 𝐴 ∈ ( Moore ‘ 𝑋 ) )
	mrissmrcd.2	⊢ 𝑁 = ( mrCls ‘ 𝐴 )
	mrissmrcd.3	⊢ 𝐼 = ( mrInd ‘ 𝐴 )
	mrissmrcd.4	⊢ ( 𝜑 → 𝑆 ⊆ ( 𝑁 ‘ 𝑇 ) )
	mrissmrcd.5	⊢ ( 𝜑 → 𝑇 ⊆ 𝑆 )
	mrissmrcd.6	⊢ ( 𝜑 → 𝑆 ∈ 𝐼 )
Assertion	mrissmrcd	⊢ ( 𝜑 → 𝑆 = 𝑇 )

Proof

Step	Hyp	Ref	Expression
1		mrissmrcd.1	⊢ ( 𝜑 → 𝐴 ∈ ( Moore ‘ 𝑋 ) )
2		mrissmrcd.2	⊢ 𝑁 = ( mrCls ‘ 𝐴 )
3		mrissmrcd.3	⊢ 𝐼 = ( mrInd ‘ 𝐴 )
4		mrissmrcd.4	⊢ ( 𝜑 → 𝑆 ⊆ ( 𝑁 ‘ 𝑇 ) )
5		mrissmrcd.5	⊢ ( 𝜑 → 𝑇 ⊆ 𝑆 )
6		mrissmrcd.6	⊢ ( 𝜑 → 𝑆 ∈ 𝐼 )
7	1 2 4 5	mressmrcd	⊢ ( 𝜑 → ( 𝑁 ‘ 𝑆 ) = ( 𝑁 ‘ 𝑇 ) )
8		pssne	⊢ ( ( 𝑁 ‘ 𝑇 ) ⊊ ( 𝑁 ‘ 𝑆 ) → ( 𝑁 ‘ 𝑇 ) ≠ ( 𝑁 ‘ 𝑆 ) )
9	8	necomd	⊢ ( ( 𝑁 ‘ 𝑇 ) ⊊ ( 𝑁 ‘ 𝑆 ) → ( 𝑁 ‘ 𝑆 ) ≠ ( 𝑁 ‘ 𝑇 ) )
10	9	necon2bi	⊢ ( ( 𝑁 ‘ 𝑆 ) = ( 𝑁 ‘ 𝑇 ) → ¬ ( 𝑁 ‘ 𝑇 ) ⊊ ( 𝑁 ‘ 𝑆 ) )
11	7 10	syl	⊢ ( 𝜑 → ¬ ( 𝑁 ‘ 𝑇 ) ⊊ ( 𝑁 ‘ 𝑆 ) )
12	3 1 6	mrissd	⊢ ( 𝜑 → 𝑆 ⊆ 𝑋 )
13	1 2 3 12	mrieqv2d	⊢ ( 𝜑 → ( 𝑆 ∈ 𝐼 ↔ ∀ 𝑠 ( 𝑠 ⊊ 𝑆 → ( 𝑁 ‘ 𝑠 ) ⊊ ( 𝑁 ‘ 𝑆 ) ) ) )
14	6 13	mpbid	⊢ ( 𝜑 → ∀ 𝑠 ( 𝑠 ⊊ 𝑆 → ( 𝑁 ‘ 𝑠 ) ⊊ ( 𝑁 ‘ 𝑆 ) ) )
15	6 5	ssexd	⊢ ( 𝜑 → 𝑇 ∈ V )
16		simpr	⊢ ( ( 𝜑 ∧ 𝑠 = 𝑇 ) → 𝑠 = 𝑇 )
17	16	psseq1d	⊢ ( ( 𝜑 ∧ 𝑠 = 𝑇 ) → ( 𝑠 ⊊ 𝑆 ↔ 𝑇 ⊊ 𝑆 ) )
18	16	fveq2d	⊢ ( ( 𝜑 ∧ 𝑠 = 𝑇 ) → ( 𝑁 ‘ 𝑠 ) = ( 𝑁 ‘ 𝑇 ) )
19	18	psseq1d	⊢ ( ( 𝜑 ∧ 𝑠 = 𝑇 ) → ( ( 𝑁 ‘ 𝑠 ) ⊊ ( 𝑁 ‘ 𝑆 ) ↔ ( 𝑁 ‘ 𝑇 ) ⊊ ( 𝑁 ‘ 𝑆 ) ) )
20	17 19	imbi12d	⊢ ( ( 𝜑 ∧ 𝑠 = 𝑇 ) → ( ( 𝑠 ⊊ 𝑆 → ( 𝑁 ‘ 𝑠 ) ⊊ ( 𝑁 ‘ 𝑆 ) ) ↔ ( 𝑇 ⊊ 𝑆 → ( 𝑁 ‘ 𝑇 ) ⊊ ( 𝑁 ‘ 𝑆 ) ) ) )
21	15 20	spcdv	⊢ ( 𝜑 → ( ∀ 𝑠 ( 𝑠 ⊊ 𝑆 → ( 𝑁 ‘ 𝑠 ) ⊊ ( 𝑁 ‘ 𝑆 ) ) → ( 𝑇 ⊊ 𝑆 → ( 𝑁 ‘ 𝑇 ) ⊊ ( 𝑁 ‘ 𝑆 ) ) ) )
22	14 21	mpd	⊢ ( 𝜑 → ( 𝑇 ⊊ 𝑆 → ( 𝑁 ‘ 𝑇 ) ⊊ ( 𝑁 ‘ 𝑆 ) ) )
23	11 22	mtod	⊢ ( 𝜑 → ¬ 𝑇 ⊊ 𝑆 )
24		sspss	⊢ ( 𝑇 ⊆ 𝑆 ↔ ( 𝑇 ⊊ 𝑆 ∨ 𝑇 = 𝑆 ) )
25	5 24	sylib	⊢ ( 𝜑 → ( 𝑇 ⊊ 𝑆 ∨ 𝑇 = 𝑆 ) )
26	25	ord	⊢ ( 𝜑 → ( ¬ 𝑇 ⊊ 𝑆 → 𝑇 = 𝑆 ) )
27	23 26	mpd	⊢ ( 𝜑 → 𝑇 = 𝑆 )
28	27	eqcomd	⊢ ( 𝜑 → 𝑆 = 𝑇 )

Metamath Proof Explorer

Theorem mrissmrcd

Proof