Theorem unidom 5970

Description: An upper bound for the cardinality of a union. Theorem 10.47 of [TakeutiZaring] p. 98.

Hypotheses

Ref	Expression
unidom.1	|- A e. _V
unidom.2	|- B e. _V

Assertion

Ref	Expression
unidom	|- (A.x e. A x ~<_ B -> U.A ~<_ (A X. B))

Distinct variable groups:   x,A   x,B

Proof of Theorem unidom

Step	Hyp	Ref	Expression
1		unidom.2	. . . . 5 |- B e. _V
2	1	brdom 5437	. . . 4 |- (x ~<_ B <-> E.g g:x-1-1->B)
3	2	ralbii 2127	. . 3 |- (A.x e. A x ~<_ B <-> A.x e. A E.g g:x-1-1->B)
4		unidom.1	. . . 4 |- A e. _V
5		f1eq1 4605	. . . 4 |- (g = (f` x) -> (g:x-1-1->B <-> (f` x):x-1-1->B))
6	4, 5	ac6s3 5921	. . 3 |- (A.x e. A E.g g:x-1-1->B -> E.fA.x e. A (f` x):x-1-1->B)
7	3, 6	sylbi 216	. 2 |- (A.x e. A x ~<_ B -> E.fA.x e. A (f` x):x-1-1->B)
8	4	uniex 3794	. . . . 5 |- U.A e. _V
9		eleq2 1958	. . . . . 6 |- (g = (h` x) -> (x e. g <-> x e. (h` x)))
10		eleq1 1957	. . . . . 6 |- (g = (h` x) -> (g e. A <-> (h` x) e. A))
11	9, 10	anbi12d 690	. . . . 5 |- (g = (h` x) -> ((x e. g /\ g e. A) <-> (x e. (h` x) /\ (h` x) e. A)))
12	8, 11	ac6s3 5921	. . . 4 |- (A.x e. U.AE.g(x e. g /\ g e. A) -> E.hA.x e. U.A(x e. (h` x) /\ (h` x) e. A))
13		eluni 3180	. . . . 5 |- (x e. U.A <-> E.g(x e. g /\ g e. A))
14	13	biimpi 168	. . . 4 |- (x e. U.A -> E.g(x e. g /\ g e. A))
15	12, 14	mprg 2162	. . 3 |- E.hA.x e. U.A(x e. (h` x) /\ (h` x) e. A)
16	15	a1i 8	. 2 |- (A.x e. A x ~<_ B -> E.hA.x e. U.A(x e. (h` x) /\ (h` x) e. A))
17		id 73	. . . . . . . . . . . . . 14 |- (x = y -> x = y)
18		fveq2 4681	. . . . . . . . . . . . . 14 |- (x = y -> (h` x) = (h` y))
19	17, 18	eleq12d 1965	. . . . . . . . . . . . 13 |- (x = y -> (x e. (h` x) <-> y e. (h` y)))
20	18	eleq1d 1963	. . . . . . . . . . . . 13 |- (x = y -> ((h` x) e. A <-> (h` y) e. A))
21	19, 20	anbi12d 690	. . . . . . . . . . . 12 |- (x = y -> ((x e. (h` x) /\ (h` x) e. A) <-> (y e. (h` y) /\ (h` y) e. A)))
22	21	rcla4cv 2377	. . . . . . . . . . 11 |- (A.x e. U.A(x e. (h` x) /\ (h` x) e. A) -> (y e. U.A -> (y e. (h` y) /\ (h` y) e. A)))
23		simpr 350	. . . . . . . . . . 11 |- ((y e. (h` y) /\ (h` y) e. A) -> (h` y) e. A)
24	22, 23	syl6 25	. . . . . . . . . 10 |- (A.x e. U.A(x e. (h` x) /\ (h` x) e. A) -> (y e. U.A -> (h` y) e. A))
25	24	adantl 424	. . . . . . . . 9 |- ((A.x e. A (f` x):x-1-1->B /\ A.x e. U.A(x e. (h` x) /\ (h` x) e. A)) -> (y e. U.A -> (h` y) e. A))
26		fveq2 4681	. . . . . . . . . . . . . . . . 17 |- (x = (h` y) -> (f` x) = (f` (h` y)))
27		f1eq1 4605	. . . . . . . . . . . . . . . . 17 |- ((f` x) = (f` (h` y)) -> ((f` x):x-1-1->B <-> (f` (h` y)):x-1-1->B))
28	26, 27	syl 12	. . . . . . . . . . . . . . . 16 |- (x = (h` y) -> ((f` x):x-1-1->B <-> (f` (h` y)):x-1-1->B))
29		f1eq2 4606	. . . . . . . . . . . . . . . 16 |- (x = (h` y) -> ((f` (h` y)):x-1-1->B <-> (f` (h` y)):(h` y)-1-1->B))
30	28, 29	bitrd 587	. . . . . . . . . . . . . . 15 |- (x = (h` y) -> ((f` x):x-1-1->B <-> (f` (h` y)):(h` y)-1-1->B))
31	30	rcla4v 2376	. . . . . . . . . . . . . 14 |- ((h` y) e. A -> (A.x e. A (f` x):x-1-1->B -> (f` (h` y)):(h` y)-1-1->B))
32		f1f 4610	. . . . . . . . . . . . . 14 |- ((f` (h` y)):(h` y)-1-1->B -> (f` (h` y)):(h` y)-->B)
33	31, 32	syl6 25	. . . . . . . . . . . . 13 |- ((h` y) e. A -> (A.x e. A (f` x):x-1-1->B -> (f` (h` y)):(h` y)-->B))
34		ffvelrn 4787	. . . . . . . . . . . . . 14 |- (((f` (h` y)):(h` y)-->B /\ y e. (h` y)) -> ((f` (h` y))` y) e. B)
35	34	expcom 403	. . . . . . . . . . . . 13 |- (y e. (h` y) -> ((f` (h` y)):(h` y)-->B -> ((f` (h` y))` y) e. B))
36	33, 35	sylan9r 519	. . . . . . . . . . . 12 |- ((y e. (h` y) /\ (h` y) e. A) -> (A.x e. A (f` x):x-1-1->B -> ((f` (h` y))` y) e. B))
37	22, 36	syl6 25	. . . . . . . . . . 11 |- (A.x e. U.A(x e. (h` x) /\ (h` x) e. A) -> (y e. U.A -> (A.x e. A (f` x):x-1-1->B -> ((f` (h` y))` y) e. B)))
38	37	com3r 39	. . . . . . . . . 10 |- (A.x e. A (f` x):x-1-1->B -> (A.x e. U.A(x e. (h` x) /\ (h` x) e. A) -> (y e. U.A -> ((f` (h` y))` y) e. B)))
39	38	imp 377	. . . . . . . . 9 |- ((A.x e. A (f` x):x-1-1->B /\ A.x e. U.A(x e. (h` x) /\ (h` x) e. A)) -> (y e. U.A -> ((f` (h` y))` y) e. B))
40	25, 39	jcad 661	. . . . . . . 8 |- ((A.x e. A (f` x):x-1-1->B /\ A.x e. U.A(x e. (h` x) /\ (h` x) e. A)) -> (y e. U.A -> ((h` y) e. A /\ ((f` (h` y))` y) e. B)))
41		opelxpi 4040	. . . . . . . 8 |- (((h` y) e. A /\ ((f` (h` y))` y) e. B) -> <.(h` y), ((f` (h` y))` y)>. e. (A X. B))
42	40, 41	syl6 25	. . . . . . 7 |- ((A.x e. A (f` x):x-1-1->B /\ A.x e. U.A(x e. (h` x) /\ (h` x) e. A)) -> (y e. U.A -> <.(h` y), ((f` (h` y))` y)>. e. (A X. B)))
43		fveq2 4681	. . . . . . . . . . . . . . 15 |- ((h` y) = (h` z) -> (f` (h` y)) = (f` (h` z)))
44	43	fveq1d 4683	. . . . . . . . . . . . . 14 |- ((h` y) = (h` z) -> ((f` (h` y))` z) = ((f` (h` z))` z))
45	44	eqeq2d 1895	. . . . . . . . . . . . 13 |- ((h` y) = (h` z) -> (((f` (h` y))` y) = ((f` (h` y))` z) <-> ((f` (h` y))` y) = ((f` (h` z))` z)))
46	45	adantl 424	. . . . . . . . . . . 12 |- ((((A.x e. A (f` x):x-1-1->B /\ A.x e. U.A(x e. (h` x) /\ (h` x) e. A)) /\ (y e. U.A /\ z e. U.A)) /\ (h` y) = (h` z)) -> (((f` (h` y))` y) = ((f` (h` y))` z) <-> ((f` (h` y))` y) = ((f` (h` z))` z)))
47	31	adantl 424	. . . . . . . . . . . . . . . . . 18 |- ((y e. (h` y) /\ (h` y) e. A) -> (A.x e. A (f` x):x-1-1->B -> (f` (h` y)):(h` y)-1-1->B))
48	22, 47	syl6 25	. . . . . . . . . . . . . . . . 17 |- (A.x e. U.A(x e. (h` x) /\ (h` x) e. A) -> (y e. U.A -> (A.x e. A (f` x):x-1-1->B -> (f` (h` y)):(h` y)-1-1->B)))
49	48	com3r 39	. . . . . . . . . . . . . . . 16 |- (A.x e. A (f` x):x-1-1->B -> (A.x e. U.A(x e. (h` x) /\ (h` x) e. A) -> (y e. U.A -> (f` (h` y)):(h` y)-1-1->B)))
50	49	imp31 389	. . . . . . . . . . . . . . 15 |- (((A.x e. A (f` x):x-1-1->B /\ A.x e. U.A(x e. (h` x) /\ (h` x) e. A)) /\ y e. U.A) -> (f` (h` y)):(h` y)-1-1->B)
51	50	adantrr 431	. . . . . . . . . . . . . 14 |- (((A.x e. A (f` x):x-1-1->B /\ A.x e. U.A(x e. (h` x) /\ (h` x) e. A)) /\ (y e. U.A /\ z e. U.A)) -> (f` (h` y)):(h` y)-1-1->B)
52	51	adantr 425	. . . . . . . . . . . . 13 |- ((((A.x e. A (f` x):x-1-1->B /\ A.x e. U.A(x e. (h` x) /\ (h` x) e. A)) /\ (y e. U.A /\ z e. U.A)) /\ (h` y) = (h` z)) -> (f` (h` y)):(h` y)-1-1->B)
53		simpl 346	. . . . . . . . . . . . . . . . . . 19 |- ((y e. (h` y) /\ (h` y) e. A) -> y e. (h` y))
54	22, 53	syl6 25	. . . . . . . . . . . . . . . . . 18 |- (A.x e. U.A(x e. (h` x) /\ (h` x) e. A) -> (y e. U.A -> y e. (h` y)))
55	54	adantr 425	. . . . . . . . . . . . . . . . 17 |- ((A.x e. U.A(x e. (h` x) /\ (h` x) e. A) /\ (h` y) = (h` z)) -> (y e. U.A -> y e. (h` y)))
56		id 73	. . . . . . . . . . . . . . . . . . . . . 22 |- (x = z -> x = z)
57		fveq2 4681	. . . . . . . . . . . . . . . . . . . . . 22 |- (x = z -> (h` x) = (h` z))
58	56, 57	eleq12d 1965	. . . . . . . . . . . . . . . . . . . . 21 |- (x = z -> (x e. (h` x) <-> z e. (h` z)))
59	57	eleq1d 1963	. . . . . . . . . . . . . . . . . . . . 21 |- (x = z -> ((h` x) e. A <-> (h` z) e. A))
60	58, 59	anbi12d 690	. . . . . . . . . . . . . . . . . . . 20 |- (x = z -> ((x e. (h` x) /\ (h` x) e. A) <-> (z e. (h` z) /\ (h` z) e. A)))
61	60	rcla4cv 2377	. . . . . . . . . . . . . . . . . . 19 |- (A.x e. U.A(x e. (h` x) /\ (h` x) e. A) -> (z e. U.A -> (z e. (h` z) /\ (h` z) e. A)))
62		simpl 346	. . . . . . . . . . . . . . . . . . 19 |- ((z e. (h` z) /\ (h` z) e. A) -> z e. (h` z))
63	61, 62	syl6 25	. . . . . . . . . . . . . . . . . 18 |- (A.x e. U.A(x e. (h` x) /\ (h` x) e. A) -> (z e. U.A -> z e. (h` z)))
64		eleq2 1958	. . . . . . . . . . . . . . . . . . 19 |- ((h` y) = (h` z) -> (z e. (h` y) <-> z e. (h` z)))
65	64	biimprd 171	. . . . . . . . . . . . . . . . . 18 |- ((h` y) = (h` z) -> (z e. (h` z) -> z e. (h` y)))
66	63, 65	sylan9 517	. . . . . . . . . . . . . . . . 17 |- ((A.x e. U.A(x e. (h` x) /\ (h` x) e. A) /\ (h` y) = (h` z)) -> (z e. U.A -> z e. (h` y)))
67	55, 66	anim12d 617	. . . . . . . . . . . . . . . 16 |- ((A.x e. U.A(x e. (h` x) /\ (h` x) e. A) /\ (h` y) = (h` z)) -> ((y e. U.A /\ z e. U.A) -> (y e. (h` y) /\ z e. (h` y))))
68	67	imp 377	. . . . . . . . . . . . . . 15 |- (((A.x e. U.A(x e. (h` x) /\ (h` x) e. A) /\ (h` y) = (h` z)) /\ (y e. U.A /\ z e. U.A)) -> (y e. (h` y) /\ z e. (h` y)))
69	68	an1rs 547	. . . . . . . . . . . . . 14 |- (((A.x e. U.A(x e. (h` x) /\ (h` x) e. A) /\ (y e. U.A /\ z e. U.A)) /\ (h` y) = (h` z)) -> (y e. (h` y) /\ z e. (h` y)))
70	69	adantlll 432	. . . . . . . . . . . . 13 |- ((((A.x e. A (f` x):x-1-1->B /\ A.x e. U.A(x e. (h` x) /\ (h` x) e. A)) /\ (y e. U.A /\ z e. U.A)) /\ (h` y) = (h` z)) -> (y e. (h` y) /\ z e. (h` y)))
71		f1fveq 4852	. . . . . . . . . . . . . 14 |- (((f` (h` y)):(h` y)-1-1->B /\ (y e. (h` y) /\ z e. (h` y))) -> (((f` (h` y))` y) = ((f` (h` y))` z) <-> y = z))
72	71	biimpd 170	. . . . . . . . . . . . 13 |- (((f` (h` y)):(h` y)-1-1->B /\ (y e. (h` y) /\ z e. (h` y))) -> (((f` (h` y))` y) = ((f` (h` y))` z) -> y = z))
73	52, 70, 72	syl11anc 524	. . . . . . . . . . . 12 |- ((((A.x e. A (f` x):x-1-1->B /\ A.x e. U.A(x e. (h` x) /\ (h` x) e. A)) /\ (y e. U.A /\ z e. U.A)) /\ (h` y) = (h` z)) -> (((f` (h` y))` y) = ((f` (h` y))` z) -> y = z))
74	46, 73	sylbird 222	. . . . . . . . . . 11 |- ((((A.x e. A (f` x):x-1-1->B /\ A.x e. U.A(x e. (h` x) /\ (h` x) e. A)) /\ (y e. U.A /\ z e. U.A)) /\ (h` y) = (h` z)) -> (((f` (h` y))` y) = ((f` (h` z))` z) -> y = z))
75	74	expimpd 404	. . . . . . . . . 10 |- (((A.x e. A (f` x):x-1-1->B /\ A.x e. U.A(x e. (h` x) /\ (h` x) e. A)) /\ (y e. U.A /\ z e. U.A)) -> (((h` y) = (h` z) /\ ((f` (h` y))` y) = ((f` (h` z))` z)) -> y = z))
76		fvex 4689	. . . . . . . . . . 11 |- (h` y) e. _V
77		fvex 4689	. . . . . . . . . . 11 |- ((f` (h` y))` y) e. _V
78		fvex 4689	. . . . . . . . . . 11 |- ((f` (h` z))` z) e. _V
79	76, 77, 78	opth 3532	. . . . . . . . . 10 |- (<.(h` y), ((f` (h` y))` y)>. = <.(h` z), ((f` (h` z))` z)>. <-> ((h` y) = (h` z) /\ ((f` (h` y))` y) = ((f` (h` z))` z)))
80	75, 79	syl5ib 223	. . . . . . . . 9 |- (((A.x e. A (f` x):x-1-1->B /\ A.x e. U.A(x e. (h` x) /\ (h` x) e. A)) /\ (y e. U.A /\ z e. U.A)) -> (<.(h` y), ((f` (h` y))` y)>. = <.(h` z), ((f` (h` z))` z)>. -> y = z))
81		fveq2 4681	. . . . . . . . . 10 |- (y = z -> (h` y) = (h` z))
82	81	fveq2d 4685	. . . . . . . . . . . 12 |- (y = z -> (f` (h` y)) = (f` (h` z)))
83	82	fveq1d 4683	. . . . . . . . . . 11 |- (y = z -> ((f` (h` y))` y) = ((f` (h` z))` y))
84		fveq2 4681	. . . . . . . . . . 11 |- (y = z -> ((f` (h` z))` y) = ((f` (h` z))` z))
85	83, 84	eqtrd 1925	. . . . . . . . . 10 |- (y = z -> ((f` (h` y))` y) = ((f` (h` z))` z))
86	81, 85	opeq12d 3166	. . . . . . . . 9 |- (y = z -> <.(h` y), ((f` (h` y))` y)>. = <.(h` z), ((f` (h` z))` z)>.)
87	80, 86	impbid1 575	. . . . . . . 8 |- (((A.x e. A (f` x):x-1-1->B /\ A.x e. U.A(x e. (h` x) /\ (h` x) e. A)) /\ (y e. U.A /\ z e. U.A)) -> (<.(h` y), ((f` (h` y))` y)>. = <.(h` z), ((f` (h` z))` z)>. <-> y = z))
88	87	ex 402	. . . . . . 7 |- ((A.x e. A (f` x):x-1-1->B /\ A.x e. U.A(x e. (h` x) /\ (h` x) e. A)) -> ((y e. U.A /\ z e. U.A) -> (<.(h` y), ((f` (h` y))` y)>. = <.(h` z), ((f` (h` z))` z)>. <-> y = z)))
89	42, 88	dom2d 5463	. . . . . 6 |- ((A.x e. A (f` x):x-1-1->B /\ A.x e. U.A(x e. (h` x) /\ (h` x) e. A)) -> (U.A e. _V -> U.A ~<_ (A X. B)))
90	8, 89	mpi 55	. . . . 5 |- ((A.x e. A (f` x):x-1-1->B /\ A.x e. U.A(x e. (h` x) /\ (h` x) e. A)) -> U.A ~<_ (A X. B))
91	90	ex 402	. . . 4 |- (A.x e. A (f` x):x-1-1->B -> (A.x e. U.A(x e. (h` x) /\ (h` x) e. A) -> U.A ~<_ (A X. B)))
92	91	19.23adv 1584	. . 3 |- (A.x e. A (f` x):x-1-1->B -> (E.hA.x e. U.A(x e. (h` x) /\ (h` x) e. A) -> U.A ~<_ (A X. B)))
93	92	19.23aiv 1674	. 2 |- (E.fA.x e. A (f` x):x-1-1->B -> (E.hA.x e. U.A(x e. (h` x) /\ (h` x) e. A) -> U.A ~<_ (A X. B)))
94	7, 16, 93	sylc 83	1 |- (A.x e. A x ~<_ B -> U.A ~<_ (A X. B))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   = wceq 1298   e. wcel 1300  E.wex 1326  A.wral 2105  _Vcvv 2292  <.cop 3046  U.cuni 3177   class class class wbr 3338   X. cxp 3984  -->wf 3994  -1-1->wf1 3995  ` cfv 3998   ~<_ cdom 5424

This theorem is referenced by:  unidomg 5971

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790  ax-reg 5695  ax-inf2 5731  ax-ac 5906

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3or 859  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-reu 2111  df-rab 2112  df-v 2294  df-sbc 2454  df-csb 2541  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-pss 2607  df-nul 2876  df-if 2983  df-pw 3035  df-sn 3049  df-pr 3050  df-tp 3052  df-op 3053  df-uni 3178  df-int 3215  df-iun 3257  df-iin 3258  df-br 3339  df-opab 3396  df-tr 3412  df-eprel 3583  df-id 3586  df-po 3591  df-so 3604  df-fr 3625  df-we 3644  df-ord 3660  df-on 3661  df-lim 3662  df-suc 3663  df-om 3950  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-f1 4011  df-fo 4012  df-f1o 4013  df-fv 4014  df-rdg 5140  df-en 5427  df-dom 5428  df-r1 5750  df-rank 5751

Copyright terms: Public domain