Theorem dfon2lem3 28810

Description: Lemma for dfon2 28817. 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 28571	. . . . 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 4249	. . . . . 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 3116	. . . . . . . . . 10 |- x e. _V
4		sseq1 3525	. . . . . . . . . . 11 |- ( w = x -> ( w C_ A <-> x C_ A ) )
5		treq 4546	. . . . . . . . . . 11 |- ( w = x -> ( Tr w <-> Tr x ) )
6		raleq 3058	. . . . . . . . . . 11 |- ( w = x -> ( A. t e. w -. t e. t <-> A. t e. x -. t e. t ) )
7	4, 5, 6	3anbi123d 1299	. . . . . . . . . 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 3250	. . . . . . . . 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 1770	. . . . . . . . . . . . . 14 |- ( t = z -> ( t e. t <-> z e. t ) )
10		elequ2 1772	. . . . . . . . . . . . . 14 |- ( t = z -> ( z e. t <-> z e. z ) )
11	9, 10	bitrd 253	. . . . . . . . . . . . 13 |- ( t = z -> ( t e. t <-> z e. z ) )
12	11	notbid 294	. . . . . . . . . . . 12 |- ( t = z -> ( -. t e. t <-> -. z e. z ) )
13	12	cbvralv 3088	. . . . . . . . . . 11 |- ( A. t e. x -. t e. t <-> A. z e. x -. z e. z )
14	13	biimpi 194	. . . . . . . . . 10 |- ( A. t e. x -. t e. t -> A. z e. x -. z e. z )
15	14	3ad2ant3 1019	. . . . . . . . 9 |- ( ( x C_ A /\ Tr x /\ A. t e. x -. t e. t ) -> A. z e. x -. z e. z )
16	8, 15	sylbi 195	. . . . . . . 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 2830	. . . . . . . 8 |- ( A. z e. x -. z e. z -> ( z e. x -> -. z e. z ) )
18	16, 17	syl 16	. . . . . . 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 2949	. . . . . 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 195	. . . . 5 |- ( z e. U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } -> -. z e. z )
21	1, 20	mprg 2827	. . . 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 28809	. . . . 5 |- U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } C_ A
23		dfpss2 3589	. . . . . 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 28808	. . . . . . 7 |- Tr U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) }
25		ssexg 4593	. . . . . . . . . 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 670	. . . . . . . . 9 |- ( A e. V -> U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } e. _V )
27		psseq1 3591	. . . . . . . . . . . . 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 4546	. . . . . . . . . . . . 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 710	. . . . . . . . . . . 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 2539	. . . . . . . . . . . 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 320	. . . . . . . . . . 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 3198	. . . . . . . . . 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 429	. . . . . . . . 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 471	. . . . . . . 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 4171	. . . . . . . . . 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 4884	. . . . . . . . . . . . 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 3528	. . . . . . . . . . . 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 3678	. . . . . . . . . . . 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 252	. . . . . . . . . . 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 206	. . . . . . . . . 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 663	. . . . . . . . 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 4961	. . . . . . . . . . . . 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 28572	. . . . . . . . . . . . . 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 2828	. . . . . . . . . . . . 13 |- A. z e. U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } -. z e. z
46		nfv 1683	. . . . . . . . . . . . . . . . 17 |- F/ t w C_ A
47		nfv 1683	. . . . . . . . . . . . . . . . 17 |- F/ t Tr w
48		nfra1 2845	. . . . . . . . . . . . . . . . 17 |- F/ t A. t e. w -. t e. t
49	46, 47, 48	nf3an 1877	. . . . . . . . . . . . . . . 16 |- F/ t ( w C_ A /\ Tr w /\ A. t e. w -. t e. t )
50	49	nfab 2633	. . . . . . . . . . . . . . 15 |- F/_ t { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) }
51	50	nfuni 4251	. . . . . . . . . . . . . 14 |- F/_ t U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) }
52	51	untsucf 28573	. . . . . . . . . . . . 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 6624	. . . . . . . . . . . . . 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 3525	. . . . . . . . . . . . . . . . 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 4546	. . . . . . . . . . . . . . . . 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 2629	. . . . . . . . . . . . . . . . . 18 |- F/_ t z
58	51	nfsuc 4949	. . . . . . . . . . . . . . . . . 18 |- F/_ t suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) }
59	57, 58	raleqf 3054	. . . . . . . . . . . . . . . . 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 1299	. . . . . . . . . . . . . . . 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 3525	. . . . . . . . . . . . . . . . . 18 |- ( w = z -> ( w C_ A <-> z C_ A ) )
62		treq 4546	. . . . . . . . . . . . . . . . . 18 |- ( w = z -> ( Tr w <-> Tr z ) )
63		raleq 3058	. . . . . . . . . . . . . . . . . 18 |- ( w = z -> ( A. t e. w -. t e. t <-> A. t e. z -. t e. t ) )
64	61, 62, 63	3anbi123d 1299	. . . . . . . . . . . . . . . . 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 2610	. . . . . . . . . . . . . . . 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 3252	. . . . . . . . . . . . . . 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 223	. . . . . . . . . . . . . 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 16	. . . . . . . . . . . . 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 31	. . . . . . . . . . . 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 1316	. . . . . . . . . . 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 31	. . . . . . . . . 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 4275	. . . . . . . . . . 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 4970	. . . . . . . . . . 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 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 ) } 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 44	. . . . . . . . 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 33	. . . . . . 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 677	. . . . . 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 218	. . . . 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 676	. . . 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 126	. . 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 455	. . . 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 4546	. . . . 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 3058	. . . . 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 710	. . . 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 211	. . 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 16	. 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 434	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 369   /\ w3a 973   A.wal 1377   = wceq 1379   e. wcel 1767   {cab 2452   A.wral 2814   E.wrex 2815   _Vcvv 3113   u. cun 3474   C_ wss 3476   C. wpss 3477   {csn 4027   U.cuni 4245   Tr wtr 4540   suc csuc 4880

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pr 4686  ax-un 6575

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-v 3115  df-sbc 3332  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-pss 3492  df-nul 3786  df-pw 4012  df-sn 4028  df-pr 4030  df-uni 4246  df-iun 4327  df-tr 4541  df-suc 4884

This theorem is referenced by:  dfon2lem4  28811  dfon2lem5  28812  dfon2lem7  28814  dfon2lem8  28815  dfon2lem9  28816  dfon2  28817