wefrc

Description: A nonempty subclass of a class well-ordered by membership has a minimal element. Special case of Proposition 6.26 of TakeutiZaring p. 31. (Contributed by NM, 17-Feb-2004)

		Ref	Expression
	Assertion	wefrc	$⊢ (E We A \land B \subseteq A \land B \neq \emptyset) \to \exists x \in B B \cap x = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		wess	$⊢ B \subseteq A \to (E We A \to E We B)$
2		n0	$⊢ B \neq \emptyset \leftrightarrow \exists y y \in B$
3		ineq2	$⊢ x = y \to B \cap x = B \cap y$
4	3	eqeq1d	$⊢ x = y \to (B \cap x = \emptyset \leftrightarrow B \cap y = \emptyset)$
5	4	rspcev	$⊢ (y \in B \land B \cap y = \emptyset) \to \exists x \in B B \cap x = \emptyset$
6	5	ex	$⊢ y \in B \to (B \cap y = \emptyset \to \exists x \in B B \cap x = \emptyset)$
7	6	adantl	$⊢ (E We B \land y \in B) \to (B \cap y = \emptyset \to \exists x \in B B \cap x = \emptyset)$
8		inss1	$⊢ B \cap y \subseteq B$
9		wefr	$⊢ E We B \to E Fr B$
10		vex	$⊢ y \in V$
11	10	inex2	$⊢ B \cap y \in V$
12	11	epfrc	$⊢ (E Fr B \land B \cap y \subseteq B \land B \cap y \neq \emptyset) \to \exists x \in (B \cap y) (B \cap y) \cap x = \emptyset$
13	9 12	syl3an1	$⊢ (E We B \land B \cap y \subseteq B \land B \cap y \neq \emptyset) \to \exists x \in (B \cap y) (B \cap y) \cap x = \emptyset$
14	13	3exp	$⊢ E We B \to (B \cap y \subseteq B \to (B \cap y \neq \emptyset \to \exists x \in (B \cap y) (B \cap y) \cap x = \emptyset))$
15	8 14	mpi	$⊢ E We B \to (B \cap y \neq \emptyset \to \exists x \in (B \cap y) (B \cap y) \cap x = \emptyset)$
16		rexin	$⊢ \exists x \in (B \cap y) (B \cap y) \cap x = \emptyset \leftrightarrow \exists x \in B (x \in y \land (B \cap y) \cap x = \emptyset)$
17	15 16	syl6ib	$⊢ E We B \to (B \cap y \neq \emptyset \to \exists x \in B (x \in y \land (B \cap y) \cap x = \emptyset))$
18	17	adantr	$⊢ (E We B \land y \in B) \to (B \cap y \neq \emptyset \to \exists x \in B (x \in y \land (B \cap y) \cap x = \emptyset))$
19		elin	$⊢ z \in (B \cap x) \leftrightarrow (z \in B \land z \in x)$
20		df-3an	$⊢ (y \in B \land z \in B \land x \in B) \leftrightarrow ((y \in B \land z \in B) \land x \in B)$
21		3anrot	$⊢ (y \in B \land z \in B \land x \in B) \leftrightarrow (z \in B \land x \in B \land y \in B)$
22	20 21	bitr3i	$⊢ ((y \in B \land z \in B) \land x \in B) \leftrightarrow (z \in B \land x \in B \land y \in B)$
23		wetrep	$⊢ (E We B \land (z \in B \land x \in B \land y \in B)) \to ((z \in x \land x \in y) \to z \in y)$
24	23	expd	$⊢ (E We B \land (z \in B \land x \in B \land y \in B)) \to (z \in x \to (x \in y \to z \in y))$
25	22 24	sylan2b	$⊢ (E We B \land ((y \in B \land z \in B) \land x \in B)) \to (z \in x \to (x \in y \to z \in y))$
26	25	exp44	$⊢ E We B \to (y \in B \to (z \in B \to (x \in B \to (z \in x \to (x \in y \to z \in y)))))$
27	26	imp	$⊢ (E We B \land y \in B) \to (z \in B \to (x \in B \to (z \in x \to (x \in y \to z \in y))))$
28	27	com34	$⊢ (E We B \land y \in B) \to (z \in B \to (z \in x \to (x \in B \to (x \in y \to z \in y))))$
29	28	impd	$⊢ (E We B \land y \in B) \to ((z \in B \land z \in x) \to (x \in B \to (x \in y \to z \in y)))$
30	19 29	syl5bi	$⊢ (E We B \land y \in B) \to (z \in (B \cap x) \to (x \in B \to (x \in y \to z \in y)))$
31	30	imp4a	$⊢ (E We B \land y \in B) \to (z \in (B \cap x) \to ((x \in B \land x \in y) \to z \in y))$
32	31	com23	$⊢ (E We B \land y \in B) \to ((x \in B \land x \in y) \to (z \in (B \cap x) \to z \in y))$
33	32	ralrimdv	$⊢ (E We B \land y \in B) \to ((x \in B \land x \in y) \to \forall z \in (B \cap x) z \in y)$
34		dfss3	$⊢ B \cap x \subseteq y \leftrightarrow \forall z \in (B \cap x) z \in y$
35	33 34	syl6ibr	$⊢ (E We B \land y \in B) \to ((x \in B \land x \in y) \to B \cap x \subseteq y)$
36		dfss	$⊢ B \cap x \subseteq y \leftrightarrow B \cap x = (B \cap x) \cap y$
37		in32	$⊢ (B \cap x) \cap y = (B \cap y) \cap x$
38	37	eqeq2i	$⊢ B \cap x = (B \cap x) \cap y \leftrightarrow B \cap x = (B \cap y) \cap x$
39	36 38	sylbb	$⊢ B \cap x \subseteq y \to B \cap x = (B \cap y) \cap x$
40	39	eqeq1d	$⊢ B \cap x \subseteq y \to (B \cap x = \emptyset \leftrightarrow (B \cap y) \cap x = \emptyset)$
41	40	biimprd	$⊢ B \cap x \subseteq y \to ((B \cap y) \cap x = \emptyset \to B \cap x = \emptyset)$
42	35 41	syl6	$⊢ (E We B \land y \in B) \to ((x \in B \land x \in y) \to ((B \cap y) \cap x = \emptyset \to B \cap x = \emptyset))$
43	42	expd	$⊢ (E We B \land y \in B) \to (x \in B \to (x \in y \to ((B \cap y) \cap x = \emptyset \to B \cap x = \emptyset)))$
44	43	imp4a	$⊢ (E We B \land y \in B) \to (x \in B \to ((x \in y \land (B \cap y) \cap x = \emptyset) \to B \cap x = \emptyset))$
45	44	reximdvai	$⊢ (E We B \land y \in B) \to (\exists x \in B (x \in y \land (B \cap y) \cap x = \emptyset) \to \exists x \in B B \cap x = \emptyset)$
46	18 45	syld	$⊢ (E We B \land y \in B) \to (B \cap y \neq \emptyset \to \exists x \in B B \cap x = \emptyset)$
47	7 46	pm2.61dne	$⊢ (E We B \land y \in B) \to \exists x \in B B \cap x = \emptyset$
48	47	ex	$⊢ E We B \to (y \in B \to \exists x \in B B \cap x = \emptyset)$
49	48	exlimdv	$⊢ E We B \to (\exists y y \in B \to \exists x \in B B \cap x = \emptyset)$
50	2 49	syl5bi	$⊢ E We B \to (B \neq \emptyset \to \exists x \in B B \cap x = \emptyset)$
51	1 50	syl6com	$⊢ E We A \to (B \subseteq A \to (B \neq \emptyset \to \exists x \in B B \cap x = \emptyset))$
52	51	3imp	$⊢ (E We A \land B \subseteq A \land B \neq \emptyset) \to \exists x \in B B \cap x = \emptyset$

Metamath Proof Explorer

Theorem wefrc

Proof