Theorem dfon2lem8 29149

Description: Lemma for dfon2 29151. 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 3121	. . . . . . 7 |- x e. _V
2		dfon2lem3 29144	. . . . . . 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 459	. . . . 5 |- ( A. y ( ( y C. x /\ Tr y ) -> y e. x ) -> Tr x )
5	4	ralimi 2860	. . . 4 |- ( A. x e. A A. y ( ( y C. x /\ Tr y ) -> y e. x ) -> A. x e. A Tr x )
6		trint 4561	. . . 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 466	. 2 |- ( ( A =/= (/) /\ A. x e. A A. y ( ( y C. x /\ Tr y ) -> y e. x ) ) -> Tr |^| A )
9	1	dfon2lem7 29148	. . . . . . 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 1695	. . . . . 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 2860	. . . . 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 2822	. . . . . . 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 1930	. . . . . . . 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 1620	. . . . . . 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 446	. . . . . . . 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 1621	. . . . . . 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 4255	. . . . . . . . . . 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 1614	. . . . . . . 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 1794	. . . . . . . . 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 1932	. . . . . . . . . . 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 2823	. . . . . . . . . . . 12 |- ( E. x e. A w e. x <-> E. x ( x e. A /\ w e. x ) )
25	24	imbi1i 325	. . . . . . . . . . 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 1620	. . . . . . . . 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 2822	. . . . . . . 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 466	. . 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 4310	. . . . 5 |- ( A =/= (/) -> |^| A C_ U. A )
36		ssralv 3569	. . . . 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 465	. . 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 29147	. . 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 4609	. . . . . . . . . . 11 |- ( A =/= (/) <-> |^| A e. _V )
42		dfon2lem3 29144	. . . . . . . . . . 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 429	. . . . . . . . 9 |- ( ( A =/= (/) /\ A. z ( ( z C. |^| A /\ Tr z ) -> z e. |^| A ) ) -> ( Tr |^| A /\ A. t e. |^| A -. t e. t ) )
45	44	simprd 463	. . . . . . . 8 |- ( ( A =/= (/) /\ A. z ( ( z C. |^| A /\ Tr z ) -> z e. |^| A ) ) -> A. t e. |^| A -. t e. t )
46		untelirr 28905	. . . . . . . 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 714	. . . . . 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 2992	. . . . . . . . . 10 |- ( |^| A e. A <-> E. t e. A t = |^| A )
50	49	notbii 296	. . . . . . . . 9 |- ( -. |^| A e. A <-> -. E. t e. A t = |^| A )
51		ralnex 2913	. . . . . . . . 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 2476	. . . . . . . . . . . 12 |- ( t = |^| A <-> |^| A = t )
54	53	notbii 296	. . . . . . . . . . 11 |- ( -. t = |^| A <-> -. |^| A = t )
55	44	simpld 459	. . . . . . . . . . . . 13 |- ( ( A =/= (/) /\ A. z ( ( z C. |^| A /\ Tr z ) -> z e. |^| A ) ) -> Tr |^| A )
56	55	adantlr 714	. . . . . . . . . . . 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 3597	. . . . . . . . . . . . . . . . . . 19 |- ( x = t -> ( y C. x <-> y C. t ) )
58	57	anbi1d 704	. . . . . . . . . . . . . . . . . 18 |- ( x = t -> ( ( y C. x /\ Tr y ) <-> ( y C. t /\ Tr y ) ) )
59		elequ2 1772	. . . . . . . . . . . . . . . . . 18 |- ( x = t -> ( y e. x <-> y e. t ) )
60	58, 59	imbi12d 320	. . . . . . . . . . . . . . . . 17 |- ( x = t -> ( ( ( y C. x /\ Tr y ) -> y e. x ) <-> ( ( y C. t /\ Tr y ) -> y e. t ) ) )
61	60	albidv 1689	. . . . . . . . . . . . . . . 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 3216	. . . . . . . . . . . . . . 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 466	. . . . . . . . . . . . . 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 4303	. . . . . . . . . . . . . . . 16 |- ( t e. A -> |^| A C_ t )
65		dfpss2 3594	. . . . . . . . . . . . . . . . . . . 20 |- ( |^| A C. t <-> ( |^| A C_ t /\ -. |^| A = t ) )
66		psseq1 3596	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( y = |^| A -> ( y C. t <-> |^| A C. t ) )
67		treq 4552	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( y = |^| A -> ( Tr y <-> Tr |^| A ) )
68	66, 67	anbi12d 710	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( y = |^| A -> ( ( y C. t /\ Tr y ) <-> ( |^| A C. t /\ Tr |^| A ) ) )
69		eleq1 2539	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( y = |^| A -> ( y e. t <-> |^| A e. t ) )
70	68, 69	imbi12d 320	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( y = |^| A -> ( ( ( y C. t /\ Tr y ) -> y e. t ) <-> ( ( |^| A C. t /\ Tr |^| A ) -> |^| A e. t ) ) )
71	70	spcgv 3203	. . . . . . . . . . . . . . . . . . . . . . 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 429	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( A =/= (/) /\ A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) -> ( ( |^| A C. t /\ Tr |^| A ) -> |^| A e. t ) )
74	73	expd 436	. . . . . . . . . . . . . . . . . . . 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 607	. . . . . . . . . . . . . . . . . 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 465	. . . . . . . . . . . . . 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 465	. . . . . . . . . . . 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 2879	. . . . . . . . 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 2856	. . . . . . . . 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 4296	. . . . . . . . 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 725	. . . . . . 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 434	. . . 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 553	. . 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 679	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 369   A.wal 1377   = wceq 1379   E.wex 1596   e. wcel 1767   =/= wne 2662   A.wral 2817   E.wrex 2818   _Vcvv 3118   C_ wss 3481   C. wpss 3482   (/)c0 3790   U.cuni 4251   |^|cint 4288   Tr wtr 4546

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 4574  ax-nul 4582  ax-pr 4692  ax-un 6587

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  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 2822  df-rex 2823  df-v 3120  df-sbc 3337  df-dif 3484  df-un 3486  df-in 3488  df-ss 3495  df-pss 3497  df-nul 3791  df-pw 4018  df-sn 4034  df-pr 4036  df-uni 4252  df-int 4289  df-iun 4333  df-tr 4547  df-suc 4890

This theorem is referenced by:  dfon2lem9  29150