frpomin

Description: Every nonempty (possibly proper) subclass of a class A with a well-founded set-like partial order R has a minimal element. The additional condition of partial order over frmin enables avoiding the axiom of infinity. (Contributed by Scott Fenton, 11-Feb-2022)

		Ref	Expression
	Assertion	frpomin	$⊢ ((R Fr A \land R Po A \land R Se A) \land (B \subseteq A \land B \neq \emptyset)) \to \exists x \in B \forall y \in B \neg y R x$

Proof

Step	Hyp	Ref	Expression
1		n0	$⊢ B \neq \emptyset \leftrightarrow \exists z z \in B$
2		rabeq0	$⊢ \{w \in B \| w R z\} = \emptyset \leftrightarrow \forall w \in B \neg w R z$
3		simprr	$⊢ ((R Fr A \land R Po A \land R Se A) \land (B \subseteq A \land z \in B)) \to z \in B$
4		breq1	$⊢ y = w \to (y R x \leftrightarrow w R x)$
5	4	notbid	$⊢ y = w \to (\neg y R x \leftrightarrow \neg w R x)$
6	5	cbvralvw	$⊢ \forall y \in B \neg y R x \leftrightarrow \forall w \in B \neg w R x$
7		breq2	$⊢ x = z \to (w R x \leftrightarrow w R z)$
8	7	notbid	$⊢ x = z \to (\neg w R x \leftrightarrow \neg w R z)$
9	8	ralbidv	$⊢ x = z \to (\forall w \in B \neg w R x \leftrightarrow \forall w \in B \neg w R z)$
10	6 9	bitrid	$⊢ x = z \to (\forall y \in B \neg y R x \leftrightarrow \forall w \in B \neg w R z)$
11	10	rspcev	$⊢ (z \in B \land \forall w \in B \neg w R z) \to \exists x \in B \forall y \in B \neg y R x$
12	11	ex	$⊢ z \in B \to (\forall w \in B \neg w R z \to \exists x \in B \forall y \in B \neg y R x)$
13	3 12	syl	$⊢ ((R Fr A \land R Po A \land R Se A) \land (B \subseteq A \land z \in B)) \to (\forall w \in B \neg w R z \to \exists x \in B \forall y \in B \neg y R x)$
14	2 13	syl5bi	$⊢ ((R Fr A \land R Po A \land R Se A) \land (B \subseteq A \land z \in B)) \to (\{w \in B \| w R z\} = \emptyset \to \exists x \in B \forall y \in B \neg y R x)$
15		simprl	$⊢ ((R Fr A \land R Po A \land R Se A) \land (B \subseteq A \land z \in B)) \to B \subseteq A$
16		simpl3	$⊢ ((R Fr A \land R Po A \land R Se A) \land (B \subseteq A \land z \in B)) \to R Se A$
17		sess2	$⊢ B \subseteq A \to (R Se A \to R Se B)$
18	15 16 17	sylc	$⊢ ((R Fr A \land R Po A \land R Se A) \land (B \subseteq A \land z \in B)) \to R Se B$
19		seex	$⊢ (R Se B \land z \in B) \to \{w \in B \| w R z\} \in V$
20	18 3 19	syl2anc	$⊢ ((R Fr A \land R Po A \land R Se A) \land (B \subseteq A \land z \in B)) \to \{w \in B \| w R z\} \in V$
21		simpl1	$⊢ ((R Fr A \land R Po A \land R Se A) \land (B \subseteq A \land z \in B)) \to R Fr A$
22		ssrab2	$⊢ \{w \in B \| w R z\} \subseteq B$
23	22 15	sstrid	$⊢ ((R Fr A \land R Po A \land R Se A) \land (B \subseteq A \land z \in B)) \to \{w \in B \| w R z\} \subseteq A$
24		fri	$⊢ ((\{w \in B \| w R z\} \in V \land R Fr A) \land (\{w \in B \| w R z\} \subseteq A \land \{w \in B \| w R z\} \neq \emptyset)) \to \exists x \in \{w \in B \| w R z\} \forall y \in \{w \in B \| w R z\} \neg y R x$
25	24	expr	$⊢ ((\{w \in B \| w R z\} \in V \land R Fr A) \land \{w \in B \| w R z\} \subseteq A) \to (\{w \in B \| w R z\} \neq \emptyset \to \exists x \in \{w \in B \| w R z\} \forall y \in \{w \in B \| w R z\} \neg y R x)$
26	20 21 23 25	syl21anc	$⊢ ((R Fr A \land R Po A \land R Se A) \land (B \subseteq A \land z \in B)) \to (\{w \in B \| w R z\} \neq \emptyset \to \exists x \in \{w \in B \| w R z\} \forall y \in \{w \in B \| w R z\} \neg y R x)$
27		breq1	$⊢ w = x \to (w R z \leftrightarrow x R z)$
28	27	rexrab	$⊢ \exists x \in \{w \in B \| w R z\} \forall y \in \{w \in B \| w R z\} \neg y R x \leftrightarrow \exists x \in B (x R z \land \forall y \in \{w \in B \| w R z\} \neg y R x)$
29		breq1	$⊢ w = y \to (w R z \leftrightarrow y R z)$
30	29	ralrab	$⊢ \forall y \in \{w \in B \| w R z\} \neg y R x \leftrightarrow \forall y \in B (y R z \to \neg y R x)$
31		simprr	$⊢ (((((R Fr A \land R Po A \land R Se A) \land (B \subseteq A \land z \in B)) \land x \in B) \land x R z) \land (y \in B \land y R x)) \to y R x$
32		simplr	$⊢ (((((R Fr A \land R Po A \land R Se A) \land (B \subseteq A \land z \in B)) \land x \in B) \land x R z) \land (y \in B \land y R x)) \to x R z$
33		simplrl	$⊢ (((R Fr A \land R Po A \land R Se A) \land (B \subseteq A \land z \in B)) \land x \in B) \to B \subseteq A$
34	33	ad2antrr	$⊢ (((((R Fr A \land R Po A \land R Se A) \land (B \subseteq A \land z \in B)) \land x \in B) \land x R z) \land (y \in B \land y R x)) \to B \subseteq A$
35		simpll2	$⊢ (((R Fr A \land R Po A \land R Se A) \land (B \subseteq A \land z \in B)) \land x \in B) \to R Po A$
36	35	ad2antrr	$⊢ (((((R Fr A \land R Po A \land R Se A) \land (B \subseteq A \land z \in B)) \land x \in B) \land x R z) \land (y \in B \land y R x)) \to R Po A$
37		poss	$⊢ B \subseteq A \to (R Po A \to R Po B)$
38	34 36 37	sylc	$⊢ (((((R Fr A \land R Po A \land R Se A) \land (B \subseteq A \land z \in B)) \land x \in B) \land x R z) \land (y \in B \land y R x)) \to R Po B$
39		simprl	$⊢ (((((R Fr A \land R Po A \land R Se A) \land (B \subseteq A \land z \in B)) \land x \in B) \land x R z) \land (y \in B \land y R x)) \to y \in B$
40		simpllr	$⊢ (((((R Fr A \land R Po A \land R Se A) \land (B \subseteq A \land z \in B)) \land x \in B) \land x R z) \land (y \in B \land y R x)) \to x \in B$
41		simplrr	$⊢ (((R Fr A \land R Po A \land R Se A) \land (B \subseteq A \land z \in B)) \land x \in B) \to z \in B$
42	41	ad2antrr	$⊢ (((((R Fr A \land R Po A \land R Se A) \land (B \subseteq A \land z \in B)) \land x \in B) \land x R z) \land (y \in B \land y R x)) \to z \in B$
43		potr	$⊢ (R Po B \land (y \in B \land x \in B \land z \in B)) \to ((y R x \land x R z) \to y R z)$
44	38 39 40 42 43	syl13anc	$⊢ (((((R Fr A \land R Po A \land R Se A) \land (B \subseteq A \land z \in B)) \land x \in B) \land x R z) \land (y \in B \land y R x)) \to ((y R x \land x R z) \to y R z)$
45	31 32 44	mp2and	$⊢ (((((R Fr A \land R Po A \land R Se A) \land (B \subseteq A \land z \in B)) \land x \in B) \land x R z) \land (y \in B \land y R x)) \to y R z$
46	45	expr	$⊢ (((((R Fr A \land R Po A \land R Se A) \land (B \subseteq A \land z \in B)) \land x \in B) \land x R z) \land y \in B) \to (y R x \to y R z)$
47	46	con3d	$⊢ (((((R Fr A \land R Po A \land R Se A) \land (B \subseteq A \land z \in B)) \land x \in B) \land x R z) \land y \in B) \to (\neg y R z \to \neg y R x)$
48		idd	$⊢ (((((R Fr A \land R Po A \land R Se A) \land (B \subseteq A \land z \in B)) \land x \in B) \land x R z) \land y \in B) \to (\neg y R x \to \neg y R x)$
49	47 48	jad	$⊢ (((((R Fr A \land R Po A \land R Se A) \land (B \subseteq A \land z \in B)) \land x \in B) \land x R z) \land y \in B) \to ((y R z \to \neg y R x) \to \neg y R x)$
50	49	ralimdva	$⊢ ((((R Fr A \land R Po A \land R Se A) \land (B \subseteq A \land z \in B)) \land x \in B) \land x R z) \to (\forall y \in B (y R z \to \neg y R x) \to \forall y \in B \neg y R x)$
51	30 50	syl5bi	$⊢ ((((R Fr A \land R Po A \land R Se A) \land (B \subseteq A \land z \in B)) \land x \in B) \land x R z) \to (\forall y \in \{w \in B \| w R z\} \neg y R x \to \forall y \in B \neg y R x)$
52	51	expimpd	$⊢ (((R Fr A \land R Po A \land R Se A) \land (B \subseteq A \land z \in B)) \land x \in B) \to ((x R z \land \forall y \in \{w \in B \| w R z\} \neg y R x) \to \forall y \in B \neg y R x)$
53	52	reximdva	$⊢ ((R Fr A \land R Po A \land R Se A) \land (B \subseteq A \land z \in B)) \to (\exists x \in B (x R z \land \forall y \in \{w \in B \| w R z\} \neg y R x) \to \exists x \in B \forall y \in B \neg y R x)$
54	28 53	syl5bi	$⊢ ((R Fr A \land R Po A \land R Se A) \land (B \subseteq A \land z \in B)) \to (\exists x \in \{w \in B \| w R z\} \forall y \in \{w \in B \| w R z\} \neg y R x \to \exists x \in B \forall y \in B \neg y R x)$
55	26 54	syld	$⊢ ((R Fr A \land R Po A \land R Se A) \land (B \subseteq A \land z \in B)) \to (\{w \in B \| w R z\} \neq \emptyset \to \exists x \in B \forall y \in B \neg y R x)$
56	14 55	pm2.61dne	$⊢ ((R Fr A \land R Po A \land R Se A) \land (B \subseteq A \land z \in B)) \to \exists x \in B \forall y \in B \neg y R x$
57	56	expr	$⊢ ((R Fr A \land R Po A \land R Se A) \land B \subseteq A) \to (z \in B \to \exists x \in B \forall y \in B \neg y R x)$
58	57	exlimdv	$⊢ ((R Fr A \land R Po A \land R Se A) \land B \subseteq A) \to (\exists z z \in B \to \exists x \in B \forall y \in B \neg y R x)$
59	1 58	syl5bi	$⊢ ((R Fr A \land R Po A \land R Se A) \land B \subseteq A) \to (B \neq \emptyset \to \exists x \in B \forall y \in B \neg y R x)$
60	59	impr	$⊢ ((R Fr A \land R Po A \land R Se A) \land (B \subseteq A \land B \neq \emptyset)) \to \exists x \in B \forall y \in B \neg y R x$

Metamath Proof Explorer

Theorem frpomin

Proof