acsfiindd

Description: In an algebraic closure system, a set is independent if and only if all its finite subsets are independent. Part of Proposition 4.1.3 in FaureFrolicher p. 83. (Contributed by David Moews, 1-May-2017)

	Ref	Expression
Hypotheses	acsfiindd.1	$⊢ φ \to A \in ACS (X)$
	acsfiindd.2	$⊢ N = mrCls (A)$
	acsfiindd.3	$⊢ I = mrInd (A)$
	acsfiindd.4	$⊢ φ \to S \subseteq X$
Assertion	acsfiindd	$⊢ φ \to (S \in I \leftrightarrow 𝒫 S \cap Fin \subseteq I)$

Proof

Step	Hyp	Ref	Expression
1		acsfiindd.1	$⊢ φ \to A \in ACS (X)$
2		acsfiindd.2	$⊢ N = mrCls (A)$
3		acsfiindd.3	$⊢ I = mrInd (A)$
4		acsfiindd.4	$⊢ φ \to S \subseteq X$
5	1	acsmred	$⊢ φ \to A \in Moore (X)$
6	5	ad2antrr	$⊢ ((φ \land S \in I) \land s \in (𝒫 S \cap Fin)) \to A \in Moore (X)$
7		simplr	$⊢ ((φ \land S \in I) \land s \in (𝒫 S \cap Fin)) \to S \in I$
8		simpr	$⊢ ((φ \land S \in I) \land s \in (𝒫 S \cap Fin)) \to s \in (𝒫 S \cap Fin)$
9	8	elin1d	$⊢ ((φ \land S \in I) \land s \in (𝒫 S \cap Fin)) \to s \in 𝒫 S$
10	9	elpwid	$⊢ ((φ \land S \in I) \land s \in (𝒫 S \cap Fin)) \to s \subseteq S$
11	6 2 3 7 10	mrissmrid	$⊢ ((φ \land S \in I) \land s \in (𝒫 S \cap Fin)) \to s \in I$
12	11	ralrimiva	$⊢ (φ \land S \in I) \to \forall s \in (𝒫 S \cap Fin) s \in I$
13		dfss3	$⊢ 𝒫 S \cap Fin \subseteq I \leftrightarrow \forall s \in (𝒫 S \cap Fin) s \in I$
14	12 13	sylibr	$⊢ (φ \land S \in I) \to 𝒫 S \cap Fin \subseteq I$
15	5	adantr	$⊢ (φ \land 𝒫 S \cap Fin \subseteq I) \to A \in Moore (X)$
16	4	adantr	$⊢ (φ \land 𝒫 S \cap Fin \subseteq I) \to S \subseteq X$
17		simpr	$⊢ ((φ \land x \in S) \land t \in (𝒫 (S ∖ \{x\}) \cap Fin)) \to t \in (𝒫 (S ∖ \{x\}) \cap Fin)$
18		elfpw	$⊢ t \in (𝒫 (S ∖ \{x\}) \cap Fin) \leftrightarrow (t \subseteq S ∖ \{x\} \land t \in Fin)$
19	17 18	sylib	$⊢ ((φ \land x \in S) \land t \in (𝒫 (S ∖ \{x\}) \cap Fin)) \to (t \subseteq S ∖ \{x\} \land t \in Fin)$
20	19	simpld	$⊢ ((φ \land x \in S) \land t \in (𝒫 (S ∖ \{x\}) \cap Fin)) \to t \subseteq S ∖ \{x\}$
21	20	difss2d	$⊢ ((φ \land x \in S) \land t \in (𝒫 (S ∖ \{x\}) \cap Fin)) \to t \subseteq S$
22		simplr	$⊢ ((φ \land x \in S) \land t \in (𝒫 (S ∖ \{x\}) \cap Fin)) \to x \in S$
23	22	snssd	$⊢ ((φ \land x \in S) \land t \in (𝒫 (S ∖ \{x\}) \cap Fin)) \to \{x\} \subseteq S$
24	21 23	unssd	$⊢ ((φ \land x \in S) \land t \in (𝒫 (S ∖ \{x\}) \cap Fin)) \to t \cup \{x\} \subseteq S$
25	19	simprd	$⊢ ((φ \land x \in S) \land t \in (𝒫 (S ∖ \{x\}) \cap Fin)) \to t \in Fin$
26		snfi	$⊢ \{x\} \in Fin$
27		unfi	$⊢ (t \in Fin \land \{x\} \in Fin) \to t \cup \{x\} \in Fin$
28	25 26 27	sylancl	$⊢ ((φ \land x \in S) \land t \in (𝒫 (S ∖ \{x\}) \cap Fin)) \to t \cup \{x\} \in Fin$
29		elfpw	$⊢ t \cup \{x\} \in (𝒫 S \cap Fin) \leftrightarrow (t \cup \{x\} \subseteq S \land t \cup \{x\} \in Fin)$
30	24 28 29	sylanbrc	$⊢ ((φ \land x \in S) \land t \in (𝒫 (S ∖ \{x\}) \cap Fin)) \to t \cup \{x\} \in (𝒫 S \cap Fin)$
31	5	ad4antr	$⊢ ((((φ \land x \in S) \land t \in (𝒫 (S ∖ \{x\}) \cap Fin)) \land s = t \cup \{x\}) \land s \in I) \to A \in Moore (X)$
32		simpr	$⊢ ((((φ \land x \in S) \land t \in (𝒫 (S ∖ \{x\}) \cap Fin)) \land s = t \cup \{x\}) \land s \in I) \to s \in I$
33		simpllr	$⊢ (((φ \land x \in S) \land t \in (𝒫 (S ∖ \{x\}) \cap Fin)) \land s = t \cup \{x\}) \to x \in S$
34		snidg	$⊢ x \in S \to x \in \{x\}$
35		elun2	$⊢ x \in \{x\} \to x \in (t \cup \{x\})$
36	33 34 35	3syl	$⊢ (((φ \land x \in S) \land t \in (𝒫 (S ∖ \{x\}) \cap Fin)) \land s = t \cup \{x\}) \to x \in (t \cup \{x\})$
37		simpr	$⊢ (((φ \land x \in S) \land t \in (𝒫 (S ∖ \{x\}) \cap Fin)) \land s = t \cup \{x\}) \to s = t \cup \{x\}$
38	36 37	eleqtrrd	$⊢ (((φ \land x \in S) \land t \in (𝒫 (S ∖ \{x\}) \cap Fin)) \land s = t \cup \{x\}) \to x \in s$
39	38	adantr	$⊢ ((((φ \land x \in S) \land t \in (𝒫 (S ∖ \{x\}) \cap Fin)) \land s = t \cup \{x\}) \land s \in I) \to x \in s$
40	2 3 31 32 39	ismri2dad	$⊢ ((((φ \land x \in S) \land t \in (𝒫 (S ∖ \{x\}) \cap Fin)) \land s = t \cup \{x\}) \land s \in I) \to \neg x \in N (s ∖ \{x\})$
41	5	ad3antrrr	$⊢ (((φ \land x \in S) \land t \in (𝒫 (S ∖ \{x\}) \cap Fin)) \land s = t \cup \{x\}) \to A \in Moore (X)$
42	20	adantr	$⊢ (((φ \land x \in S) \land t \in (𝒫 (S ∖ \{x\}) \cap Fin)) \land s = t \cup \{x\}) \to t \subseteq S ∖ \{x\}$
43		neldifsnd	$⊢ (((φ \land x \in S) \land t \in (𝒫 (S ∖ \{x\}) \cap Fin)) \land s = t \cup \{x\}) \to \neg x \in (S ∖ \{x\})$
44	42 43	ssneldd	$⊢ (((φ \land x \in S) \land t \in (𝒫 (S ∖ \{x\}) \cap Fin)) \land s = t \cup \{x\}) \to \neg x \in t$
45		difsnb	$⊢ \neg x \in t \leftrightarrow t ∖ \{x\} = t$
46	44 45	sylib	$⊢ (((φ \land x \in S) \land t \in (𝒫 (S ∖ \{x\}) \cap Fin)) \land s = t \cup \{x\}) \to t ∖ \{x\} = t$
47		ssun1	$⊢ t \subseteq t \cup \{x\}$
48	47 37	sseqtrrid	$⊢ (((φ \land x \in S) \land t \in (𝒫 (S ∖ \{x\}) \cap Fin)) \land s = t \cup \{x\}) \to t \subseteq s$
49	48	ssdifd	$⊢ (((φ \land x \in S) \land t \in (𝒫 (S ∖ \{x\}) \cap Fin)) \land s = t \cup \{x\}) \to t ∖ \{x\} \subseteq s ∖ \{x\}$
50	46 49	eqsstrrd	$⊢ (((φ \land x \in S) \land t \in (𝒫 (S ∖ \{x\}) \cap Fin)) \land s = t \cup \{x\}) \to t \subseteq s ∖ \{x\}$
51	24	adantr	$⊢ (((φ \land x \in S) \land t \in (𝒫 (S ∖ \{x\}) \cap Fin)) \land s = t \cup \{x\}) \to t \cup \{x\} \subseteq S$
52	4	ad3antrrr	$⊢ (((φ \land x \in S) \land t \in (𝒫 (S ∖ \{x\}) \cap Fin)) \land s = t \cup \{x\}) \to S \subseteq X$
53	51 52	sstrd	$⊢ (((φ \land x \in S) \land t \in (𝒫 (S ∖ \{x\}) \cap Fin)) \land s = t \cup \{x\}) \to t \cup \{x\} \subseteq X$
54	37 53	eqsstrd	$⊢ (((φ \land x \in S) \land t \in (𝒫 (S ∖ \{x\}) \cap Fin)) \land s = t \cup \{x\}) \to s \subseteq X$
55	54	ssdifssd	$⊢ (((φ \land x \in S) \land t \in (𝒫 (S ∖ \{x\}) \cap Fin)) \land s = t \cup \{x\}) \to s ∖ \{x\} \subseteq X$
56	41 2 50 55	mrcssd	$⊢ (((φ \land x \in S) \land t \in (𝒫 (S ∖ \{x\}) \cap Fin)) \land s = t \cup \{x\}) \to N (t) \subseteq N (s ∖ \{x\})$
57	56	sseld	$⊢ (((φ \land x \in S) \land t \in (𝒫 (S ∖ \{x\}) \cap Fin)) \land s = t \cup \{x\}) \to (x \in N (t) \to x \in N (s ∖ \{x\}))$
58	57	adantr	$⊢ ((((φ \land x \in S) \land t \in (𝒫 (S ∖ \{x\}) \cap Fin)) \land s = t \cup \{x\}) \land s \in I) \to (x \in N (t) \to x \in N (s ∖ \{x\}))$
59	40 58	mtod	$⊢ ((((φ \land x \in S) \land t \in (𝒫 (S ∖ \{x\}) \cap Fin)) \land s = t \cup \{x\}) \land s \in I) \to \neg x \in N (t)$
60	59	ex	$⊢ (((φ \land x \in S) \land t \in (𝒫 (S ∖ \{x\}) \cap Fin)) \land s = t \cup \{x\}) \to (s \in I \to \neg x \in N (t))$
61	30 60	rspcimdv	$⊢ ((φ \land x \in S) \land t \in (𝒫 (S ∖ \{x\}) \cap Fin)) \to (\forall s \in (𝒫 S \cap Fin) s \in I \to \neg x \in N (t))$
62	13 61	syl5bi	$⊢ ((φ \land x \in S) \land t \in (𝒫 (S ∖ \{x\}) \cap Fin)) \to (𝒫 S \cap Fin \subseteq I \to \neg x \in N (t))$
63	62	impancom	$⊢ ((φ \land x \in S) \land 𝒫 S \cap Fin \subseteq I) \to (t \in (𝒫 (S ∖ \{x\}) \cap Fin) \to \neg x \in N (t))$
64	63	ralrimiv	$⊢ ((φ \land x \in S) \land 𝒫 S \cap Fin \subseteq I) \to \forall t \in (𝒫 (S ∖ \{x\}) \cap Fin) \neg x \in N (t)$
65	4	ssdifssd	$⊢ φ \to S ∖ \{x\} \subseteq X$
66	1 2 65	acsficl2d	$⊢ φ \to (x \in N (S ∖ \{x\}) \leftrightarrow \exists t \in (𝒫 (S ∖ \{x\}) \cap Fin) x \in N (t))$
67	66	notbid	$⊢ φ \to (\neg x \in N (S ∖ \{x\}) \leftrightarrow \neg \exists t \in (𝒫 (S ∖ \{x\}) \cap Fin) x \in N (t))$
68		ralnex	$⊢ \forall t \in (𝒫 (S ∖ \{x\}) \cap Fin) \neg x \in N (t) \leftrightarrow \neg \exists t \in (𝒫 (S ∖ \{x\}) \cap Fin) x \in N (t)$
69	67 68	bitr4di	$⊢ φ \to (\neg x \in N (S ∖ \{x\}) \leftrightarrow \forall t \in (𝒫 (S ∖ \{x\}) \cap Fin) \neg x \in N (t))$
70	69	ad2antrr	$⊢ ((φ \land x \in S) \land 𝒫 S \cap Fin \subseteq I) \to (\neg x \in N (S ∖ \{x\}) \leftrightarrow \forall t \in (𝒫 (S ∖ \{x\}) \cap Fin) \neg x \in N (t))$
71	64 70	mpbird	$⊢ ((φ \land x \in S) \land 𝒫 S \cap Fin \subseteq I) \to \neg x \in N (S ∖ \{x\})$
72	71	an32s	$⊢ ((φ \land 𝒫 S \cap Fin \subseteq I) \land x \in S) \to \neg x \in N (S ∖ \{x\})$
73	72	ralrimiva	$⊢ (φ \land 𝒫 S \cap Fin \subseteq I) \to \forall x \in S \neg x \in N (S ∖ \{x\})$
74	2 3 15 16 73	ismri2dd	$⊢ (φ \land 𝒫 S \cap Fin \subseteq I) \to S \in I$
75	14 74	impbida	$⊢ φ \to (S \in I \leftrightarrow 𝒫 S \cap Fin \subseteq I)$

Metamath Proof Explorer

Theorem acsfiindd

Proof