dfon2lem6

Description: Lemma for dfon2 . A transitive class of sets satisfying the new definition satisfies the new definition. (Contributed by Scott Fenton, 25-Feb-2011)

		Ref	Expression
	Assertion	dfon2lem6	$⊢ (Tr S \land \forall x \in S \forall z ((z \subset x \land Tr z) \to z \in x)) \to \forall y ((y \subset S \land Tr y) \to y \in S)$

Proof

Step	Hyp	Ref	Expression
1		pssss	$⊢ y \subset S \to y \subseteq S$
2		ssralv	$⊢ y \subseteq S \to (\forall x \in S \forall z ((z \subset x \land Tr z) \to z \in x) \to \forall x \in y \forall z ((z \subset x \land Tr z) \to z \in x))$
3	1 2	syl	$⊢ y \subset S \to (\forall x \in S \forall z ((z \subset x \land Tr z) \to z \in x) \to \forall x \in y \forall z ((z \subset x \land Tr z) \to z \in x))$
4	3	impcom	$⊢ (\forall x \in S \forall z ((z \subset x \land Tr z) \to z \in x) \land y \subset S) \to \forall x \in y \forall z ((z \subset x \land Tr z) \to z \in x)$
5	4	adantrr	$⊢ (\forall x \in S \forall z ((z \subset x \land Tr z) \to z \in x) \land (y \subset S \land Tr y)) \to \forall x \in y \forall z ((z \subset x \land Tr z) \to z \in x)$
6	5	ad2ant2lr	$⊢ ((Tr S \land \forall x \in S \forall z ((z \subset x \land Tr z) \to z \in x)) \land ((y \subset S \land Tr y) \land s \in (S ∖ y))) \to \forall x \in y \forall z ((z \subset x \land Tr z) \to z \in x)$
7		psseq2	$⊢ x = w \to (z \subset x \leftrightarrow z \subset w)$
8	7	anbi1d	$⊢ x = w \to ((z \subset x \land Tr z) \leftrightarrow (z \subset w \land Tr z))$
9		elequ2	$⊢ x = w \to (z \in x \leftrightarrow z \in w)$
10	8 9	imbi12d	$⊢ x = w \to (((z \subset x \land Tr z) \to z \in x) \leftrightarrow ((z \subset w \land Tr z) \to z \in w))$
11	10	albidv	$⊢ x = w \to (\forall z ((z \subset x \land Tr z) \to z \in x) \leftrightarrow \forall z ((z \subset w \land Tr z) \to z \in w))$
12	11	rspccv	$⊢ \forall x \in y \forall z ((z \subset x \land Tr z) \to z \in x) \to (w \in y \to \forall z ((z \subset w \land Tr z) \to z \in w))$
13	6 12	syl	$⊢ ((Tr S \land \forall x \in S \forall z ((z \subset x \land Tr z) \to z \in x)) \land ((y \subset S \land Tr y) \land s \in (S ∖ y))) \to (w \in y \to \forall z ((z \subset w \land Tr z) \to z \in w))$
14	13	imp	$⊢ (((Tr S \land \forall x \in S \forall z ((z \subset x \land Tr z) \to z \in x)) \land ((y \subset S \land Tr y) \land s \in (S ∖ y))) \land w \in y) \to \forall z ((z \subset w \land Tr z) \to z \in w)$
15		eldifi	$⊢ s \in (S ∖ y) \to s \in S$
16		psseq2	$⊢ x = s \to (z \subset x \leftrightarrow z \subset s)$
17	16	anbi1d	$⊢ x = s \to ((z \subset x \land Tr z) \leftrightarrow (z \subset s \land Tr z))$
18		elequ2	$⊢ x = s \to (z \in x \leftrightarrow z \in s)$
19	17 18	imbi12d	$⊢ x = s \to (((z \subset x \land Tr z) \to z \in x) \leftrightarrow ((z \subset s \land Tr z) \to z \in s))$
20	19	albidv	$⊢ x = s \to (\forall z ((z \subset x \land Tr z) \to z \in x) \leftrightarrow \forall z ((z \subset s \land Tr z) \to z \in s))$
21	20	rspcv	$⊢ s \in S \to (\forall x \in S \forall z ((z \subset x \land Tr z) \to z \in x) \to \forall z ((z \subset s \land Tr z) \to z \in s))$
22	15 21	syl	$⊢ s \in (S ∖ y) \to (\forall x \in S \forall z ((z \subset x \land Tr z) \to z \in x) \to \forall z ((z \subset s \land Tr z) \to z \in s))$
23		psseq1	$⊢ z = t \to (z \subset s \leftrightarrow t \subset s)$
24		treq	$⊢ z = t \to (Tr z \leftrightarrow Tr t)$
25	23 24	anbi12d	$⊢ z = t \to ((z \subset s \land Tr z) \leftrightarrow (t \subset s \land Tr t))$
26		elequ1	$⊢ z = t \to (z \in s \leftrightarrow t \in s)$
27	25 26	imbi12d	$⊢ z = t \to (((z \subset s \land Tr z) \to z \in s) \leftrightarrow ((t \subset s \land Tr t) \to t \in s))$
28	27	cbvalvw	$⊢ \forall z ((z \subset s \land Tr z) \to z \in s) \leftrightarrow \forall t ((t \subset s \land Tr t) \to t \in s)$
29	22 28	syl6ib	$⊢ s \in (S ∖ y) \to (\forall x \in S \forall z ((z \subset x \land Tr z) \to z \in x) \to \forall t ((t \subset s \land Tr t) \to t \in s))$
30	29	impcom	$⊢ (\forall x \in S \forall z ((z \subset x \land Tr z) \to z \in x) \land s \in (S ∖ y)) \to \forall t ((t \subset s \land Tr t) \to t \in s)$
31	30	ad2ant2l	$⊢ ((Tr S \land \forall x \in S \forall z ((z \subset x \land Tr z) \to z \in x)) \land ((y \subset S \land Tr y) \land s \in (S ∖ y))) \to \forall t ((t \subset s \land Tr t) \to t \in s)$
32	31	adantr	$⊢ (((Tr S \land \forall x \in S \forall z ((z \subset x \land Tr z) \to z \in x)) \land ((y \subset S \land Tr y) \land s \in (S ∖ y))) \land w \in y) \to \forall t ((t \subset s \land Tr t) \to t \in s)$
33		vex	$⊢ w \in V$
34		vex	$⊢ s \in V$
35	33 34	dfon2lem5	$⊢ (\forall z ((z \subset w \land Tr z) \to z \in w) \land \forall t ((t \subset s \land Tr t) \to t \in s)) \to (w \in s \lor w = s \lor s \in w)$
36		3orrot	$⊢ (w \in s \lor w = s \lor s \in w) \leftrightarrow (w = s \lor s \in w \lor w \in s)$
37		3orass	$⊢ (w = s \lor s \in w \lor w \in s) \leftrightarrow (w = s \lor (s \in w \lor w \in s))$
38	36 37	bitri	$⊢ (w \in s \lor w = s \lor s \in w) \leftrightarrow (w = s \lor (s \in w \lor w \in s))$
39		eleq1a	$⊢ s \in (S ∖ y) \to (w = s \to w \in (S ∖ y))$
40		elndif	$⊢ w \in y \to \neg w \in (S ∖ y)$
41	39 40	nsyli	$⊢ s \in (S ∖ y) \to (w \in y \to \neg w = s)$
42	41	imp	$⊢ (s \in (S ∖ y) \land w \in y) \to \neg w = s$
43	42	adantll	$⊢ (((y \subset S \land Tr y) \land s \in (S ∖ y)) \land w \in y) \to \neg w = s$
44	43	adantll	$⊢ (((Tr S \land \forall x \in S \forall z ((z \subset x \land Tr z) \to z \in x)) \land ((y \subset S \land Tr y) \land s \in (S ∖ y))) \land w \in y) \to \neg w = s$
45		orel1	$⊢ \neg w = s \to ((w = s \lor (s \in w \lor w \in s)) \to (s \in w \lor w \in s))$
46		trss	$⊢ Tr y \to (w \in y \to w \subseteq y)$
47		eldifn	$⊢ s \in (S ∖ y) \to \neg s \in y$
48		ssel	$⊢ w \subseteq y \to (s \in w \to s \in y)$
49	48	con3d	$⊢ w \subseteq y \to (\neg s \in y \to \neg s \in w)$
50	47 49	syl5com	$⊢ s \in (S ∖ y) \to (w \subseteq y \to \neg s \in w)$
51	46 50	syl9	$⊢ Tr y \to (s \in (S ∖ y) \to (w \in y \to \neg s \in w))$
52	51	adantl	$⊢ (y \subset S \land Tr y) \to (s \in (S ∖ y) \to (w \in y \to \neg s \in w))$
53	52	imp31	$⊢ (((y \subset S \land Tr y) \land s \in (S ∖ y)) \land w \in y) \to \neg s \in w$
54	53	adantll	$⊢ (((Tr S \land \forall x \in S \forall z ((z \subset x \land Tr z) \to z \in x)) \land ((y \subset S \land Tr y) \land s \in (S ∖ y))) \land w \in y) \to \neg s \in w$
55		orel1	$⊢ \neg s \in w \to ((s \in w \lor w \in s) \to w \in s)$
56	54 55	syl	$⊢ (((Tr S \land \forall x \in S \forall z ((z \subset x \land Tr z) \to z \in x)) \land ((y \subset S \land Tr y) \land s \in (S ∖ y))) \land w \in y) \to ((s \in w \lor w \in s) \to w \in s)$
57	45 56	syl9r	$⊢ (((Tr S \land \forall x \in S \forall z ((z \subset x \land Tr z) \to z \in x)) \land ((y \subset S \land Tr y) \land s \in (S ∖ y))) \land w \in y) \to (\neg w = s \to ((w = s \lor (s \in w \lor w \in s)) \to w \in s))$
58	44 57	mpd	$⊢ (((Tr S \land \forall x \in S \forall z ((z \subset x \land Tr z) \to z \in x)) \land ((y \subset S \land Tr y) \land s \in (S ∖ y))) \land w \in y) \to ((w = s \lor (s \in w \lor w \in s)) \to w \in s)$
59	38 58	syl5bi	$⊢ (((Tr S \land \forall x \in S \forall z ((z \subset x \land Tr z) \to z \in x)) \land ((y \subset S \land Tr y) \land s \in (S ∖ y))) \land w \in y) \to ((w \in s \lor w = s \lor s \in w) \to w \in s)$
60	35 59	syl5	$⊢ (((Tr S \land \forall x \in S \forall z ((z \subset x \land Tr z) \to z \in x)) \land ((y \subset S \land Tr y) \land s \in (S ∖ y))) \land w \in y) \to ((\forall z ((z \subset w \land Tr z) \to z \in w) \land \forall t ((t \subset s \land Tr t) \to t \in s)) \to w \in s)$
61	14 32 60	mp2and	$⊢ (((Tr S \land \forall x \in S \forall z ((z \subset x \land Tr z) \to z \in x)) \land ((y \subset S \land Tr y) \land s \in (S ∖ y))) \land w \in y) \to w \in s$
62	61	ex	$⊢ ((Tr S \land \forall x \in S \forall z ((z \subset x \land Tr z) \to z \in x)) \land ((y \subset S \land Tr y) \land s \in (S ∖ y))) \to (w \in y \to w \in s)$
63	62	ssrdv	$⊢ ((Tr S \land \forall x \in S \forall z ((z \subset x \land Tr z) \to z \in x)) \land ((y \subset S \land Tr y) \land s \in (S ∖ y))) \to y \subseteq s$
64		dfpss2	$⊢ y \subset s \leftrightarrow (y \subseteq s \land \neg y = s)$
65		psseq1	$⊢ z = y \to (z \subset s \leftrightarrow y \subset s)$
66		treq	$⊢ z = y \to (Tr z \leftrightarrow Tr y)$
67	65 66	anbi12d	$⊢ z = y \to ((z \subset s \land Tr z) \leftrightarrow (y \subset s \land Tr y))$
68		elequ1	$⊢ z = y \to (z \in s \leftrightarrow y \in s)$
69	67 68	imbi12d	$⊢ z = y \to (((z \subset s \land Tr z) \to z \in s) \leftrightarrow ((y \subset s \land Tr y) \to y \in s))$
70	69	spvv	$⊢ \forall z ((z \subset s \land Tr z) \to z \in s) \to ((y \subset s \land Tr y) \to y \in s)$
71	70	expd	$⊢ \forall z ((z \subset s \land Tr z) \to z \in s) \to (y \subset s \to (Tr y \to y \in s))$
72	71	com23	$⊢ \forall z ((z \subset s \land Tr z) \to z \in s) \to (Tr y \to (y \subset s \to y \in s))$
73	22 72	syl6	$⊢ s \in (S ∖ y) \to (\forall x \in S \forall z ((z \subset x \land Tr z) \to z \in x) \to (Tr y \to (y \subset s \to y \in s)))$
74	73	com3l	$⊢ \forall x \in S \forall z ((z \subset x \land Tr z) \to z \in x) \to (Tr y \to (s \in (S ∖ y) \to (y \subset s \to y \in s)))$
75	74	adantld	$⊢ \forall x \in S \forall z ((z \subset x \land Tr z) \to z \in x) \to ((y \subset S \land Tr y) \to (s \in (S ∖ y) \to (y \subset s \to y \in s)))$
76	75	adantl	$⊢ (Tr S \land \forall x \in S \forall z ((z \subset x \land Tr z) \to z \in x)) \to ((y \subset S \land Tr y) \to (s \in (S ∖ y) \to (y \subset s \to y \in s)))$
77	76	imp32	$⊢ ((Tr S \land \forall x \in S \forall z ((z \subset x \land Tr z) \to z \in x)) \land ((y \subset S \land Tr y) \land s \in (S ∖ y))) \to (y \subset s \to y \in s)$
78	64 77	syl5bir	$⊢ ((Tr S \land \forall x \in S \forall z ((z \subset x \land Tr z) \to z \in x)) \land ((y \subset S \land Tr y) \land s \in (S ∖ y))) \to ((y \subseteq s \land \neg y = s) \to y \in s)$
79	63 78	mpand	$⊢ ((Tr S \land \forall x \in S \forall z ((z \subset x \land Tr z) \to z \in x)) \land ((y \subset S \land Tr y) \land s \in (S ∖ y))) \to (\neg y = s \to y \in s)$
80	79	orrd	$⊢ ((Tr S \land \forall x \in S \forall z ((z \subset x \land Tr z) \to z \in x)) \land ((y \subset S \land Tr y) \land s \in (S ∖ y))) \to (y = s \lor y \in s)$
81	80	anassrs	$⊢ (((Tr S \land \forall x \in S \forall z ((z \subset x \land Tr z) \to z \in x)) \land (y \subset S \land Tr y)) \land s \in (S ∖ y)) \to (y = s \lor y \in s)$
82	81	ralrimiva	$⊢ ((Tr S \land \forall x \in S \forall z ((z \subset x \land Tr z) \to z \in x)) \land (y \subset S \land Tr y)) \to \forall s \in (S ∖ y) (y = s \lor y \in s)$
83		pssdif	$⊢ y \subset S \to S ∖ y \neq \emptyset$
84		r19.2z	$⊢ (S ∖ y \neq \emptyset \land \forall s \in (S ∖ y) (y = s \lor y \in s)) \to \exists s \in (S ∖ y) (y = s \lor y \in s)$
85	84	ex	$⊢ S ∖ y \neq \emptyset \to (\forall s \in (S ∖ y) (y = s \lor y \in s) \to \exists s \in (S ∖ y) (y = s \lor y \in s))$
86	83 85	syl	$⊢ y \subset S \to (\forall s \in (S ∖ y) (y = s \lor y \in s) \to \exists s \in (S ∖ y) (y = s \lor y \in s))$
87	86	ad2antrl	$⊢ ((Tr S \land \forall x \in S \forall z ((z \subset x \land Tr z) \to z \in x)) \land (y \subset S \land Tr y)) \to (\forall s \in (S ∖ y) (y = s \lor y \in s) \to \exists s \in (S ∖ y) (y = s \lor y \in s))$
88		eleq1w	$⊢ y = s \to (y \in S \leftrightarrow s \in S)$
89	15 88	syl5ibr	$⊢ y = s \to (s \in (S ∖ y) \to y \in S)$
90	89	a1i	$⊢ ((Tr S \land \forall x \in S \forall z ((z \subset x \land Tr z) \to z \in x)) \land (y \subset S \land Tr y)) \to (y = s \to (s \in (S ∖ y) \to y \in S))$
91		trel	$⊢ Tr S \to ((y \in s \land s \in S) \to y \in S)$
92	91	expd	$⊢ Tr S \to (y \in s \to (s \in S \to y \in S))$
93	15 92	syl7	$⊢ Tr S \to (y \in s \to (s \in (S ∖ y) \to y \in S))$
94	93	ad2antrr	$⊢ ((Tr S \land \forall x \in S \forall z ((z \subset x \land Tr z) \to z \in x)) \land (y \subset S \land Tr y)) \to (y \in s \to (s \in (S ∖ y) \to y \in S))$
95	90 94	jaod	$⊢ ((Tr S \land \forall x \in S \forall z ((z \subset x \land Tr z) \to z \in x)) \land (y \subset S \land Tr y)) \to ((y = s \lor y \in s) \to (s \in (S ∖ y) \to y \in S))$
96	95	com23	$⊢ ((Tr S \land \forall x \in S \forall z ((z \subset x \land Tr z) \to z \in x)) \land (y \subset S \land Tr y)) \to (s \in (S ∖ y) \to ((y = s \lor y \in s) \to y \in S))$
97	96	rexlimdv	$⊢ ((Tr S \land \forall x \in S \forall z ((z \subset x \land Tr z) \to z \in x)) \land (y \subset S \land Tr y)) \to (\exists s \in (S ∖ y) (y = s \lor y \in s) \to y \in S)$
98	87 97	syld	$⊢ ((Tr S \land \forall x \in S \forall z ((z \subset x \land Tr z) \to z \in x)) \land (y \subset S \land Tr y)) \to (\forall s \in (S ∖ y) (y = s \lor y \in s) \to y \in S)$
99	82 98	mpd	$⊢ ((Tr S \land \forall x \in S \forall z ((z \subset x \land Tr z) \to z \in x)) \land (y \subset S \land Tr y)) \to y \in S$
100	99	ex	$⊢ (Tr S \land \forall x \in S \forall z ((z \subset x \land Tr z) \to z \in x)) \to ((y \subset S \land Tr y) \to y \in S)$
101	100	alrimiv	$⊢ (Tr S \land \forall x \in S \forall z ((z \subset x \land Tr z) \to z \in x)) \to \forall y ((y \subset S \land Tr y) \to y \in S)$

Metamath Proof Explorer

Theorem dfon2lem6

Proof