wereu2

Description: All nonempty subclasses of a class having a well-ordered and set-like relation have a minimal element for that relation. Proposition 6.26 of TakeutiZaring p. 31. (Contributed by Scott Fenton, 29-Jan-2011) (Revised by Mario Carneiro, 24-Jun-2015)

		Ref	Expression
	Assertion	wereu2	$⊢ ((R We 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		breq1	$⊢ y = w \to (y R x \leftrightarrow w R x)$
4	3	notbid	$⊢ y = w \to (\neg y R x \leftrightarrow \neg w R x)$
5	4	cbvralvw	$⊢ \forall y \in B \neg y R x \leftrightarrow \forall w \in B \neg w R x$
6		breq2	$⊢ x = z \to (w R x \leftrightarrow w R z)$
7	6	notbid	$⊢ x = z \to (\neg w R x \leftrightarrow \neg w R z)$
8	7	ralbidv	$⊢ x = z \to (\forall w \in B \neg w R x \leftrightarrow \forall w \in B \neg w R z)$
9	5 8	syl5bb	$⊢ x = z \to (\forall y \in B \neg y R x \leftrightarrow \forall w \in B \neg w R z)$
10	9	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$
11	10	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)$
12	11	ad2antll	$⊢ ((R We 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)$
13	2 12	syl5bi	$⊢ ((R We 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)$
14		simprl	$⊢ ((R We A \land R Se A) \land (B \subseteq A \land z \in B)) \to B \subseteq A$
15		simplr	$⊢ ((R We A \land R Se A) \land (B \subseteq A \land z \in B)) \to R Se A$
16		sess2	$⊢ B \subseteq A \to (R Se A \to R Se B)$
17	14 15 16	sylc	$⊢ ((R We A \land R Se A) \land (B \subseteq A \land z \in B)) \to R Se B$
18		simprr	$⊢ ((R We A \land R Se A) \land (B \subseteq A \land z \in B)) \to z \in B$
19		seex	$⊢ (R Se B \land z \in B) \to \{w \in B \| w R z\} \in V$
20	17 18 19	syl2anc	$⊢ ((R We A \land R Se A) \land (B \subseteq A \land z \in B)) \to \{w \in B \| w R z\} \in V$
21		wefr	$⊢ R We A \to R Fr A$
22	21	ad2antrr	$⊢ ((R We A \land R Se A) \land (B \subseteq A \land z \in B)) \to R Fr A$
23		ssrab2	$⊢ \{w \in B \| w R z\} \subseteq B$
24	23 14	sstrid	$⊢ ((R We A \land R Se A) \land (B \subseteq A \land z \in B)) \to \{w \in B \| w R z\} \subseteq A$
25		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$
26	25	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)$
27	20 22 24 26	syl21anc	$⊢ ((R We 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)$
28		breq1	$⊢ w = x \to (w R z \leftrightarrow x R z)$
29	28	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)$
30		breq1	$⊢ w = y \to (w R z \leftrightarrow y R z)$
31	30	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)$
32		weso	$⊢ R We A \to R Or A$
33	32	ad2antrr	$⊢ ((R We A \land R Se A) \land (B \subseteq A \land z \in B)) \to R Or A$
34		soss	$⊢ B \subseteq A \to (R Or A \to R Or B)$
35	14 33 34	sylc	$⊢ ((R We A \land R Se A) \land (B \subseteq A \land z \in B)) \to R Or B$
36	35	ad2antrr	$⊢ ((((R We A \land R Se A) \land (B \subseteq A \land z \in B)) \land x \in B) \land y \in B) \to R Or B$
37		simpr	$⊢ ((((R We A \land R Se A) \land (B \subseteq A \land z \in B)) \land x \in B) \land y \in B) \to y \in B$
38		simplr	$⊢ ((((R We A \land R Se A) \land (B \subseteq A \land z \in B)) \land x \in B) \land y \in B) \to x \in B$
39	18	ad2antrr	$⊢ ((((R We A \land R Se A) \land (B \subseteq A \land z \in B)) \land x \in B) \land y \in B) \to z \in B$
40		sotr	$⊢ (R Or 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)$
41	36 37 38 39 40	syl13anc	$⊢ ((((R We A \land R Se A) \land (B \subseteq A \land z \in B)) \land x \in B) \land y \in B) \to ((y R x \land x R z) \to y R z)$
42	41	ancomsd	$⊢ ((((R We A \land R Se A) \land (B \subseteq A \land z \in B)) \land x \in B) \land y \in B) \to ((x R z \land y R x) \to y R z)$
43	42	expdimp	$⊢ (((((R We A \land R Se A) \land (B \subseteq A \land z \in B)) \land x \in B) \land y \in B) \land x R z) \to (y R x \to y R z)$
44	43	an32s	$⊢ (((((R We 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)$
45	44	con3d	$⊢ (((((R We 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)$
46		idd	$⊢ (((((R We 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)$
47	45 46	jad	$⊢ (((((R We 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)$
48	47	ralimdva	$⊢ ((((R We 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)$
49	31 48	syl5bi	$⊢ ((((R We 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)$
50	49	expimpd	$⊢ (((R We 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)$
51	50	reximdva	$⊢ ((R We 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)$
52	29 51	syl5bi	$⊢ ((R We 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)$
53	27 52	syld	$⊢ ((R We 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)$
54	13 53	pm2.61dne	$⊢ ((R We 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$
55	54	expr	$⊢ ((R We 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)$
56	55	exlimdv	$⊢ ((R We 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)$
57	1 56	syl5bi	$⊢ ((R We 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)$
58	57	impr	$⊢ ((R We 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$
59		simprl	$⊢ ((R We A \land R Se A) \land (B \subseteq A \land B \neq \emptyset)) \to B \subseteq A$
60	32	ad2antrr	$⊢ ((R We A \land R Se A) \land (B \subseteq A \land B \neq \emptyset)) \to R Or A$
61	59 60 34	sylc	$⊢ ((R We A \land R Se A) \land (B \subseteq A \land B \neq \emptyset)) \to R Or B$
62		somo	$⊢ R Or B \to \exists^{*} x \in B \forall y \in B \neg y R x$
63	61 62	syl	$⊢ ((R We 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$
64		reu5	$⊢ \exists! x \in B \forall y \in B \neg y R x \leftrightarrow (\exists x \in B \forall y \in B \neg y R x \land \exists^{*} x \in B \forall y \in B \neg y R x)$
65	58 63 64	sylanbrc	$⊢ ((R We 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 wereu2

Proof