ssfin4

Description: Dedekind finite sets have Dedekind finite subsets. (Contributed by Stefan O'Rear, 30-Oct-2014) (Revised by Mario Carneiro, 6-May-2015) (Revised by Mario Carneiro, 16-May-2015)

		Ref	Expression
	Assertion	ssfin4	$⊢ (A \in {Fin}^{IV} \land B \subseteq A) \to B \in {Fin}^{IV}$

Proof

Step	Hyp	Ref	Expression
1		simpll	$⊢ ((A \in {Fin}^{IV} \land B \subseteq A) \land (x \subset B \land x \approx B)) \to A \in {Fin}^{IV}$
2		pssss	$⊢ x \subset B \to x \subseteq B$
3		simpr	$⊢ (A \in {Fin}^{IV} \land B \subseteq A) \to B \subseteq A$
4	2 3	sylan9ssr	$⊢ ((A \in {Fin}^{IV} \land B \subseteq A) \land x \subset B) \to x \subseteq A$
5		difssd	$⊢ ((A \in {Fin}^{IV} \land B \subseteq A) \land x \subset B) \to A ∖ B \subseteq A$
6	4 5	unssd	$⊢ ((A \in {Fin}^{IV} \land B \subseteq A) \land x \subset B) \to x \cup (A ∖ B) \subseteq A$
7		pssnel	$⊢ x \subset B \to \exists c (c \in B \land \neg c \in x)$
8	7	adantl	$⊢ ((A \in {Fin}^{IV} \land B \subseteq A) \land x \subset B) \to \exists c (c \in B \land \neg c \in x)$
9		simpllr	$⊢ (((A \in {Fin}^{IV} \land B \subseteq A) \land x \subset B) \land (c \in B \land \neg c \in x)) \to B \subseteq A$
10		simprl	$⊢ (((A \in {Fin}^{IV} \land B \subseteq A) \land x \subset B) \land (c \in B \land \neg c \in x)) \to c \in B$
11	9 10	sseldd	$⊢ (((A \in {Fin}^{IV} \land B \subseteq A) \land x \subset B) \land (c \in B \land \neg c \in x)) \to c \in A$
12		simprr	$⊢ (((A \in {Fin}^{IV} \land B \subseteq A) \land x \subset B) \land (c \in B \land \neg c \in x)) \to \neg c \in x$
13		elndif	$⊢ c \in B \to \neg c \in (A ∖ B)$
14	13	ad2antrl	$⊢ (((A \in {Fin}^{IV} \land B \subseteq A) \land x \subset B) \land (c \in B \land \neg c \in x)) \to \neg c \in (A ∖ B)$
15		ioran	$⊢ \neg (c \in x \lor c \in (A ∖ B)) \leftrightarrow (\neg c \in x \land \neg c \in (A ∖ B))$
16		elun	$⊢ c \in (x \cup (A ∖ B)) \leftrightarrow (c \in x \lor c \in (A ∖ B))$
17	15 16	xchnxbir	$⊢ \neg c \in (x \cup (A ∖ B)) \leftrightarrow (\neg c \in x \land \neg c \in (A ∖ B))$
18	12 14 17	sylanbrc	$⊢ (((A \in {Fin}^{IV} \land B \subseteq A) \land x \subset B) \land (c \in B \land \neg c \in x)) \to \neg c \in (x \cup (A ∖ B))$
19		nelneq2	$⊢ (c \in A \land \neg c \in (x \cup (A ∖ B))) \to \neg A = x \cup (A ∖ B)$
20	11 18 19	syl2anc	$⊢ (((A \in {Fin}^{IV} \land B \subseteq A) \land x \subset B) \land (c \in B \land \neg c \in x)) \to \neg A = x \cup (A ∖ B)$
21		eqcom	$⊢ A = x \cup (A ∖ B) \leftrightarrow x \cup (A ∖ B) = A$
22	20 21	sylnib	$⊢ (((A \in {Fin}^{IV} \land B \subseteq A) \land x \subset B) \land (c \in B \land \neg c \in x)) \to \neg x \cup (A ∖ B) = A$
23	8 22	exlimddv	$⊢ ((A \in {Fin}^{IV} \land B \subseteq A) \land x \subset B) \to \neg x \cup (A ∖ B) = A$
24		dfpss2	$⊢ x \cup (A ∖ B) \subset A \leftrightarrow (x \cup (A ∖ B) \subseteq A \land \neg x \cup (A ∖ B) = A)$
25	6 23 24	sylanbrc	$⊢ ((A \in {Fin}^{IV} \land B \subseteq A) \land x \subset B) \to x \cup (A ∖ B) \subset A$
26	25	adantrr	$⊢ ((A \in {Fin}^{IV} \land B \subseteq A) \land (x \subset B \land x \approx B)) \to x \cup (A ∖ B) \subset A$
27		simprr	$⊢ ((A \in {Fin}^{IV} \land B \subseteq A) \land (x \subset B \land x \approx B)) \to x \approx B$
28		difexg	$⊢ A \in {Fin}^{IV} \to A ∖ B \in V$
29		enrefg	$⊢ A ∖ B \in V \to (A ∖ B) \approx (A ∖ B)$
30	1 28 29	3syl	$⊢ ((A \in {Fin}^{IV} \land B \subseteq A) \land (x \subset B \land x \approx B)) \to (A ∖ B) \approx (A ∖ B)$
31	2	ad2antrl	$⊢ ((A \in {Fin}^{IV} \land B \subseteq A) \land (x \subset B \land x \approx B)) \to x \subseteq B$
32		ssinss1	$⊢ x \subseteq B \to x \cap A \subseteq B$
33	31 32	syl	$⊢ ((A \in {Fin}^{IV} \land B \subseteq A) \land (x \subset B \land x \approx B)) \to x \cap A \subseteq B$
34		inssdif0	$⊢ x \cap A \subseteq B \leftrightarrow x \cap (A ∖ B) = \emptyset$
35	33 34	sylib	$⊢ ((A \in {Fin}^{IV} \land B \subseteq A) \land (x \subset B \land x \approx B)) \to x \cap (A ∖ B) = \emptyset$
36		disjdif	$⊢ B \cap (A ∖ B) = \emptyset$
37	35 36	jctir	$⊢ ((A \in {Fin}^{IV} \land B \subseteq A) \land (x \subset B \land x \approx B)) \to (x \cap (A ∖ B) = \emptyset \land B \cap (A ∖ B) = \emptyset)$
38		unen	$⊢ ((x \approx B \land (A ∖ B) \approx (A ∖ B)) \land (x \cap (A ∖ B) = \emptyset \land B \cap (A ∖ B) = \emptyset)) \to (x \cup (A ∖ B)) \approx (B \cup (A ∖ B))$
39	27 30 37 38	syl21anc	$⊢ ((A \in {Fin}^{IV} \land B \subseteq A) \land (x \subset B \land x \approx B)) \to (x \cup (A ∖ B)) \approx (B \cup (A ∖ B))$
40		simplr	$⊢ ((A \in {Fin}^{IV} \land B \subseteq A) \land (x \subset B \land x \approx B)) \to B \subseteq A$
41		undif	$⊢ B \subseteq A \leftrightarrow B \cup (A ∖ B) = A$
42	40 41	sylib	$⊢ ((A \in {Fin}^{IV} \land B \subseteq A) \land (x \subset B \land x \approx B)) \to B \cup (A ∖ B) = A$
43	39 42	breqtrd	$⊢ ((A \in {Fin}^{IV} \land B \subseteq A) \land (x \subset B \land x \approx B)) \to (x \cup (A ∖ B)) \approx A$
44		fin4i	$⊢ (x \cup (A ∖ B) \subset A \land (x \cup (A ∖ B)) \approx A) \to \neg A \in {Fin}^{IV}$
45	26 43 44	syl2anc	$⊢ ((A \in {Fin}^{IV} \land B \subseteq A) \land (x \subset B \land x \approx B)) \to \neg A \in {Fin}^{IV}$
46	1 45	pm2.65da	$⊢ (A \in {Fin}^{IV} \land B \subseteq A) \to \neg (x \subset B \land x \approx B)$
47	46	nexdv	$⊢ (A \in {Fin}^{IV} \land B \subseteq A) \to \neg \exists x (x \subset B \land x \approx B)$
48		ssexg	$⊢ (B \subseteq A \land A \in {Fin}^{IV}) \to B \in V$
49	48	ancoms	$⊢ (A \in {Fin}^{IV} \land B \subseteq A) \to B \in V$
50		isfin4	$⊢ B \in V \to (B \in {Fin}^{IV} \leftrightarrow \neg \exists x (x \subset B \land x \approx B))$
51	49 50	syl	$⊢ (A \in {Fin}^{IV} \land B \subseteq A) \to (B \in {Fin}^{IV} \leftrightarrow \neg \exists x (x \subset B \land x \approx B))$
52	47 51	mpbird	$⊢ (A \in {Fin}^{IV} \land B \subseteq A) \to B \in {Fin}^{IV}$

Metamath Proof Explorer

Theorem ssfin4

Proof