onfr

Description: The ordinal class is well-founded. This proof does not require the axiom of regularity. This lemma is used in ordon (through epweon ) in order to eliminate the need for the axiom of regularity. (Contributed by NM, 17-May-1994)

		Ref	Expression
	Assertion	onfr	$⊢ E Fr On$

Proof

Step	Hyp	Ref	Expression
1		dfepfr	$⊢ E Fr On \leftrightarrow \forall x ((x \subseteq On \land x \neq \emptyset) \to \exists z \in x x \cap z = \emptyset)$
2		n0	$⊢ x \neq \emptyset \leftrightarrow \exists y y \in x$
3		ineq2	$⊢ z = y \to x \cap z = x \cap y$
4	3	eqeq1d	$⊢ z = y \to (x \cap z = \emptyset \leftrightarrow x \cap y = \emptyset)$
5	4	rspcev	$⊢ (y \in x \land x \cap y = \emptyset) \to \exists z \in x x \cap z = \emptyset$
6	5	adantll	$⊢ ((x \subseteq On \land y \in x) \land x \cap y = \emptyset) \to \exists z \in x x \cap z = \emptyset$
7		inss1	$⊢ x \cap y \subseteq x$
8		ssel2	$⊢ (x \subseteq On \land y \in x) \to y \in On$
9		eloni	$⊢ y \in On \to Ord y$
10		ordfr	$⊢ Ord y \to E Fr y$
11	8 9 10	3syl	$⊢ (x \subseteq On \land y \in x) \to E Fr y$
12		inss2	$⊢ x \cap y \subseteq y$
13		vex	$⊢ x \in V$
14	13	inex1	$⊢ x \cap y \in V$
15	14	epfrc	$⊢ (E Fr y \land x \cap y \subseteq y \land x \cap y \neq \emptyset) \to \exists z \in (x \cap y) (x \cap y) \cap z = \emptyset$
16	12 15	mp3an2	$⊢ (E Fr y \land x \cap y \neq \emptyset) \to \exists z \in (x \cap y) (x \cap y) \cap z = \emptyset$
17	11 16	sylan	$⊢ ((x \subseteq On \land y \in x) \land x \cap y \neq \emptyset) \to \exists z \in (x \cap y) (x \cap y) \cap z = \emptyset$
18		inass	$⊢ (x \cap y) \cap z = x \cap (y \cap z)$
19	8 9	syl	$⊢ (x \subseteq On \land y \in x) \to Ord y$
20		elinel2	$⊢ z \in (x \cap y) \to z \in y$
21		ordelss	$⊢ (Ord y \land z \in y) \to z \subseteq y$
22	19 20 21	syl2an	$⊢ ((x \subseteq On \land y \in x) \land z \in (x \cap y)) \to z \subseteq y$
23		sseqin2	$⊢ z \subseteq y \leftrightarrow y \cap z = z$
24	22 23	sylib	$⊢ ((x \subseteq On \land y \in x) \land z \in (x \cap y)) \to y \cap z = z$
25	24	ineq2d	$⊢ ((x \subseteq On \land y \in x) \land z \in (x \cap y)) \to x \cap (y \cap z) = x \cap z$
26	18 25	eqtrid	$⊢ ((x \subseteq On \land y \in x) \land z \in (x \cap y)) \to (x \cap y) \cap z = x \cap z$
27	26	eqeq1d	$⊢ ((x \subseteq On \land y \in x) \land z \in (x \cap y)) \to ((x \cap y) \cap z = \emptyset \leftrightarrow x \cap z = \emptyset)$
28	27	rexbidva	$⊢ (x \subseteq On \land y \in x) \to (\exists z \in (x \cap y) (x \cap y) \cap z = \emptyset \leftrightarrow \exists z \in (x \cap y) x \cap z = \emptyset)$
29	28	adantr	$⊢ ((x \subseteq On \land y \in x) \land x \cap y \neq \emptyset) \to (\exists z \in (x \cap y) (x \cap y) \cap z = \emptyset \leftrightarrow \exists z \in (x \cap y) x \cap z = \emptyset)$
30	17 29	mpbid	$⊢ ((x \subseteq On \land y \in x) \land x \cap y \neq \emptyset) \to \exists z \in (x \cap y) x \cap z = \emptyset$
31		ssrexv	$⊢ x \cap y \subseteq x \to (\exists z \in (x \cap y) x \cap z = \emptyset \to \exists z \in x x \cap z = \emptyset)$
32	7 30 31	mpsyl	$⊢ ((x \subseteq On \land y \in x) \land x \cap y \neq \emptyset) \to \exists z \in x x \cap z = \emptyset$
33	6 32	pm2.61dane	$⊢ (x \subseteq On \land y \in x) \to \exists z \in x x \cap z = \emptyset$
34	33	ex	$⊢ x \subseteq On \to (y \in x \to \exists z \in x x \cap z = \emptyset)$
35	34	exlimdv	$⊢ x \subseteq On \to (\exists y y \in x \to \exists z \in x x \cap z = \emptyset)$
36	2 35	biimtrid	$⊢ x \subseteq On \to (x \neq \emptyset \to \exists z \in x x \cap z = \emptyset)$
37	36	imp	$⊢ (x \subseteq On \land x \neq \emptyset) \to \exists z \in x x \cap z = \emptyset$
38	1 37	mpgbir	$⊢ E Fr On$

Metamath Proof Explorer

Theorem onfr

Proof