Theorem unidom 4791

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.1	. . . . . . 7 |- A e. V
2	1	uniex 2866	. . . . . 6 |- U.A e. V
3		id 59	. . . . . . . . . . . . . 14 |- (x = y -> x = y)
4		fveq2 3719	. . . . . . . . . . . . . 14 |- (x = y -> (h` x) = (h` y))
5	3, 4	eleq12d 1540	. . . . . . . . . . . . 13 |- (x = y -> (x e. (h` x) <-> y e. (h` y)))
6	4	eleq1d 1538	. . . . . . . . . . . . 13 |- (x = y -> ((h` x) e. A <-> (h` y) e. A))
7	5, 6	anbi12d 627	. . . . . . . . . . . 12 |- (x = y -> ((x e. (h` x) /\ (h` x) e. A) <-> (y e. (h` y) /\ (h` y) e. A)))
8	7	rcla4cv 1871	. . . . . . . . . . 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)))
9		pm3.27 323	. . . . . . . . . . 11 |- ((y e. (h` y) /\ (h` y) e. A) -> (h` y) e. A)
10	8, 9	syl6 22	. . . . . . . . . 10 |- (A.x e. U.A(x e. (h` x) /\ (h` x) e. A) -> (y e. U.A -> (h` y) e. A))
11	10	adantl 388	. . . . . . . . 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))
12		fveq2 3719	. . . . . . . . . . . . . . . . 17 |- (x = (h` y) -> (f` x) = (f` (h` y)))
13		f1eq1 3655	. . . . . . . . . . . . . . . . 17 |- ((f` x) = (f` (h` y)) -> ((f` x):x-1-1->B <-> (f` (h` y)):x-1-1->B))
14	12, 13	syl 10	. . . . . . . . . . . . . . . 16 |- (x = (h` y) -> ((f` x):x-1-1->B <-> (f` (h` y)):x-1-1->B))
15		f1eq2 3656	. . . . . . . . . . . . . . . 16 |- (x = (h` y) -> ((f` (h` y)):x-1-1->B <-> (f` (h` y)):(h` y)-1-1->B))
16	14, 15	bitrd 527	. . . . . . . . . . . . . . 15 |- (x = (h` y) -> ((f` x):x-1-1->B <-> (f` (h` y)):(h` y)-1-1->B))
17	16	rcla4v 1870	. . . . . . . . . . . . . 14 |- ((h` y) e. A -> (A.x e. A (f` x):x-1-1->B -> (f` (h` y)):(h` y)-1-1->B))
18		f1f 3660	. . . . . . . . . . . . . 14 |- ((f` (h` y)):(h` y)-1-1->B -> (f` (h` y)):(h` y)-->B)
19	17, 18	syl6 22	. . . . . . . . . . . . 13 |- ((h` y) e. A -> (A.x e. A (f` x):x-1-1->B -> (f` (h` y)):(h` y)-->B))
20		ffvelrn 3809	. . . . . . . . . . . . . 14 |- (((f` (h` y)):(h` y)-->B /\ y e. (h` y)) -> ((f` (h` y))` y) e. B)
21	20	expcom 374	. . . . . . . . . . . . 13 |- (y e. (h` y) -> ((f` (h` y)):(h` y)-->B -> ((f` (h` y))` y) e. B))
22	19, 21	sylan9r 469	. . . . . . . . . . . 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))
23	8, 22	syl6 22	. . . . . . . . . . 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)))
24	23	com3r 35	. . . . . . . . . 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)))
25	24	imp 350	. . . . . . . . 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))
26	11, 25	jcad 599	. . . . . . . 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)))
27		opelxpi 3213	. . . . . . . 8 |- (((h` y) e. A /\ ((f` (h` y))` y) e. B) -> <.(h` y), ((f` (h` y))` y)>. e. (A X. B))
28	26, 27	syl6 22	. . . . . . 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)))
29		fveq2 3719	. . . . . . . . . . . . . . . 16 |- ((h` y) = (h` z) -> (f` (h` y)) = (f` (h` z)))
30	29	fveq1d 3721	. . . . . . . . . . . . . . 15 |- ((h` y) = (h` z) -> ((f` (h` y))` z) = ((f` (h` z))` z))
31	30	eqeq2d 1484	. . . . . . . . . . . . . 14 |- ((h` y) = (h` z) -> (((f` (h` y))` y) = ((f` (h` y))` z) <-> ((f` (h` y))` y) = ((f` (h` z))` z)))
32	31	adantl 388	. . . . . . . . . . . . 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))` y) = ((f` (h` y))` z) <-> ((f` (h` y))` y) = ((f` (h` z))` z)))
33		f1fveq 3871	. . . . . . . . . . . . . . 15 |- (((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))
34	33	biimpd 153	. . . . . . . . . . . . . 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))
35	17	adantl 388	. . . . . . . . . . . . . . . . . . 19 |- ((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))
36	8, 35	syl6 22	. . . . . . . . . . . . . . . . . 18 |- (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)))
37	36	com3r 35	. . . . . . . . . . . . . . . . 17 |- (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)))
38	37	imp31 362	. . . . . . . . . . . . . . . 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)
39	38	adantrr 395	. . . . . . . . . . . . . . 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 /\ z e. U.A)) -> (f` (h` y)):(h` y)-1-1->B)
40	39	adantr 389	. . . . . . . . . . . . . 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)) /\ (h` y) = (h` z)) -> (f` (h` y)):(h` y)-1-1->B)
41		pm3.26 319	. . . . . . . . . . . . . . . . . . . 20 |- ((y e. (h` y) /\ (h` y) e. A) -> y e. (h` y))
42	8, 41	syl6 22	. . . . . . . . . . . . . . . . . . 19 |- (A.x e. U.A(x e. (h` x) /\ (h` x) e.