dfon2lem3

Description: Lemma for dfon2 . All sets satisfying the new definition are transitive and untangled. (Contributed by Scott Fenton, 25-Feb-2011)

		Ref	Expression
	Assertion	dfon2lem3	$⊢ A \in V \to (\forall x ((x \subset A \land Tr x) \to x \in A) \to (Tr A \land \forall z \in A \neg z \in z))$

Proof

Step	Hyp	Ref	Expression
1		untelirr	$⊢ \forall z \in ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \neg z \in z \to \neg ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \in ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\}$
2		eluni2	$⊢ z \in ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \leftrightarrow \exists x \in \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} z \in x$
3		vex	$⊢ x \in V$
4		sseq1	$⊢ w = x \to (w \subseteq A \leftrightarrow x \subseteq A)$
5		treq	$⊢ w = x \to (Tr w \leftrightarrow Tr x)$
6		raleq	$⊢ w = x \to (\forall t \in w \neg t \in t \leftrightarrow \forall t \in x \neg t \in t)$
7	4 5 6	3anbi123d	$⊢ w = x \to ((w \subseteq A \land Tr w \land \forall t \in w \neg t \in t) \leftrightarrow (x \subseteq A \land Tr x \land \forall t \in x \neg t \in t))$
8	3 7	elab	$⊢ x \in \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \leftrightarrow (x \subseteq A \land Tr x \land \forall t \in x \neg t \in t)$
9		elequ1	$⊢ t = z \to (t \in t \leftrightarrow z \in t)$
10		elequ2	$⊢ t = z \to (z \in t \leftrightarrow z \in z)$
11	9 10	bitrd	$⊢ t = z \to (t \in t \leftrightarrow z \in z)$
12	11	notbid	$⊢ t = z \to (\neg t \in t \leftrightarrow \neg z \in z)$
13	12	cbvralvw	$⊢ \forall t \in x \neg t \in t \leftrightarrow \forall z \in x \neg z \in z$
14	13	biimpi	$⊢ \forall t \in x \neg t \in t \to \forall z \in x \neg z \in z$
15	14	3ad2ant3	$⊢ (x \subseteq A \land Tr x \land \forall t \in x \neg t \in t) \to \forall z \in x \neg z \in z$
16	8 15	sylbi	$⊢ x \in \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \to \forall z \in x \neg z \in z$
17		rsp	$⊢ \forall z \in x \neg z \in z \to (z \in x \to \neg z \in z)$
18	16 17	syl	$⊢ x \in \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \to (z \in x \to \neg z \in z)$
19	18	rexlimiv	$⊢ \exists x \in \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} z \in x \to \neg z \in z$
20	2 19	sylbi	$⊢ z \in ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \to \neg z \in z$
21	1 20	mprg	$⊢ \neg ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \in ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\}$
22		dfon2lem2	$⊢ ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \subseteq A$
23		dfpss2	$⊢ ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \subset A \leftrightarrow (⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \subseteq A \land \neg ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} = A)$
24		dfon2lem1	$⊢ Tr ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\}$
25		ssexg	$⊢ (⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \subseteq A \land A \in V) \to ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \in V$
26	22 25	mpan	$⊢ A \in V \to ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \in V$
27		psseq1	$⊢ x = ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \to (x \subset A \leftrightarrow ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \subset A)$
28		treq	$⊢ x = ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \to (Tr x \leftrightarrow Tr ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\})$
29	27 28	anbi12d	$⊢ x = ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \to ((x \subset A \land Tr x) \leftrightarrow (⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \subset A \land Tr ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\}))$
30		eleq1	$⊢ x = ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \to (x \in A \leftrightarrow ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \in A)$
31	29 30	imbi12d	$⊢ x = ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \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 \neg t \in t)\} \subset A \land Tr ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\}) \to ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \in A))$
32	31	spcgv	$⊢ ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \in V \to (\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 \neg t \in t)\} \subset A \land Tr ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\}) \to ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \in A))$
33	32	imp	$⊢ (⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \in V \land \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 \neg t \in t)\} \subset A \land Tr ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\}) \to ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \in A)$
34	26 33	sylan	$⊢ (A \in V \land \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 \neg t \in t)\} \subset A \land Tr ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\}) \to ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \in A)$
35		snssi	$⊢ ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \in A \to \{⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\}\} \subseteq A$
36		unss	$⊢ (⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \subseteq A \land \{⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\}\} \subseteq A) \leftrightarrow ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \cup \{⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\}\} \subseteq A$
37		df-suc	$⊢ suc ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} = ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \cup \{⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\}\}$
38	37	sseq1i	$⊢ suc ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \subseteq A \leftrightarrow ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \cup \{⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\}\} \subseteq A$
39	36 38	sylbb2	$⊢ (⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \subseteq A \land \{⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\}\} \subseteq A) \to suc ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \subseteq A$
40	22 35 39	sylancr	$⊢ ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \in A \to suc ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \subseteq A$
41		suctr	$⊢ Tr ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \to Tr suc ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\}$
42	24 41	ax-mp	$⊢ Tr suc ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\}$
43		untuni	$⊢ \forall z \in ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \neg z \in z \leftrightarrow \forall x \in \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \forall z \in x \neg z \in z$
44	43 16	mprgbir	$⊢ \forall z \in ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \neg z \in z$
45		nfv	$⊢ Ⅎ t w \subseteq A$
46		nfv	$⊢ Ⅎ t Tr w$
47		nfra1	$⊢ Ⅎ t \forall t \in w \neg t \in t$
48	45 46 47	nf3an	$⊢ Ⅎ t (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)$
49	48	nfab	$⊢ \underline{Ⅎ} t \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\}$
50	49	nfuni	$⊢ \underline{Ⅎ} t ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\}$
51	50	untsucf	$⊢ \forall z \in ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \neg z \in z \to \forall t \in suc ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \neg t \in t$
52	44 51	ax-mp	$⊢ \forall t \in suc ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \neg t \in t$
53		sseq1	$⊢ z = suc ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \to (z \subseteq A \leftrightarrow suc ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \subseteq A)$
54		treq	$⊢ z = suc ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \to (Tr z \leftrightarrow Tr suc ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\})$
55		nfcv	$⊢ \underline{Ⅎ} t z$
56	50	nfsuc	$⊢ \underline{Ⅎ} t suc ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\}$
57	55 56	raleqf	$⊢ z = suc ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \to (\forall t \in z \neg t \in t \leftrightarrow \forall t \in suc ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \neg t \in t)$
58	53 54 57	3anbi123d	$⊢ z = suc ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \to ((z \subseteq A \land Tr z \land \forall t \in z \neg t \in t) \leftrightarrow (suc ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \subseteq A \land Tr suc ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \land \forall t \in suc ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \neg t \in t))$
59		sseq1	$⊢ w = z \to (w \subseteq A \leftrightarrow z \subseteq A)$
60		treq	$⊢ w = z \to (Tr w \leftrightarrow Tr z)$
61		raleq	$⊢ w = z \to (\forall t \in w \neg t \in t \leftrightarrow \forall t \in z \neg t \in t)$
62	59 60 61	3anbi123d	$⊢ w = z \to ((w \subseteq A \land Tr w \land \forall t \in w \neg t \in t) \leftrightarrow (z \subseteq A \land Tr z \land \forall t \in z \neg t \in t))$
63	62	cbvabv	$⊢ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} = \{z \| (z \subseteq A \land Tr z \land \forall t \in z \neg t \in t)\}$
64	58 63	elab2g	$⊢ suc ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \in V \to (suc ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \in \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \leftrightarrow (suc ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \subseteq A \land Tr suc ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \land \forall t \in suc ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \neg t \in t))$
65	64	biimprd	$⊢ suc ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \in V \to ((suc ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \subseteq A \land Tr suc ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \land \forall t \in suc ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \neg t \in t) \to suc ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \in \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\})$
66		sucexg	$⊢ ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \in A \to suc ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \in V$
67	65 66	syl11	$⊢ (suc ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \subseteq A \land Tr suc ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \land \forall t \in suc ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \neg t \in t) \to (⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \in A \to suc ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \in \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\})$
68	42 52 67	mp3an23	$⊢ suc ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \subseteq A \to (⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \in A \to suc ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \in \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\})$
69	68	com12	$⊢ ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \in A \to (suc ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \subseteq A \to suc ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \in \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\})$
70		elssuni	$⊢ suc ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \in \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \to suc ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \subseteq ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\}$
71		sucssel	$⊢ ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \in A \to (suc ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \subseteq ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \to ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \in ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\})$
72	70 71	syl5	$⊢ ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \in A \to (suc ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \in \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \to ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \in ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\})$
73	69 72	syld	$⊢ ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \in A \to (suc ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \subseteq A \to ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \in ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\})$
74	40 73	mpd	$⊢ ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \in A \to ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \in ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\}$
75	34 74	syl6	$⊢ (A \in V \land \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 \neg t \in t)\} \subset A \land Tr ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\}) \to ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \in ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\})$
76	24 75	mpan2i	$⊢ (A \in V \land \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 \neg t \in t)\} \subset A \to ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \in ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\})$
77	23 76	syl5bir	$⊢ (A \in V \land \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 \neg t \in t)\} \subseteq A \land \neg ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} = A) \to ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \in ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\})$
78	22 77	mpani	$⊢ (A \in V \land \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 \neg t \in t)\} = A \to ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \in ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\})$
79	21 78	mt3i	$⊢ (A \in V \land \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 \neg t \in t)\} = A$
80	24 44	pm3.2i	$⊢ (Tr ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \land \forall z \in ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \neg z \in z)$
81		treq	$⊢ ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} = A \to (Tr ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \leftrightarrow Tr A)$
82		raleq	$⊢ ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} = A \to (\forall z \in ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \neg z \in z \leftrightarrow \forall z \in A \neg z \in z)$
83	81 82	anbi12d	$⊢ ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} = A \to ((Tr ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \land \forall z \in ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} \neg z \in z) \leftrightarrow (Tr A \land \forall z \in A \neg z \in z))$
84	80 83	mpbii	$⊢ ⋃ \{w \| (w \subseteq A \land Tr w \land \forall t \in w \neg t \in t)\} = A \to (Tr A \land \forall z \in A \neg z \in z)$
85	79 84	syl	$⊢ (A \in V \land \forall x ((x \subset A \land Tr x) \to x \in A)) \to (Tr A \land \forall z \in A \neg z \in z)$
86	85	ex	$⊢ A \in V \to (\forall x ((x \subset A \land Tr x) \to x \in A) \to (Tr A \land \forall z \in A \neg z \in z))$

Metamath Proof Explorer

Theorem dfon2lem3

Proof