dfon2lem9

Description: Lemma for dfon2 . A class of new ordinals is well-founded by _E . (Contributed by Scott Fenton, 3-Mar-2011)

		Ref	Expression
	Assertion	dfon2lem9	$⊢ \forall x \in A \forall y ((y \subset x \land Tr y) \to y \in x) \to E Fr A$

Proof

Step	Hyp	Ref	Expression
1		ssralv	$⊢ z \subseteq A \to (\forall x \in A \forall y ((y \subset x \land Tr y) \to y \in x) \to \forall x \in z \forall y ((y \subset x \land Tr y) \to y \in x))$
2		dfon2lem8	$⊢ (z \neq \emptyset \land \forall x \in z \forall y ((y \subset x \land Tr y) \to y \in x)) \to (\forall u ((u \subset ⋂ z \land Tr u) \to u \in ⋂ z) \land ⋂ z \in z)$
3	2	simprd	$⊢ (z \neq \emptyset \land \forall x \in z \forall y ((y \subset x \land Tr y) \to y \in x)) \to ⋂ z \in z$
4		intss1	$⊢ t \in z \to ⋂ z \subseteq t$
5	2	simpld	$⊢ (z \neq \emptyset \land \forall x \in z \forall y ((y \subset x \land Tr y) \to y \in x)) \to \forall u ((u \subset ⋂ z \land Tr u) \to u \in ⋂ z)$
6		intex	$⊢ z \neq \emptyset \leftrightarrow ⋂ z \in V$
7		dfon2lem3	$⊢ ⋂ z \in V \to (\forall u ((u \subset ⋂ z \land Tr u) \to u \in ⋂ z) \to (Tr ⋂ z \land \forall x \in ⋂ z \neg x \in x))$
8	7	imp	$⊢ (⋂ z \in V \land \forall u ((u \subset ⋂ z \land Tr u) \to u \in ⋂ z)) \to (Tr ⋂ z \land \forall x \in ⋂ z \neg x \in x)$
9	8	simprd	$⊢ (⋂ z \in V \land \forall u ((u \subset ⋂ z \land Tr u) \to u \in ⋂ z)) \to \forall x \in ⋂ z \neg x \in x$
10		untelirr	$⊢ \forall x \in ⋂ z \neg x \in x \to \neg ⋂ z \in ⋂ z$
11	9 10	syl	$⊢ (⋂ z \in V \land \forall u ((u \subset ⋂ z \land Tr u) \to u \in ⋂ z)) \to \neg ⋂ z \in ⋂ z$
12		eleq1	$⊢ ⋂ z = t \to (⋂ z \in ⋂ z \leftrightarrow t \in ⋂ z)$
13	12	notbid	$⊢ ⋂ z = t \to (\neg ⋂ z \in ⋂ z \leftrightarrow \neg t \in ⋂ z)$
14	11 13	syl5ibcom	$⊢ (⋂ z \in V \land \forall u ((u \subset ⋂ z \land Tr u) \to u \in ⋂ z)) \to (⋂ z = t \to \neg t \in ⋂ z)$
15	14	a1dd	$⊢ (⋂ z \in V \land \forall u ((u \subset ⋂ z \land Tr u) \to u \in ⋂ z)) \to (⋂ z = t \to (⋂ z \subseteq t \to \neg t \in ⋂ z))$
16	8	simpld	$⊢ (⋂ z \in V \land \forall u ((u \subset ⋂ z \land Tr u) \to u \in ⋂ z)) \to Tr ⋂ z$
17		trss	$⊢ Tr ⋂ z \to (t \in ⋂ z \to t \subseteq ⋂ z)$
18	16 17	syl	$⊢ (⋂ z \in V \land \forall u ((u \subset ⋂ z \land Tr u) \to u \in ⋂ z)) \to (t \in ⋂ z \to t \subseteq ⋂ z)$
19		eqss	$⊢ ⋂ z = t \leftrightarrow (⋂ z \subseteq t \land t \subseteq ⋂ z)$
20	19	simplbi2com	$⊢ t \subseteq ⋂ z \to (⋂ z \subseteq t \to ⋂ z = t)$
21	18 20	syl6	$⊢ (⋂ z \in V \land \forall u ((u \subset ⋂ z \land Tr u) \to u \in ⋂ z)) \to (t \in ⋂ z \to (⋂ z \subseteq t \to ⋂ z = t))$
22	21	com23	$⊢ (⋂ z \in V \land \forall u ((u \subset ⋂ z \land Tr u) \to u \in ⋂ z)) \to (⋂ z \subseteq t \to (t \in ⋂ z \to ⋂ z = t))$
23		con3	$⊢ (t \in ⋂ z \to ⋂ z = t) \to (\neg ⋂ z = t \to \neg t \in ⋂ z)$
24	22 23	syl6	$⊢ (⋂ z \in V \land \forall u ((u \subset ⋂ z \land Tr u) \to u \in ⋂ z)) \to (⋂ z \subseteq t \to (\neg ⋂ z = t \to \neg t \in ⋂ z))$
25	24	com23	$⊢ (⋂ z \in V \land \forall u ((u \subset ⋂ z \land Tr u) \to u \in ⋂ z)) \to (\neg ⋂ z = t \to (⋂ z \subseteq t \to \neg t \in ⋂ z))$
26	15 25	pm2.61d	$⊢ (⋂ z \in V \land \forall u ((u \subset ⋂ z \land Tr u) \to u \in ⋂ z)) \to (⋂ z \subseteq t \to \neg t \in ⋂ z)$
27	6 26	sylanb	$⊢ (z \neq \emptyset \land \forall u ((u \subset ⋂ z \land Tr u) \to u \in ⋂ z)) \to (⋂ z \subseteq t \to \neg t \in ⋂ z)$
28	5 27	syldan	$⊢ (z \neq \emptyset \land \forall x \in z \forall y ((y \subset x \land Tr y) \to y \in x)) \to (⋂ z \subseteq t \to \neg t \in ⋂ z)$
29	4 28	syl5	$⊢ (z \neq \emptyset \land \forall x \in z \forall y ((y \subset x \land Tr y) \to y \in x)) \to (t \in z \to \neg t \in ⋂ z)$
30	29	ralrimiv	$⊢ (z \neq \emptyset \land \forall x \in z \forall y ((y \subset x \land Tr y) \to y \in x)) \to \forall t \in z \neg t \in ⋂ z$
31		eleq2	$⊢ w = ⋂ z \to (t \in w \leftrightarrow t \in ⋂ z)$
32	31	notbid	$⊢ w = ⋂ z \to (\neg t \in w \leftrightarrow \neg t \in ⋂ z)$
33	32	ralbidv	$⊢ w = ⋂ z \to (\forall t \in z \neg t \in w \leftrightarrow \forall t \in z \neg t \in ⋂ z)$
34	33	rspcev	$⊢ (⋂ z \in z \land \forall t \in z \neg t \in ⋂ z) \to \exists w \in z \forall t \in z \neg t \in w$
35	3 30 34	syl2anc	$⊢ (z \neq \emptyset \land \forall x \in z \forall y ((y \subset x \land Tr y) \to y \in x)) \to \exists w \in z \forall t \in z \neg t \in w$
36	35	expcom	$⊢ \forall x \in z \forall y ((y \subset x \land Tr y) \to y \in x) \to (z \neq \emptyset \to \exists w \in z \forall t \in z \neg t \in w)$
37	1 36	syl6com	$⊢ \forall x \in A \forall y ((y \subset x \land Tr y) \to y \in x) \to (z \subseteq A \to (z \neq \emptyset \to \exists w \in z \forall t \in z \neg t \in w))$
38	37	impd	$⊢ \forall x \in A \forall y ((y \subset x \land Tr y) \to y \in x) \to ((z \subseteq A \land z \neq \emptyset) \to \exists w \in z \forall t \in z \neg t \in w)$
39	38	alrimiv	$⊢ \forall x \in A \forall y ((y \subset x \land Tr y) \to y \in x) \to \forall z ((z \subseteq A \land z \neq \emptyset) \to \exists w \in z \forall t \in z \neg t \in w)$
40		df-fr	$⊢ E Fr A \leftrightarrow \forall z ((z \subseteq A \land z \neq \emptyset) \to \exists w \in z \forall t \in z \neg t E w)$
41		epel	$⊢ t E w \leftrightarrow t \in w$
42	41	notbii	$⊢ \neg t E w \leftrightarrow \neg t \in w$
43	42	ralbii	$⊢ \forall t \in z \neg t E w \leftrightarrow \forall t \in z \neg t \in w$
44	43	rexbii	$⊢ \exists w \in z \forall t \in z \neg t E w \leftrightarrow \exists w \in z \forall t \in z \neg t \in w$
45	44	imbi2i	$⊢ ((z \subseteq A \land z \neq \emptyset) \to \exists w \in z \forall t \in z \neg t E w) \leftrightarrow ((z \subseteq A \land z \neq \emptyset) \to \exists w \in z \forall t \in z \neg t \in w)$
46	45	albii	$⊢ \forall z ((z \subseteq A \land z \neq \emptyset) \to \exists w \in z \forall t \in z \neg t E w) \leftrightarrow \forall z ((z \subseteq A \land z \neq \emptyset) \to \exists w \in z \forall t \in z \neg t \in w)$
47	40 46	bitri	$⊢ E Fr A \leftrightarrow \forall z ((z \subseteq A \land z \neq \emptyset) \to \exists w \in z \forall t \in z \neg t \in w)$
48	39 47	sylibr	$⊢ \forall x \in A \forall y ((y \subset x \land Tr y) \to y \in x) \to E Fr A$

Metamath Proof Explorer

Theorem dfon2lem9

Proof