finminlem

Description: A useful lemma about finite sets. If a property holds for a finite set, it holds for a minimal set. (Contributed by Jeff Hankins, 4-Dec-2009)

		Ref	Expression
	Hypothesis	finminlem.1	$⊢ x = y \to (φ \leftrightarrow ψ)$
	Assertion	finminlem	$⊢ \exists x \in Fin φ \to \exists x (φ \land \forall y ((y \subseteq x \land ψ) \to x = y))$

Proof

Step	Hyp	Ref	Expression
1		finminlem.1	$⊢ x = y \to (φ \leftrightarrow ψ)$
2		nfe1	$⊢ Ⅎ x \exists x (x \approx n \land φ)$
3		nfcv	$⊢ \underline{Ⅎ} x ω$
4	2 3	nfrabw	$⊢ \underline{Ⅎ} x \{n \in ω \| \exists x (x \approx n \land φ)\}$
5		nfcv	$⊢ \underline{Ⅎ} x \emptyset$
6	4 5	nfne	$⊢ Ⅎ x \{n \in ω \| \exists x (x \approx n \land φ)\} \neq \emptyset$
7		isfi	$⊢ x \in Fin \leftrightarrow \exists m \in ω x \approx m$
8		19.8a	$⊢ (x \approx m \land φ) \to \exists x (x \approx m \land φ)$
9	8	anim2i	$⊢ (m \in ω \land (x \approx m \land φ)) \to (m \in ω \land \exists x (x \approx m \land φ))$
10	9	3impb	$⊢ (m \in ω \land x \approx m \land φ) \to (m \in ω \land \exists x (x \approx m \land φ))$
11		breq2	$⊢ n = m \to (x \approx n \leftrightarrow x \approx m)$
12	11	anbi1d	$⊢ n = m \to ((x \approx n \land φ) \leftrightarrow (x \approx m \land φ))$
13	12	exbidv	$⊢ n = m \to (\exists x (x \approx n \land φ) \leftrightarrow \exists x (x \approx m \land φ))$
14	13	elrab	$⊢ m \in \{n \in ω \| \exists x (x \approx n \land φ)\} \leftrightarrow (m \in ω \land \exists x (x \approx m \land φ))$
15	10 14	sylibr	$⊢ (m \in ω \land x \approx m \land φ) \to m \in \{n \in ω \| \exists x (x \approx n \land φ)\}$
16	15	ne0d	$⊢ (m \in ω \land x \approx m \land φ) \to \{n \in ω \| \exists x (x \approx n \land φ)\} \neq \emptyset$
17	16	3exp	$⊢ m \in ω \to (x \approx m \to (φ \to \{n \in ω \| \exists x (x \approx n \land φ)\} \neq \emptyset))$
18	17	rexlimiv	$⊢ \exists m \in ω x \approx m \to (φ \to \{n \in ω \| \exists x (x \approx n \land φ)\} \neq \emptyset)$
19	7 18	sylbi	$⊢ x \in Fin \to (φ \to \{n \in ω \| \exists x (x \approx n \land φ)\} \neq \emptyset)$
20	6 19	rexlimi	$⊢ \exists x \in Fin φ \to \{n \in ω \| \exists x (x \approx n \land φ)\} \neq \emptyset$
21		epweon	$⊢ E We On$
22		ssrab2	$⊢ \{n \in ω \| \exists x (x \approx n \land φ)\} \subseteq ω$
23		omsson	$⊢ ω \subseteq On$
24	22 23	sstri	$⊢ \{n \in ω \| \exists x (x \approx n \land φ)\} \subseteq On$
25		wefrc	$⊢ (E We On \land \{n \in ω \| \exists x (x \approx n \land φ)\} \subseteq On \land \{n \in ω \| \exists x (x \approx n \land φ)\} \neq \emptyset) \to \exists m \in \{n \in ω \| \exists x (x \approx n \land φ)\} \{n \in ω \| \exists x (x \approx n \land φ)\} \cap m = \emptyset$
26	21 24 25	mp3an12	$⊢ \{n \in ω \| \exists x (x \approx n \land φ)\} \neq \emptyset \to \exists m \in \{n \in ω \| \exists x (x \approx n \land φ)\} \{n \in ω \| \exists x (x \approx n \land φ)\} \cap m = \emptyset$
27		nfv	$⊢ Ⅎ x m \in ω$
28		nfcv	$⊢ \underline{Ⅎ} x m$
29	4 28	nfin	$⊢ \underline{Ⅎ} x (\{n \in ω \| \exists x (x \approx n \land φ)\} \cap m)$
30	29	nfeq1	$⊢ Ⅎ x \{n \in ω \| \exists x (x \approx n \land φ)\} \cap m = \emptyset$
31	27 30	nfan	$⊢ Ⅎ x (m \in ω \land \{n \in ω \| \exists x (x \approx n \land φ)\} \cap m = \emptyset)$
32		simprr	$⊢ ((m \in ω \land \{n \in ω \| \exists x (x \approx n \land φ)\} \cap m = \emptyset) \land (x \approx m \land φ)) \to φ$
33		sspss	$⊢ y \subseteq x \leftrightarrow (y \subset x \lor y = x)$
34		rspe	$⊢ (m \in ω \land x \approx m) \to \exists m \in ω x \approx m$
35		pssss	$⊢ y \subset x \to y \subseteq x$
36		ssfi	$⊢ (x \in Fin \land y \subseteq x) \to y \in Fin$
37	35 36	sylan2	$⊢ (x \in Fin \land y \subset x) \to y \in Fin$
38	37	ex	$⊢ x \in Fin \to (y \subset x \to y \in Fin)$
39	7 38	sylbir	$⊢ \exists m \in ω x \approx m \to (y \subset x \to y \in Fin)$
40	34 39	syl	$⊢ (m \in ω \land x \approx m) \to (y \subset x \to y \in Fin)$
41	40	adantrr	$⊢ (m \in ω \land (x \approx m \land φ)) \to (y \subset x \to y \in Fin)$
42	41	adantrr	$⊢ (m \in ω \land ((x \approx m \land φ) \land ψ)) \to (y \subset x \to y \in Fin)$
43		isfi	$⊢ y \in Fin \leftrightarrow \exists k \in ω y \approx k$
44		simprll	$⊢ ((m \in ω \land ((x \approx m \land φ) \land ψ)) \land ((k \in ω \land y \approx k) \land y \subset x)) \to k \in ω$
45		simprlr	$⊢ ((m \in ω \land ((x \approx m \land φ) \land ψ)) \land ((k \in ω \land y \approx k) \land y \subset x)) \to y \approx k$
46		simplrr	$⊢ ((m \in ω \land ((x \approx m \land φ) \land ψ)) \land ((k \in ω \land y \approx k) \land y \subset x)) \to ψ$
47		vex	$⊢ y \in V$
48		breq1	$⊢ x = y \to (x \approx k \leftrightarrow y \approx k)$
49	48 1	anbi12d	$⊢ x = y \to ((x \approx k \land φ) \leftrightarrow (y \approx k \land ψ))$
50	47 49	spcev	$⊢ (y \approx k \land ψ) \to \exists x (x \approx k \land φ)$
51	45 46 50	syl2anc	$⊢ ((m \in ω \land ((x \approx m \land φ) \land ψ)) \land ((k \in ω \land y \approx k) \land y \subset x)) \to \exists x (x \approx k \land φ)$
52	34 7	sylibr	$⊢ (m \in ω \land x \approx m) \to x \in Fin$
53	52	adantrr	$⊢ (m \in ω \land (x \approx m \land φ)) \to x \in Fin$
54	53	adantrr	$⊢ (m \in ω \land ((x \approx m \land φ) \land ψ)) \to x \in Fin$
55	54	adantr	$⊢ ((m \in ω \land ((x \approx m \land φ) \land ψ)) \land (k \in ω \land y \approx k)) \to x \in Fin$
56		php3	$⊢ (x \in Fin \land y \subset x) \to y ≺ x$
57	56	ex	$⊢ x \in Fin \to (y \subset x \to y ≺ x)$
58	55 57	syl	$⊢ ((m \in ω \land ((x \approx m \land φ) \land ψ)) \land (k \in ω \land y \approx k)) \to (y \subset x \to y ≺ x)$
59		vex	$⊢ k \in V$
60		ssdomg	$⊢ k \in V \to (m \subseteq k \to m ≼ k)$
61	59 60	ax-mp	$⊢ m \subseteq k \to m ≼ k$
62		endomtr	$⊢ (x \approx m \land m ≼ k) \to x ≼ k$
63	62	ex	$⊢ x \approx m \to (m ≼ k \to x ≼ k)$
64	63	ad2antrr	$⊢ ((x \approx m \land φ) \land ψ) \to (m ≼ k \to x ≼ k)$
65	64	ad2antlr	$⊢ ((m \in ω \land ((x \approx m \land φ) \land ψ)) \land (k \in ω \land y \approx k)) \to (m ≼ k \to x ≼ k)$
66		ensym	$⊢ y \approx k \to k \approx y$
67		domentr	$⊢ (x ≼ k \land k \approx y) \to x ≼ y$
68	66 67	sylan2	$⊢ (x ≼ k \land y \approx k) \to x ≼ y$
69	68	expcom	$⊢ y \approx k \to (x ≼ k \to x ≼ y)$
70	69	ad2antll	$⊢ ((m \in ω \land ((x \approx m \land φ) \land ψ)) \land (k \in ω \land y \approx k)) \to (x ≼ k \to x ≼ y)$
71	65 70	syld	$⊢ ((m \in ω \land ((x \approx m \land φ) \land ψ)) \land (k \in ω \land y \approx k)) \to (m ≼ k \to x ≼ y)$
72	61 71	syl5	$⊢ ((m \in ω \land ((x \approx m \land φ) \land ψ)) \land (k \in ω \land y \approx k)) \to (m \subseteq k \to x ≼ y)$
73		domnsym	$⊢ x ≼ y \to \neg y ≺ x$
74	73	con2i	$⊢ y ≺ x \to \neg x ≼ y$
75	72 74	nsyli	$⊢ ((m \in ω \land ((x \approx m \land φ) \land ψ)) \land (k \in ω \land y \approx k)) \to (y ≺ x \to \neg m \subseteq k)$
76	58 75	syld	$⊢ ((m \in ω \land ((x \approx m \land φ) \land ψ)) \land (k \in ω \land y \approx k)) \to (y \subset x \to \neg m \subseteq k)$
77	76	impr	$⊢ ((m \in ω \land ((x \approx m \land φ) \land ψ)) \land ((k \in ω \land y \approx k) \land y \subset x)) \to \neg m \subseteq k$
78		nnord	$⊢ m \in ω \to Ord m$
79	78	ad2antrr	$⊢ ((m \in ω \land ((x \approx m \land φ) \land ψ)) \land ((k \in ω \land y \approx k) \land y \subset x)) \to Ord m$
80		nnord	$⊢ k \in ω \to Ord k$
81	80	adantr	$⊢ (k \in ω \land y \approx k) \to Ord k$
82	81	ad2antrl	$⊢ ((m \in ω \land ((x \approx m \land φ) \land ψ)) \land ((k \in ω \land y \approx k) \land y \subset x)) \to Ord k$
83		ordtri1	$⊢ (Ord m \land Ord k) \to (m \subseteq k \leftrightarrow \neg k \in m)$
84	83	con2bid	$⊢ (Ord m \land Ord k) \to (k \in m \leftrightarrow \neg m \subseteq k)$
85	79 82 84	syl2anc	$⊢ ((m \in ω \land ((x \approx m \land φ) \land ψ)) \land ((k \in ω \land y \approx k) \land y \subset x)) \to (k \in m \leftrightarrow \neg m \subseteq k)$
86	77 85	mpbird	$⊢ ((m \in ω \land ((x \approx m \land φ) \land ψ)) \land ((k \in ω \land y \approx k) \land y \subset x)) \to k \in m$
87	44 51 86	jca31	$⊢ ((m \in ω \land ((x \approx m \land φ) \land ψ)) \land ((k \in ω \land y \approx k) \land y \subset x)) \to ((k \in ω \land \exists x (x \approx k \land φ)) \land k \in m)$
88		elin	$⊢ k \in (\{n \in ω \| \exists x (x \approx n \land φ)\} \cap m) \leftrightarrow (k \in \{n \in ω \| \exists x (x \approx n \land φ)\} \land k \in m)$
89		breq2	$⊢ n = k \to (x \approx n \leftrightarrow x \approx k)$
90	89	anbi1d	$⊢ n = k \to ((x \approx n \land φ) \leftrightarrow (x \approx k \land φ))$
91	90	exbidv	$⊢ n = k \to (\exists x (x \approx n \land φ) \leftrightarrow \exists x (x \approx k \land φ))$
92	91	elrab	$⊢ k \in \{n \in ω \| \exists x (x \approx n \land φ)\} \leftrightarrow (k \in ω \land \exists x (x \approx k \land φ))$
93	92	anbi1i	$⊢ (k \in \{n \in ω \| \exists x (x \approx n \land φ)\} \land k \in m) \leftrightarrow ((k \in ω \land \exists x (x \approx k \land φ)) \land k \in m)$
94	88 93	bitri	$⊢ k \in (\{n \in ω \| \exists x (x \approx n \land φ)\} \cap m) \leftrightarrow ((k \in ω \land \exists x (x \approx k \land φ)) \land k \in m)$
95	87 94	sylibr	$⊢ ((m \in ω \land ((x \approx m \land φ) \land ψ)) \land ((k \in ω \land y \approx k) \land y \subset x)) \to k \in (\{n \in ω \| \exists x (x \approx n \land φ)\} \cap m)$
96	95	ne0d	$⊢ ((m \in ω \land ((x \approx m \land φ) \land ψ)) \land ((k \in ω \land y \approx k) \land y \subset x)) \to \{n \in ω \| \exists x (x \approx n \land φ)\} \cap m \neq \emptyset$
97	96	exp44	$⊢ (m \in ω \land ((x \approx m \land φ) \land ψ)) \to (k \in ω \to (y \approx k \to (y \subset x \to \{n \in ω \| \exists x (x \approx n \land φ)\} \cap m \neq \emptyset)))$
98	97	rexlimdv	$⊢ (m \in ω \land ((x \approx m \land φ) \land ψ)) \to (\exists k \in ω y \approx k \to (y \subset x \to \{n \in ω \| \exists x (x \approx n \land φ)\} \cap m \neq \emptyset))$
99	43 98	biimtrid	$⊢ (m \in ω \land ((x \approx m \land φ) \land ψ)) \to (y \in Fin \to (y \subset x \to \{n \in ω \| \exists x (x \approx n \land φ)\} \cap m \neq \emptyset))$
100	99	com23	$⊢ (m \in ω \land ((x \approx m \land φ) \land ψ)) \to (y \subset x \to (y \in Fin \to \{n \in ω \| \exists x (x \approx n \land φ)\} \cap m \neq \emptyset))$
101	42 100	mpdd	$⊢ (m \in ω \land ((x \approx m \land φ) \land ψ)) \to (y \subset x \to \{n \in ω \| \exists x (x \approx n \land φ)\} \cap m \neq \emptyset)$
102	101	necon2bd	$⊢ (m \in ω \land ((x \approx m \land φ) \land ψ)) \to (\{n \in ω \| \exists x (x \approx n \land φ)\} \cap m = \emptyset \to \neg y \subset x)$
103	102	ex	$⊢ m \in ω \to (((x \approx m \land φ) \land ψ) \to (\{n \in ω \| \exists x (x \approx n \land φ)\} \cap m = \emptyset \to \neg y \subset x))$
104	103	com23	$⊢ m \in ω \to (\{n \in ω \| \exists x (x \approx n \land φ)\} \cap m = \emptyset \to (((x \approx m \land φ) \land ψ) \to \neg y \subset x))$
105	104	imp31	$⊢ ((m \in ω \land \{n \in ω \| \exists x (x \approx n \land φ)\} \cap m = \emptyset) \land ((x \approx m \land φ) \land ψ)) \to \neg y \subset x$
106	105	pm2.21d	$⊢ ((m \in ω \land \{n \in ω \| \exists x (x \approx n \land φ)\} \cap m = \emptyset) \land ((x \approx m \land φ) \land ψ)) \to (y \subset x \to x = y)$
107		equcomi	$⊢ y = x \to x = y$
108	107	a1i	$⊢ ((m \in ω \land \{n \in ω \| \exists x (x \approx n \land φ)\} \cap m = \emptyset) \land ((x \approx m \land φ) \land ψ)) \to (y = x \to x = y)$
109	106 108	jaod	$⊢ ((m \in ω \land \{n \in ω \| \exists x (x \approx n \land φ)\} \cap m = \emptyset) \land ((x \approx m \land φ) \land ψ)) \to ((y \subset x \lor y = x) \to x = y)$
110	33 109	biimtrid	$⊢ ((m \in ω \land \{n \in ω \| \exists x (x \approx n \land φ)\} \cap m = \emptyset) \land ((x \approx m \land φ) \land ψ)) \to (y \subseteq x \to x = y)$
111	110	expr	$⊢ ((m \in ω \land \{n \in ω \| \exists x (x \approx n \land φ)\} \cap m = \emptyset) \land (x \approx m \land φ)) \to (ψ \to (y \subseteq x \to x = y))$
112	111	com23	$⊢ ((m \in ω \land \{n \in ω \| \exists x (x \approx n \land φ)\} \cap m = \emptyset) \land (x \approx m \land φ)) \to (y \subseteq x \to (ψ \to x = y))$
113	112	impd	$⊢ ((m \in ω \land \{n \in ω \| \exists x (x \approx n \land φ)\} \cap m = \emptyset) \land (x \approx m \land φ)) \to ((y \subseteq x \land ψ) \to x = y)$
114	113	alrimiv	$⊢ ((m \in ω \land \{n \in ω \| \exists x (x \approx n \land φ)\} \cap m = \emptyset) \land (x \approx m \land φ)) \to \forall y ((y \subseteq x \land ψ) \to x = y)$
115	32 114	jca	$⊢ ((m \in ω \land \{n \in ω \| \exists x (x \approx n \land φ)\} \cap m = \emptyset) \land (x \approx m \land φ)) \to (φ \land \forall y ((y \subseteq x \land ψ) \to x = y))$
116	115	ex	$⊢ (m \in ω \land \{n \in ω \| \exists x (x \approx n \land φ)\} \cap m = \emptyset) \to ((x \approx m \land φ) \to (φ \land \forall y ((y \subseteq x \land ψ) \to x = y)))$
117	31 116	eximd	$⊢ (m \in ω \land \{n \in ω \| \exists x (x \approx n \land φ)\} \cap m = \emptyset) \to (\exists x (x \approx m \land φ) \to \exists x (φ \land \forall y ((y \subseteq x \land ψ) \to x = y)))$
118	117	impancom	$⊢ (m \in ω \land \exists x (x \approx m \land φ)) \to (\{n \in ω \| \exists x (x \approx n \land φ)\} \cap m = \emptyset \to \exists x (φ \land \forall y ((y \subseteq x \land ψ) \to x = y)))$
119	14 118	sylbi	$⊢ m \in \{n \in ω \| \exists x (x \approx n \land φ)\} \to (\{n \in ω \| \exists x (x \approx n \land φ)\} \cap m = \emptyset \to \exists x (φ \land \forall y ((y \subseteq x \land ψ) \to x = y)))$
120	119	rexlimiv	$⊢ \exists m \in \{n \in ω \| \exists x (x \approx n \land φ)\} \{n \in ω \| \exists x (x \approx n \land φ)\} \cap m = \emptyset \to \exists x (φ \land \forall y ((y \subseteq x \land ψ) \to x = y))$
121	20 26 120	3syl	$⊢ \exists x \in Fin φ \to \exists x (φ \land \forall y ((y \subseteq x \land ψ) \to x = y))$

Metamath Proof Explorer

Theorem finminlem

Proof