dfon2lem7

Description: Lemma for dfon2 . All elements of a new ordinal are new ordinals. (Contributed by Scott Fenton, 25-Feb-2011)

		Ref	Expression
	Hypothesis	dfon2lem7.1	$⊢ A \in V$
	Assertion	dfon2lem7	$⊢ \forall x ((x \subset A \land Tr x) \to x \in A) \to (B \in A \to \forall y ((y \subset B \land Tr y) \to y \in B))$

Proof

Step	Hyp	Ref	Expression
1		dfon2lem7.1	$⊢ A \in V$
2		elequ1	$⊢ t = z \to (t \in t \leftrightarrow z \in t)$
3		elequ2	$⊢ t = z \to (z \in t \leftrightarrow z \in z)$
4	2 3	bitrd	$⊢ t = z \to (t \in t \leftrightarrow z \in z)$
5	4	notbid	$⊢ t = z \to (\neg t \in t \leftrightarrow \neg z \in z)$
6	5	cbvralvw	$⊢ \forall t \in x \neg t \in t \leftrightarrow \forall z \in x \neg z \in z$
7	6	biimpi	$⊢ \forall t \in x \neg t \in t \to \forall z \in x \neg z \in z$
8	7	ralimi	$⊢ \forall x \in \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \forall t \in x \neg t \in t \to \forall x \in \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \forall z \in x \neg z \in z$
9		untuni	$⊢ \forall z \in ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \neg z \in z \leftrightarrow \forall x \in \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \forall z \in x \neg z \in z$
10	8 9	sylibr	$⊢ \forall x \in \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \forall t \in x \neg t \in t \to \forall z \in ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \neg z \in z$
11		vex	$⊢ x \in V$
12		sseq1	$⊢ w = x \to (w \subseteq A \leftrightarrow x \subseteq A)$
13		treq	$⊢ w = x \to (Tr w \leftrightarrow Tr x)$
14		raleq	$⊢ w = x \to (\forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t) \leftrightarrow \forall t \in x \forall y ((y \subset t \land Tr y) \to y \in t))$
15	12 13 14	3anbi123d	$⊢ w = x \to ((w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t)) \leftrightarrow (x \subseteq A \land Tr x \land \forall t \in x \forall y ((y \subset t \land Tr y) \to y \in t)))$
16	11 15	elab	$⊢ x \in \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \leftrightarrow (x \subseteq A \land Tr x \land \forall t \in x \forall y ((y \subset t \land Tr y) \to y \in t))$
17		vex	$⊢ t \in V$
18		dfon2lem3	$⊢ t \in V \to (\forall y ((y \subset t \land Tr y) \to y \in t) \to (Tr t \land \forall u \in t \neg u \in u))$
19	17 18	ax-mp	$⊢ \forall y ((y \subset t \land Tr y) \to y \in t) \to (Tr t \land \forall u \in t \neg u \in u)$
20	19	simprd	$⊢ \forall y ((y \subset t \land Tr y) \to y \in t) \to \forall u \in t \neg u \in u$
21		untelirr	$⊢ \forall u \in t \neg u \in u \to \neg t \in t$
22	20 21	syl	$⊢ \forall y ((y \subset t \land Tr y) \to y \in t) \to \neg t \in t$
23	22	ralimi	$⊢ \forall t \in x \forall y ((y \subset t \land Tr y) \to y \in t) \to \forall t \in x \neg t \in t$
24	23	3ad2ant3	$⊢ (x \subseteq A \land Tr x \land \forall t \in x \forall y ((y \subset t \land Tr y) \to y \in t)) \to \forall t \in x \neg t \in t$
25	16 24	sylbi	$⊢ x \in \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \to \forall t \in x \neg t \in t$
26	10 25	mprg	$⊢ \forall z \in ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \neg z \in z$
27		untelirr	$⊢ \forall z \in ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \neg z \in z \to \neg ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \in ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\}$
28		psseq2	$⊢ t = u \to (y \subset t \leftrightarrow y \subset u)$
29	28	anbi1d	$⊢ t = u \to ((y \subset t \land Tr y) \leftrightarrow (y \subset u \land Tr y))$
30		elequ2	$⊢ t = u \to (y \in t \leftrightarrow y \in u)$
31	29 30	imbi12d	$⊢ t = u \to (((y \subset t \land Tr y) \to y \in t) \leftrightarrow ((y \subset u \land Tr y) \to y \in u))$
32	31	albidv	$⊢ t = u \to (\forall y ((y \subset t \land Tr y) \to y \in t) \leftrightarrow \forall y ((y \subset u \land Tr y) \to y \in u))$
33	32	cbvralvw	$⊢ \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t) \leftrightarrow \forall u \in w \forall y ((y \subset u \land Tr y) \to y \in u)$
34	33	3anbi3i	$⊢ (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t)) \leftrightarrow (w \subseteq A \land Tr w \land \forall u \in w \forall y ((y \subset u \land Tr y) \to y \in u))$
35	34	abbii	$⊢ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} = \{w \| (w \subseteq A \land Tr w \land \forall u \in w \forall y ((y \subset u \land Tr y) \to y \in u))\}$
36	35	unieqi	$⊢ ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} = ⋃ \{w \| (w \subseteq A \land Tr w \land \forall u \in w \forall y ((y \subset u \land Tr y) \to y \in u))\}$
37	36	eleq2i	$⊢ ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \in ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \leftrightarrow ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \in ⋃ \{w \| (w \subseteq A \land Tr w \land \forall u \in w \forall y ((y \subset u \land Tr y) \to y \in u))\}$
38	27 37	sylnib	$⊢ \forall z \in ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \neg z \in z \to \neg ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \in ⋃ \{w \| (w \subseteq A \land Tr w \land \forall u \in w \forall y ((y \subset u \land Tr y) \to y \in u))\}$
39	26 38	ax-mp	$⊢ \neg ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \in ⋃ \{w \| (w \subseteq A \land Tr w \land \forall u \in w \forall y ((y \subset u \land Tr y) \to y \in u))\}$
40		dfon2lem2	$⊢ ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \subseteq A$
41	1 40	ssexi	$⊢ ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \in V$
42	41	snss	$⊢ ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \in ⋃ \{w \| (w \subseteq A \land Tr w \land \forall u \in w \forall y ((y \subset u \land Tr y) \to y \in u))\} \leftrightarrow \{⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\}\} \subseteq ⋃ \{w \| (w \subseteq A \land Tr w \land \forall u \in w \forall y ((y \subset u \land Tr y) \to y \in u))\}$
43	39 42	mtbi	$⊢ \neg \{⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\}\} \subseteq ⋃ \{w \| (w \subseteq A \land Tr w \land \forall u \in w \forall y ((y \subset u \land Tr y) \to y \in u))\}$
44	43	intnan	$⊢ \neg (⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \subseteq ⋃ \{w \| (w \subseteq A \land Tr w \land \forall u \in w \forall y ((y \subset u \land Tr y) \to y \in u))\} \land \{⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\}\} \subseteq ⋃ \{w \| (w \subseteq A \land Tr w \land \forall u \in w \forall y ((y \subset u \land Tr y) \to y \in u))\})$
45		df-suc	$⊢ suc ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} = ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \cup \{⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\}\}$
46	45	sseq1i	$⊢ suc ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \subseteq ⋃ \{w \| (w \subseteq A \land Tr w \land \forall u \in w \forall y ((y \subset u \land Tr y) \to y \in u))\} \leftrightarrow ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \cup \{⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\}\} \subseteq ⋃ \{w \| (w \subseteq A \land Tr w \land \forall u \in w \forall y ((y \subset u \land Tr y) \to y \in u))\}$
47		unss	$⊢ (⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \subseteq ⋃ \{w \| (w \subseteq A \land Tr w \land \forall u \in w \forall y ((y \subset u \land Tr y) \to y \in u))\} \land \{⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\}\} \subseteq ⋃ \{w \| (w \subseteq A \land Tr w \land \forall u \in w \forall y ((y \subset u \land Tr y) \to y \in u))\}) \leftrightarrow ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \cup \{⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\}\} \subseteq ⋃ \{w \| (w \subseteq A \land Tr w \land \forall u \in w \forall y ((y \subset u \land Tr y) \to y \in u))\}$
48	46 47	bitr4i	$⊢ suc ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \subseteq ⋃ \{w \| (w \subseteq A \land Tr w \land \forall u \in w \forall y ((y \subset u \land Tr y) \to y \in u))\} \leftrightarrow (⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \subseteq ⋃ \{w \| (w \subseteq A \land Tr w \land \forall u \in w \forall y ((y \subset u \land Tr y) \to y \in u))\} \land \{⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\}\} \subseteq ⋃ \{w \| (w \subseteq A \land Tr w \land \forall u \in w \forall y ((y \subset u \land Tr y) \to y \in u))\})$
49	44 48	mtbir	$⊢ \neg suc ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \subseteq ⋃ \{w \| (w \subseteq A \land Tr w \land \forall u \in w \forall y ((y \subset u \land Tr y) \to y \in u))\}$
50	41	snss	$⊢ ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \in A \leftrightarrow \{⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\}\} \subseteq A$
51	45	sseq1i	$⊢ suc ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \subseteq A \leftrightarrow ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \cup \{⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\}\} \subseteq A$
52		unss	$⊢ (⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \subseteq A \land \{⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\}\} \subseteq A) \leftrightarrow ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \cup \{⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\}\} \subseteq A$
53	51 52	bitr4i	$⊢ suc ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \subseteq A \leftrightarrow (⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \subseteq A \land \{⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\}\} \subseteq A)$
54		dfon2lem1	$⊢ Tr ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\}$
55		suctr	$⊢ Tr ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \to Tr suc ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\}$
56	54 55	ax-mp	$⊢ Tr suc ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\}$
57		vex	$⊢ u \in V$
58	57	elsuc	$⊢ u \in suc ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \leftrightarrow (u \in ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \lor u = ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\})$
59		eluni2	$⊢ u \in ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \leftrightarrow \exists x \in \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} u \in x$
60		nfa1	$⊢ Ⅎ x \forall x ((x \subset u \land Tr x) \to x \in u)$
61	32	rspccv	$⊢ \forall t \in x \forall y ((y \subset t \land Tr y) \to y \in t) \to (u \in x \to \forall y ((y \subset u \land Tr y) \to y \in u))$
62		psseq1	$⊢ y = x \to (y \subset u \leftrightarrow x \subset u)$
63		treq	$⊢ y = x \to (Tr y \leftrightarrow Tr x)$
64	62 63	anbi12d	$⊢ y = x \to ((y \subset u \land Tr y) \leftrightarrow (x \subset u \land Tr x))$
65		elequ1	$⊢ y = x \to (y \in u \leftrightarrow x \in u)$
66	64 65	imbi12d	$⊢ y = x \to (((y \subset u \land Tr y) \to y \in u) \leftrightarrow ((x \subset u \land Tr x) \to x \in u))$
67	66	cbvalvw	$⊢ \forall y ((y \subset u \land Tr y) \to y \in u) \leftrightarrow \forall x ((x \subset u \land Tr x) \to x \in u)$
68	61 67	syl6ib	$⊢ \forall t \in x \forall y ((y \subset t \land Tr y) \to y \in t) \to (u \in x \to \forall x ((x \subset u \land Tr x) \to x \in u))$
69	68	3ad2ant3	$⊢ (x \subseteq A \land Tr x \land \forall t \in x \forall y ((y \subset t \land Tr y) \to y \in t)) \to (u \in x \to \forall x ((x \subset u \land Tr x) \to x \in u))$
70	16 69	sylbi	$⊢ x \in \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \to (u \in x \to \forall x ((x \subset u \land Tr x) \to x \in u))$
71	60 70	rexlimi	$⊢ \exists x \in \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} u \in x \to \forall x ((x \subset u \land Tr x) \to x \in u)$
72	59 71	sylbi	$⊢ u \in ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \to \forall x ((x \subset u \land Tr x) \to x \in u)$
73		psseq1	$⊢ y = z \to (y \subset u \leftrightarrow z \subset u)$
74		treq	$⊢ y = z \to (Tr y \leftrightarrow Tr z)$
75	73 74	anbi12d	$⊢ y = z \to ((y \subset u \land Tr y) \leftrightarrow (z \subset u \land Tr z))$
76		elequ1	$⊢ y = z \to (y \in u \leftrightarrow z \in u)$
77	75 76	imbi12d	$⊢ y = z \to (((y \subset u \land Tr y) \to y \in u) \leftrightarrow ((z \subset u \land Tr z) \to z \in u))$
78	77	cbvalvw	$⊢ \forall y ((y \subset u \land Tr y) \to y \in u) \leftrightarrow \forall z ((z \subset u \land Tr z) \to z \in u)$
79	61 78	syl6ib	$⊢ \forall t \in x \forall y ((y \subset t \land Tr y) \to y \in t) \to (u \in x \to \forall z ((z \subset u \land Tr z) \to z \in u))$
80	79	3ad2ant3	$⊢ (x \subseteq A \land Tr x \land \forall t \in x \forall y ((y \subset t \land Tr y) \to y \in t)) \to (u \in x \to \forall z ((z \subset u \land Tr z) \to z \in u))$
81	16 80	sylbi	$⊢ x \in \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \to (u \in x \to \forall z ((z \subset u \land Tr z) \to z \in u))$
82	81	rexlimiv	$⊢ \exists x \in \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} u \in x \to \forall z ((z \subset u \land Tr z) \to z \in u)$
83	59 82	sylbi	$⊢ u \in ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \to \forall z ((z \subset u \land Tr z) \to z \in u)$
84	83	rgen	$⊢ \forall u \in ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \forall z ((z \subset u \land Tr z) \to z \in u)$
85		dfon2lem6	$⊢ (Tr ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \land \forall u \in ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \forall z ((z \subset u \land Tr z) \to z \in u)) \to \forall x ((x \subset ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \land Tr x) \to x \in ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\})$
86	54 84 85	mp2an	$⊢ \forall x ((x \subset ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \land Tr x) \to x \in ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\})$
87		psseq2	$⊢ u = ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \to (x \subset u \leftrightarrow x \subset ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\})$
88	87	anbi1d	$⊢ u = ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \to ((x \subset u \land Tr x) \leftrightarrow (x \subset ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \land Tr x))$
89		eleq2	$⊢ u = ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \to (x \in u \leftrightarrow x \in ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\})$
90	88 89	imbi12d	$⊢ u = ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \to (((x \subset u \land Tr x) \to x \in u) \leftrightarrow ((x \subset ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \land Tr x) \to x \in ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\}))$
91	90	albidv	$⊢ u = ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \to (\forall x ((x \subset u \land Tr x) \to x \in u) \leftrightarrow \forall x ((x \subset ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \land Tr x) \to x \in ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\}))$
92	86 91	mpbiri	$⊢ u = ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \to \forall x ((x \subset u \land Tr x) \to x \in u)$
93	72 92	jaoi	$⊢ (u \in ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \lor u = ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\}) \to \forall x ((x \subset u \land Tr x) \to x \in u)$
94	58 93	sylbi	$⊢ u \in suc ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \to \forall x ((x \subset u \land Tr x) \to x \in u)$
95	94	rgen	$⊢ \forall u \in suc ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \forall x ((x \subset u \land Tr x) \to x \in u)$
96	41	sucex	$⊢ suc ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \in V$
97		sseq1	$⊢ s = suc ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \to (s \subseteq A \leftrightarrow suc ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \subseteq A)$
98		treq	$⊢ s = suc ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \to (Tr s \leftrightarrow Tr suc ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\})$
99		raleq	$⊢ s = suc ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \to (\forall u \in s \forall x ((x \subset u \land Tr x) \to x \in u) \leftrightarrow \forall u \in suc ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \forall x ((x \subset u \land Tr x) \to x \in u))$
100	97 98 99	3anbi123d	$⊢ s = suc ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \to ((s \subseteq A \land Tr s \land \forall u \in s \forall x ((x \subset u \land Tr x) \to x \in u)) \leftrightarrow (suc ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \subseteq A \land Tr suc ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \land \forall u \in suc ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \forall x ((x \subset u \land Tr x) \to x \in u)))$
101	96 100	elab	$⊢ suc ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \in \{s \| (s \subseteq A \land Tr s \land \forall u \in s \forall x ((x \subset u \land Tr x) \to x \in u))\} \leftrightarrow (suc ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \subseteq A \land Tr suc ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \land \forall u \in suc ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \forall x ((x \subset u \land Tr x) \to x \in u))$
102		elssuni	$⊢ suc ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \in \{s \| (s \subseteq A \land Tr s \land \forall u \in s \forall x ((x \subset u \land Tr x) \to x \in u))\} \to suc ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \subseteq ⋃ \{s \| (s \subseteq A \land Tr s \land \forall u \in s \forall x ((x \subset u \land Tr x) \to x \in u))\}$
103	101 102	sylbir	$⊢ (suc ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \subseteq A \land Tr suc ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \land \forall u \in suc ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \forall x ((x \subset u \land Tr x) \to x \in u)) \to suc ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \subseteq ⋃ \{s \| (s \subseteq A \land Tr s \land \forall u \in s \forall x ((x \subset u \land Tr x) \to x \in u))\}$
104	56 95 103	mp3an23	$⊢ suc ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \subseteq A \to suc ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \subseteq ⋃ \{s \| (s \subseteq A \land Tr s \land \forall u \in s \forall x ((x \subset u \land Tr x) \to x \in u))\}$
105		sseq1	$⊢ s = w \to (s \subseteq A \leftrightarrow w \subseteq A)$
106		treq	$⊢ s = w \to (Tr s \leftrightarrow Tr w)$
107		raleq	$⊢ s = w \to (\forall u \in s \forall x ((x \subset u \land Tr x) \to x \in u) \leftrightarrow \forall u \in w \forall x ((x \subset u \land Tr x) \to x \in u))$
108		psseq1	$⊢ x = y \to (x \subset u \leftrightarrow y \subset u)$
109		treq	$⊢ x = y \to (Tr x \leftrightarrow Tr y)$
110	108 109	anbi12d	$⊢ x = y \to ((x \subset u \land Tr x) \leftrightarrow (y \subset u \land Tr y))$
111		elequ1	$⊢ x = y \to (x \in u \leftrightarrow y \in u)$
112	110 111	imbi12d	$⊢ x = y \to (((x \subset u \land Tr x) \to x \in u) \leftrightarrow ((y \subset u \land Tr y) \to y \in u))$
113	112	cbvalvw	$⊢ \forall x ((x \subset u \land Tr x) \to x \in u) \leftrightarrow \forall y ((y \subset u \land Tr y) \to y \in u)$
114	113	ralbii	$⊢ \forall u \in w \forall x ((x \subset u \land Tr x) \to x \in u) \leftrightarrow \forall u \in w \forall y ((y \subset u \land Tr y) \to y \in u)$
115	107 114	syl6bb	$⊢ s = w \to (\forall u \in s \forall x ((x \subset u \land Tr x) \to x \in u) \leftrightarrow \forall u \in w \forall y ((y \subset u \land Tr y) \to y \in u))$
116	105 106 115	3anbi123d	$⊢ s = w \to ((s \subseteq A \land Tr s \land \forall u \in s \forall x ((x \subset u \land Tr x) \to x \in u)) \leftrightarrow (w \subseteq A \land Tr w \land \forall u \in w \forall y ((y \subset u \land Tr y) \to y \in u)))$
117	116	cbvabv	$⊢ \{s \| (s \subseteq A \land Tr s \land \forall u \in s \forall x ((x \subset u \land Tr x) \to x \in u))\} = \{w \| (w \subseteq A \land Tr w \land \forall u \in w \forall y ((y \subset u \land Tr y) \to y \in u))\}$
118	117	unieqi	$⊢ ⋃ \{s \| (s \subseteq A \land Tr s \land \forall u \in s \forall x ((x \subset u \land Tr x) \to x \in u))\} = ⋃ \{w \| (w \subseteq A \land Tr w \land \forall u \in w \forall y ((y \subset u \land Tr y) \to y \in u))\}$
119	104 118	sseqtrdi	$⊢ suc ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \subseteq A \to suc ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \subseteq ⋃ \{w \| (w \subseteq A \land Tr w \land \forall u \in w \forall y ((y \subset u \land Tr y) \to y \in u))\}$
120	119	a1i	$⊢ \forall x ((x \subset A \land Tr x) \to x \in A) \to (suc ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \subseteq A \to suc ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \subseteq ⋃ \{w \| (w \subseteq A \land Tr w \land \forall u \in w \forall y ((y \subset u \land Tr y) \to y \in u))\})$
121	53 120	syl5bir	$⊢ \forall x ((x \subset A \land Tr x) \to x \in A) \to ((⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \subseteq A \land \{⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\}\} \subseteq A) \to suc ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \subseteq ⋃ \{w \| (w \subseteq A \land Tr w \land \forall u \in w \forall y ((y \subset u \land Tr y) \to y \in u))\})$
122	40 121	mpani	$⊢ \forall x ((x \subset A \land Tr x) \to x \in A) \to (\{⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\}\} \subseteq A \to suc ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \subseteq ⋃ \{w \| (w \subseteq A \land Tr w \land \forall u \in w \forall y ((y \subset u \land Tr y) \to y \in u))\})$
123	50 122	syl5bi	$⊢ \forall x ((x \subset A \land Tr x) \to x \in A) \to (⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \in A \to suc ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \subseteq ⋃ \{w \| (w \subseteq A \land Tr w \land \forall u \in w \forall y ((y \subset u \land Tr y) \to y \in u))\})$
124	49 123	mtoi	$⊢ \forall x ((x \subset A \land Tr x) \to x \in A) \to \neg ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \in A$
125		psseq1	$⊢ x = ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \to (x \subset A \leftrightarrow ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \subset A)$
126		treq	$⊢ x = ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \to (Tr x \leftrightarrow Tr ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\})$
127	125 126	anbi12d	$⊢ x = ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \to ((x \subset A \land Tr x) \leftrightarrow (⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \subset A \land Tr ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\}))$
128		eleq1	$⊢ x = ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \to (x \in A \leftrightarrow ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \in A)$
129	127 128	imbi12d	$⊢ x = ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \to (((x \subset A \land Tr x) \to x \in A) \leftrightarrow ((⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \subset A \land Tr ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\}) \to ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \in A))$
130	41 129	spcv	$⊢ \forall x ((x \subset A \land Tr x) \to x \in A) \to ((⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \subset A \land Tr ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\}) \to ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \in A)$
131	54 130	mpan2i	$⊢ \forall x ((x \subset A \land Tr x) \to x \in A) \to (⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \subset A \to ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \in A)$
132	124 131	mtod	$⊢ \forall x ((x \subset A \land Tr x) \to x \in A) \to \neg ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \subset A$
133		dfpss2	$⊢ ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \subset A \leftrightarrow (⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \subseteq A \land \neg ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} = A)$
134	133	biimpri	$⊢ (⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \subseteq A \land \neg ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} = A) \to ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \subset A$
135	40 134	mpan	$⊢ \neg ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} = A \to ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \subset A$
136	132 135	nsyl2	$⊢ \forall x ((x \subset A \land Tr x) \to x \in A) \to ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} = A$
137		eluni2	$⊢ z \in ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \leftrightarrow \exists x \in \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} z \in x$
138		psseq2	$⊢ t = z \to (y \subset t \leftrightarrow y \subset z)$
139	138	anbi1d	$⊢ t = z \to ((y \subset t \land Tr y) \leftrightarrow (y \subset z \land Tr y))$
140		elequ2	$⊢ t = z \to (y \in t \leftrightarrow y \in z)$
141	139 140	imbi12d	$⊢ t = z \to (((y \subset t \land Tr y) \to y \in t) \leftrightarrow ((y \subset z \land Tr y) \to y \in z))$
142	141	albidv	$⊢ t = z \to (\forall y ((y \subset t \land Tr y) \to y \in t) \leftrightarrow \forall y ((y \subset z \land Tr y) \to y \in z))$
143	142	cbvralvw	$⊢ \forall t \in x \forall y ((y \subset t \land Tr y) \to y \in t) \leftrightarrow \forall z \in x \forall y ((y \subset z \land Tr y) \to y \in z)$
144	14 143	syl6bb	$⊢ w = x \to (\forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t) \leftrightarrow \forall z \in x \forall y ((y \subset z \land Tr y) \to y \in z))$
145	12 13 144	3anbi123d	$⊢ w = x \to ((w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t)) \leftrightarrow (x \subseteq A \land Tr x \land \forall z \in x \forall y ((y \subset z \land Tr y) \to y \in z)))$
146	11 145	elab	$⊢ x \in \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \leftrightarrow (x \subseteq A \land Tr x \land \forall z \in x \forall y ((y \subset z \land Tr y) \to y \in z))$
147		rsp	$⊢ \forall z \in x \forall y ((y \subset z \land Tr y) \to y \in z) \to (z \in x \to \forall y ((y \subset z \land Tr y) \to y \in z))$
148	147	3ad2ant3	$⊢ (x \subseteq A \land Tr x \land \forall z \in x \forall y ((y \subset z \land Tr y) \to y \in z)) \to (z \in x \to \forall y ((y \subset z \land Tr y) \to y \in z))$
149	146 148	sylbi	$⊢ x \in \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \to (z \in x \to \forall y ((y \subset z \land Tr y) \to y \in z))$
150	149	rexlimiv	$⊢ \exists x \in \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} z \in x \to \forall y ((y \subset z \land Tr y) \to y \in z)$
151	137 150	sylbi	$⊢ z \in ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \to \forall y ((y \subset z \land Tr y) \to y \in z)$
152	151	rgen	$⊢ \forall z \in ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \forall y ((y \subset z \land Tr y) \to y \in z)$
153		raleq	$⊢ ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} = A \to (\forall z \in ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} \forall y ((y \subset z \land Tr y) \to y \in z) \leftrightarrow \forall z \in A \forall y ((y \subset z \land Tr y) \to y \in z))$
154	152 153	mpbii	$⊢ ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \forall y ((y \subset t \land Tr y) \to y \in t))\} = A \to \forall z \in A \forall y ((y \subset z \land Tr y) \to y \in z)$
155		psseq2	$⊢ z = B \to (y \subset z \leftrightarrow y \subset B)$
156	155	anbi1d	$⊢ z = B \to ((y \subset z \land Tr y) \leftrightarrow (y \subset B \land Tr y))$
157		eleq2	$⊢ z = B \to (y \in z \leftrightarrow y \in B)$
158	156 157	imbi12d	$⊢ z = B \to (((y \subset z \land Tr y) \to y \in z) \leftrightarrow ((y \subset B \land Tr y) \to y \in B))$
159	158	albidv	$⊢ z = B \to (\forall y ((y \subset z \land Tr y) \to y \in z) \leftrightarrow \forall y ((y \subset B \land Tr y) \to y \in B))$
160	159	rspccv	$⊢ \forall z \in A \forall y ((y \subset z \land Tr y) \to y \in z) \to (B \in A \to \forall y ((y \subset B \land Tr y) \to y \in B))$
161	136 154 160	3syl	$⊢ \forall x ((x \subset A \land Tr x) \to x \in A) \to (B \in A \to \forall y ((y \subset B \land Tr y) \to y \in B))$

Metamath Proof Explorer

Theorem dfon2lem7

Proof