epfrs

Description: The strong form of the Axiom of Regularity (no sethood requirement on A ), with the axiom itself present as an antecedent. See also zfregs . (Contributed by Mario Carneiro, 22-Mar-2013)

		Ref	Expression
	Assertion	epfrs	$⊢ (E Fr A \land A \neq \emptyset) \to \exists x \in A x \cap A = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		n0	$⊢ A \neq \emptyset \leftrightarrow \exists z z \in A$
2		snssi	$⊢ z \in A \to \{z\} \subseteq A$
3	2	anim2i	$⊢ (\{z\} \subseteq y \land z \in A) \to (\{z\} \subseteq y \land \{z\} \subseteq A)$
4		ssin	$⊢ (\{z\} \subseteq y \land \{z\} \subseteq A) \leftrightarrow \{z\} \subseteq y \cap A$
5		vex	$⊢ z \in V$
6	5	snss	$⊢ z \in (y \cap A) \leftrightarrow \{z\} \subseteq y \cap A$
7	4 6	bitr4i	$⊢ (\{z\} \subseteq y \land \{z\} \subseteq A) \leftrightarrow z \in (y \cap A)$
8	3 7	sylib	$⊢ (\{z\} \subseteq y \land z \in A) \to z \in (y \cap A)$
9	8	ne0d	$⊢ (\{z\} \subseteq y \land z \in A) \to y \cap A \neq \emptyset$
10		inss2	$⊢ y \cap A \subseteq A$
11		vex	$⊢ y \in V$
12	11	inex1	$⊢ y \cap A \in V$
13	12	epfrc	$⊢ (E Fr A \land y \cap A \subseteq A \land y \cap A \neq \emptyset) \to \exists x \in (y \cap A) (y \cap A) \cap x = \emptyset$
14	10 13	mp3an2	$⊢ (E Fr A \land y \cap A \neq \emptyset) \to \exists x \in (y \cap A) (y \cap A) \cap x = \emptyset$
15		elin	$⊢ x \in (y \cap A) \leftrightarrow (x \in y \land x \in A)$
16	15	anbi1i	$⊢ (x \in (y \cap A) \land (y \cap A) \cap x = \emptyset) \leftrightarrow ((x \in y \land x \in A) \land (y \cap A) \cap x = \emptyset)$
17		anass	$⊢ ((x \in y \land x \in A) \land (y \cap A) \cap x = \emptyset) \leftrightarrow (x \in y \land (x \in A \land (y \cap A) \cap x = \emptyset))$
18	16 17	bitri	$⊢ (x \in (y \cap A) \land (y \cap A) \cap x = \emptyset) \leftrightarrow (x \in y \land (x \in A \land (y \cap A) \cap x = \emptyset))$
19		n0	$⊢ x \cap A \neq \emptyset \leftrightarrow \exists w w \in (x \cap A)$
20		elinel1	$⊢ w \in (x \cap A) \to w \in x$
21	20	ancri	$⊢ w \in (x \cap A) \to (w \in x \land w \in (x \cap A))$
22		trel	$⊢ Tr y \to ((w \in x \land x \in y) \to w \in y)$
23		inass	$⊢ (y \cap A) \cap x = y \cap (A \cap x)$
24		incom	$⊢ A \cap x = x \cap A$
25	24	ineq2i	$⊢ y \cap (A \cap x) = y \cap (x \cap A)$
26	23 25	eqtri	$⊢ (y \cap A) \cap x = y \cap (x \cap A)$
27	26	eleq2i	$⊢ w \in ((y \cap A) \cap x) \leftrightarrow w \in (y \cap (x \cap A))$
28		elin	$⊢ w \in (y \cap (x \cap A)) \leftrightarrow (w \in y \land w \in (x \cap A))$
29	27 28	bitr2i	$⊢ (w \in y \land w \in (x \cap A)) \leftrightarrow w \in ((y \cap A) \cap x)$
30		ne0i	$⊢ w \in ((y \cap A) \cap x) \to (y \cap A) \cap x \neq \emptyset$
31	29 30	sylbi	$⊢ (w \in y \land w \in (x \cap A)) \to (y \cap A) \cap x \neq \emptyset$
32	31	ex	$⊢ w \in y \to (w \in (x \cap A) \to (y \cap A) \cap x \neq \emptyset)$
33	22 32	syl6	$⊢ Tr y \to ((w \in x \land x \in y) \to (w \in (x \cap A) \to (y \cap A) \cap x \neq \emptyset))$
34	33	expd	$⊢ Tr y \to (w \in x \to (x \in y \to (w \in (x \cap A) \to (y \cap A) \cap x \neq \emptyset)))$
35	34	com34	$⊢ Tr y \to (w \in x \to (w \in (x \cap A) \to (x \in y \to (y \cap A) \cap x \neq \emptyset)))$
36	35	impd	$⊢ Tr y \to ((w \in x \land w \in (x \cap A)) \to (x \in y \to (y \cap A) \cap x \neq \emptyset))$
37	21 36	syl5	$⊢ Tr y \to (w \in (x \cap A) \to (x \in y \to (y \cap A) \cap x \neq \emptyset))$
38	37	exlimdv	$⊢ Tr y \to (\exists w w \in (x \cap A) \to (x \in y \to (y \cap A) \cap x \neq \emptyset))$
39	19 38	syl5bi	$⊢ Tr y \to (x \cap A \neq \emptyset \to (x \in y \to (y \cap A) \cap x \neq \emptyset))$
40	39	com23	$⊢ Tr y \to (x \in y \to (x \cap A \neq \emptyset \to (y \cap A) \cap x \neq \emptyset))$
41	40	imp	$⊢ (Tr y \land x \in y) \to (x \cap A \neq \emptyset \to (y \cap A) \cap x \neq \emptyset)$
42	41	necon4d	$⊢ (Tr y \land x \in y) \to ((y \cap A) \cap x = \emptyset \to x \cap A = \emptyset)$
43	42	anim2d	$⊢ (Tr y \land x \in y) \to ((x \in A \land (y \cap A) \cap x = \emptyset) \to (x \in A \land x \cap A = \emptyset))$
44	43	expimpd	$⊢ Tr y \to ((x \in y \land (x \in A \land (y \cap A) \cap x = \emptyset)) \to (x \in A \land x \cap A = \emptyset))$
45	18 44	syl5bi	$⊢ Tr y \to ((x \in (y \cap A) \land (y \cap A) \cap x = \emptyset) \to (x \in A \land x \cap A = \emptyset))$
46	45	reximdv2	$⊢ Tr y \to (\exists x \in (y \cap A) (y \cap A) \cap x = \emptyset \to \exists x \in A x \cap A = \emptyset)$
47	14 46	syl5	$⊢ Tr y \to ((E Fr A \land y \cap A \neq \emptyset) \to \exists x \in A x \cap A = \emptyset)$
48	47	expcomd	$⊢ Tr y \to (y \cap A \neq \emptyset \to (E Fr A \to \exists x \in A x \cap A = \emptyset))$
49	9 48	syl5	$⊢ Tr y \to ((\{z\} \subseteq y \land z \in A) \to (E Fr A \to \exists x \in A x \cap A = \emptyset))$
50	49	expd	$⊢ Tr y \to (\{z\} \subseteq y \to (z \in A \to (E Fr A \to \exists x \in A x \cap A = \emptyset)))$
51	50	impcom	$⊢ (\{z\} \subseteq y \land Tr y) \to (z \in A \to (E Fr A \to \exists x \in A x \cap A = \emptyset))$
52	51	3adant3	$⊢ (\{z\} \subseteq y \land Tr y \land \forall w ((\{z\} \subseteq w \land Tr w) \to y \subseteq w)) \to (z \in A \to (E Fr A \to \exists x \in A x \cap A = \emptyset))$
53		snex	$⊢ \{z\} \in V$
54	53	tz9.1	$⊢ \exists y (\{z\} \subseteq y \land Tr y \land \forall w ((\{z\} \subseteq w \land Tr w) \to y \subseteq w))$
55	52 54	exlimiiv	$⊢ z \in A \to (E Fr A \to \exists x \in A x \cap A = \emptyset)$
56	55	exlimiv	$⊢ \exists z z \in A \to (E Fr A \to \exists x \in A x \cap A = \emptyset)$
57	1 56	sylbi	$⊢ A \neq \emptyset \to (E Fr A \to \exists x \in A x \cap A = \emptyset)$
58	57	impcom	$⊢ (E Fr A \land A \neq \emptyset) \to \exists x \in A x \cap A = \emptyset$

Metamath Proof Explorer

Theorem epfrs

Proof