Theorem dfon2lem8 27608

Description: Lemma for dfon2 27610. 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 2980	. . . . . . 7 |- x e. _V
2		dfon2lem3 27603	. . . . . . 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 2796	. . . 4 |- ( A. x e. A A. y ( ( y C. x /\ Tr y ) -> y e. x ) -> A. x e. A Tr x )
6		trint 4405	. . . 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 27607	. . . . . . 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 1685	. . . . . 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 2796	. . . . 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 2725	. . . . . . 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 1909	. . . . . . . 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 1610	. . . . . . 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 1611	. . . . . . 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 4100	. . . . . . . . . . 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 1604	. . . . . . . 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 1783	. . . . . . . . 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 1910	. . . . . . . . . . 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 2726	. . . . . . . . . . . 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 1610	. . . . . . . . 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 2725	. . . . . . . 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 4155	. . . . 5 |- ( A =/= (/) -> |^| A C_ U. A )
36		ssralv 3421	. . . . 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 27606	. . 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 4453	. . . . . . . . . . 11 |- ( A =/= (/) <-> |^| A e. _V )
42		dfon2lem3 27603	. . . . . . . . . . 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 27364	. . . . . . . 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 2768	. . . . . . . . . 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 2730	. . . . . . . . 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 2445	. . . . . . . . . . . 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 3449	. . . . . . . . . . . . . . . . . . 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 1761	. . . . . . . . . . . . . . . . . 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 1679	. . . . . . . . . . . . . . . 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 3075	. . . . . . . . . . . . . . 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 4148	. . . . . . . . . . . . . . . 16 |- ( t e. A -> |^| A C_ t )
65		dfpss2 3446	. . . . . . . . . . . . . . . . . . . 20 |- ( |^| A C. t <-> ( |^| A C_ t /\ -. |^| A = t ) )
66		psseq1 3448	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( y = |^| A -> ( y C. t <-> |^| A C. t ) )
67		treq 4396	. . . . . . . . . . . . . . . . . . . . . . . . . 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 2503	. . . . . . . . . . . . . . . . . . . . . . . . 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 3062	. . . . . . . . . . . . . . . . . . . . . . 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 2803	. . . . . . . . 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 2792	. . . . . . . . 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 4141	. . . . . . . . 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 1367   = wceq 1369   E.wex 1586   e. wcel 1756   =/= wne 2611   A.wral 2720   E.wrex 2721   _Vcvv 2977   C_ wss 3333   C. wpss 3334   (/)c0 3642   U.cuni 4096   |^|cint 4133   Tr wtr 4390

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 4418  ax-nul 4426  ax-pr 4536  ax-un 6377

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  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 2573  df-ne 2613  df-ral 2725  df-rex 2726  df-v 2979  df-sbc 3192  df-dif 3336  df-un 3338  df-in 3340  df-ss 3347  df-pss 3349  df-nul 3643  df-pw 3867  df-sn 3883  df-pr 3885  df-uni 4097  df-int 4134  df-iun 4178  df-tr 4391  df-suc 4730

This theorem is referenced by:  dfon2lem9  27609