dfon2lem8

Description: Lemma for dfon2 . The intersection of a nonempty class A of new ordinals is itself a new ordinal and is contained within A (Contributed by Scott Fenton, 26-Feb-2011)

		Ref	Expression
	Assertion	dfon2lem8	$⊢ (A \neq \emptyset \land \forall x \in A \forall y ((y \subset x \land Tr y) \to y \in x)) \to (\forall z ((z \subset ⋂ A \land Tr z) \to z \in ⋂ A) \land ⋂ A \in A)$

Proof

Step	Hyp	Ref	Expression
1		vex	$⊢ x \in V$
2		dfon2lem3	$⊢ x \in V \to (\forall y ((y \subset x \land Tr y) \to y \in x) \to (Tr x \land \forall z \in x \neg z \in z))$
3	1 2	ax-mp	$⊢ \forall y ((y \subset x \land Tr y) \to y \in x) \to (Tr x \land \forall z \in x \neg z \in z)$
4	3	simpld	$⊢ \forall y ((y \subset x \land Tr y) \to y \in x) \to Tr x$
5	4	ralimi	$⊢ \forall x \in A \forall y ((y \subset x \land Tr y) \to y \in x) \to \forall x \in A Tr x$
6		trint	$⊢ \forall x \in A Tr x \to Tr ⋂ A$
7	5 6	syl	$⊢ \forall x \in A \forall y ((y \subset x \land Tr y) \to y \in x) \to Tr ⋂ A$
8	7	adantl	$⊢ (A \neq \emptyset \land \forall x \in A \forall y ((y \subset x \land Tr y) \to y \in x)) \to Tr ⋂ A$
9	1	dfon2lem7	$⊢ \forall y ((y \subset x \land Tr y) \to y \in x) \to (w \in x \to \forall t ((t \subset w \land Tr t) \to t \in w))$
10	9	alrimiv	$⊢ \forall y ((y \subset x \land Tr y) \to y \in x) \to \forall w (w \in x \to \forall t ((t \subset w \land Tr t) \to t \in w))$
11	10	ralimi	$⊢ \forall x \in A \forall y ((y \subset x \land Tr y) \to y \in x) \to \forall x \in A \forall w (w \in x \to \forall t ((t \subset w \land Tr t) \to t \in w))$
12		df-ral	$⊢ \forall x \in A \forall w (w \in x \to \forall t ((t \subset w \land Tr t) \to t \in w)) \leftrightarrow \forall x (x \in A \to \forall w (w \in x \to \forall t ((t \subset w \land Tr t) \to t \in w)))$
13		19.21v	$⊢ \forall w (x \in A \to (w \in x \to \forall t ((t \subset w \land Tr t) \to t \in w))) \leftrightarrow (x \in A \to \forall w (w \in x \to \forall t ((t \subset w \land Tr t) \to t \in w)))$
14	13	albii	$⊢ \forall x \forall w (x \in A \to (w \in x \to \forall t ((t \subset w \land Tr t) \to t \in w))) \leftrightarrow \forall x (x \in A \to \forall w (w \in x \to \forall t ((t \subset w \land Tr t) \to t \in w)))$
15	12 14	bitr4i	$⊢ \forall x \in A \forall w (w \in x \to \forall t ((t \subset w \land Tr t) \to t \in w)) \leftrightarrow \forall x \forall w (x \in A \to (w \in x \to \forall t ((t \subset w \land Tr t) \to t \in w)))$
16		impexp	$⊢ ((x \in A \land w \in x) \to \forall t ((t \subset w \land Tr t) \to t \in w)) \leftrightarrow (x \in A \to (w \in x \to \forall t ((t \subset w \land Tr t) \to t \in w)))$
17	16	2albii	$⊢ \forall x \forall w ((x \in A \land w \in x) \to \forall t ((t \subset w \land Tr t) \to t \in w)) \leftrightarrow \forall x \forall w (x \in A \to (w \in x \to \forall t ((t \subset w \land Tr t) \to t \in w)))$
18		eluni2	$⊢ w \in ⋃ A \leftrightarrow \exists x \in A w \in x$
19	18	biimpi	$⊢ w \in ⋃ A \to \exists x \in A w \in x$
20	19	imim1i	$⊢ (\exists x \in A w \in x \to \forall t ((t \subset w \land Tr t) \to t \in w)) \to (w \in ⋃ A \to \forall t ((t \subset w \land Tr t) \to t \in w))$
21	20	alimi	$⊢ \forall w (\exists x \in A w \in x \to \forall t ((t \subset w \land Tr t) \to t \in w)) \to \forall w (w \in ⋃ A \to \forall t ((t \subset w \land Tr t) \to t \in w))$
22		alcom	$⊢ \forall x \forall w ((x \in A \land w \in x) \to \forall t ((t \subset w \land Tr t) \to t \in w)) \leftrightarrow \forall w \forall x ((x \in A \land w \in x) \to \forall t ((t \subset w \land Tr t) \to t \in w))$
23		19.23v	$⊢ \forall x ((x \in A \land w \in x) \to \forall t ((t \subset w \land Tr t) \to t \in w)) \leftrightarrow (\exists x (x \in A \land w \in x) \to \forall t ((t \subset w \land Tr t) \to t \in w))$
24		df-rex	$⊢ \exists x \in A w \in x \leftrightarrow \exists x (x \in A \land w \in x)$
25	24	imbi1i	$⊢ (\exists x \in A w \in x \to \forall t ((t \subset w \land Tr t) \to t \in w)) \leftrightarrow (\exists x (x \in A \land w \in x) \to \forall t ((t \subset w \land Tr t) \to t \in w))$
26	23 25	bitr4i	$⊢ \forall x ((x \in A \land w \in x) \to \forall t ((t \subset w \land Tr t) \to t \in w)) \leftrightarrow (\exists x \in A w \in x \to \forall t ((t \subset w \land Tr t) \to t \in w))$
27	26	albii	$⊢ \forall w \forall x ((x \in A \land w \in x) \to \forall t ((t \subset w \land Tr t) \to t \in w)) \leftrightarrow \forall w (\exists x \in A w \in x \to \forall t ((t \subset w \land Tr t) \to t \in w))$
28	22 27	bitri	$⊢ \forall x \forall w ((x \in A \land w \in x) \to \forall t ((t \subset w \land Tr t) \to t \in w)) \leftrightarrow \forall w (\exists x \in A w \in x \to \forall t ((t \subset w \land Tr t) \to t \in w))$
29		df-ral	$⊢ \forall w \in ⋃ A \forall t ((t \subset w \land Tr t) \to t \in w) \leftrightarrow \forall w (w \in ⋃ A \to \forall t ((t \subset w \land Tr t) \to t \in w))$
30	21 28 29	3imtr4i	$⊢ \forall x \forall w ((x \in A \land w \in x) \to \forall t ((t \subset w \land Tr t) \to t \in w)) \to \forall w \in ⋃ A \forall t ((t \subset w \land Tr t) \to t \in w)$
31	17 30	sylbir	$⊢ \forall x \forall w (x \in A \to (w \in x \to \forall t ((t \subset w \land Tr t) \to t \in w))) \to \forall w \in ⋃ A \forall t ((t \subset w \land Tr t) \to t \in w)$
32	15 31	sylbi	$⊢ \forall x \in A \forall w (w \in x \to \forall t ((t \subset w \land Tr t) \to t \in w)) \to \forall w \in ⋃ A \forall t ((t \subset w \land Tr t) \to t \in w)$
33	11 32	syl	$⊢ \forall x \in A \forall y ((y \subset x \land Tr y) \to y \in x) \to \forall w \in ⋃ A \forall t ((t \subset w \land Tr t) \to t \in w)$
34	33	adantl	$⊢ (A \neq \emptyset \land \forall x \in A \forall y ((y \subset x \land Tr y) \to y \in x)) \to \forall w \in ⋃ A \forall t ((t \subset w \land Tr t) \to t \in w)$
35		intssuni	$⊢ A \neq \emptyset \to ⋂ A \subseteq ⋃ A$
36		ssralv	$⊢ ⋂ A \subseteq ⋃ A \to (\forall w \in ⋃ A \forall t ((t \subset w \land Tr t) \to t \in w) \to \forall w \in ⋂ A \forall t ((t \subset w \land Tr t) \to t \in w))$
37	35 36	syl	$⊢ A \neq \emptyset \to (\forall w \in ⋃ A \forall t ((t \subset w \land Tr t) \to t \in w) \to \forall w \in ⋂ A \forall t ((t \subset w \land Tr t) \to t \in w))$
38	37	adantr	$⊢ (A \neq \emptyset \land \forall x \in A \forall y ((y \subset x \land Tr y) \to y \in x)) \to (\forall w \in ⋃ A \forall t ((t \subset w \land Tr t) \to t \in w) \to \forall w \in ⋂ A \forall t ((t \subset w \land Tr t) \to t \in w))$
39	34 38	mpd	$⊢ (A \neq \emptyset \land \forall x \in A \forall y ((y \subset x \land Tr y) \to y \in x)) \to \forall w \in ⋂ A \forall t ((t \subset w \land Tr t) \to t \in w)$
40		dfon2lem6	$⊢ (Tr ⋂ A \land \forall w \in ⋂ A \forall t ((t \subset w \land Tr t) \to t \in w)) \to \forall z ((z \subset ⋂ A \land Tr z) \to z \in ⋂ A)$
41		intex	$⊢ A \neq \emptyset \leftrightarrow ⋂ A \in V$
42		dfon2lem3	$⊢ ⋂ A \in V \to (\forall z ((z \subset ⋂ A \land Tr z) \to z \in ⋂ A) \to (Tr ⋂ A \land \forall t \in ⋂ A \neg t \in t))$
43	41 42	sylbi	$⊢ A \neq \emptyset \to (\forall z ((z \subset ⋂ A \land Tr z) \to z \in ⋂ A) \to (Tr ⋂ A \land \forall t \in ⋂ A \neg t \in t))$
44	43	imp	$⊢ (A \neq \emptyset \land \forall z ((z \subset ⋂ A \land Tr z) \to z \in ⋂ A)) \to (Tr ⋂ A \land \forall t \in ⋂ A \neg t \in t)$
45	44	simprd	$⊢ (A \neq \emptyset \land \forall z ((z \subset ⋂ A \land Tr z) \to z \in ⋂ A)) \to \forall t \in ⋂ A \neg t \in t$
46		untelirr	$⊢ \forall t \in ⋂ A \neg t \in t \to \neg ⋂ A \in ⋂ A$
47	45 46	syl	$⊢ (A \neq \emptyset \land \forall z ((z \subset ⋂ A \land Tr z) \to z \in ⋂ A)) \to \neg ⋂ A \in ⋂ A$
48	47	adantlr	$⊢ ((A \neq \emptyset \land \forall x \in A \forall y ((y \subset x \land Tr y) \to y \in x)) \land \forall z ((z \subset ⋂ A \land Tr z) \to z \in ⋂ A)) \to \neg ⋂ A \in ⋂ A$
49		risset	$⊢ ⋂ A \in A \leftrightarrow \exists t \in A t = ⋂ A$
50	49	notbii	$⊢ \neg ⋂ A \in A \leftrightarrow \neg \exists t \in A t = ⋂ A$
51		ralnex	$⊢ \forall t \in A \neg t = ⋂ A \leftrightarrow \neg \exists t \in A t = ⋂ A$
52	50 51	bitr4i	$⊢ \neg ⋂ A \in A \leftrightarrow \forall t \in A \neg t = ⋂ A$
53		eqcom	$⊢ t = ⋂ A \leftrightarrow ⋂ A = t$
54	53	notbii	$⊢ \neg t = ⋂ A \leftrightarrow \neg ⋂ A = t$
55	44	simpld	$⊢ (A \neq \emptyset \land \forall z ((z \subset ⋂ A \land Tr z) \to z \in ⋂ A)) \to Tr ⋂ A$
56	55	adantlr	$⊢ ((A \neq \emptyset \land \forall x \in A \forall y ((y \subset x \land Tr y) \to y \in x)) \land \forall z ((z \subset ⋂ A \land Tr z) \to z \in ⋂ A)) \to Tr ⋂ A$
57		psseq2	$⊢ x = t \to (y \subset x \leftrightarrow y \subset t)$
58	57	anbi1d	$⊢ x = t \to ((y \subset x \land Tr y) \leftrightarrow (y \subset t \land Tr y))$
59		elequ2	$⊢ x = t \to (y \in x \leftrightarrow y \in t)$
60	58 59	imbi12d	$⊢ x = t \to (((y \subset x \land Tr y) \to y \in x) \leftrightarrow ((y \subset t \land Tr y) \to y \in t))$
61	60	albidv	$⊢ x = t \to (\forall y ((y \subset x \land Tr y) \to y \in x) \leftrightarrow \forall y ((y \subset t \land Tr y) \to y \in t))$
62	61	rspccv	$⊢ \forall x \in A \forall y ((y \subset x \land Tr y) \to y \in x) \to (t \in A \to \forall y ((y \subset t \land Tr y) \to y \in t))$
63	62	adantl	$⊢ (A \neq \emptyset \land \forall x \in A \forall y ((y \subset x \land Tr y) \to y \in x)) \to (t \in A \to \forall y ((y \subset t \land Tr y) \to y \in t))$
64		intss1	$⊢ t \in A \to ⋂ A \subseteq t$
65		dfpss2	$⊢ ⋂ A \subset t \leftrightarrow (⋂ A \subseteq t \land \neg ⋂ A = t)$
66		psseq1	$⊢ y = ⋂ A \to (y \subset t \leftrightarrow ⋂ A \subset t)$
67		treq	$⊢ y = ⋂ A \to (Tr y \leftrightarrow Tr ⋂ A)$
68	66 67	anbi12d	$⊢ y = ⋂ A \to ((y \subset t \land Tr y) \leftrightarrow (⋂ A \subset t \land Tr ⋂ A))$
69		eleq1	$⊢ y = ⋂ A \to (y \in t \leftrightarrow ⋂ A \in t)$
70	68 69	imbi12d	$⊢ y = ⋂ A \to (((y \subset t \land Tr y) \to y \in t) \leftrightarrow ((⋂ A \subset t \land Tr ⋂ A) \to ⋂ A \in t))$
71	70	spcgv	$⊢ ⋂ A \in V \to (\forall y ((y \subset t \land Tr y) \to y \in t) \to ((⋂ A \subset t \land Tr ⋂ A) \to ⋂ A \in t))$
72	41 71	sylbi	$⊢ A \neq \emptyset \to (\forall y ((y \subset t \land Tr y) \to y \in t) \to ((⋂ A \subset t \land Tr ⋂ A) \to ⋂ A \in t))$
73	72	imp	$⊢ (A \neq \emptyset \land \forall y ((y \subset t \land Tr y) \to y \in t)) \to ((⋂ A \subset t \land Tr ⋂ A) \to ⋂ A \in t)$
74	73	expd	$⊢ (A \neq \emptyset \land \forall y ((y \subset t \land Tr y) \to y \in t)) \to (⋂ A \subset t \to (Tr ⋂ A \to ⋂ A \in t))$
75	65 74	syl5bir	$⊢ (A \neq \emptyset \land \forall y ((y \subset t \land Tr y) \to y \in t)) \to ((⋂ A \subseteq t \land \neg ⋂ A = t) \to (Tr ⋂ A \to ⋂ A \in t))$
76	75	exp4b	$⊢ A \neq \emptyset \to (\forall y ((y \subset t \land Tr y) \to y \in t) \to (⋂ A \subseteq t \to (\neg ⋂ A = t \to (Tr ⋂ A \to ⋂ A \in t))))$
77	76	com45	$⊢ A \neq \emptyset \to (\forall y ((y \subset t \land Tr y) \to y \in t) \to (⋂ A \subseteq t \to (Tr ⋂ A \to (\neg ⋂ A = t \to ⋂ A \in t))))$
78	77	com23	$⊢ A \neq \emptyset \to (⋂ A \subseteq t \to (\forall y ((y \subset t \land Tr y) \to y \in t) \to (Tr ⋂ A \to (\neg ⋂ A = t \to ⋂ A \in t))))$
79	64 78	syl5	$⊢ A \neq \emptyset \to (t \in A \to (\forall y ((y \subset t \land Tr y) \to y \in t) \to (Tr ⋂ A \to (\neg ⋂ A = t \to ⋂ A \in t))))$
80	79	adantr	$⊢ (A \neq \emptyset \land \forall x \in A \forall y ((y \subset x \land Tr y) \to y \in x)) \to (t \in A \to (\forall y ((y \subset t \land Tr y) \to y \in t) \to (Tr ⋂ A \to (\neg ⋂ A = t \to ⋂ A \in t))))$
81	63 80	mpdd	$⊢ (A \neq \emptyset \land \forall x \in A \forall y ((y \subset x \land Tr y) \to y \in x)) \to (t \in A \to (Tr ⋂ A \to (\neg ⋂ A = t \to ⋂ A \in t)))$
82	81	adantr	$⊢ ((A \neq \emptyset \land \forall x \in A \forall y ((y \subset x \land Tr y) \to y \in x)) \land \forall z ((z \subset ⋂ A \land Tr z) \to z \in ⋂ A)) \to (t \in A \to (Tr ⋂ A \to (\neg ⋂ A = t \to ⋂ A \in t)))$
83	56 82	mpid	$⊢ ((A \neq \emptyset \land \forall x \in A \forall y ((y \subset x \land Tr y) \to y \in x)) \land \forall z ((z \subset ⋂ A \land Tr z) \to z \in ⋂ A)) \to (t \in A \to (\neg ⋂ A = t \to ⋂ A \in t))$
84	54 83	syl7bi	$⊢ ((A \neq \emptyset \land \forall x \in A \forall y ((y \subset x \land Tr y) \to y \in x)) \land \forall z ((z \subset ⋂ A \land Tr z) \to z \in ⋂ A)) \to (t \in A \to (\neg t = ⋂ A \to ⋂ A \in t))$
85	84	ralrimiv	$⊢ ((A \neq \emptyset \land \forall x \in A \forall y ((y \subset x \land Tr y) \to y \in x)) \land \forall z ((z \subset ⋂ A \land Tr z) \to z \in ⋂ A)) \to \forall t \in A (\neg t = ⋂ A \to ⋂ A \in t)$
86		ralim	$⊢ \forall t \in A (\neg t = ⋂ A \to ⋂ A \in t) \to (\forall t \in A \neg t = ⋂ A \to \forall t \in A ⋂ A \in t)$
87	85 86	syl	$⊢ ((A \neq \emptyset \land \forall x \in A \forall y ((y \subset x \land Tr y) \to y \in x)) \land \forall z ((z \subset ⋂ A \land Tr z) \to z \in ⋂ A)) \to (\forall t \in A \neg t = ⋂ A \to \forall t \in A ⋂ A \in t)$
88	52 87	syl5bi	$⊢ ((A \neq \emptyset \land \forall x \in A \forall y ((y \subset x \land Tr y) \to y \in x)) \land \forall z ((z \subset ⋂ A \land Tr z) \to z \in ⋂ A)) \to (\neg ⋂ A \in A \to \forall t \in A ⋂ A \in t)$
89		elintg	$⊢ ⋂ A \in V \to (⋂ A \in ⋂ A \leftrightarrow \forall t \in A ⋂ A \in t)$
90	41 89	sylbi	$⊢ A \neq \emptyset \to (⋂ A \in ⋂ A \leftrightarrow \forall t \in A ⋂ A \in t)$
91	90	ad2antrr	$⊢ ((A \neq \emptyset \land \forall x \in A \forall y ((y \subset x \land Tr y) \to y \in x)) \land \forall z ((z \subset ⋂ A \land Tr z) \to z \in ⋂ A)) \to (⋂ A \in ⋂ A \leftrightarrow \forall t \in A ⋂ A \in t)$
92	88 91	sylibrd	$⊢ ((A \neq \emptyset \land \forall x \in A \forall y ((y \subset x \land Tr y) \to y \in x)) \land \forall z ((z \subset ⋂ A \land Tr z) \to z \in ⋂ A)) \to (\neg ⋂ A \in A \to ⋂ A \in ⋂ A)$
93	48 92	mt3d	$⊢ ((A \neq \emptyset \land \forall x \in A \forall y ((y \subset x \land Tr y) \to y \in x)) \land \forall z ((z \subset ⋂ A \land Tr z) \to z \in ⋂ A)) \to ⋂ A \in A$
94	93	ex	$⊢ (A \neq \emptyset \land \forall x \in A \forall y ((y \subset x \land Tr y) \to y \in x)) \to (\forall z ((z \subset ⋂ A \land Tr z) \to z \in ⋂ A) \to ⋂ A \in A)$
95	94	ancld	$⊢ (A \neq \emptyset \land \forall x \in A \forall y ((y \subset x \land Tr y) \to y \in x)) \to (\forall z ((z \subset ⋂ A \land Tr z) \to z \in ⋂ A) \to (\forall z ((z \subset ⋂ A \land Tr z) \to z \in ⋂ A) \land ⋂ A \in A))$
96	40 95	syl5	$⊢ (A \neq \emptyset \land \forall x \in A \forall y ((y \subset x \land Tr y) \to y \in x)) \to ((Tr ⋂ A \land \forall w \in ⋂ A \forall t ((t \subset w \land Tr t) \to t \in w)) \to (\forall z ((z \subset ⋂ A \land Tr z) \to z \in ⋂ A) \land ⋂ A \in A))$
97	8 39 96	mp2and	$⊢ (A \neq \emptyset \land \forall x \in A \forall y ((y \subset x \land Tr y) \to y \in x)) \to (\forall z ((z \subset ⋂ A \land Tr z) \to z \in ⋂ A) \land ⋂ A \in A)$

Metamath Proof Explorer

Theorem dfon2lem8

Proof