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	35	difexd	$⊢ (φ \land x \in S) \to S ∖ \{x\} \in V$
37		simp1r	$⊢ ((φ \land x \in S) \land s = S ∖ \{x\} \land (s \subset S \to N (s) \subset N (S))) \to x \in S$
38		difsnpss	$⊢ x \in S \leftrightarrow S ∖ \{x\} \subset S$
39	37 38	sylib	$⊢ ((φ \land x \in S) \land s = S ∖ \{x\} \land (s \subset S \to N (s) \subset N (S))) \to S ∖ \{x\} \subset S$
40		simp2	$⊢ ((φ \land x \in S) \land s = S ∖ \{x\} \land (s \subset S \to N (s) \subset N (S))) \to s = S ∖ \{x\}$
41	40	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)$
42	39 41	mpbird	$⊢ ((φ \land x \in S) \land s = S ∖ \{x\} \land (s \subset S \to N (s) \subset N (S))) \to s \subset S$
43		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))$
44	42 43	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)$
45	40	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\})$
46	45	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))$
47	44 46	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)$
48	47	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))$
49	36 48	spcimdv	$⊢ (φ \land x \in S) \to (\forall s (s \subset S \to N (s) \subset N (S)) \to N (S ∖ \{x\}) \subset N (S))$
50	49	3impia	$⊢ (φ \land x \in S \land \forall s (s \subset S \to N (s) \subset N (S))) \to N (S ∖ \{x\}) \subset N (S)$
51	50	pssned	$⊢ (φ \land x \in S \land \forall s (s \subset S \to N (s) \subset N (S))) \to N (S ∖ \{x\}) \neq N (S)$
52	51	3com23	$⊢ (φ \land \forall s (s \subset S \to N (s) \subset N (S)) \land x \in S) \to N (S ∖ \{x\}) \neq N (S)$
53	1	3ad2ant1	$⊢ (φ \land \forall s (s \subset S \to N (s) \subset N (S)) \land x \in S) \to A \in Moore (X)$
54	4	3ad2ant1	$⊢ (φ \land \forall s (s \subset S \to N (s) \subset N (S)) \land x \in S) \to S \subseteq X$
55		simp3	$⊢ (φ \land \forall s (s \subset S \to N (s) \subset N (S)) \land x \in S) \to x \in S$
56	53 2 54 55	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))$
57	56	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))$
58	52 57	mpbird	$⊢ (φ \land \forall s (s \subset S \to N (s) \subset N (S)) \land x \in S) \to \neg x \in N (S ∖ \{x\})$
59	58	3expia	$⊢ (φ \land \forall s (s \subset S \to N (s) \subset N (S))) \to (x \in S \to \neg x \in N (S ∖ \{x\}))$
60	59	ralrimiv	$⊢ (φ \land \forall s (s \subset S \to N (s) \subset N (S))) \to \forall x \in S \neg x \in N (S ∖ \{x\})$
61	60	ex	$⊢ φ \to (\forall s (s \subset S \to N (s) \subset N (S)) \to \forall x \in S \neg x \in N (S ∖ \{x\}))$
62	2 3 1 4	ismri2d	$⊢ φ \to (S \in I \leftrightarrow \forall x \in S \neg x \in N (S ∖ \{x\}))$
63	61 62	sylibrd	$⊢ φ \to (\forall s (s \subset S \to N (s) \subset N (S)) \to S \in I)$
64	31 63	impbid	$⊢ φ \to (S \in I \leftrightarrow \forall s (s \subset S \to N (s) \subset N (S)))$

Metamath Proof Explorer

Theorem mrieqv2d

Proof