Theorem dfon2lem3 30480

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

Assertion

Ref	Expression
dfon2lem3	|- ( A e. V -> ( A. x ( ( x C. A /\ Tr x ) -> x e. A ) -> ( Tr A /\ A. z e. A -. z e. z ) ) )

Distinct variable group:   x, A, z

Allowed substitution hints:   V( x, z)

Proof of Theorem dfon2lem3

Dummy variables w t are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		untelirr 30384	. . . . 5 |- ( A. z e. U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } -. z e. z -> -. U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } e. U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } )
2		eluni2 4216	. . . . . 6 |- ( z e. U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } <-> E. x e. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } z e. x )
3		vex 3060	. . . . . . . . . 10 |- x e. _V
4		sseq1 3465	. . . . . . . . . . 11 |- ( w = x -> ( w C_ A <-> x C_ A ) )
5		treq 4517	. . . . . . . . . . 11 |- ( w = x -> ( Tr w <-> Tr x ) )
6		raleq 2999	. . . . . . . . . . 11 |- ( w = x -> ( A. t e. w -. t e. t <-> A. t e. x -. t e. t ) )
7	4, 5, 6	3anbi123d 1348	. . . . . . . . . 10 |- ( w = x -> ( ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) <-> ( x C_ A /\ Tr x /\ A. t e. x -. t e. t ) ) )
8	3, 7	elab 3197	. . . . . . . . 9 |- ( x e. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } <-> ( x C_ A /\ Tr x /\ A. t e. x -. t e. t ) )
9		elequ1 1905	. . . . . . . . . . . . . 14 |- ( t = z -> ( t e. t <-> z e. t ) )
10		elequ2 1912	. . . . . . . . . . . . . 14 |- ( t = z -> ( z e. t <-> z e. z ) )
11	9, 10	bitrd 261	. . . . . . . . . . . . 13 |- ( t = z -> ( t e. t <-> z e. z ) )
12	11	notbid 300	. . . . . . . . . . . 12 |- ( t = z -> ( -. t e. t <-> -. z e. z ) )
13	12	cbvralv 3031	. . . . . . . . . . 11 |- ( A. t e. x -. t e. t <-> A. z e. x -. z e. z )
14	13	biimpi 199	. . . . . . . . . 10 |- ( A. t e. x -. t e. t -> A. z e. x -. z e. z )
15	14	3ad2ant3 1037	. . . . . . . . 9 |- ( ( x C_ A /\ Tr x /\ A. t e. x -. t e. t ) -> A. z e. x -. z e. z )
16	8, 15	sylbi 200	. . . . . . . 8 |- ( x e. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } -> A. z e. x -. z e. z )
17		rsp 2766	. . . . . . . 8 |- ( A. z e. x -. z e. z -> ( z e. x -> -. z e. z ) )
18	16, 17	syl 17	. . . . . . 7 |- ( x e. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } -> ( z e. x -> -. z e. z ) )
19	18	rexlimiv 2885	. . . . . 6 |- ( E. x e. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } z e. x -> -. z e. z )
20	2, 19	sylbi 200	. . . . 5 |- ( z e. U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } -> -. z e. z )
21	1, 20	mprg 2763	. . . 4 |- -. U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } e. U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) }
22		dfon2lem2 30479	. . . . 5 |- U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } C_ A
23		dfpss2 3530	. . . . . 6 |- ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } C. A <-> ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } C_ A /\ -. U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } = A ) )
24		dfon2lem1 30478	. . . . . . 7 |- Tr U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) }
25		ssexg 4563	. . . . . . . . . 10 |- ( ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } C_ A /\ A e. V ) -> U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } e. _V )
26	22, 25	mpan 681	. . . . . . . . 9 |- ( A e. V -> U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } e. _V )
27		psseq1 3532	. . . . . . . . . . . . 13 |- ( x = U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } -> ( x C. A <-> U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } C. A ) )
28		treq 4517	. . . . . . . . . . . . 13 |- ( x = U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } -> ( Tr x <-> Tr U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } ) )
29	27, 28	anbi12d 722	. . . . . . . . . . . 12 |- ( x = U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } -> ( ( x C. A /\ Tr x ) <-> ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } C. A /\ Tr U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } ) ) )
30		eleq1 2528	. . . . . . . . . . . 12 |- ( x = U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } -> ( x e. A <-> U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } e. A ) )
31	29, 30	imbi12d 326	. . . . . . . . . . 11 |- ( x = U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } -> ( ( ( x C. A /\ Tr x ) -> x e. A ) <-> ( ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } C. A /\ Tr U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } ) -> U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } e. A ) ) )
32	31	spcgv 3146	. . . . . . . . . 10 |- ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } e. _V -> ( A. x ( ( x C. A /\ Tr x ) -> x e. A ) -> ( ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } C. A /\ Tr U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } ) -> U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } e. A ) ) )
33	32	imp 435	. . . . . . . . 9 |- ( ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } e. _V /\ A. x ( ( x C. A /\ Tr x ) -> x e. A ) ) -> ( ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } C. A /\ Tr U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } ) -> U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } e. A ) )
34	26, 33	sylan 478	. . . . . . . 8 |- ( ( A e. V /\ A. x ( ( x C. A /\ Tr x ) -> x e. A ) ) -> ( ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } C. A /\ Tr U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } ) -> U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } e. A ) )
35		snssi 4129	. . . . . . . . . 10 |- ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } e. A -> { U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } } C_ A )
36		df-suc 5448	. . . . . . . . . . . . 13 |- suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } = ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } u. { U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } } )
37	36	sseq1i 3468	. . . . . . . . . . . 12 |- ( suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } C_ A <-> ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } u. { U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } } ) C_ A )
38		unss 3620	. . . . . . . . . . . 12 |- ( ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } C_ A /\ { U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } } C_ A ) <-> ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } u. { U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } } ) C_ A )
39	37, 38	bitr4i 260	. . . . . . . . . . 11 |- ( suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } C_ A <-> ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } C_ A /\ { U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } } C_ A ) )
40	39	biimpri 211	. . . . . . . . . 10 |- ( ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } C_ A /\ { U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } } C_ A ) -> suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } C_ A )
41	22, 35, 40	sylancr 674	. . . . . . . . 9 |- ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } e. A -> suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } C_ A )
42		suctr 5525	. . . . . . . . . . . . 13 |- ( Tr U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } -> Tr suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } )
43	24, 42	ax-mp 5	. . . . . . . . . . . 12 |- Tr suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) }
44		untuni 30385	. . . . . . . . . . . . . 14 |- ( A. z e. U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } -. z e. z <-> A. x e. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } A. z e. x -. z e. z )
45	44, 16	mprgbir 2764	. . . . . . . . . . . . 13 |- A. z e. U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } -. z e. z
46		nfv 1772	. . . . . . . . . . . . . . . . 17 |- F/ t w C_ A
47		nfv 1772	. . . . . . . . . . . . . . . . 17 |- F/ t Tr w
48		nfra1 2781	. . . . . . . . . . . . . . . . 17 |- F/ t A. t e. w -. t e. t
49	46, 47, 48	nf3an 2024	. . . . . . . . . . . . . . . 16 |- F/ t ( w C_ A /\ Tr w /\ A. t e. w -. t e. t )
50	49	nfab 2607	. . . . . . . . . . . . . . 15 |- F/_ t { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) }
51	50	nfuni 4218	. . . . . . . . . . . . . 14 |- F/_ t U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) }
52	51	untsucf 30386	. . . . . . . . . . . . 13 |- ( A. z e. U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } -. z e. z -> A. t e. suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } -. t e. t )
53	45, 52	ax-mp 5	. . . . . . . . . . . 12 |- A. t e. suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } -. t e. t
54		sucexg 6664	. . . . . . . . . . . . . 14 |- ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } e. A -> suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } e. _V )
55		sseq1 3465	. . . . . . . . . . . . . . . . 17 |- ( z = suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } -> ( z C_ A <-> suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } C_ A ) )
56		treq 4517	. . . . . . . . . . . . . . . . 17 |- ( z = suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } -> ( Tr z <-> Tr suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } ) )
57		nfcv 2603	. . . . . . . . . . . . . . . . . 18 |- F/_ t z
58	51	nfsuc 5513	. . . . . . . . . . . . . . . . . 18 |- F/_ t suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) }
59	57, 58	raleqf 2995	. . . . . . . . . . . . . . . . 17 |- ( z = suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } -> ( A. t e. z -. t e. t <-> A. t e. suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } -. t e. t ) )
60	55, 56, 59	3anbi123d 1348	. . . . . . . . . . . . . . . 16 |- ( z = suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } -> ( ( z C_ A /\ Tr z /\ A. t e. z -. t e. t ) <-> ( suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } C_ A /\ Tr suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } /\ A. t e. suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } -. t e. t ) ) )
61		sseq1 3465	. . . . . . . . . . . . . . . . . 18 |- ( w = z -> ( w C_ A <-> z C_ A ) )
62		treq 4517	. . . . . . . . . . . . . . . . . 18 |- ( w = z -> ( Tr w <-> Tr z ) )
63		raleq 2999	. . . . . . . . . . . . . . . . . 18 |- ( w = z -> ( A. t e. w -. t e. t <-> A. t e. z -. t e. t ) )
64	61, 62, 63	3anbi123d 1348	. . . . . . . . . . . . . . . . 17 |- ( w = z -> ( ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) <-> ( z C_ A /\ Tr z /\ A. t e. z -. t e. t ) ) )
65	64	cbvabv 2586	. . . . . . . . . . . . . . . 16 |- { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } = { z | ( z C_ A /\ Tr z /\ A. t e. z -. t e. t ) }
66	60, 65	elab2g 3199	. . . . . . . . . . . . . . 15 |- ( suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } e. _V -> ( suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } e. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } <-> ( suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } C_ A /\ Tr suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } /\ A. t e. suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } -. t e. t ) ) )
67	66	biimprd 231	. . . . . . . . . . . . . 14 |- ( suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } e. _V -> ( ( suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } C_ A /\ Tr suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } /\ A. t e. suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } -. t e. t ) -> suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } e. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } ) )
68	54, 67	syl 17	. . . . . . . . . . . . 13 |- ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } e. A -> ( ( suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } C_ A /\ Tr suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } /\ A. t e. suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } -. t e. t ) -> suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } e. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } ) )
69	68	com12 32	. . . . . . . . . . . 12 |- ( ( suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } C_ A /\ Tr suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } /\ A. t e. suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } -. t e. t ) -> ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } e. A -> suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } e. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } ) )
70	43, 53, 69	mp3an23 1365	. . . . . . . . . . 11 |- ( suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } C_ A -> ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } e. A -> suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } e. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } ) )
71	70	com12 32	. . . . . . . . . 10 |- ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } e. A -> ( suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } C_ A -> suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } e. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } ) )
72		elssuni 4241	. . . . . . . . . . 11 |- ( suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } e. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } -> suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } C_ U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } )
73		sucssel 5534	. . . . . . . . . . 11 |- ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } e. A -> ( suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } C_ U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } -> U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } e. U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } ) )
74	72, 73	syl5 33	. . . . . . . . . 10 |- ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } e. A -> ( suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } e. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } -> U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } e. U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } ) )
75	71, 74	syld 45	. . . . . . . . 9 |- ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } e. A -> ( suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } C_ A -> U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } e. U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } ) )
76	41, 75	mpd 15	. . . . . . . 8 |- ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } e. A -> U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } e. U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } )
77	34, 76	syl6 34	. . . . . . 7 |- ( ( A e. V /\ A. x ( ( x C. A /\ Tr x ) -> x e. A ) ) -> ( ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } C. A /\ Tr U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } ) -> U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } e. U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } ) )
78	24, 77	mpan2i 688	. . . . . 6 |- ( ( A e. V /\ A. x ( ( x C. A /\ Tr x ) -> x e. A ) ) -> ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } C. A -> U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } e. U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } ) )
79	23, 78	syl5bir 226	. . . . 5 |- ( ( A e. V /\ A. x ( ( x C. A /\ Tr x ) -> x e. A ) ) -> ( ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } C_ A /\ -. U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } = A ) -> U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } e. U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } ) )
80	22, 79	mpani 687	. . . 4 |- ( ( A e. V /\ A. x ( ( x C. A /\ Tr x ) -> x e. A ) ) -> ( -. U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } = A -> U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } e. U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } ) )
81	21, 80	mt3i 131	. . 3 |- ( ( A e. V /\ A. x ( ( x C. A /\ Tr x ) -> x e. A ) ) -> U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } = A )
82	24, 45	pm3.2i 461	. . . 4 |- ( Tr U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } /\ A. z e. U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } -. z e. z )
83		treq 4517	. . . . 5 |- ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } = A -> ( Tr U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } <-> Tr A ) )
84		raleq 2999	. . . . 5 |- ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } = A -> ( A. z e. U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } -. z e. z <-> A. z e. A -. z e. z ) )
85	83, 84	anbi12d 722	. . . 4 |- ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } = A -> ( ( Tr U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } /\ A. z e. U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } -. z e. z ) <-> ( Tr A /\ A. z e. A -. z e. z ) ) )
86	82, 85	mpbii 216	. . 3 |- ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } = A -> ( Tr A /\ A. z e. A -. z e. z ) )
87	81, 86	syl 17	. 2 |- ( ( A e. V /\ A. x ( ( x C. A /\ Tr x ) -> x e. A ) ) -> ( Tr A /\ A. z e. A -. z e. z ) )
88	87	ex 440	1 |- ( A e. V -> ( A. x ( ( x C. A /\ Tr x ) -> x e. A ) -> ( Tr A /\ A. z e. A -. z e. z ) ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 375   /\ w3a 991   A.wal 1453   = wceq 1455   e. wcel 1898   {cab 2448   A.wral 2749   E.wrex 2750   _Vcvv 3057   u. cun 3414   C_ wss 3416   C. wpss 3417   {csn 3980   U.cuni 4212   Tr wtr 4511   suc csuc 5444

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4539  ax-nul 4548  ax-pr 4653  ax-un 6610

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-ral 2754  df-rex 2755  df-v 3059  df-sbc 3280  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-pss 3432  df-nul 3744  df-pw 3965  df-sn 3981  df-pr 3983  df-uni 4213  df-iun 4294  df-tr 4512  df-suc 5448

This theorem is referenced by:  dfon2lem4  30481  dfon2lem5  30482  dfon2lem7  30484  dfon2lem8  30485  dfon2lem9  30486  dfon2  30487