mreexmrid

Description: In a Moore system whose closure operator has the exchange property, if a set is independent and an element is not in its closure, then adding the element to the set gives another independent set. Lemma 4.1.5 in FaureFrolicher p. 84. (Contributed by David Moews, 1-May-2017)

	Ref	Expression
Hypotheses	mreexmrid.1	$⊢ φ \to A \in Moore (X)$
	mreexmrid.2	$⊢ N = mrCls (A)$
	mreexmrid.3	$⊢ I = mrInd (A)$
	mreexmrid.4	$⊢ φ \to \forall s \in 𝒫 X \forall y \in X \forall z \in (N (s \cup \{y\}) ∖ N (s)) y \in N (s \cup \{z\})$
	mreexmrid.5	$⊢ φ \to S \in I$
	mreexmrid.6	$⊢ φ \to Y \in X$
	mreexmrid.7	$⊢ φ \to \neg Y \in N (S)$
Assertion	mreexmrid	$⊢ φ \to S \cup \{Y\} \in I$

Proof

Step	Hyp	Ref	Expression
1		mreexmrid.1	$⊢ φ \to A \in Moore (X)$
2		mreexmrid.2	$⊢ N = mrCls (A)$
3		mreexmrid.3	$⊢ I = mrInd (A)$
4		mreexmrid.4	$⊢ φ \to \forall s \in 𝒫 X \forall y \in X \forall z \in (N (s \cup \{y\}) ∖ N (s)) y \in N (s \cup \{z\})$
5		mreexmrid.5	$⊢ φ \to S \in I$
6		mreexmrid.6	$⊢ φ \to Y \in X$
7		mreexmrid.7	$⊢ φ \to \neg Y \in N (S)$
8	3 1 5	mrissd	$⊢ φ \to S \subseteq X$
9	6	snssd	$⊢ φ \to \{Y\} \subseteq X$
10	8 9	unssd	$⊢ φ \to S \cup \{Y\} \subseteq X$
11	1	3ad2ant1	$⊢ (φ \land x \in S \land x \in N ((S \cup \{Y\}) ∖ \{x\})) \to A \in Moore (X)$
12	11	elfvexd	$⊢ (φ \land x \in S \land x \in N ((S \cup \{Y\}) ∖ \{x\})) \to X \in V$
13	4	3ad2ant1	$⊢ (φ \land x \in S \land x \in N ((S \cup \{Y\}) ∖ \{x\})) \to \forall s \in 𝒫 X \forall y \in X \forall z \in (N (s \cup \{y\}) ∖ N (s)) y \in N (s \cup \{z\})$
14	5	3ad2ant1	$⊢ (φ \land x \in S \land x \in N ((S \cup \{Y\}) ∖ \{x\})) \to S \in I$
15	3 11 14	mrissd	$⊢ (φ \land x \in S \land x \in N ((S \cup \{Y\}) ∖ \{x\})) \to S \subseteq X$
16	15	ssdifssd	$⊢ (φ \land x \in S \land x \in N ((S \cup \{Y\}) ∖ \{x\})) \to S ∖ \{x\} \subseteq X$
17	6	3ad2ant1	$⊢ (φ \land x \in S \land x \in N ((S \cup \{Y\}) ∖ \{x\})) \to Y \in X$
18		simp3	$⊢ (φ \land x \in S \land x \in N ((S \cup \{Y\}) ∖ \{x\})) \to x \in N ((S \cup \{Y\}) ∖ \{x\})$
19		difundir	$⊢ (S \cup \{Y\}) ∖ \{x\} = (S ∖ \{x\}) \cup (\{Y\} ∖ \{x\})$
20		simp2	$⊢ (φ \land x \in S \land x \in N ((S \cup \{Y\}) ∖ \{x\})) \to x \in S$
21	1 2 8	mrcssidd	$⊢ φ \to S \subseteq N (S)$
22	21 7	ssneldd	$⊢ φ \to \neg Y \in S$
23	22	3ad2ant1	$⊢ (φ \land x \in S \land x \in N ((S \cup \{Y\}) ∖ \{x\})) \to \neg Y \in S$
24		nelneq	$⊢ (x \in S \land \neg Y \in S) \to \neg x = Y$
25	20 23 24	syl2anc	$⊢ (φ \land x \in S \land x \in N ((S \cup \{Y\}) ∖ \{x\})) \to \neg x = Y$
26		elsni	$⊢ x \in \{Y\} \to x = Y$
27	25 26	nsyl	$⊢ (φ \land x \in S \land x \in N ((S \cup \{Y\}) ∖ \{x\})) \to \neg x \in \{Y\}$
28		difsnb	$⊢ \neg x \in \{Y\} \leftrightarrow \{Y\} ∖ \{x\} = \{Y\}$
29	27 28	sylib	$⊢ (φ \land x \in S \land x \in N ((S \cup \{Y\}) ∖ \{x\})) \to \{Y\} ∖ \{x\} = \{Y\}$
30	29	uneq2d	$⊢ (φ \land x \in S \land x \in N ((S \cup \{Y\}) ∖ \{x\})) \to (S ∖ \{x\}) \cup (\{Y\} ∖ \{x\}) = (S ∖ \{x\}) \cup \{Y\}$
31	19 30	eqtrid	$⊢ (φ \land x \in S \land x \in N ((S \cup \{Y\}) ∖ \{x\})) \to (S \cup \{Y\}) ∖ \{x\} = (S ∖ \{x\}) \cup \{Y\}$
32	31	fveq2d	$⊢ (φ \land x \in S \land x \in N ((S \cup \{Y\}) ∖ \{x\})) \to N ((S \cup \{Y\}) ∖ \{x\}) = N ((S ∖ \{x\}) \cup \{Y\})$
33	18 32	eleqtrd	$⊢ (φ \land x \in S \land x \in N ((S \cup \{Y\}) ∖ \{x\})) \to x \in N ((S ∖ \{x\}) \cup \{Y\})$
34	2 3 11 14 20	ismri2dad	$⊢ (φ \land x \in S \land x \in N ((S \cup \{Y\}) ∖ \{x\})) \to \neg x \in N (S ∖ \{x\})$
35	12 13 16 17 33 34	mreexd	$⊢ (φ \land x \in S \land x \in N ((S \cup \{Y\}) ∖ \{x\})) \to Y \in N ((S ∖ \{x\}) \cup \{x\})$
36	7	3ad2ant1	$⊢ (φ \land x \in S \land x \in N ((S \cup \{Y\}) ∖ \{x\})) \to \neg Y \in N (S)$
37		undif1	$⊢ (S ∖ \{x\}) \cup \{x\} = S \cup \{x\}$
38	20	snssd	$⊢ (φ \land x \in S \land x \in N ((S \cup \{Y\}) ∖ \{x\})) \to \{x\} \subseteq S$
39		ssequn2	$⊢ \{x\} \subseteq S \leftrightarrow S \cup \{x\} = S$
40	38 39	sylib	$⊢ (φ \land x \in S \land x \in N ((S \cup \{Y\}) ∖ \{x\})) \to S \cup \{x\} = S$
41	37 40	eqtrid	$⊢ (φ \land x \in S \land x \in N ((S \cup \{Y\}) ∖ \{x\})) \to (S ∖ \{x\}) \cup \{x\} = S$
42	41	fveq2d	$⊢ (φ \land x \in S \land x \in N ((S \cup \{Y\}) ∖ \{x\})) \to N ((S ∖ \{x\}) \cup \{x\}) = N (S)$
43	36 42	neleqtrrd	$⊢ (φ \land x \in S \land x \in N ((S \cup \{Y\}) ∖ \{x\})) \to \neg Y \in N ((S ∖ \{x\}) \cup \{x\})$
44	35 43	pm2.65i	$⊢ \neg (φ \land x \in S \land x \in N ((S \cup \{Y\}) ∖ \{x\}))$
45		df-3an	$⊢ (φ \land x \in S \land x \in N ((S \cup \{Y\}) ∖ \{x\})) \leftrightarrow ((φ \land x \in S) \land x \in N ((S \cup \{Y\}) ∖ \{x\}))$
46	44 45	mtbi	$⊢ \neg ((φ \land x \in S) \land x \in N ((S \cup \{Y\}) ∖ \{x\}))$
47	46	imnani	$⊢ (φ \land x \in S) \to \neg x \in N ((S \cup \{Y\}) ∖ \{x\})$
48	47	adantlr	$⊢ ((φ \land x \in (S \cup \{Y\})) \land x \in S) \to \neg x \in N ((S \cup \{Y\}) ∖ \{x\})$
49	26	adantl	$⊢ ((φ \land x \in (S \cup \{Y\})) \land x \in \{Y\}) \to x = Y$
50	7	ad2antrr	$⊢ ((φ \land x \in (S \cup \{Y\})) \land x \in \{Y\}) \to \neg Y \in N (S)$
51	49 50	eqneltrd	$⊢ ((φ \land x \in (S \cup \{Y\})) \land x \in \{Y\}) \to \neg x \in N (S)$
52	49	sneqd	$⊢ ((φ \land x \in (S \cup \{Y\})) \land x \in \{Y\}) \to \{x\} = \{Y\}$
53	52	difeq2d	$⊢ ((φ \land x \in (S \cup \{Y\})) \land x \in \{Y\}) \to (S \cup \{Y\}) ∖ \{x\} = (S \cup \{Y\}) ∖ \{Y\}$
54		difun2	$⊢ (S \cup \{Y\}) ∖ \{Y\} = S ∖ \{Y\}$
55	53 54	eqtrdi	$⊢ ((φ \land x \in (S \cup \{Y\})) \land x \in \{Y\}) \to (S \cup \{Y\}) ∖ \{x\} = S ∖ \{Y\}$
56		difsnb	$⊢ \neg Y \in S \leftrightarrow S ∖ \{Y\} = S$
57	22 56	sylib	$⊢ φ \to S ∖ \{Y\} = S$
58	57	ad2antrr	$⊢ ((φ \land x \in (S \cup \{Y\})) \land x \in \{Y\}) \to S ∖ \{Y\} = S$
59	55 58	eqtrd	$⊢ ((φ \land x \in (S \cup \{Y\})) \land x \in \{Y\}) \to (S \cup \{Y\}) ∖ \{x\} = S$
60	59	fveq2d	$⊢ ((φ \land x \in (S \cup \{Y\})) \land x \in \{Y\}) \to N ((S \cup \{Y\}) ∖ \{x\}) = N (S)$
61	51 60	neleqtrrd	$⊢ ((φ \land x \in (S \cup \{Y\})) \land x \in \{Y\}) \to \neg x \in N ((S \cup \{Y\}) ∖ \{x\})$
62		elun	$⊢ x \in (S \cup \{Y\}) \leftrightarrow (x \in S \lor x \in \{Y\})$
63	62	bilani	$⊢ (φ \land x \in (S \cup \{Y\})) \to (x \in S \lor x \in \{Y\})$
64	48 61 63	mpjaodan	$⊢ (φ \land x \in (S \cup \{Y\})) \to \neg x \in N ((S \cup \{Y\}) ∖ \{x\})$
65	64	ralrimiva	$⊢ φ \to \forall x \in (S \cup \{Y\}) \neg x \in N ((S \cup \{Y\}) ∖ \{x\})$
66	2 3 1 10 65	ismri2dd	$⊢ φ \to S \cup \{Y\} \in I$

Metamath Proof Explorer

Theorem mreexmrid

Proof