Theorem pwsdompw 9026

Description: Lemma for domtriom 9265. This is the equinumerosity version of the algebraic identity sum_ k e. n ( 2 ^ k ) = ( 2 ^ n ) - 1. (Contributed by Mario Carneiro, 7-Feb-2013.)

Assertion

Ref	Expression
pwsdompw	|- ( ( n e. om /\ A. k e. suc n ( B ` k ) ~~ ~P k ) -> U_ k e. n ( B ` k ) ~< ( B ` n ) )

Distinct variable group:   B, k, n

Proof of Theorem pwsdompw

Dummy variable m is distinct from all other variables.

Step	Hyp	Ref	Expression
1		suceq 5790	. . . . 5 |- ( n = (/) -> suc n = suc (/) )
2	1	raleqdv 3144	. . . 4 |- ( n = (/) -> ( A. k e. suc n ( B ` k ) ~~ ~P k <-> A. k e. suc (/) ( B ` k ) ~~ ~P k ) )
3		iuneq1 4534	. . . . 5 |- ( n = (/) -> U_ k e. n ( B ` k ) = U_ k e. (/) ( B ` k ) )
4		fveq2 6191	. . . . 5 |- ( n = (/) -> ( B ` n ) = ( B ` (/) ) )
5	3, 4	breq12d 4666	. . . 4 |- ( n = (/) -> ( U_ k e. n ( B ` k ) ~< ( B ` n ) <-> U_ k e. (/) ( B ` k ) ~< ( B ` (/) ) ) )
6	2, 5	imbi12d 334	. . 3 |- ( n = (/) -> ( ( A. k e. suc n ( B ` k ) ~~ ~P k -> U_ k e. n ( B ` k ) ~< ( B ` n ) ) <-> ( A. k e. suc (/) ( B ` k ) ~~ ~P k -> U_ k e. (/) ( B ` k ) ~< ( B ` (/) ) ) ) )
7		suceq 5790	. . . . 5 |- ( n = m -> suc n = suc m )
8	7	raleqdv 3144	. . . 4 |- ( n = m -> ( A. k e. suc n ( B ` k ) ~~ ~P k <-> A. k e. suc m ( B ` k ) ~~ ~P k ) )
9		iuneq1 4534	. . . . 5 |- ( n = m -> U_ k e. n ( B ` k ) = U_ k e. m ( B ` k ) )
10		fveq2 6191	. . . . 5 |- ( n = m -> ( B ` n ) = ( B ` m ) )
11	9, 10	breq12d 4666	. . . 4 |- ( n = m -> ( U_ k e. n ( B ` k ) ~< ( B ` n ) <-> U_ k e. m ( B ` k ) ~< ( B ` m ) ) )
12	8, 11	imbi12d 334	. . 3 |- ( n = m -> ( ( A. k e. suc n ( B ` k ) ~~ ~P k -> U_ k e. n ( B ` k ) ~< ( B ` n ) ) <-> ( A. k e. suc m ( B ` k ) ~~ ~P k -> U_ k e. m ( B ` k ) ~< ( B ` m ) ) ) )
13		suceq 5790	. . . . 5 |- ( n = suc m -> suc n = suc suc m )
14	13	raleqdv 3144	. . . 4 |- ( n = suc m -> ( A. k e. suc n ( B ` k ) ~~ ~P k <-> A. k e. suc suc m ( B ` k ) ~~ ~P k ) )
15		iuneq1 4534	. . . . 5 |- ( n = suc m -> U_ k e. n ( B ` k ) = U_ k e. suc m ( B ` k ) )
16		fveq2 6191	. . . . 5 |- ( n = suc m -> ( B ` n ) = ( B ` suc m ) )
17	15, 16	breq12d 4666	. . . 4 |- ( n = suc m -> ( U_ k e. n ( B ` k ) ~< ( B ` n ) <-> U_ k e. suc m ( B ` k ) ~< ( B ` suc m ) ) )
18	14, 17	imbi12d 334	. . 3 |- ( n = suc m -> ( ( A. k e. suc n ( B ` k ) ~~ ~P k -> U_ k e. n ( B ` k ) ~< ( B ` n ) ) <-> ( A. k e. suc suc m ( B ` k ) ~~ ~P k -> U_ k e. suc m ( B ` k ) ~< ( B ` suc m ) ) ) )
19		0iun 4577	. . . 4 |- U_ k e. (/) ( B ` k ) = (/)
20		0ex 4790	. . . . . . 7 |- (/) e. _V
21	20	sucid 5804	. . . . . 6 |- (/) e. suc (/)
22		fveq2 6191	. . . . . . . 8 |- ( k = (/) -> ( B ` k ) = ( B ` (/) ) )
23		pweq 4161	. . . . . . . 8 |- ( k = (/) -> ~P k = ~P (/) )
24	22, 23	breq12d 4666	. . . . . . 7 |- ( k = (/) -> ( ( B ` k ) ~~ ~P k <-> ( B ` (/) ) ~~ ~P (/) ) )
25	24	rspcv 3305	. . . . . 6 |- ( (/) e. suc (/) -> ( A. k e. suc (/) ( B ` k ) ~~ ~P k -> ( B ` (/) ) ~~ ~P (/) ) )
26	21, 25	ax-mp 5	. . . . 5 |- ( A. k e. suc (/) ( B ` k ) ~~ ~P k -> ( B ` (/) ) ~~ ~P (/) )
27	20	canth2 8113	. . . . . 6 |- (/) ~< ~P (/)
28		ensym 8005	. . . . . 6 |- ( ( B ` (/) ) ~~ ~P (/) -> ~P (/) ~~ ( B ` (/) ) )
29		sdomentr 8094	. . . . . 6 |- ( ( (/) ~< ~P (/) /\ ~P (/) ~~ ( B ` (/) ) ) -> (/) ~< ( B ` (/) ) )
30	27, 28, 29	sylancr 695	. . . . 5 |- ( ( B ` (/) ) ~~ ~P (/) -> (/) ~< ( B ` (/) ) )
31	26, 30	syl 17	. . . 4 |- ( A. k e. suc (/) ( B ` k ) ~~ ~P k -> (/) ~< ( B ` (/) ) )
32	19, 31	syl5eqbr 4688	. . 3 |- ( A. k e. suc (/) ( B ` k ) ~~ ~P k -> U_ k e. (/) ( B ` k ) ~< ( B ` (/) ) )
33		sssucid 5802	. . . . . . . . 9 |- suc m C_ suc suc m
34		ssralv 3666	. . . . . . . . 9 |- ( suc m C_ suc suc m -> ( A. k e. suc suc m ( B ` k ) ~~ ~P k -> A. k e. suc m ( B ` k ) ~~ ~P k ) )
35	33, 34	ax-mp 5	. . . . . . . 8 |- ( A. k e. suc suc m ( B ` k ) ~~ ~P k -> A. k e. suc m ( B ` k ) ~~ ~P k )
36		pm2.27 42	. . . . . . . 8 |- ( A. k e. suc m ( B ` k ) ~~ ~P k -> ( ( A. k e. suc m ( B ` k ) ~~ ~P k -> U_ k e. m ( B ` k ) ~< ( B ` m ) ) -> U_ k e. m ( B ` k ) ~< ( B ` m ) ) )
37	35, 36	syl 17	. . . . . . 7 |- ( A. k e. suc suc m ( B ` k ) ~~ ~P k -> ( ( A. k e. suc m ( B ` k ) ~~ ~P k -> U_ k e. m ( B ` k ) ~< ( B ` m ) ) -> U_ k e. m ( B ` k ) ~< ( B ` m ) ) )
38	37	adantl 482	. . . . . 6 |- ( ( m e. om /\ A. k e. suc suc m ( B ` k ) ~~ ~P k ) -> ( ( A. k e. suc m ( B ` k ) ~~ ~P k -> U_ k e. m ( B ` k ) ~< ( B ` m ) ) -> U_ k e. m ( B ` k ) ~< ( B ` m ) ) )
39		vex 3203	. . . . . . . . . . . . 13 |- m e. _V
40	39	sucid 5804	. . . . . . . . . . . 12 |- m e. suc m
41		elelsuc 5797	. . . . . . . . . . . 12 |- ( m e. suc m -> m e. suc suc m )
42		fveq2 6191	. . . . . . . . . . . . . 14 |- ( k = m -> ( B ` k ) = ( B ` m ) )
43		pweq 4161	. . . . . . . . . . . . . 14 |- ( k = m -> ~P k = ~P m )
44	42, 43	breq12d 4666	. . . . . . . . . . . . 13 |- ( k = m -> ( ( B ` k ) ~~ ~P k <-> ( B ` m ) ~~ ~P m ) )
45	44	rspcv 3305	. . . . . . . . . . . 12 |- ( m e. suc suc m -> ( A. k e. suc suc m ( B ` k ) ~~ ~P k -> ( B ` m ) ~~ ~P m ) )
46	40, 41, 45	mp2b 10	. . . . . . . . . . 11 |- ( A. k e. suc suc m ( B ` k ) ~~ ~P k -> ( B ` m ) ~~ ~P m )
47		cdaen 8995	. . . . . . . . . . 11 |- ( ( ( B ` m ) ~~ ~P m /\ ( B ` m ) ~~ ~P m ) -> ( ( B ` m ) +c ( B ` m ) ) ~~ ( ~P m +c ~P m ) )
48	46, 46, 47	syl2anc 693	. . . . . . . . . 10 |- ( A. k e. suc suc m ( B ` k ) ~~ ~P k -> ( ( B ` m ) +c ( B ` m ) ) ~~ ( ~P m +c ~P m ) )
49		pwcda1 9016	. . . . . . . . . . 11 |- ( m e. om -> ( ~P m +c ~P m ) ~~ ~P ( m +c 1o ) )
50		nnord 7073	. . . . . . . . . . . . . 14 |- ( m e. om -> Ord m )
51		ordirr 5741	. . . . . . . . . . . . . 14 |- ( Ord m -> -. m e. m )
52	50, 51	syl 17	. . . . . . . . . . . . 13 |- ( m e. om -> -. m e. m )
53		cda1en 8997	. . . . . . . . . . . . 13 |- ( ( m e. om /\ -. m e. m ) -> ( m +c 1o ) ~~ suc m )
54	52, 53	mpdan 702	. . . . . . . . . . . 12 |- ( m e. om -> ( m +c 1o ) ~~ suc m )
55		pwen 8133	. . . . . . . . . . . 12 |- ( ( m +c 1o ) ~~ suc m -> ~P ( m +c 1o ) ~~ ~P suc m )
56	54, 55	syl 17	. . . . . . . . . . 11 |- ( m e. om -> ~P ( m +c 1o ) ~~ ~P suc m )
57		entr 8008	. . . . . . . . . . 11 |- ( ( ( ~P m +c ~P m ) ~~ ~P ( m +c 1o ) /\ ~P ( m +c 1o ) ~~ ~P suc m ) -> ( ~P m +c ~P m ) ~~ ~P suc m )
58	49, 56, 57	syl2anc 693	. . . . . . . . . 10 |- ( m e. om -> ( ~P m +c ~P m ) ~~ ~P suc m )
59		entr 8008	. . . . . . . . . 10 |- ( ( ( ( B ` m ) +c ( B ` m ) ) ~~ ( ~P m +c ~P m ) /\ ( ~P m +c ~P m ) ~~ ~P suc m ) -> ( ( B ` m ) +c ( B ` m ) ) ~~ ~P suc m )
60	48, 58, 59	syl2an 494	. . . . . . . . 9 |- ( ( A. k e. suc suc m ( B ` k ) ~~ ~P k /\ m e. om ) -> ( ( B ` m ) +c ( B ` m ) ) ~~ ~P suc m )
61	39	sucex 7011	. . . . . . . . . . . . 13 |- suc m e. _V
62	61	sucid 5804	. . . . . . . . . . . 12 |- suc m e. suc suc m
63		fveq2 6191	. . . . . . . . . . . . . 14 |- ( k = suc m -> ( B ` k ) = ( B ` suc m ) )
64		pweq 4161	. . . . . . . . . . . . . 14 |- ( k = suc m -> ~P k = ~P suc m )
65	63, 64	breq12d 4666	. . . . . . . . . . . . 13 |- ( k = suc m -> ( ( B ` k ) ~~ ~P k <-> ( B ` suc m ) ~~ ~P suc m ) )
66	65	rspcv 3305	. . . . . . . . . . . 12 |- ( suc m e. suc suc m -> ( A. k e. suc suc m ( B ` k ) ~~ ~P k -> ( B ` suc m ) ~~ ~P suc m ) )
67	62, 66	ax-mp 5	. . . . . . . . . . 11 |- ( A. k e. suc suc m ( B ` k ) ~~ ~P k -> ( B ` suc m ) ~~ ~P suc m )
68	67	ensymd 8007	. . . . . . . . . 10 |- ( A. k e. suc suc m ( B ` k ) ~~ ~P k -> ~P suc m ~~ ( B ` suc m ) )
69	68	adantr 481	. . . . . . . . 9 |- ( ( A. k e. suc suc m ( B ` k ) ~~ ~P k /\ m e. om ) -> ~P suc m ~~ ( B ` suc m ) )
70		entr 8008	. . . . . . . . 9 |- ( ( ( ( B ` m ) +c ( B ` m ) ) ~~ ~P suc m /\ ~P suc m ~~ ( B ` suc m ) ) -> ( ( B ` m ) +c ( B ` m ) ) ~~ ( B ` suc m ) )
71	60, 69, 70	syl2anc 693	. . . . . . . 8 |- ( ( A. k e. suc suc m ( B ` k ) ~~ ~P k /\ m e. om ) -> ( ( B ` m ) +c ( B ` m ) ) ~~ ( B ` suc m ) )
72	71	ancoms 469	. . . . . . 7 |- ( ( m e. om /\ A. k e. suc suc m ( B ` k ) ~~ ~P k ) -> ( ( B ` m ) +c ( B ` m ) ) ~~ ( B ` suc m ) )
73		nnfi 8153	. . . . . . . . . . . 12 |- ( m e. om -> m e. Fin )
74		pwfi 8261	. . . . . . . . . . . . 13 |- ( m e. Fin <-> ~P m e. Fin )
75		isfinite 8549	. . . . . . . . . . . . 13 |- ( ~P m e. Fin <-> ~P m ~< om )
76	74, 75	bitri 264	. . . . . . . . . . . 12 |- ( m e. Fin <-> ~P m ~< om )
77	73, 76	sylib 208	. . . . . . . . . . 11 |- ( m e. om -> ~P m ~< om )
78		ensdomtr 8096	. . . . . . . . . . 11 |- ( ( ( B ` m ) ~~ ~P m /\ ~P m ~< om ) -> ( B ` m ) ~< om )
79	46, 77, 78	syl2an 494	. . . . . . . . . 10 |- ( ( A. k e. suc suc m ( B ` k ) ~~ ~P k /\ m e. om ) -> ( B ` m ) ~< om )
80		isfinite 8549	. . . . . . . . . 10 |- ( ( B ` m ) e. Fin <-> ( B ` m ) ~< om )
81	79, 80	sylibr 224	. . . . . . . . 9 |- ( ( A. k e. suc suc m ( B ` k ) ~~ ~P k /\ m e. om ) -> ( B ` m ) e. Fin )
82	81	ancoms 469	. . . . . . . 8 |- ( ( m e. om /\ A. k e. suc suc m ( B ` k ) ~~ ~P k ) -> ( B ` m ) e. Fin )
83	39, 42	iunsuc 5807	. . . . . . . . . . 11 |- U_ k e. suc m ( B ` k ) = ( U_ k e. m ( B ` k ) u. ( B ` m ) )
84		fvex 6201	. . . . . . . . . . . . 13 |- ( B ` k ) e. _V
85	39, 84	iunex 7147	. . . . . . . . . . . 12 |- U_ k e. m ( B ` k ) e. _V
86		fvex 6201	. . . . . . . . . . . 12 |- ( B ` m ) e. _V
87		uncdadom 8993	. . . . . . . . . . . 12 |- ( ( U_ k e. m ( B ` k ) e. _V /\ ( B ` m ) e. _V ) -> ( U_ k e. m ( B ` k ) u. ( B ` m ) ) ~<_ ( U_ k e. m ( B ` k ) +c ( B ` m ) ) )
88	85, 86, 87	mp2an 708	. . . . . . . . . . 11 |- ( U_ k e. m ( B ` k ) u. ( B ` m ) ) ~<_ ( U_ k e. m ( B ` k ) +c ( B ` m ) )
89	83, 88	eqbrtri 4674	. . . . . . . . . 10 |- U_ k e. suc m ( B ` k ) ~<_ ( U_ k e. m ( B ` k ) +c ( B ` m ) )
90		sdomtr 8098	. . . . . . . . . . . . . . . 16 |- ( ( U_ k e. m ( B ` k ) ~< ( B ` m ) /\ ( B ` m ) ~< om ) -> U_ k e. m ( B ` k ) ~< om )
91	80, 90	sylan2b 492	. . . . . . . . . . . . . . 15 |- ( ( U_ k e. m ( B ` k ) ~< ( B ` m ) /\ ( B ` m ) e. Fin ) -> U_ k e. m ( B ` k ) ~< om )
92		isfinite 8549	. . . . . . . . . . . . . . 15 |- ( U_ k e. m ( B ` k ) e. Fin <-> U_ k e. m ( B ` k ) ~< om )
93	91, 92	sylibr 224	. . . . . . . . . . . . . 14 |- ( ( U_ k e. m ( B ` k ) ~< ( B ` m ) /\ ( B ` m ) e. Fin ) -> U_ k e. m ( B ` k ) e. Fin )
94		finnum 8774	. . . . . . . . . . . . . 14 |- ( U_ k e. m ( B ` k ) e. Fin -> U_ k e. m ( B ` k ) e. dom card )
95	93, 94	syl 17	. . . . . . . . . . . . 13 |- ( ( U_ k e. m ( B ` k ) ~< ( B ` m ) /\ ( B ` m ) e. Fin ) -> U_ k e. m ( B ` k ) e. dom card )
96		finnum 8774	. . . . . . . . . . . . . 14 |- ( ( B ` m ) e. Fin -> ( B ` m ) e. dom card )
97	96	adantl 482	. . . . . . . . . . . . 13 |- ( ( U_ k e. m ( B ` k ) ~< ( B ` m ) /\ ( B ` m ) e. Fin ) -> ( B ` m ) e. dom card )
98		cardacda 9020	. . . . . . . . . . . . 13 |- ( ( U_ k e. m ( B ` k ) e. dom card /\ ( B ` m ) e. dom card ) -> ( U_ k e. m ( B ` k ) +c ( B ` m ) ) ~~ ( ( card ` U_ k e. m ( B ` k ) ) +o ( card ` ( B ` m ) ) ) )
99	95, 97, 98	syl2anc 693	. . . . . . . . . . . 12 |- ( ( U_ k e. m ( B ` k ) ~< ( B ` m ) /\ ( B ` m ) e. Fin ) -> ( U_ k e. m ( B ` k ) +c ( B ` m ) ) ~~ ( ( card ` U_ k e. m ( B ` k ) ) +o ( card ` ( B ` m ) ) ) )
100		ficardom 8787	. . . . . . . . . . . . . . . 16 |- ( U_ k e. m ( B ` k ) e. Fin -> ( card ` U_ k e. m ( B ` k ) ) e. om )
101	93, 100	syl 17	. . . . . . . . . . . . . . 15 |- ( ( U_ k e. m ( B ` k ) ~< ( B ` m ) /\ ( B ` m ) e. Fin ) -> ( card ` U_ k e. m ( B ` k ) ) e. om )
102		ficardom 8787	. . . . . . . . . . . . . . . 16 |- ( ( B ` m ) e. Fin -> ( card ` ( B ` m ) ) e. om )
103	102	adantl 482	. . . . . . . . . . . . . . 15 |- ( ( U_ k e. m ( B ` k ) ~< ( B ` m ) /\ ( B ` m ) e. Fin ) -> ( card ` ( B ` m ) ) e. om )
104		cardid2 8779	. . . . . . . . . . . . . . . . . 18 |- ( U_ k e. m ( B ` k ) e. dom card -> ( card ` U_ k e. m ( B ` k ) ) ~~ U_ k e. m ( B ` k ) )
105	93, 94, 104	3syl 18	. . . . . . . . . . . . . . . . 17 |- ( ( U_ k e. m ( B ` k ) ~< ( B ` m ) /\ ( B ` m ) e. Fin ) -> ( card ` U_ k e. m ( B ` k ) ) ~~ U_ k e. m ( B ` k ) )
106		simpl 473	. . . . . . . . . . . . . . . . 17 |- ( ( U_ k e. m ( B ` k ) ~< ( B ` m ) /\ ( B ` m ) e. Fin ) -> U_ k e. m ( B ` k ) ~< ( B ` m ) )
107		cardid2 8779	. . . . . . . . . . . . . . . . . . 19 |- ( ( B ` m ) e. dom card -> ( card ` ( B ` m ) ) ~~ ( B ` m ) )
108		ensym 8005	. . . . . . . . . . . . . . . . . . 19 |- ( ( card ` ( B ` m ) ) ~~ ( B ` m ) -> ( B ` m ) ~~ ( card ` ( B ` m ) ) )
109	96, 107, 108	3syl 18	. . . . . . . . . . . . . . . . . 18 |- ( ( B ` m ) e. Fin -> ( B ` m ) ~~ ( card ` ( B ` m ) ) )
110	109	adantl 482	. . . . . . . . . . . . . . . . 17 |- ( ( U_ k e. m ( B ` k ) ~< ( B ` m ) /\ ( B ` m ) e. Fin ) -> ( B ` m ) ~~ ( card ` ( B ` m ) ) )
111		ensdomtr 8096	. . . . . . . . . . . . . . . . . 18 |- ( ( ( card ` U_ k e. m ( B ` k ) ) ~~ U_ k e. m ( B ` k ) /\ U_ k e. m ( B ` k ) ~< ( B ` m ) ) -> ( card ` U_ k e. m ( B ` k ) ) ~< ( B ` m ) )
112		sdomentr 8094	. . . . . . . . . . . . . . . . . 18 |- ( ( ( card ` U_ k e. m ( B ` k ) ) ~< ( B ` m ) /\ ( B ` m ) ~~ ( card ` ( B ` m ) ) ) -> ( card ` U_ k e. m ( B ` k ) ) ~< ( card ` ( B ` m ) ) )
113	111, 112	sylan 488	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( card ` U_ k e. m ( B ` k ) ) ~~ U_ k e. m ( B ` k ) /\ U_ k e. m ( B ` k ) ~< ( B ` m ) ) /\ ( B ` m ) ~~ ( card ` ( B ` m ) ) ) -> ( card ` U_ k e. m ( B ` k ) ) ~< ( card ` ( B ` m ) ) )
114	105, 106, 110, 113	syl21anc 1325	. . . . . . . . . . . . . . . 16 |- ( ( U_ k e. m ( B ` k ) ~< ( B ` m ) /\ ( B ` m ) e. Fin ) -> ( card ` U_ k e. m ( B ` k ) ) ~< ( card ` ( B ` m ) ) )
115		cardon 8770	. . . . . . . . . . . . . . . . . 18 |- ( card ` U_ k e. m ( B ` k ) ) e. On
116		cardon 8770	. . . . . . . . . . . . . . . . . . 19 |- ( card ` ( B ` m ) ) e. On
117		onenon 8775	. . . . . . . . . . . . . . . . . . 19 |- ( ( card ` ( B ` m ) ) e. On -> ( card ` ( B ` m ) ) e. dom card )
118	116, 117	ax-mp 5	. . . . . . . . . . . . . . . . . 18 |- ( card ` ( B ` m ) ) e. dom card
119		cardsdomel 8800	. . . . . . . . . . . . . . . . . 18 |- ( ( ( card ` U_ k e. m ( B ` k ) ) e. On /\ ( card ` ( B ` m ) ) e. dom card ) -> ( ( card ` U_ k e. m ( B ` k ) ) ~< ( card ` ( B ` m ) ) <-> ( card ` U_ k e. m ( B ` k ) ) e. ( card ` ( card ` ( B ` m ) ) ) ) )
120	115, 118, 119	mp2an 708	. . . . . . . . . . . . . . . . 17 |- ( ( card ` U_ k e. m ( B ` k ) ) ~< ( card ` ( B ` m ) ) <-> ( card ` U_ k e. m ( B ` k ) ) e. ( card ` ( card ` ( B ` m ) ) ) )
121		cardidm 8785	. . . . . . . . . . . . . . . . . 18 |- ( card ` ( card ` ( B ` m ) ) ) = ( card ` ( B ` m ) )
122	121	eleq2i 2693	. . . . . . . . . . . . . . . . 17 |- ( ( card ` U_ k e. m ( B ` k ) ) e. ( card ` ( card ` ( B ` m ) ) ) <-> ( card ` U_ k e. m ( B ` k ) ) e. ( card ` ( B ` m ) ) )
123	120, 122	bitri 264	. . . . . . . . . . . . . . . 16 |- ( ( card ` U_ k e. m ( B ` k ) ) ~< ( card ` ( B ` m ) ) <-> ( card ` U_ k e. m ( B ` k ) ) e. ( card ` ( B ` m ) ) )
124	114, 123	sylib 208	. . . . . . . . . . . . . . 15 |- ( ( U_ k e. m ( B ` k ) ~< ( B ` m ) /\ ( B ` m ) e. Fin ) -> ( card ` U_ k e. m ( B ` k ) ) e. ( card ` ( B ` m ) ) )
125		nnaordr 7700	. . . . . . . . . . . . . . . 16 |- ( ( ( card ` U_ k e. m ( B ` k ) ) e. om /\ ( card ` ( B ` m ) ) e. om /\ ( card ` ( B ` m ) ) e. om ) -> ( ( card ` U_ k e. m ( B ` k ) ) e. ( card ` ( B ` m ) ) <-> ( ( card ` U_ k e. m ( B ` k ) ) +o ( card ` ( B ` m ) ) ) e. ( ( card ` ( B ` m ) ) +o ( card ` ( B ` m ) ) ) ) )
126	125	biimpa 501	. . . . . . . . . . . . . . 15 |- ( ( ( ( card ` U_ k e. m ( B ` k ) ) e. om /\ ( card ` ( B ` m ) ) e. om /\ ( card ` ( B ` m ) ) e. om ) /\ ( card ` U_ k e. m ( B ` k ) ) e. ( card ` ( B ` m ) ) ) -> ( ( card ` U_ k e. m ( B ` k ) ) +o ( card ` ( B ` m ) ) ) e. ( ( card ` ( B ` m ) ) +o ( card ` ( B ` m ) ) ) )
127	101, 103, 103, 124, 126	syl31anc 1329	. . . . . . . . . . . . . 14 |- ( ( U_ k e. m ( B ` k ) ~< ( B ` m ) /\ ( B ` m ) e. Fin ) -> ( ( card ` U_ k e. m ( B ` k ) ) +o ( card ` ( B ` m ) ) ) e. ( ( card ` ( B ` m ) ) +o ( card ` ( B ` m ) ) ) )
128		nnacl 7691	. . . . . . . . . . . . . . . . 17 |- ( ( ( card ` ( B ` m ) ) e. om /\ ( card ` ( B ` m ) ) e. om ) -> ( ( card ` ( B ` m ) ) +o ( card ` ( B ` m ) ) ) e. om )
129	102, 102, 128	syl2anc 693	. . . . . . . . . . . . . . . 16 |- ( ( B ` m ) e. Fin -> ( ( card ` ( B ` m ) ) +o ( card ` ( B ` m ) ) ) e. om )
130		cardnn 8789	. . . . . . . . . . . . . . . 16 |- ( ( ( card ` ( B ` m ) ) +o ( card ` ( B ` m ) ) ) e. om -> ( card ` ( ( card ` ( B ` m ) ) +o ( card ` ( B ` m ) ) ) ) = ( ( card ` ( B ` m ) ) +o ( card ` ( B ` m ) ) ) )
131	129, 130	syl 17	. . . . . . . . . . . . . . 15 |- ( ( B ` m ) e. Fin -> ( card ` ( ( card ` ( B ` m ) ) +o ( card ` ( B ` m ) ) ) ) = ( ( card ` ( B ` m ) ) +o ( card ` ( B ` m ) ) ) )
132	131	adantl 482	. . . . . . . . . . . . . 14 |- ( ( U_ k e. m ( B ` k ) ~< ( B ` m ) /\ ( B ` m ) e. Fin ) -> ( card ` ( ( card ` ( B ` m ) ) +o ( card ` ( B ` m ) ) ) ) = ( ( card ` ( B ` m ) ) +o ( card ` ( B ` m ) ) ) )
133	127, 132	eleqtrrd 2704	. . . . . . . . . . . . 13 |- ( ( U_ k e. m ( B ` k ) ~< ( B ` m ) /\ ( B ` m ) e. Fin ) -> ( ( card ` U_ k e. m ( B ` k ) ) +o ( card ` ( B ` m ) ) ) e. ( card ` ( ( card ` ( B ` m ) ) +o ( card ` ( B ` m ) ) ) ) )
134		cardsdomelir 8799	. . . . . . . . . . . . 13 |- ( ( ( card ` U_ k e. m ( B ` k ) ) +o ( card ` ( B ` m ) ) ) e. ( card ` ( ( card ` ( B ` m ) ) +o ( card ` ( B ` m ) ) ) ) -> ( ( card ` U_ k e. m ( B ` k ) ) +o ( card ` ( B ` m ) ) ) ~< ( ( card ` ( B ` m ) ) +o ( card ` ( B ` m ) ) ) )
135	133, 134	syl 17	. . . . . . . . . . . 12 |- ( ( U_ k e. m ( B ` k ) ~< ( B ` m ) /\ ( B ` m ) e. Fin ) -> ( ( card ` U_ k e. m ( B ` k ) ) +o ( card ` ( B ` m ) ) ) ~< ( ( card ` ( B ` m ) ) +o ( card ` ( B ` m ) ) ) )
136		ensdomtr 8096	. . . . . . . . . . . 12 |- ( ( ( U_ k e. m ( B ` k ) +c ( B ` m ) ) ~~ ( ( card ` U_ k e. m ( B ` k ) ) +o ( card ` ( B ` m ) ) ) /\ ( ( card ` U_ k e. m ( B ` k ) ) +o ( card ` ( B ` m ) ) ) ~< ( ( card ` ( B ` m ) ) +o ( card ` ( B ` m ) ) ) ) -> ( U_ k e. m ( B ` k ) +c ( B ` m ) ) ~< ( ( card ` ( B ` m ) ) +o ( card ` ( B ` m ) ) ) )
137	99, 135, 136	syl2anc 693	. . . . . . . . . . 11 |- ( ( U_ k e. m ( B ` k ) ~< ( B ` m ) /\ ( B ` m ) e. Fin ) -> ( U_ k e. m ( B ` k ) +c ( B ` m ) ) ~< ( ( card ` ( B ` m ) ) +o ( card ` ( B ` m ) ) ) )
138		cardacda 9020	. . . . . . . . . . . . . 14 |- ( ( ( B ` m ) e. dom card /\ ( B ` m ) e. dom card ) -> ( ( B ` m ) +c ( B ` m ) ) ~~ ( ( card ` ( B ` m ) ) +o ( card ` ( B ` m ) ) ) )
139	96, 96, 138	syl2anc 693	. . . . . . . . . . . . 13 |- ( ( B ` m ) e. Fin -> ( ( B ` m ) +c ( B ` m ) ) ~~ ( ( card ` ( B ` m ) ) +o ( card ` ( B ` m ) ) ) )
140	139	ensymd 8007	. . . . . . . . . . . 12 |- ( ( B ` m ) e. Fin -> ( ( card ` ( B ` m ) ) +o ( card ` ( B ` m ) ) ) ~~ ( ( B ` m ) +c ( B ` m ) ) )
141	140	adantl 482	. . . . . . . . . . 11 |- ( ( U_ k e. m ( B ` k ) ~< ( B ` m ) /\ ( B ` m ) e. Fin ) -> ( ( card ` ( B ` m ) ) +o ( card ` ( B ` m ) ) ) ~~ ( ( B ` m ) +c ( B ` m ) ) )
142		sdomentr 8094	. . . . . . . . . . 11 |- ( ( ( U_ k e. m ( B ` k ) +c ( B ` m ) ) ~< ( ( card ` ( B ` m ) ) +o ( card ` ( B ` m ) ) ) /\ ( ( card ` ( B ` m ) ) +o ( card ` ( B ` m ) ) ) ~~ ( ( B ` m ) +c ( B ` m ) ) ) -> ( U_ k e. m ( B ` k ) +c ( B ` m ) ) ~< ( ( B ` m ) +c ( B ` m ) ) )
143	137, 141, 142	syl2anc 693	. . . . . . . . . 10 |- ( ( U_ k e. m ( B ` k ) ~< ( B ` m ) /\ ( B ` m ) e. Fin ) -> ( U_ k e. m ( B ` k ) +c ( B ` m ) ) ~< ( ( B ` m ) +c ( B ` m ) ) )
144		domsdomtr 8095	. . . . . . . . . 10 |- ( ( U_ k e. suc m ( B ` k ) ~<_ ( U_ k e. m ( B ` k ) +c ( B ` m ) ) /\ ( U_ k e. m ( B ` k ) +c ( B ` m ) ) ~< ( ( B ` m ) +c ( B ` m ) ) ) -> U_ k e. suc m ( B ` k ) ~< ( ( B ` m ) +c ( B ` m ) ) )
145	89, 143, 144	sylancr 695	. . . . . . . . 9 |- ( ( U_ k e. m ( B ` k ) ~< ( B ` m ) /\ ( B ` m ) e. Fin ) -> U_ k e. suc m ( B ` k ) ~< ( ( B ` m ) +c ( B ` m ) ) )
146	145	expcom 451	. . . . . . . 8 |- ( ( B ` m ) e. Fin -> ( U_ k e. m ( B ` k ) ~< ( B ` m ) -> U_ k e. suc m ( B ` k ) ~< ( ( B ` m ) +c ( B ` m ) ) ) )
147	82, 146	syl 17	. . . . . . 7 |- ( ( m e. om /\ A. k e. suc suc m ( B ` k ) ~~ ~P k ) -> ( U_ k e. m ( B ` k ) ~< ( B ` m ) -> U_ k e. suc m ( B ` k ) ~< ( ( B ` m ) +c ( B ` m ) ) ) )
148		sdomentr 8094	. . . . . . . 8 |- ( ( U_ k e. suc m ( B ` k ) ~< ( ( B ` m ) +c ( B ` m ) ) /\ ( ( B ` m ) +c ( B ` m ) ) ~~ ( B ` suc m ) ) -> U_ k e. suc m ( B ` k ) ~< ( B ` suc m ) )
149	148	expcom 451	. . . . . . 7 |- ( ( ( B ` m ) +c ( B ` m ) ) ~~ ( B ` suc m ) -> ( U_ k e. suc m ( B ` k ) ~< ( ( B ` m ) +c ( B ` m ) ) -> U_ k e. suc m ( B ` k ) ~< ( B ` suc m ) ) )
150	72, 147, 149	sylsyld 61	. . . . . 6 |- ( ( m e. om /\ A. k e. suc suc m ( B ` k ) ~~ ~P k ) -> ( U_ k e. m ( B ` k ) ~< ( B ` m ) -> U_ k e. suc m ( B ` k ) ~< ( B ` suc m ) ) )
151	38, 150	syld 47	. . . . 5 |- ( ( m e. om /\ A. k e. suc suc m ( B ` k ) ~~ ~P k ) -> ( ( A. k e. suc m ( B ` k ) ~~ ~P k -> U_ k e. m ( B ` k ) ~< ( B ` m ) ) -> U_ k e. suc m ( B ` k ) ~< ( B ` suc m ) ) )
152	151	ex 450	. . . 4 |- ( m e. om -> ( A. k e. suc suc m ( B ` k ) ~~ ~P k -> ( ( A. k e. suc m ( B ` k ) ~~ ~P k -> U_ k e. m ( B ` k ) ~< ( B ` m ) ) -> U_ k e. suc m ( B ` k ) ~< ( B ` suc m ) ) ) )
153	152	com23 86	. . 3 |- ( m e. om -> ( ( A. k e. suc m ( B ` k ) ~~ ~P k -> U_ k e. m ( B ` k ) ~< ( B ` m ) ) -> ( A. k e. suc suc m ( B ` k ) ~~ ~P k -> U_ k e. suc m ( B ` k ) ~< ( B ` suc m ) ) ) )
154	6, 12, 18, 32, 153	finds1 7095	. 2 |- ( n e. om -> ( A. k e. suc n ( B ` k ) ~~ ~P k -> U_ k e. n ( B ` k ) ~< ( B ` n ) ) )
155	154	imp 445	1 |- ( ( n e. om /\ A. k e. suc n ( B ` k ) ~~ ~P k ) -> U_ k e. n ( B ` k ) ~< ( B ` n ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   /\ wa 384   /\ w3a 1037   = wceq 1483   e. wcel 1990   A.wral 2912   _Vcvv 3200   u. cun 3572   C_ wss 3574   (/)c0 3915   ~Pcpw 4158   U_ciun 4520   class class class wbr 4653   dom cdm 5114   Ord word 5722   Oncon0 5723   suc csuc 5725   ` cfv 5888  (class class class)co 6650   omcom 7065   1oc1o 7553   +o coa 7557   ~~ cen 7952   ~<_ cdom 7953   ~< csdm 7954   Fincfn 7955   cardccrd 8761   +c ccda 8989

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-inf2 8538

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-2o 7561  df-oadd 7564  df-er 7742  df-map 7859  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-card 8765  df-cda 8990

This theorem is referenced by:  domtriomlem  9264