Theorem dfon2lem3 27598

Description: Lemma for dfon2 27605. 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 27359	. . . . 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 4095	. . . . . 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 2975	. . . . . . . . . 10 |- x e. _V
4		sseq1 3377	. . . . . . . . . . 11 |- ( w = x -> ( w C_ A <-> x C_ A ) )
5		treq 4391	. . . . . . . . . . 11 |- ( w = x -> ( Tr w <-> Tr x ) )
6		raleq 2917	. . . . . . . . . . 11 |- ( w = x -> ( A. t e. w -. t e. t <-> A. t e. x -. t e. t ) )
7	4, 5, 6	3anbi123d 1289	. . . . . . . . . 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 3106	. . . . . . . . 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 1759	. . . . . . . . . . . . . 14 |- ( t = z -> ( t e. t <-> z e. t ) )
10		elequ2 1761	. . . . . . . . . . . . . 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 2947	. . . . . . . . . . 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 1011	. . . . . . . . 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 2776	. . . . . . . 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 2835	. . . . . 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 2785	. . . 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 27597	. . . . 5 |- U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } C_ A
23		dfpss2 3441	. . . . . 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 27596	. . . . . . 7 |- Tr U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) }
25		ssexg 4438	. . . . . . . . . 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 3443	. . . . . . . . . . . . 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 4391	. . . . . . . . . . . . 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 2503	. . . . . . . . . . . 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 3057	. . . . . . . . . 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 4017	. . . . . . . . . 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 4725	. . . . . . . . . . . . 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 3380	. . . . . . . . . . . 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 3530	. . . . . . . . . . . 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 4802	. . . . . . . . . . . . 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 27360	. . . . . . . . . . . . . 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 2786	. . . . . . . . . . . . 13 |- A. z e. U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } -. z e. z
46		nfv 1673	. . . . . . . . . . . . . . . . 17 |- F/ t w C_ A
47		nfv 1673	. . . . . . . . . . . . . . . . 17 |- F/ t Tr w
48		nfra1 2766	. . . . . . . . . . . . . . . . 17 |- F/ t A. t e. w -. t e. t
49	46, 47, 48	nf3an 1863	. . . . . . . . . . . . . . . 16 |- F/ t ( w C_ A /\ Tr w /\ A. t e. w -. t e. t )
50	49	nfab 2583	. . . . . . . . . . . . . . 15 |- F/_ t { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) }
51	50	nfuni 4097	. . . . . . . . . . . . . 14 |- F/_ t U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) }
52	51	untsucf 27361	. . . . . . . . . . . . 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 6421	. . . . . . . . . . . . . 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 3377	. . . . . . . . . . . . . . . . 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 4391	. . . . . . . . . . . . . . . . 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 2579	. . . . . . . . . . . . . . . . . 18 |- F/_ t z
58	51	nfsuc 4790	. . . . . . . . . . . . . . . . . 18 |- F/_ t suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) }
59	57, 58	raleqf 2913	. . . . . . . . . . . . . . . . 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 1289	. . . . . . . . . . . . . . . 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 3377	. . . . . . . . . . . . . . . . . 18 |- ( w = z -> ( w C_ A <-> z C_ A ) )
62		treq 4391	. . . . . . . . . . . . . . . . . 18 |- ( w = z -> ( Tr w <-> Tr z ) )
63		raleq 2917	. . . . . . . . . . . . . . . . . 18 |- ( w = z -> ( A. t e. w -. t e. t <-> A. t e. z -. t e. t ) )
64	61, 62, 63	3anbi123d 1289	. . . . . . . . . . . . . . . . 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 2562	. . . . . . . . . . . . . . . 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 3108	. . . . . . . . . . . . . . 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 1306	. . . . . . . . . . 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 4121	. . . . . . . . . . 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 4811	. . . . . . . . . . 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 4391	. . . . 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 2917	. . . . 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 965   A.wal 1367   = wceq 1369   e. wcel 1756   {cab 2429   A.wral 2715   E.wrex 2716   _Vcvv 2972   u. cun 3326   C_ wss 3328   C. wpss 3329   {csn 3877   U.cuni 4091   Tr wtr 4385   suc csuc 4721

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4413  ax-nul 4421  ax-pr 4531  ax-un 6372

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-ral 2720  df-rex 2721  df-v 2974  df-sbc 3187  df-dif 3331  df-un 3333  df-in 3335  df-ss 3342  df-pss 3344  df-nul 3638  df-pw 3862  df-sn 3878  df-pr 3880  df-uni 4092  df-iun 4173  df-tr 4386  df-suc 4725

This theorem is referenced by:  dfon2lem4  27599  dfon2lem5  27600  dfon2lem7  27602  dfon2lem8  27603  dfon2lem9  27604  dfon2  27605