mrieqv2d

Description: In a Moore system, a set is independent if and only if all its proper subsets have closure properly contained in the closure of the set. Part of Proposition 4.1.3 in FaureFrolicher p. 83. (Contributed by David Moews, 1-May-2017)

	Ref	Expression
Hypotheses	mrieqvd.1	$⊢ φ \to A \in Moore (X)$
	mrieqvd.2	$⊢ N = mrCls (A)$
	mrieqvd.3	$⊢ I = mrInd (A)$
	mrieqvd.4	$⊢ φ \to S \subseteq X$
Assertion	mrieqv2d	$⊢ φ \to (S \in I \leftrightarrow \forall s (s \subset S \to N (s) \subset N (S)))$

Proof

Step	Hyp	Ref	Expression
1		mrieqvd.1	$⊢ φ \to A \in Moore (X)$
2		mrieqvd.2	$⊢ N = mrCls (A)$
3		mrieqvd.3	$⊢ I = mrInd (A)$
4		mrieqvd.4	$⊢ φ \to S \subseteq X$
5		pssnel	$⊢ s \subset S \to \exists x (x \in S \land \neg x \in s)$
6	5	3ad2ant3	$⊢ (φ \land S \in I \land s \subset S) \to \exists x (x \in S \land \neg x \in s)$
7	1	3ad2ant1	$⊢ (φ \land S \in I \land s \subset S) \to A \in Moore (X)$
8	7	adantr	$⊢ ((φ \land S \in I \land s \subset S) \land (x \in S \land \neg x \in s)) \to A \in Moore (X)$
9		simprr	$⊢ ((φ \land S \in I \land s \subset S) \land (x \in S \land \neg x \in s)) \to \neg x \in s$
10		difsnb	$⊢ \neg x \in s \leftrightarrow s ∖ \{x\} = s$
11	9 10	sylib	$⊢ ((φ \land S \in I \land s \subset S) \land (x \in S \land \neg x \in s)) \to s ∖ \{x\} = s$
12		simpl3	$⊢ ((φ \land S \in I \land s \subset S) \land (x \in S \land \neg x \in s)) \to s \subset S$
13	12	pssssd	$⊢ ((φ \land S \in I \land s \subset S) \land (x \in S \land \neg x \in s)) \to s \subseteq S$
14	13	ssdifd	$⊢ ((φ \land S \in I \land s \subset S) \land (x \in S \land \neg x \in s)) \to s ∖ \{x\} \subseteq S ∖ \{x\}$
15	11 14	eqsstrrd	$⊢ ((φ \land S \in I \land s \subset S) \land (x \in S \land \neg x \in s)) \to s \subseteq S ∖ \{x\}$
16		simpl2	$⊢ ((φ \land S \in I \land s \subset S) \land (x \in S \land \neg x \in s)) \to S \in I$
17	3 8 16	mrissd	$⊢ ((φ \land S \in I \land s \subset S) \land (x \in S \land \neg x \in s)) \to S \subseteq X$
18	17	ssdifssd	$⊢ ((φ \land S \in I \land s \subset S) \land (x \in S \land \neg x \in s)) \to S ∖ \{x\} \subseteq X$
19	8 2 15 18	mrcssd	$⊢ ((φ \land S \in I \land s \subset S) \land (x \in S \land \neg x \in s)) \to N (s) \subseteq N (S ∖ \{x\})$
20		difssd	$⊢ ((φ \land S \in I \land s \subset S) \land (x \in S \land \neg x \in s)) \to S ∖ \{x\} \subseteq S$
21	8 2 20 17	mrcssd	$⊢ ((φ \land S \in I \land s \subset S) \land (x \in S \land \neg x \in s)) \to N (S ∖ \{x\}) \subseteq N (S)$
22	8 2 17	mrcssidd	$⊢ ((φ \land S \in I \land s \subset S) \land (x \in S \land \neg x \in s)) \to S \subseteq N (S)$
23		simprl	$⊢ ((φ \land S \in I \land s \subset S) \land (x \in S \land \neg x \in s)) \to x \in S$
24	22 23	sseldd	$⊢ ((φ \land S \in I \land s \subset S) \land (x \in S \land \neg x \in s)) \to x \in N (S)$
25	2 3 8 16 23	ismri2dad	$⊢ ((φ \land S \in I \land s \subset S) \land (x \in S \land \neg x \in s)) \to \neg x \in N (S ∖ \{x\})$
26	21 24 25	ssnelpssd	$⊢ ((φ \land S \in I \land s \subset S) \land (x \in S \land \neg x \in s)) \to N (S ∖ \{x\}) \subset N (S)$
27	19 26	sspsstrd	$⊢ ((φ \land S \in I \land s \subset S) \land (x \in S \land \neg x \in s)) \to N (s) \subset N (S)$
28	6 27	exlimddv	$⊢ (φ \land S \in I \land s \subset S) \to N (s) \subset N (S)$
29	28	3expia	$⊢ (φ \land S \in I) \to (s \subset S \to N (s) \subset N (S))$
30	29	alrimiv	$⊢ (φ \land S \in I) \to \forall s (s \subset S \to N (s) \subset N (S))$
31	30	ex	$⊢ φ \to (S \in I \to \forall s (s \subset S \to N (s) \subset N (S)))$
32	1	adantr	$⊢ (φ \land x \in S) \to A \in Moore (X)$
33	32	elfvexd	$⊢ (φ \land x \in S) \to X \in V$
34	4	adantr	$⊢ (φ \land x \in S) \to S \subseteq X$
35	33 34	ssexd	$⊢ (φ \land x \in S) \to S \in V$
36		difexg	$⊢ S \in V \to S ∖ \{x\} \in V$
37	35 36	syl	$⊢ (φ \land x \in S) \to S ∖ \{x\} \in V$
38		simp1r	$⊢ ((φ \land x \in S) \land s = S ∖ \{x\} \land (s \subset S \to N (s) \subset N (S))) \to x \in S$
39		difsnpss	$⊢ x \in S \leftrightarrow S ∖ \{x\} \subset S$
40	38 39	sylib	$⊢ ((φ \land x \in S) \land s = S ∖ \{x\} \land (s \subset S \to N (s) \subset N (S))) \to S ∖ \{x\} \subset S$
41		simp2	$⊢ ((φ \land x \in S) \land s = S ∖ \{x\} \land (s \subset S \to N (s) \subset N (S))) \to s = S ∖ \{x\}$
42	41	psseq1d	$⊢ ((φ \land x \in S) \land s = S ∖ \{x\} \land (s \subset S \to N (s) \subset N (S))) \to (s \subset S \leftrightarrow S ∖ \{x\} \subset S)$
43	40 42	mpbird	$⊢ ((φ \land x \in S) \land s = S ∖ \{x\} \land (s \subset S \to N (s) \subset N (S))) \to s \subset S$
44		simp3	$⊢ ((φ \land x \in S) \land s = S ∖ \{x\} \land (s \subset S \to N (s) \subset N (S))) \to (s \subset S \to N (s) \subset N (S))$
45	43 44	mpd	$⊢ ((φ \land x \in S) \land s = S ∖ \{x\} \land (s \subset S \to N (s) \subset N (S))) \to N (s) \subset N (S)$
46	41	fveq2d	$⊢ ((φ \land x \in S) \land s = S ∖ \{x\} \land (s \subset S \to N (s) \subset N (S))) \to N (s) = N (S ∖ \{x\})$
47	46	psseq1d	$⊢ ((φ \land x \in S) \land s = S ∖ \{x\} \land (s \subset S \to N (s) \subset N (S))) \to (N (s) \subset N (S) \leftrightarrow N (S ∖ \{x\}) \subset N (S))$
48	45 47	mpbid	$⊢ ((φ \land x \in S) \land s = S ∖ \{x\} \land (s \subset S \to N (s) \subset N (S))) \to N (S ∖ \{x\}) \subset N (S)$
49	48	3expia	$⊢ ((φ \land x \in S) \land s = S ∖ \{x\}) \to ((s \subset S \to N (s) \subset N (S)) \to N (S ∖ \{x\}) \subset N (S))$
50	37 49	spcimdv	$⊢ (φ \land x \in S) \to (\forall s (s \subset S \to N (s) \subset N (S)) \to N (S ∖ \{x\}) \subset N (S))$
51	50	3impia	$⊢ (φ \land x \in S \land \forall s (s \subset S \to N (s) \subset N (S))) \to N (S ∖ \{x\}) \subset N (S)$
52	51	pssned	$⊢ (φ \land x \in S \land \forall s (s \subset S \to N (s) \subset N (S))) \to N (S ∖ \{x\}) \neq N (S)$
53	52	3com23	$⊢ (φ \land \forall s (s \subset S \to N (s) \subset N (S)) \land x \in S) \to N (S ∖ \{x\}) \neq N (S)$
54	1	3ad2ant1	$⊢ (φ \land \forall s (s \subset S \to N (s) \subset N (S)) \land x \in S) \to A \in Moore (X)$
55	4	3ad2ant1	$⊢ (φ \land \forall s (s \subset S \to N (s) \subset N (S)) \land x \in S) \to S \subseteq X$
56		simp3	$⊢ (φ \land \forall s (s \subset S \to N (s) \subset N (S)) \land x \in S) \to x \in S$
57	54 2 55 56	mrieqvlemd	$⊢ (φ \land \forall s (s \subset S \to N (s) \subset N (S)) \land x \in S) \to (x \in N (S ∖ \{x\}) \leftrightarrow N (S ∖ \{x\}) = N (S))$
58	57	necon3bbid	$⊢ (φ \land \forall s (s \subset S \to N (s) \subset N (S)) \land x \in S) \to (\neg x \in N (S ∖ \{x\}) \leftrightarrow N (S ∖ \{x\}) \neq N (S))$
59	53 58	mpbird	$⊢ (φ \land \forall s (s \subset S \to N (s) \subset N (S)) \land x \in S) \to \neg x \in N (S ∖ \{x\})$
60	59	3expia	$⊢ (φ \land \forall s (s \subset S \to N (s) \subset N (S))) \to (x \in S \to \neg x \in N (S ∖ \{x\}))$
61	60	ralrimiv	$⊢ (φ \land \forall s (s \subset S \to N (s) \subset N (S))) \to \forall x \in S \neg x \in N (S ∖ \{x\})$
62	61	ex	$⊢ φ \to (\forall s (s \subset S \to N (s) \subset N (S)) \to \forall x \in S \neg x \in N (S ∖ \{x\}))$
63	2 3 1 4	ismri2d	$⊢ φ \to (S \in I \leftrightarrow \forall x \in S \neg x \in N (S ∖ \{x\}))$
64	62 63	sylibrd	$⊢ φ \to (\forall s (s \subset S \to N (s) \subset N (S)) \to S \in I)$
65	31 64	impbid	$⊢ φ \to (S \in I \leftrightarrow \forall s (s \subset S \to N (s) \subset N (S)))$

Metamath Proof Explorer

Theorem mrieqv2d

Proof