Theorem mapunen 4488

Description: Equinumerosity law for set exponentiation of a disjoint union. Exercise 4.45 of [Mendelson] p. 255.

Hypotheses

Ref	Expression
mapunen.1	|- A e. V
mapunen.2	|- B e. V
mapunen.3	|- C e. V

Assertion

Ref	Expression
mapunen	|- ((A i^i B) = (/) -> (C ^m (A u. B)) ~~ ((C ^m A) X. (C ^m B)))

Proof of Theorem mapunen

Step	Hyp	Ref	Expression
1		oprex 3974	. . 3 |- (C ^m (A u. B)) e. V
2	1	a1i 8	. 2 |- ((A i^i B) = (/) -> (C ^m (A u. B)) e. V)
3		ssun1 2189	. . . . . . 7 |- A (_ (A u. B)
4		fssres 3634	. . . . . . 7 |- ((x:(A u. B)-->C /\ A (_ (A u. B)) -> (x |` A):A-->C)
5	3, 4	mpan2 695	. . . . . 6 |- (x:(A u. B)-->C -> (x |` A):A-->C)
6		mapunen.3	. . . . . . 7 |- C e. V
7		mapunen.1	. . . . . . 7 |- A e. V
8	6, 7	elmap 4324	. . . . . 6 |- ((x |` A) e. (C ^m A) <-> (x |` A):A-->C)
9	5, 8	sylibr 200	. . . . 5 |- (x:(A u. B)-->C -> (x |` A) e. (C ^m A))
10		ssun2 2190	. . . . . . 7 |- B (_ (A u. B)
11		fssres 3634	. . . . . . 7 |- ((x:(A u. B)-->C /\ B (_ (A u. B)) -> (x |` B):B-->C)
12	10, 11	mpan2 695	. . . . . 6 |- (x:(A u. B)-->C -> (x |` B):B-->C)
13		mapunen.2	. . . . . . 7 |- B e. V
14	6, 13	elmap 4324	. . . . . 6 |- ((x |` B) e. (C ^m B) <-> (x |` B):B-->C)
15	12, 14	sylibr 200	. . . . 5 |- (x:(A u. B)-->C -> (x |` B) e. (C ^m B))
16	9, 15	jca 288	. . . 4 |- (x:(A u. B)-->C -> ((x |` A) e. (C ^m A) /\ (x |` B) e. (C ^m B)))
17	7, 13	unex 2867	. . . . 5 |- (A u. B) e. V
18	6, 17	elmap 4324	. . . 4 |- (x e. (C ^m (A u. B)) <-> x:(A u. B)-->C)
19		visset 1809	. . . . . 6 |- x e. V
20		resexg 3386	. . . . . 6 |- (x e. V -> (x |` B) e. V)
21	19, 20	ax-mp 7	. . . . 5 |- (x |` B) e. V
22	21	opelxp 3209	. . . 4 |- (<.(x |` A), (x |` B)>. e. ((C ^m A) X. (C ^m B)) <-> ((x |` A) e. (C ^m A) /\ (x |` B) e. (C ^m B)))
23	16, 18, 22	3imtr4 219	. . 3 |- (x e. (C ^m (A u. B)) -> <.(x |` A), (x |` B)>. e. ((C ^m A) X. (C ^m B)))
24	23	a1i 8	. 2 |- ((A i^i B) = (/) -> (x e. (C ^m (A u. B)) -> <.(x |` A), (x |` B)>. e. ((C ^m A) X. (C ^m B))))
25		fun 3632	. . . . 5 |- (((|^||^|y:A-->C /\ U.ran { y}:B-->C) /\ (A i^i B) = (/)) -> (|^||^|y u. U.ran { y}):(A u. B)-->(C u. C))
26	6, 17	elmap 4324	. . . . . 6 |- ((|^||^|y u. U.ran { y}) e. (C ^m (A u. B)) <-> (|^||^|y u. U.ran { y}):(A u. B)-->C)
27		unidm 2171	. . . . . . 7 |- (C u. C) = C
28		feq3 3614	. . . . . . 7 |- ((C u. C) = C -> ((|^||^|y u. U.ran { y}):(A u. B)-->(C u. C) <-> (|^||^|y u. U.ran { y}):(A u. B)-->C))
29	27, 28	ax-mp 7	. . . . . 6 |- ((|^||^|y u. U.ran { y}):(A u. B)-->(C u. C) <-> (|^||^|y u. U.ran { y}):(A u. B)-->C)
30	26, 29	bitr4 176	. . . . 5 |- ((|^||^|y u. U.ran { y}) e. (C ^m (A u. B)) <-> (|^||^|y u. U.ran { y}):(A u. B)-->(C u. C))
31	25, 30	sylibr 200	. . . 4 |- (((|^||^|y:A-->C /\ U.ran { y}:B-->C) /\ (A i^i B) = (/)) -> (|^||^|y u. U.ran { y}) e. (C ^m (A u. B)))
32		elxp5 3446	. . . . . 6 |- (y e. ((C ^m A) X. (C ^m B)) <-> (y = <.|^||^|y, U.ran { y}>. /\ (|^||^|y e. (C ^m A) /\ U.ran { y} e. (C ^m B))))
33	32	pm3.27bi 326	. . . . 5 |- (y e. ((C ^m A) X. (C ^m B)) -> (|^||^|y e. (C ^m A) /\ U.ran { y} e. (C ^m B)))
34	6, 7	elmap 4324	. . . . . 6 |- (|^||^|y e. (C ^m A) <-> |^||^|y:A-->C)
35	6, 13	elmap 4324	. . . . . 6 |- (U.ran { y} e. (C ^m B) <-> U.ran { y}:B-->C)
36	34, 35	anbi12i 482	. . . . 5 |- ((|^||^|y e. (C ^m A) /\ U.ran { y} e. (C ^m B)) <-> (|^||^|y:A-->C /\ U.ran { y}:B-->C))
37	33, 36	sylib 198	. . . 4 |- (y e. ((C ^m A) X. (C ^m B)) -> (|^||^|y:A-->C /\ U.ran { y}:B-->C))
38	31, 37	sylan 448	. . 3 |- ((y e. ((C ^m A) X. (C ^m B)) /\ (A i^i B) = (/)) -> (|^||^|y u. U.ran { y}) e. (C ^m (A u. B)))
39	38	expcom 374	. 2 |- ((A i^i B) = (/) -> (y e. ((C ^m A) X. (C ^m B)) -> (|^||^|y u. U.ran { y}) e. (C ^m (A u. B))))
40		reseq1 3360	. . . . . . . . . . . . . . 15 |- (x = (|^||^|y u. U.ran { y}) -> (x |` A) = ((|^||^|y u. U.ran { y}) |` A))
41		resundir 3371	. . . . . . . . . . . . . . 15 |- ((|^||^|y u. U.ran { y}) |` A) = ((|^||^|y |` A) u. (U.ran { y} |` A))
42	40, 41	syl6eq 1520	. . . . . . . . . . . . . 14 |- (x = (|^||^|y u. U.ran { y}) -> (x |` A) = ((|^||^|y |` A) u. (U.ran { y} |` A)))
43		fnresdm 3588	. . . . . . . . . . . . . . . . 17 |- (|^||^|y Fn A -> (|^||^|y |` A) = |^||^|y)
44	43	uneq1d 2179	. . . . . . . . . . . . . . . 16 |- (|^||^|y Fn A -> ((|^||^|y |` A) u. (U.ran { y} |` A)) = (|^||^|y u. (U.ran { y} |` A)))
45		fnresdisj 3589	. . . . . . . . . . . . . . . . . . . 20 |- (U.ran { y} Fn B -> ((B i^i A) = (/) <-> (U.ran { y} |` A) = (/)))
46	45	biimpa 416	. . . . . . . . . . . . . . . . . . 19 |- ((U.ran { y} Fn B /\ (B i^i A) = (/)) -> (U.ran { y} |` A) = (/))
47		incom 2204	. . . . . . . . . . . . . . . . . . . 20 |- (A i^i B) = (B i^i A)
48	47	eqeq1i 1479	. . . . . . . . . . . . . . . . . . 19 |- ((A i^i B) = (/) <-> (B i^i A) = (/))
49	46, 48	sylan2b 452	. . . . . . . . . . . . . . . . . 18 |- ((U.ran { y} Fn B /\ (A i^i B) = (/)) -> (U.ran { y} |` A) = (/))
50	49	uneq2d 2180	. . . . . . . . . . . . . . . . 17 |- ((U.ran { y} Fn B /\ (A i^i B) = (/)) -> (|^||^|y u. (U.ran { y} |` A)) = (|^||^|y u. (/)))
51		un0 2293	. . . . . . . . . . . . . . . . 17 |- (|^||^|y u. (/)) = |^||^|y
52	50, 51	syl6eq 1520	. . . . . . . . . . . . . . . 16 |- ((U.ran { y} Fn B /\ (A i^i B) = (/)) -> (|^||^|y u. (U.ran { y} |` A)) = |^||^|y)
53	44, 52	sylan9eq 1524	. . . . . . . . . . . . . . 15 |- ((|^||^|y Fn A /\ (U.ran { y} Fn B /\ (A i^i B) = (/))) -> ((|^||^|y |` A) u. (U.ran { y} |` A)) = |^||^|y)
54	53	anassrs 441	. . . . . . . . . . . . . 14 |- (((|^||^|y Fn A /\ U.ran { y} Fn B) /\ (A i^i B) = (/)) -> ((|^||^|y |` A) u. (U.ran { y} |` A)) = |^||^|y)
55	42, 54	sylan9eqr 1526	. . . . . . . . . . . . 13 |- ((((|^||^|y Fn A /\ U.ran { y} Fn B) /\ (A i^i B) = (/)) /\ x = (|^||^|y u. U.ran { y})) -> (x |` A) = |^||^|y)
56		reseq1 3360	. . . . . . . . . . . . . . 15 |- (x = (|^||^|y u. U.ran { y}) -> (x |` B) = ((|^||^|y u. U.ran { y}) |` B))
57		resundir 3371	. . . . . . . . . . . . . . 15 |- ((|^||^|y u. U.ran { y}) |` B) = ((|^||^|y |` B) u. (U.ran { y} |` B))
58	56, 57	syl6eq 1520	. . . . . . . . . . . . . 14 |- (x = (|^||^|y u. U.ran { y}) -> (x |` B) = ((|^||^|y |` B) u. (U.ran { y} |` B)))
59		fnresdm 3588	. . . . . . . . . . . . . . . . 17 |- (U.ran { y} Fn B -> (U.ran { y} |` B) = U.ran { y})
60	59	uneq2d 2180	. . . . . . . . . . . . . . . 16 |- (U.ran { y} Fn B -> ((|^||^|y |` B) u. (U.ran { y} |` B)) = ((|^||^|y |` B) u. U.ran { y}))
61		fnresdisj 3589	. . . . . . . . . . . . . . . . . . 19 |- (|^||^|y Fn A -> ((A i^i B) = (/) <-> (|^||^|y |` B)