nummin

Description: Every nonempty class of numerable sets has a minimal element. (Contributed by BTernaryTau, 18-Jul-2024)

		Ref	Expression
	Assertion	nummin	$⊢ (A \subseteq dom card \land A \neq \emptyset) \to \exists x \in A Pred (≺ A x) = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		cardf2	$⊢ card : \{z \| \exists y \in On y \approx z\} ⟶ On$
2		ffun	$⊢ card : \{z \| \exists y \in On y \approx z\} ⟶ On \to Fun card$
3	2	funfnd	$⊢ card : \{z \| \exists y \in On y \approx z\} ⟶ On \to card Fn dom card$
4	1 3	ax-mp	$⊢ card Fn dom card$
5		fnimaeq0	$⊢ (card Fn dom card \land A \subseteq dom card) \to (card [A] = \emptyset \leftrightarrow A = \emptyset)$
6	4 5	mpan	$⊢ A \subseteq dom card \to (card [A] = \emptyset \leftrightarrow A = \emptyset)$
7	6	necon3bid	$⊢ A \subseteq dom card \to (card [A] \neq \emptyset \leftrightarrow A \neq \emptyset)$
8	7	biimprd	$⊢ A \subseteq dom card \to (A \neq \emptyset \to card [A] \neq \emptyset)$
9	8	imdistani	$⊢ (A \subseteq dom card \land A \neq \emptyset) \to (A \subseteq dom card \land card [A] \neq \emptyset)$
10		fimass	$⊢ card : \{z \| \exists y \in On y \approx z\} ⟶ On \to card [A] \subseteq On$
11	1 10	ax-mp	$⊢ card [A] \subseteq On$
12		onssmin	$⊢ (card [A] \subseteq On \land card [A] \neq \emptyset) \to \exists z \in card [A] \forall y \in card [A] z \subseteq y$
13	11 12	mpan	$⊢ card [A] \neq \emptyset \to \exists z \in card [A] \forall y \in card [A] z \subseteq y$
14		ssel	$⊢ card [A] \subseteq On \to (z \in card [A] \to z \in On)$
15		ssel	$⊢ card [A] \subseteq On \to (y \in card [A] \to y \in On)$
16	14 15	anim12d	$⊢ card [A] \subseteq On \to ((z \in card [A] \land y \in card [A]) \to (z \in On \land y \in On))$
17	11 16	ax-mp	$⊢ (z \in card [A] \land y \in card [A]) \to (z \in On \land y \in On)$
18		ontri1	$⊢ (z \in On \land y \in On) \to (z \subseteq y \leftrightarrow \neg y \in z)$
19	17 18	syl	$⊢ (z \in card [A] \land y \in card [A]) \to (z \subseteq y \leftrightarrow \neg y \in z)$
20		epel	$⊢ y E z \leftrightarrow y \in z$
21	20	notbii	$⊢ \neg y E z \leftrightarrow \neg y \in z$
22	19 21	bitr4di	$⊢ (z \in card [A] \land y \in card [A]) \to (z \subseteq y \leftrightarrow \neg y E z)$
23	22	rgen2	$⊢ \forall z \in card [A] \forall y \in card [A] (z \subseteq y \leftrightarrow \neg y E z)$
24		r19.29r	$⊢ (\exists z \in card [A] \forall y \in card [A] z \subseteq y \land \forall z \in card [A] \forall y \in card [A] (z \subseteq y \leftrightarrow \neg y E z)) \to \exists z \in card [A] (\forall y \in card [A] z \subseteq y \land \forall y \in card [A] (z \subseteq y \leftrightarrow \neg y E z))$
25	13 23 24	sylancl	$⊢ card [A] \neq \emptyset \to \exists z \in card [A] (\forall y \in card [A] z \subseteq y \land \forall y \in card [A] (z \subseteq y \leftrightarrow \neg y E z))$
26		r19.26	$⊢ \forall y \in card [A] (z \subseteq y \land (z \subseteq y \leftrightarrow \neg y E z)) \leftrightarrow (\forall y \in card [A] z \subseteq y \land \forall y \in card [A] (z \subseteq y \leftrightarrow \neg y E z))$
27		bicom1	$⊢ (z \subseteq y \leftrightarrow \neg y E z) \to (\neg y E z \leftrightarrow z \subseteq y)$
28	27	biimparc	$⊢ (z \subseteq y \land (z \subseteq y \leftrightarrow \neg y E z)) \to \neg y E z$
29	28	ralimi	$⊢ \forall y \in card [A] (z \subseteq y \land (z \subseteq y \leftrightarrow \neg y E z)) \to \forall y \in card [A] \neg y E z$
30	26 29	sylbir	$⊢ (\forall y \in card [A] z \subseteq y \land \forall y \in card [A] (z \subseteq y \leftrightarrow \neg y E z)) \to \forall y \in card [A] \neg y E z$
31	30	reximi	$⊢ \exists z \in card [A] (\forall y \in card [A] z \subseteq y \land \forall y \in card [A] (z \subseteq y \leftrightarrow \neg y E z)) \to \exists z \in card [A] \forall y \in card [A] \neg y E z$
32	25 31	syl	$⊢ card [A] \neq \emptyset \to \exists z \in card [A] \forall y \in card [A] \neg y E z$
33	32	adantl	$⊢ (A \subseteq dom card \land card [A] \neq \emptyset) \to \exists z \in card [A] \forall y \in card [A] \neg y E z$
34		breq2	$⊢ z = card (x) \to (y E z \leftrightarrow y E card (x))$
35	34	notbid	$⊢ z = card (x) \to (\neg y E z \leftrightarrow \neg y E card (x))$
36	35	ralbidv	$⊢ z = card (x) \to (\forall y \in card [A] \neg y E z \leftrightarrow \forall y \in card [A] \neg y E card (x))$
37	36	rexima	$⊢ (card Fn dom card \land A \subseteq dom card) \to (\exists z \in card [A] \forall y \in card [A] \neg y E z \leftrightarrow \exists x \in A \forall y \in card [A] \neg y E card (x))$
38	4 37	mpan	$⊢ A \subseteq dom card \to (\exists z \in card [A] \forall y \in card [A] \neg y E z \leftrightarrow \exists x \in A \forall y \in card [A] \neg y E card (x))$
39	38	adantr	$⊢ (A \subseteq dom card \land card [A] \neq \emptyset) \to (\exists z \in card [A] \forall y \in card [A] \neg y E z \leftrightarrow \exists x \in A \forall y \in card [A] \neg y E card (x))$
40	33 39	mpbid	$⊢ (A \subseteq dom card \land card [A] \neq \emptyset) \to \exists x \in A \forall y \in card [A] \neg y E card (x)$
41		fvex	$⊢ card (x) \in V$
42	41	dfpred3	$⊢ Pred (E, card [A], card (x)) = \{y \in card [A] \| y E card (x)\}$
43	42	eqeq1i	$⊢ Pred (E, card [A], card (x)) = \emptyset \leftrightarrow \{y \in card [A] \| y E card (x)\} = \emptyset$
44		rabeq0	$⊢ \{y \in card [A] \| y E card (x)\} = \emptyset \leftrightarrow \forall y \in card [A] \neg y E card (x)$
45	43 44	bitri	$⊢ Pred (E, card [A], card (x)) = \emptyset \leftrightarrow \forall y \in card [A] \neg y E card (x)$
46	45	rexbii	$⊢ \exists x \in A Pred (E, card [A], card (x)) = \emptyset \leftrightarrow \exists x \in A \forall y \in card [A] \neg y E card (x)$
47	40 46	sylibr	$⊢ (A \subseteq dom card \land card [A] \neq \emptyset) \to \exists x \in A Pred (E, card [A], card (x)) = \emptyset$
48	9 47	syl	$⊢ (A \subseteq dom card \land A \neq \emptyset) \to \exists x \in A Pred (E, card [A], card (x)) = \emptyset$
49		ssel2	$⊢ (A \subseteq dom card \land x \in A) \to x \in dom card$
50		cardpred	$⊢ (A \subseteq dom card \land x \in dom card) \to Pred (E, card [A], card (x)) = card [Pred (≺ A x)]$
51	50	eqeq1d	$⊢ (A \subseteq dom card \land x \in dom card) \to (Pred (E, card [A], card (x)) = \emptyset \leftrightarrow card [Pred (≺ A x)] = \emptyset)$
52		predss	$⊢ Pred (≺ A x) \subseteq A$
53		sstr	$⊢ (Pred (≺ A x) \subseteq A \land A \subseteq dom card) \to Pred (≺ A x) \subseteq dom card$
54	52 53	mpan	$⊢ A \subseteq dom card \to Pred (≺ A x) \subseteq dom card$
55		fnimaeq0	$⊢ (card Fn dom card \land Pred (≺ A x) \subseteq dom card) \to (card [Pred (≺ A x)] = \emptyset \leftrightarrow Pred (≺ A x) = \emptyset)$
56	4 54 55	sylancr	$⊢ A \subseteq dom card \to (card [Pred (≺ A x)] = \emptyset \leftrightarrow Pred (≺ A x) = \emptyset)$
57	56	adantr	$⊢ (A \subseteq dom card \land x \in dom card) \to (card [Pred (≺ A x)] = \emptyset \leftrightarrow Pred (≺ A x) = \emptyset)$
58	51 57	bitrd	$⊢ (A \subseteq dom card \land x \in dom card) \to (Pred (E, card [A], card (x)) = \emptyset \leftrightarrow Pred (≺ A x) = \emptyset)$
59	49 58	syldan	$⊢ (A \subseteq dom card \land x \in A) \to (Pred (E, card [A], card (x)) = \emptyset \leftrightarrow Pred (≺ A x) = \emptyset)$
60	59	rexbidva	$⊢ A \subseteq dom card \to (\exists x \in A Pred (E, card [A], card (x)) = \emptyset \leftrightarrow \exists x \in A Pred (≺ A x) = \emptyset)$
61	60	adantr	$⊢ (A \subseteq dom card \land A \neq \emptyset) \to (\exists x \in A Pred (E, card [A], card (x)) = \emptyset \leftrightarrow \exists x \in A Pred (≺ A x) = \emptyset)$
62	48 61	mpbid	$⊢ (A \subseteq dom card \land A \neq \emptyset) \to \exists x \in A Pred (≺ A x) = \emptyset$

Metamath Proof Explorer

Theorem nummin

Proof