Theorem dfon2lem3 30004

Description: Lemma for dfon2 30011. 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 29909	. . . . 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 4195	. . . . . 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 3062	. . . . . . . . . 10 |- x e. _V
4		sseq1 3463	. . . . . . . . . . 11 |- ( w = x -> ( w C_ A <-> x C_ A ) )
5		treq 4495	. . . . . . . . . . 11 |- ( w = x -> ( Tr w <-> Tr x ) )
6		raleq 3004	. . . . . . . . . . 11 |- ( w = x -> ( A. t e. w -. t e. t <-> A. t e. x -. t e. t ) )
7	4, 5, 6	3anbi123d 1301	. . . . . . . . . 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 3196	. . . . . . . . 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 1845	. . . . . . . . . . . . . 14 |- ( t = z -> ( t e. t <-> z e. t ) )
10		elequ2 1847	. . . . . . . . . . . . . 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 292	. . . . . . . . . . . 12 |- ( t = z -> ( -. t e. t <-> -. z e. z ) )
13	12	cbvralv 3034	. . . . . . . . . . 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 1020	. . . . . . . . 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 2770	. . . . . . . 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 2890	. . . . . 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 2767	. . . 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 30003	. . . . 5 |- U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } C_ A
23		dfpss2 3528	. . . . . 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 30002	. . . . . . 7 |- Tr U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) }
25		ssexg 4540	. . . . . . . . . 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 668	. . . . . . . . 9 |- ( A e. V -> U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } e. _V )
27		psseq1 3530	. . . . . . . . . . . . 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 4495	. . . . . . . . . . . . 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 709	. . . . . . . . . . . 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 2474	. . . . . . . . . . . 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 318	. . . . . . . . . . 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 3144	. . . . . . . . . 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 427	. . . . . . . . 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 469	. . . . . . . 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 4116	. . . . . . . . . 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 5416	. . . . . . . . . . . . 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 3466	. . . . . . . . . . . 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 3617	. . . . . . . . . . . 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 661	. . . . . . . . 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 5493	. . . . . . . . . . . . 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 29910	. . . . . . . . . . . . . 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 2768	. . . . . . . . . . . . 13 |- A. z e. U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } -. z e. z
46		nfv 1728	. . . . . . . . . . . . . . . . 17 |- F/ t w C_ A
47		nfv 1728	. . . . . . . . . . . . . . . . 17 |- F/ t Tr w
48		nfra1 2785	. . . . . . . . . . . . . . . . 17 |- F/ t A. t e. w -. t e. t
49	46, 47, 48	nf3an 1958	. . . . . . . . . . . . . . . 16 |- F/ t ( w C_ A /\ Tr w /\ A. t e. w -. t e. t )
50	49	nfab 2568	. . . . . . . . . . . . . . 15 |- F/_ t { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) }
51	50	nfuni 4197	. . . . . . . . . . . . . 14 |- F/_ t U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) }
52	51	untsucf 29911	. . . . . . . . . . . . 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 6628	. . . . . . . . . . . . . 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 3463	. . . . . . . . . . . . . . . . 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 4495	. . . . . . . . . . . . . . . . 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 2564	. . . . . . . . . . . . . . . . . 18 |- F/_ t z
58	51	nfsuc 5481	. . . . . . . . . . . . . . . . . 18 |- F/_ t suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) }
59	57, 58	raleqf 3000	. . . . . . . . . . . . . . . . 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 1301	. . . . . . . . . . . . . . . 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 3463	. . . . . . . . . . . . . . . . . 18 |- ( w = z -> ( w C_ A <-> z C_ A ) )
62		treq 4495	. . . . . . . . . . . . . . . . . 18 |- ( w = z -> ( Tr w <-> Tr z ) )
63		raleq 3004	. . . . . . . . . . . . . . . . . 18 |- ( w = z -> ( A. t e. w -. t e. t <-> A. t e. z -. t e. t ) )
64	61, 62, 63	3anbi123d 1301	. . . . . . . . . . . . . . . . 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 2545	. . . . . . . . . . . . . . . 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 3198	. . . . . . . . . . . . . . 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 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 29	. . . . . . . . . . . 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 1318	. . . . . . . . . . 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 29	. . . . . . . . . 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 4220	. . . . . . . . . . 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 5502	. . . . . . . . . . 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 30	. . . . . . . . . 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 42	. . . . . . . . 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 31	. . . . . . 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 675	. . . . . 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 674	. . . 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 453	. . . 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 4495	. . . . 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 3004	. . . . 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 709	. . . 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 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 432	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 367   /\ w3a 974   A.wal 1403   = wceq 1405   e. wcel 1842   {cab 2387   A.wral 2754   E.wrex 2755   _Vcvv 3059   u. cun 3412   C_ wss 3414   C. wpss 3415   {csn 3972   U.cuni 4191   Tr wtr 4489   suc csuc 5412

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-8 1844  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-sep 4517  ax-nul 4525  ax-pr 4630  ax-un 6574

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-ral 2759  df-rex 2760  df-v 3061  df-sbc 3278  df-dif 3417  df-un 3419  df-in 3421  df-ss 3428  df-pss 3430  df-nul 3739  df-pw 3957  df-sn 3973  df-pr 3975  df-uni 4192  df-iun 4273  df-tr 4490  df-suc 5416

This theorem is referenced by:  dfon2lem4  30005  dfon2lem5  30006  dfon2lem7  30008  dfon2lem8  30009  dfon2lem9  30010  dfon2  30011