Theorem dfon2lem8 29462

Description: Lemma for dfon2 29464. The intersection of a nonempty class A of new ordinals is itself a new ordinal and is contained within A (Contributed by Scott Fenton, 26-Feb-2011.)

Assertion

Ref	Expression
dfon2lem8	|- ( ( A =/= (/) /\ A. x e. A A. y ( ( y C. x /\ Tr y ) -> y e. x ) ) -> ( A. z ( ( z C. |^| A /\ Tr z ) -> z e. |^| A ) /\ |^| A e. A ) )

Distinct variable group:   x, A, y, z

Proof of Theorem dfon2lem8

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

Step	Hyp	Ref	Expression
1		vex 3109	. . . . . . 7 |- x e. _V
2		dfon2lem3 29457	. . . . . . 7 |- ( x e. _V -> ( A. y ( ( y C. x /\ Tr y ) -> y e. x ) -> ( Tr x /\ A. z e. x -. z e. z ) ) )
3	1, 2	ax-mp 5	. . . . . 6 |- ( A. y ( ( y C. x /\ Tr y ) -> y e. x ) -> ( Tr x /\ A. z e. x -. z e. z ) )
4	3	simpld 457	. . . . 5 |- ( A. y ( ( y C. x /\ Tr y ) -> y e. x ) -> Tr x )
5	4	ralimi 2847	. . . 4 |- ( A. x e. A A. y ( ( y C. x /\ Tr y ) -> y e. x ) -> A. x e. A Tr x )
6		trint 4547	. . . 4 |- ( A. x e. A Tr x -> Tr |^| A )
7	5, 6	syl 16	. . 3 |- ( A. x e. A A. y ( ( y C. x /\ Tr y ) -> y e. x ) -> Tr |^| A )
8	7	adantl 464	. 2 |- ( ( A =/= (/) /\ A. x e. A A. y ( ( y C. x /\ Tr y ) -> y e. x ) ) -> Tr |^| A )
9	1	dfon2lem7 29461	. . . . . . 7 |- ( A. y ( ( y C. x /\ Tr y ) -> y e. x ) -> ( w e. x -> A. t ( ( t C. w /\ Tr t ) -> t e. w ) ) )
10	9	alrimiv 1724	. . . . . 6 |- ( A. y ( ( y C. x /\ Tr y ) -> y e. x ) -> A. w ( w e. x -> A. t ( ( t C. w /\ Tr t ) -> t e. w ) ) )
11	10	ralimi 2847	. . . . 5 |- ( A. x e. A A. y ( ( y C. x /\ Tr y ) -> y e. x ) -> A. x e. A A. w ( w e. x -> A. t ( ( t C. w /\ Tr t ) -> t e. w ) ) )
12		df-ral 2809	. . . . . . 7 |- ( A. x e. A A. w ( w e. x -> A. t ( ( t C. w /\ Tr t ) -> t e. w ) ) <-> A. x ( x e. A -> A. w ( w e. x -> A. t ( ( t C. w /\ Tr t ) -> t e. w ) ) ) )
13		19.21v 1734	. . . . . . . 8 |- ( A. w ( x e. A -> ( w e. x -> A. t ( ( t C. w /\ Tr t ) -> t e. w ) ) ) <-> ( x e. A -> A. w ( w e. x -> A. t ( ( t C. w /\ Tr t ) -> t e. w ) ) ) )
14	13	albii 1645	. . . . . . 7 |- ( A. x A. w ( x e. A -> ( w e. x -> A. t ( ( t C. w /\ Tr t ) -> t e. w ) ) ) <-> A. x ( x e. A -> A. w ( w e. x -> A. t ( ( t C. w /\ Tr t ) -> t e. w ) ) ) )
15	12, 14	bitr4i 252	. . . . . 6 |- ( A. x e. A A. w ( w e. x -> A. t ( ( t C. w /\ Tr t ) -> t e. w ) ) <-> A. x A. w ( x e. A -> ( w e. x -> A. t ( ( t C. w /\ Tr t ) -> t e. w ) ) ) )
16		impexp 444	. . . . . . . 8 |- ( ( ( x e. A /\ w e. x ) -> A. t ( ( t C. w /\ Tr t ) -> t e. w ) ) <-> ( x e. A -> ( w e. x -> A. t ( ( t C. w /\ Tr t ) -> t e. w ) ) ) )
17	16	2albii 1646	. . . . . . 7 |- ( A. x A. w ( ( x e. A /\ w e. x ) -> A. t ( ( t C. w /\ Tr t ) -> t e. w ) ) <-> A. x A. w ( x e. A -> ( w e. x -> A. t ( ( t C. w /\ Tr t ) -> t e. w ) ) ) )
18		eluni2 4239	. . . . . . . . . . 11 |- ( w e. U. A <-> E. x e. A w e. x )
19	18	biimpi 194	. . . . . . . . . 10 |- ( w e. U. A -> E. x e. A w e. x )
20	19	imim1i 58	. . . . . . . . 9 |- ( ( E. x e. A w e. x -> A. t ( ( t C. w /\ Tr t ) -> t e. w ) ) -> ( w e. U. A -> A. t ( ( t C. w /\ Tr t ) -> t e. w ) ) )
21	20	alimi 1638	. . . . . . . 8 |- ( A. w ( E. x e. A w e. x -> A. t ( ( t C. w /\ Tr t ) -> t e. w ) ) -> A. w ( w e. U. A -> A. t ( ( t C. w /\ Tr t ) -> t e. w ) ) )
22		alcom 1850	. . . . . . . . 9 |- ( A. x A. w ( ( x e. A /\ w e. x ) -> A. t ( ( t C. w /\ Tr t ) -> t e. w ) ) <-> A. w A. x ( ( x e. A /\ w e. x ) -> A. t ( ( t C. w /\ Tr t ) -> t e. w ) ) )
23		19.23v 1765	. . . . . . . . . . 11 |- ( A. x ( ( x e. A /\ w e. x ) -> A. t ( ( t C. w /\ Tr t ) -> t e. w ) ) <-> ( E. x ( x e. A /\ w e. x ) -> A. t ( ( t C. w /\ Tr t ) -> t e. w ) ) )
24		df-rex 2810	. . . . . . . . . . . 12 |- ( E. x e. A w e. x <-> E. x ( x e. A /\ w e. x ) )
25	24	imbi1i 323	. . . . . . . . . . 11 |- ( ( E. x e. A w e. x -> A. t ( ( t C. w /\ Tr t ) -> t e. w ) ) <-> ( E. x ( x e. A /\ w e. x ) -> A. t ( ( t C. w /\ Tr t ) -> t e. w ) ) )
26	23, 25	bitr4i 252	. . . . . . . . . 10 |- ( A. x ( ( x e. A /\ w e. x ) -> A. t ( ( t C. w /\ Tr t ) -> t e. w ) ) <-> ( E. x e. A w e. x -> A. t ( ( t C. w /\ Tr t ) -> t e. w ) ) )
27	26	albii 1645	. . . . . . . . 9 |- ( A. w A. x ( ( x e. A /\ w e. x ) -> A. t ( ( t C. w /\ Tr t ) -> t e. w ) ) <-> A. w ( E. x e. A w e. x -> A. t ( ( t C. w /\ Tr t ) -> t e. w ) ) )
28	22, 27	bitri 249	. . . . . . . 8 |- ( A. x A. w ( ( x e. A /\ w e. x ) -> A. t ( ( t C. w /\ Tr t ) -> t e. w ) ) <-> A. w ( E. x e. A w e. x -> A. t ( ( t C. w /\ Tr t ) -> t e. w ) ) )
29		df-ral 2809	. . . . . . . 8 |- ( A. w e. U. A A. t ( ( t C. w /\ Tr t ) -> t e. w ) <-> A. w ( w e. U. A -> A. t ( ( t C. w /\ Tr t ) -> t e. w ) ) )
30	21, 28, 29	3imtr4i 266	. . . . . . 7 |- ( A. x A. w ( ( x e. A /\ w e. x ) -> A. t ( ( t C. w /\ Tr t ) -> t e. w ) ) -> A. w e. U. A A. t ( ( t C. w /\ Tr t ) -> t e. w ) )
31	17, 30	sylbir 213	. . . . . 6 |- ( A. x A. w ( x e. A -> ( w e. x -> A. t ( ( t C. w /\ Tr t ) -> t e. w ) ) ) -> A. w e. U. A A. t ( ( t C. w /\ Tr t ) -> t e. w ) )
32	15, 31	sylbi 195	. . . . 5 |- ( A. x e. A A. w ( w e. x -> A. t ( ( t C. w /\ Tr t ) -> t e. w ) ) -> A. w e. U. A A. t ( ( t C. w /\ Tr t ) -> t e. w ) )
33	11, 32	syl 16	. . . 4 |- ( A. x e. A A. y ( ( y C. x /\ Tr y ) -> y e. x ) -> A. w e. U. A A. t ( ( t C. w /\ Tr t ) -> t e. w ) )
34	33	adantl 464	. . 3 |- ( ( A =/= (/) /\ A. x e. A A. y ( ( y C. x /\ Tr y ) -> y e. x ) ) -> A. w e. U. A A. t ( ( t C. w /\ Tr t ) -> t e. w ) )
35		intssuni 4294	. . . . 5 |- ( A =/= (/) -> |^| A C_ U. A )
36		ssralv 3550	. . . . 5 |- ( |^| A C_ U. A -> ( A. w e. U. A A. t ( ( t C. w /\ Tr t ) -> t e. w ) -> A. w e. |^| A A. t ( ( t C. w /\ Tr t ) -> t e. w ) ) )
37	35, 36	syl 16	. . . 4 |- ( A =/= (/) -> ( A. w e. U. A A. t ( ( t C. w /\ Tr t ) -> t e. w ) -> A. w e. |^| A A. t ( ( t C. w /\ Tr t ) -> t e. w ) ) )
38	37	adantr 463	. . 3 |- ( ( A =/= (/) /\ A. x e. A A. y ( ( y C. x /\ Tr y ) -> y e. x ) ) -> ( A. w e. U. A A. t ( ( t C. w /\ Tr t ) -> t e. w ) -> A. w e. |^| A A. t ( ( t C. w /\ Tr t ) -> t e. w ) ) )
39	34, 38	mpd 15	. 2 |- ( ( A =/= (/) /\ A. x e. A A. y ( ( y C. x /\ Tr y ) -> y e. x ) ) -> A. w e. |^| A A. t ( ( t C. w /\ Tr t ) -> t e. w ) )
40		dfon2lem6 29460	. . 3 |- ( ( Tr |^| A /\ A. w e. |^| A A. t ( ( t C. w /\ Tr t ) -> t e. w ) ) -> A. z ( ( z C. |^| A /\ Tr z ) -> z e. |^| A ) )
41		intex 4593	. . . . . . . . . . 11 |- ( A =/= (/) <-> |^| A e. _V )
42		dfon2lem3 29457	. . . . . . . . . . 11 |- ( |^| A e. _V -> ( A. z ( ( z C. |^| A /\ Tr z ) -> z e. |^| A ) -> ( Tr |^| A /\ A. t e. |^| A -. t e. t ) ) )
43	41, 42	sylbi 195	. . . . . . . . . 10 |- ( A =/= (/) -> ( A. z ( ( z C. |^| A /\ Tr z ) -> z e. |^| A ) -> ( Tr |^| A /\ A. t e. |^| A -. t e. t ) ) )
44	43	imp 427	. . . . . . . . 9 |- ( ( A =/= (/) /\ A. z ( ( z C. |^| A /\ Tr z ) -> z e. |^| A ) ) -> ( Tr |^| A /\ A. t e. |^| A -. t e. t ) )
45	44	simprd 461	. . . . . . . 8 |- ( ( A =/= (/) /\ A. z ( ( z C. |^| A /\ Tr z ) -> z e. |^| A ) ) -> A. t e. |^| A -. t e. t )
46		untelirr 29321	. . . . . . . 8 |- ( A. t e. |^| A -. t e. t -> -. |^| A e. |^| A )
47	45, 46	syl 16	. . . . . . 7 |- ( ( A =/= (/) /\ A. z ( ( z C. |^| A /\ Tr z ) -> z e. |^| A ) ) -> -. |^| A e. |^| A )
48	47	adantlr 712	. . . . . 6 |- ( ( ( A =/= (/) /\ A. x e. A A. y ( ( y C. x /\ Tr y ) -> y e. x ) ) /\ A. z ( ( z C. |^| A /\ Tr z ) -> z e. |^| A ) ) -> -. |^| A e. |^| A )
49		risset 2979	. . . . . . . . . 10 |- ( |^| A e. A <-> E. t e. A t = |^| A )
50	49	notbii 294	. . . . . . . . 9 |- ( -. |^| A e. A <-> -. E. t e. A t = |^| A )
51		ralnex 2900	. . . . . . . . 9 |- ( A. t e. A -. t = |^| A <-> -. E. t e. A t = |^| A )
52	50, 51	bitr4i 252	. . . . . . . 8 |- ( -. |^| A e. A <-> A. t e. A -. t = |^| A )
53		eqcom 2463	. . . . . . . . . . . 12 |- ( t = |^| A <-> |^| A = t )
54	53	notbii 294	. . . . . . . . . . 11 |- ( -. t = |^| A <-> -. |^| A = t )
55	44	simpld 457	. . . . . . . . . . . . 13 |- ( ( A =/= (/) /\ A. z ( ( z C. |^| A /\ Tr z ) -> z e. |^| A ) ) -> Tr |^| A )
56	55	adantlr 712	. . . . . . . . . . . 12 |- ( ( ( A =/= (/) /\ A. x e. A A. y ( ( y C. x /\ Tr y ) -> y e. x ) ) /\ A. z ( ( z C. |^| A /\ Tr z ) -> z e. |^| A ) ) -> Tr |^| A )
57		psseq2 3578	. . . . . . . . . . . . . . . . . . 19 |- ( x = t -> ( y C. x <-> y C. t ) )
58	57	anbi1d 702	. . . . . . . . . . . . . . . . . 18 |- ( x = t -> ( ( y C. x /\ Tr y ) <-> ( y C. t /\ Tr y ) ) )
59		elequ2 1828	. . . . . . . . . . . . . . . . . 18 |- ( x = t -> ( y e. x <-> y e. t ) )
60	58, 59	imbi12d 318	. . . . . . . . . . . . . . . . 17 |- ( x = t -> ( ( ( y C. x /\ Tr y ) -> y e. x ) <-> ( ( y C. t /\ Tr y ) -> y e. t ) ) )
61	60	albidv 1718	. . . . . . . . . . . . . . . 16 |- ( x = t -> ( A. y ( ( y C. x /\ Tr y ) -> y e. x ) <-> A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) )
62	61	rspccv 3204	. . . . . . . . . . . . . . 15 |- ( A. x e. A A. y ( ( y C. x /\ Tr y ) -> y e. x ) -> ( t e. A -> A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) )
63	62	adantl 464	. . . . . . . . . . . . . 14 |- ( ( A =/= (/) /\ A. x e. A A. y ( ( y C. x /\ Tr y ) -> y e. x ) ) -> ( t e. A -> A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) )
64		intss1 4286	. . . . . . . . . . . . . . . 16 |- ( t e. A -> |^| A C_ t )
65		dfpss2 3575	. . . . . . . . . . . . . . . . . . . 20 |- ( |^| A C. t <-> ( |^| A C_ t /\ -. |^| A = t ) )
66		psseq1 3577	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( y = |^| A -> ( y C. t <-> |^| A C. t ) )
67		treq 4538	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( y = |^| A -> ( Tr y <-> Tr |^| A ) )
68	66, 67	anbi12d 708	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( y = |^| A -> ( ( y C. t /\ Tr y ) <-> ( |^| A C. t /\ Tr |^| A ) ) )
69		eleq1 2526	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( y = |^| A -> ( y e. t <-> |^| A e. t ) )
70	68, 69	imbi12d 318	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( y = |^| A -> ( ( ( y C. t /\ Tr y ) -> y e. t ) <-> ( ( |^| A C. t /\ Tr |^| A ) -> |^| A e. t ) ) )
71	70	spcgv 3191	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( |^| A e. _V -> ( A. y ( ( y C. t /\ Tr y ) -> y e. t ) -> ( ( |^| A C. t /\ Tr |^| A ) -> |^| A e. t ) ) )
72	41, 71	sylbi 195	. . . . . . . . . . . . . . . . . . . . . 22 |- ( A =/= (/) -> ( A. y ( ( y C. t /\ Tr y ) -> y e. t ) -> ( ( |^| A C. t /\ Tr |^| A ) -> |^| A e. t ) ) )
73	72	imp 427	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( A =/= (/) /\ A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) -> ( ( |^| A C. t /\ Tr |^| A ) -> |^| A e. t ) )
74	73	expd 434	. . . . . . . . . . . . . . . . . . . 20 |- ( ( A =/= (/) /\ A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) -> ( |^| A C. t -> ( Tr |^| A -> |^| A e. t ) ) )
75	65, 74	syl5bir 218	. . . . . . . . . . . . . . . . . . 19 |- ( ( A =/= (/) /\ A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) -> ( ( |^| A C_ t /\ -. |^| A = t ) -> ( Tr |^| A -> |^| A e. t ) ) )
76	75	exp4b 605	. . . . . . . . . . . . . . . . . 18 |- ( A =/= (/) -> ( A. y ( ( y C. t /\ Tr y ) -> y e. t ) -> ( |^| A C_ t -> ( -. |^| A = t -> ( Tr |^| A -> |^| A e. t ) ) ) ) )
77	76	com45 89	. . . . . . . . . . . . . . . . 17 |- ( A =/= (/) -> ( A. y ( ( y C. t /\ Tr y ) -> y e. t ) -> ( |^| A C_ t -> ( Tr |^| A -> ( -. |^| A = t -> |^| A e. t ) ) ) ) )
78	77	com23 78	. . . . . . . . . . . . . . . 16 |- ( A =/= (/) -> ( |^| A C_ t -> ( A. y ( ( y C. t /\ Tr y ) -> y e. t ) -> ( Tr |^| A -> ( -. |^| A = t -> |^| A e. t ) ) ) ) )
79	64, 78	syl5 32	. . . . . . . . . . . . . . 15 |- ( A =/= (/) -> ( t e. A -> ( A. y ( ( y C. t /\ Tr y ) -> y e. t ) -> ( Tr |^| A -> ( -. |^| A = t -> |^| A e. t ) ) ) ) )
80	79	adantr 463	. . . . . . . . . . . . . 14 |- ( ( A =/= (/) /\ A. x e. A A. y ( ( y C. x /\ Tr y ) -> y e. x ) ) -> ( t e. A -> ( A. y ( ( y C. t /\ Tr y ) -> y e. t ) -> ( Tr |^| A -> ( -. |^| A = t -> |^| A e. t ) ) ) ) )
81	63, 80	mpdd 40	. . . . . . . . . . . . 13 |- ( ( A =/= (/) /\ A. x e. A A. y ( ( y C. x /\ Tr y ) -> y e. x ) ) -> ( t e. A -> ( Tr |^| A -> ( -. |^| A = t -> |^| A e. t ) ) ) )
82	81	adantr 463	. . . . . . . . . . . 12 |- ( ( ( A =/= (/) /\ A. x e. A A. y ( ( y C. x /\ Tr y ) -> y e. x ) ) /\ A. z ( ( z C. |^| A /\ Tr z ) -> z e. |^| A ) ) -> ( t e. A -> ( Tr |^| A -> ( -. |^| A = t -> |^| A e. t ) ) ) )
83	56, 82	mpid 41	. . . . . . . . . . 11 |- ( ( ( A =/= (/) /\ A. x e. A A. y ( ( y C. x /\ Tr y ) -> y e. x ) ) /\ A. z ( ( z C. |^| A /\ Tr z ) -> z e. |^| A ) ) -> ( t e. A -> ( -. |^| A = t -> |^| A e. t ) ) )
84	54, 83	syl7bi 230	. . . . . . . . . 10 |- ( ( ( A =/= (/) /\ A. x e. A A. y ( ( y C. x /\ Tr y ) -> y e. x ) ) /\ A. z ( ( z C. |^| A /\ Tr z ) -> z e. |^| A ) ) -> ( t e. A -> ( -. t = |^| A -> |^| A e. t ) ) )
85	84	ralrimiv 2866	. . . . . . . . 9 |- ( ( ( A =/= (/) /\ A. x e. A A. y ( ( y C. x /\ Tr y ) -> y e. x ) ) /\ A. z ( ( z C. |^| A /\ Tr z ) -> z e. |^| A ) ) -> A. t e. A ( -. t = |^| A -> |^| A e. t ) )
86		ralim 2843	. . . . . . . . 9 |- ( A. t e. A ( -. t = |^| A -> |^| A e. t ) -> ( A. t e. A -. t = |^| A -> A. t e. A |^| A e. t ) )
87	85, 86	syl 16	. . . . . . . 8 |- ( ( ( A =/= (/) /\ A. x e. A A. y ( ( y C. x /\ Tr y ) -> y e. x ) ) /\ A. z ( ( z C. |^| A /\ Tr z ) -> z e. |^| A ) ) -> ( A. t e. A -. t = |^| A -> A. t e. A |^| A e. t ) )
88	52, 87	syl5bi 217	. . . . . . 7 |- ( ( ( A =/= (/) /\ A. x e. A A. y ( ( y C. x /\ Tr y ) -> y e. x ) ) /\ A. z ( ( z C. |^| A /\ Tr z ) -> z e. |^| A ) ) -> ( -. |^| A e. A -> A. t e. A |^| A e. t ) )
89		elintg 4279	. . . . . . . . 9 |- ( |^| A e. _V -> ( |^| A e. |^| A <-> A. t e. A |^| A e. t ) )
90	41, 89	sylbi 195	. . . . . . . 8 |- ( A =/= (/) -> ( |^| A e. |^| A <-> A. t e. A |^| A e. t ) )
91	90	ad2antrr 723	. . . . . . 7 |- ( ( ( A =/= (/) /\ A. x e. A A. y ( ( y C. x /\ Tr y ) -> y e. x ) ) /\ A. z ( ( z C. |^| A /\ Tr z ) -> z e. |^| A ) ) -> ( |^| A e. |^| A <-> A. t e. A |^| A e. t ) )
92	88, 91	sylibrd 234	. . . . . 6 |- ( ( ( A =/= (/) /\ A. x e. A A. y ( ( y C. x /\ Tr y ) -> y e. x ) ) /\ A. z ( ( z C. |^| A /\ Tr z ) -> z e. |^| A ) ) -> ( -. |^| A e. A -> |^| A e. |^| A ) )
93	48, 92	mt3d 125	. . . . 5 |- ( ( ( A =/= (/) /\ A. x e. A A. y ( ( y C. x /\ Tr y ) -> y e. x ) ) /\ A. z ( ( z C. |^| A /\ Tr z ) -> z e. |^| A ) ) -> |^| A e. A )
94	93	ex 432	. . . 4 |- ( ( A =/= (/) /\ A. x e. A A. y ( ( y C. x /\ Tr y ) -> y e. x ) ) -> ( A. z ( ( z C. |^| A /\ Tr z ) -> z e. |^| A ) -> |^| A e. A ) )
95	94	ancld 551	. . 3 |- ( ( A =/= (/) /\ A. x e. A A. y ( ( y C. x /\ Tr y ) -> y e. x ) ) -> ( A. z ( ( z C. |^| A /\ Tr z ) -> z e. |^| A ) -> ( A. z ( ( z C. |^| A /\ Tr z ) -> z e. |^| A ) /\ |^| A e. A ) ) )
96	40, 95	syl5 32	. 2 |- ( ( A =/= (/) /\ A. x e. A A. y ( ( y C. x /\ Tr y ) -> y e. x ) ) -> ( ( Tr |^| A /\ A. w e. |^| A A. t ( ( t C. w /\ Tr t ) -> t e. w ) ) -> ( A. z ( ( z C. |^| A /\ Tr z ) -> z e. |^| A ) /\ |^| A e. A ) ) )
97	8, 39, 96	mp2and 677	1 |- ( ( A =/= (/) /\ A. x e. A A. y ( ( y C. x /\ Tr y ) -> y e. x ) ) -> ( A. z ( ( z C. |^| A /\ Tr z ) -> z e. |^| A ) /\ |^| A e. A ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   /\ wa 367   A.wal 1396   = wceq 1398   E.wex 1617   e. wcel 1823   =/= wne 2649   A.wral 2804   E.wrex 2805   _Vcvv 3106   C_ wss 3461   C. wpss 3462   (/)c0 3783   U.cuni 4235   |^|cint 4271   Tr wtr 4532

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-8 1825  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-nul 4568  ax-pr 4676  ax-un 6565

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-v 3108  df-sbc 3325  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-pss 3477  df-nul 3784  df-pw 4001  df-sn 4017  df-pr 4019  df-uni 4236  df-int 4272  df-iun 4317  df-tr 4533  df-suc 4873

This theorem is referenced by:  dfon2lem9  29463