Theorem dfon2lem8 25360

Description: Lemma for dfon2 25362. The intersection of a non-empty 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 2919	. . . . . . 7 |- x e. _V
2		dfon2lem3 25355	. . . . . . 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 8	. . . . . 6 |- ( A. y ( ( y C. x /\ Tr y ) -> y e. x ) -> ( Tr x /\ A. z e. x -. z e. z ) )
4	3	simpld 446	. . . . 5 |- ( A. y ( ( y C. x /\ Tr y ) -> y e. x ) -> Tr x )
5	4	ralimi 2741	. . . 4 |- ( A. x e. A A. y ( ( y C. x /\ Tr y ) -> y e. x ) -> A. x e. A Tr x )
6		trint 4277	. . . 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 453	. 2 |- ( ( A =/= (/) /\ A. x e. A A. y ( ( y C. x /\ Tr y ) -> y e. x ) ) -> Tr |^| A )
9	1	dfon2lem7 25359	. . . . . . 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 1638	. . . . . 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 2741	. . . . 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 2671	. . . . . . 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 1572	. . . . . . 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 244	. . . . . 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 434	. . . . . . . 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 1573	. . . . . . 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 3979	. . . . . . . . . . 11 |- ( w e. U. A <-> E. x e. A w e. x )
19	18	biimpi 187	. . . . . . . . . 10 |- ( w e. U. A -> E. x e. A w e. x )
20	19	imim1i 56	. . . . . . . . 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 1565	. . . . . . . 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 1748	. . . . . . . . 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 2672	. . . . . . . . . . . 12 |- ( E. x e. A w e. x <-> E. x ( x e. A /\ w e. x ) )
25	24	imbi1i 316	. . . . . . . . . . 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 244	. . . . . . . . . 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 1572	. . . . . . . . 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 241	. . . . . . . 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 2671	. . . . . . . 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 258	. . . . . . 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 205	. . . . . 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 188	. . . . 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 453	. . 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 4032	. . . . 5 |- ( A =/= (/) -> |^| A C_ U. A )
36		ssralv 3367	. . . . 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 452	. . 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 25358	. . 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 4316	. . . . . . . . . . 11 |- ( A =/= (/) <-> |^| A e. _V )
42		dfon2lem3 25355	. . . . . . . . . . 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 188	. . . . . . . . . 10 |- ( A =/= (/) -> ( A. z ( ( z C. |^| A /\ Tr z ) -> z e. |^| A ) -> ( Tr |^| A /\ A. t e. |^| A -. t e. t ) ) )
44	43	imp 419	. . . . . . . . 9 |- ( ( A =/= (/) /\ A. z ( ( z C. |^| A /\ Tr z ) -> z e. |^| A ) ) -> ( Tr |^| A /\ A. t e. |^| A -. t e. t ) )
45	44	simprd 450	. . . . . . . 8 |- ( ( A =/= (/) /\ A. z ( ( z C. |^| A /\ Tr z ) -> z e. |^| A ) ) -> A. t e. |^| A -. t e. t )
46		untelirr 25110	. . . . . . . 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 696	. . . . . 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 2713	. . . . . . . . . 10 |- ( |^| A e. A <-> E. t e. A t = |^| A )
50	49	notbii 288	. . . . . . . . 9 |- ( -. |^| A e. A <-> -. E. t e. A t = |^| A )
51		ralnex 2676	. . . . . . . . 9 |- ( A. t e. A -. t = |^| A <-> -. E. t e. A t = |^| A )
52	50, 51	bitr4i 244	. . . . . . . 8 |- ( -. |^| A e. A <-> A. t e. A -. t = |^| A )
53		eqcom 2406	. . . . . . . . . . . 12 |- ( t = |^| A <-> |^| A = t )
54	53	notbii 288	. . . . . . . . . . 11 |- ( -. t = |^| A <-> -. |^| A = t )
55	44	simpld 446	. . . . . . . . . . . . 13 |- ( ( A =/= (/) /\ A. z ( ( z C. |^| A /\ Tr z ) -> z e. |^| A ) ) -> Tr |^| A )
56	55	adantlr 696	. . . . . . . . . . . 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 3395	. . . . . . . . . . . . . . . . . . 19 |- ( x = t -> ( y C. x <-> y C. t ) )
58	57	anbi1d 686	. . . . . . . . . . . . . . . . . 18 |- ( x = t -> ( ( y C. x /\ Tr y ) <-> ( y C. t /\ Tr y ) ) )
59		elequ2 1726	. . . . . . . . . . . . . . . . . 18 |- ( x = t -> ( y e. x <-> y e. t ) )
60	58, 59	imbi12d 312	. . . . . . . . . . . . . . . . 17 |- ( x = t -> ( ( ( y C. x /\ Tr y ) -> y e. x ) <-> ( ( y C. t /\ Tr y ) -> y e. t ) ) )
61	60	albidv 1632	. . . . . . . . . . . . . . . 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 3009	. . . . . . . . . . . . . . 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 453	. . . . . . . . . . . . . 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 4025	. . . . . . . . . . . . . . . 16 |- ( t e. A -> |^| A C_ t )
65		dfpss2 3392	. . . . . . . . . . . . . . . . . . . 20 |- ( |^| A C. t <-> ( |^| A C_ t /\ -. |^| A = t ) )
66		psseq1 3394	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( y = |^| A -> ( y C. t <-> |^| A C. t ) )
67		treq 4268	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( y = |^| A -> ( Tr y <-> Tr |^| A ) )
68	66, 67	anbi12d 692	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( y = |^| A -> ( ( y C. t /\ Tr y ) <-> ( |^| A C. t /\ Tr |^| A ) ) )
69		eleq1 2464	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( y = |^| A -> ( y e. t <-> |^| A e. t ) )
70	68, 69	imbi12d 312	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( y = |^| A -> ( ( ( y C. t /\ Tr y ) -> y e. t ) <-> ( ( |^| A C. t /\ Tr |^| A ) -> |^| A e. t ) ) )
71	70	spcgv 2996	. . . . . . . . . . . . . . . . . . . . . . 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 188	. . . . . . . . . . . . . . . . . . . . . 22 |- ( A =/= (/) -> ( A. y ( ( y C. t /\ Tr y ) -> y e. t ) -> ( ( |^| A C. t /\ Tr |^| A ) -> |^| A e. t ) ) )
73	72	imp 419	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( A =/= (/) /\ A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) -> ( ( |^| A C. t /\ Tr |^| A ) -> |^| A e. t ) )
74	73	exp3a 426	. . . . . . . . . . . . . . . . . . . 20 |- ( ( A =/= (/) /\ A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) -> ( |^| A C. t -> ( Tr |^| A -> |^| A e. t ) ) )
75	65, 74	syl5bir 210	. . . . . . . . . . . . . . . . . . 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 591	. . . . . . . . . . . . . . . . . 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 85	. . . . . . . . . . . . . . . . 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 74	. . . . . . . . . . . . . . . 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 30	. . . . . . . . . . . . . . 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 452	. . . . . . . . . . . . . 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 38	. . . . . . . . . . . . 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 452	. . . . . . . . . . . 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 39	. . . . . . . . . . 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 222	. . . . . . . . . 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 2748	. . . . . . . . 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 2737	. . . . . . . . 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 209	. . . . . . 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 4018	. . . . . . . . 9 |- ( |^| A e. _V -> ( |^| A e. |^| A <-> A. t e. A |^| A e. t ) )
90	41, 89	sylbi 188	. . . . . . . 8 |- ( A =/= (/) -> ( |^| A e. |^| A <-> A. t e. A |^| A e. t ) )
91	90	ad2antrr 707	. . . . . . 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 226	. . . . . 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 119	. . . . 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 424	. . . 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 537	. . 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 30	. 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 661	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 177   /\ wa 359   A.wal 1546   E.wex 1547   = wceq 1649   e. wcel 1721   =/= wne 2567   A.wral 2666   E.wrex 2667   _Vcvv 2916   C_ wss 3280   C. wpss 3281   (/)c0 3588   U.cuni 3975   |^|cint 4010   Tr wtr 4262

This theorem is referenced by:  dfon2lem9  25361

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-nul 4298  ax-pr 4363  ax-un 4660

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-v 2918  df-sbc 3122  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-pss 3296  df-nul 3589  df-pw 3761  df-sn 3780  df-pr 3781  df-uni 3976  df-int 4011  df-iun 4055  df-tr 4263  df-suc 4547