Theorem ssenen 3399

Description: Equinumerosity of equinumerous subsets of a set.

Hypotheses

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

Assertion

Ref	Expression
ssenen	|- (A ~~ B -> {x | (x (_ A /\ x ~~ C)} ~~ {x | (x (_ B /\ x ~~ C)})

Distinct variable group(s):   x,A   x,B   x,C

Proof of Theorem ssenen

Step	Hyp	Ref	Expression
1		ssenen.2	. . . 4 |- B e. V
2	1	bren 3282	. . 3 |- (A ~~ B <-> E.f f:A-1-1-onto->B)
3		ssenen.1	. . . . . . . 8 |- A e. V
4	3	pwex 1806	. . . . . . 7 |- P~A e. V
5	4	inex1 1697	. . . . . 6 |- (P~A i^i {x | x ~~ C}) e. V
6	5	a1i 7	. . . . 5 |- (f:A-1-1-onto->B -> (P~A i^i {x | x ~~ C}) e. V)
7		f1ofo 2806	. . . . . . . . 9 |- (f:A-1-1-onto->B -> f:A-onto->B)
8		imassrn 2611	. . . . . . . . . 10 |- (f"y) (_ ran f
9		forn 2789	. . . . . . . . . . 11 |- (f:A-onto->B -> ran f = B)
10	9	sseq2d 1528	. . . . . . . . . 10 |- (f:A-onto->B -> ((f"y) (_ ran f <-> (f"y) (_ B))
11	8, 10	mpbii 168	. . . . . . . . 9 |- (f:A-onto->B -> (f"y) (_ B)
12	7, 11	syl 12	. . . . . . . 8 |- (f:A-1-1-onto->B -> (f"y) (_ B)
13	12	a1d 14	. . . . . . 7 |- (f:A-1-1-onto->B -> ((y (_ A /\ y ~~ C) -> (f"y) (_ B))
14		entrt 3319	. . . . . . . . . 10 |- (((f"y) ~~ y /\ y ~~ C) -> (f"y) ~~ C)
15		visset 1350	. . . . . . . . . . . 12 |- y e. V
16	15	f1imaen 3327	. . . . . . . . . . 11 |- ((f:A-1-1->B /\ y (_ A) -> (f"y) ~~ y)
17		f1of1 2799	. . . . . . . . . . 11 |- (f:A-1-1-onto->B -> f:A-1-1->B)
18	16, 17	sylan 343	. . . . . . . . . 10 |- ((f:A-1-1-onto->B /\ y (_ A) -> (f"y) ~~ y)
19	14, 18	sylan 343	. . . . . . . . 9 |- (((f:A-1-1-onto->B /\ y (_ A) /\ y ~~ C) -> (f"y) ~~ C)
20	19	exp31 293	. . . . . . . 8 |- (f:A-1-1-onto->B -> (y (_ A -> (y ~~ C -> (f"y) ~~ C)))
21	20	imp3a 279	. . . . . . 7 |- (f:A-1-1-onto->B -> ((y (_ A /\ y ~~ C) -> (f"y) ~~ C))
22	13, 21	jcad 455	. . . . . 6 |- (f:A-1-1-onto->B -> ((y (_ A /\ y ~~ C) -> ((f"y) (_ B /\ (f"y) ~~ C)))
23		elin 1635	. . . . . . 7 |- (y e. (P~A i^i {x | x ~~ C}) <-> (y e. P~A /\ y e. {x | x ~~ C}))
24	15	elpw 1801	. . . . . . . 8 |- (y e. P~A <-> y (_ A)
25		breq1 2065	. . . . . . . . 9 |- (x = y -> (x ~~ C <-> y ~~ C))
26	15, 25	elab 1415	. . . . . . . 8 |- (y e. {x | x ~~ C} <-> y ~~ C)
27	24, 26	anbi12i 369	. . . . . . 7 |- ((y e. P~A /\ y e. {x | x ~~ C}) <-> (y (_ A /\ y ~~ C))
28	23, 27	bitr 151	. . . . . 6 |- (y e. (P~A i^i {x | x ~~ C}) <-> (y (_ A /\ y ~~ C))
29		elin 1635	. . . . . . 7 |- ((f"y) e. (P~B i^i {x | x ~~ C}) <-> ((f"y) e. P~B /\ (f"y) e. {x | x ~~ C}))
30		visset 1350	. . . . . . . . . 10 |- f e. V
31		imaexg 2612	. . . . . . . . . 10 |- (f e. V -> (f"y) e. V)
32	30, 31	ax-mp 6	. . . . . . . . 9 |- (f"y) e. V
33	32	elpw 1801	. . . . . . . 8 |- ((f"y) e. P~B <-> (f"y) (_ B)
34		breq1 2065	. . . . . . . . 9 |- (x = (f"y) -> (x ~~ C <-> (f"y) ~~ C))
35	32, 34	elab 1415	. . . . . . . 8 |- ((f"y) e. {x | x ~~ C} <-> (f"y) ~~ C)
36	33, 35	anbi12i 369	. . . . . . 7 |- (((f"y) e. P~B /\ (f"y) e. {x | x ~~ C}) <-> ((f"y) (_ B /\ (f"y) ~~ C))
37	29, 36	bitr 151	. . . . . 6 |- ((f"y) e. (P~B i^i {x | x ~~ C}) <-> ((f"y) (_ B /\ (f"y) ~~ C))
38	22, 28, 37	3imtr4g 426	. . . . 5 |- (f:A-1-1-onto->B -> (y e. (P~A i^i {x | x ~~ C}) -> (f"y) e. (P~B i^i {x | x ~~ C})))
39		f1ocnv 2811	. . . . . . 7 |- (f:A-1-1-onto->B -> `'f:B-1-1-onto->A)
40		f1ofo 2806	. . . . . . . . . 10 |- (`'f:B-1-1-onto->A -> `'f:B-onto->A)
41		imassrn 2611	. . . . . . . . . . 11 |- (`'f"z) (_ ran `'f
42		forn 2789	. . . . . . . . . . . 12 |- (`'f:B-onto->A -> ran `'f = A)
43	42	sseq2d 1528	. . . . . . . . . . 11 |- (`'f:B-onto->A -> ((`'f"z) (_ ran `'f <-> (`'f"z) (_ A))
44	41, 43	mpbii 168	. . . . . . . . . 10 |- (`'f:B-onto->A -> (`'f"z) (_ A)
45	40, 44	syl 12	. . . . . . . . 9 |- (`'f:B-1-1-onto->A -> (`'f"z) (_ A)
46	45	a1d 14	. . . . . . . 8 |- (`'f:B-1-1-onto->A -> ((z (_ B /\ z ~~ C) -> (`'f"z) (_ A))
47		entrt 3319	. . . . . . . . . . 11 |- (((`'f"z) ~~ z /\ z ~~ C) -> (`'f"z) ~~ C)
48		visset 1350	. . . . . . . . . . . . 13 |- z e. V
49	48	f1imaen 3327	. . . . . . . . . . . 12 |- ((`'f:B-1-1->A /\ z (_ B) -> (`'f"z) ~~ z)
50		f1of1 2799	. . . . . . . . . . . 12 |- (`'f:B-1-1-onto->A -> `'f:B-1-1->A)
51	49, 50	sylan 343	. . . . . . . . . . 11 |- ((`'f:B-1-1-onto->A /\ z (_ B) -> (`'f"z) ~~ z)
52	47, 51	sylan 343	. . . . . . . . . 10 |- (((`'f:B-1-1-onto->A /\ z (_ B) /\ z ~~ C) -> (`'f"z) ~~ C)
53	52	exp31 293	. . . . . . . . 9 |- (`'f:B-1-1-onto->A -> (z (_ B -> (z ~~ C -> (`'f"z) ~~ C)))
54	53	imp3a 279	. . . . . . . 8 |- (`'f:B-1-1-onto->A -> ((z (_ B /\ z ~~ C) -> (`'f"z) ~~ C))
55	46, 54	jcad 455	. . . . . . 7 |- (`'f:B-1-1-onto->A -> ((z (_ B /\ z ~~ C) -> ((`'f"z) (_ A /\ (`'f"z) ~~ C)))
56	39, 55	syl 12	. . . . . 6 |- (f:A-1-1-onto->B -> ((z (_ B /\ z ~~ C) -> ((`'f"z) (_ A /\ (`'f"z) ~~ C)))
57		elin 1635	. . . . . . 7 |- (z e. (P~B i^i {x | x ~~ C}) <-> (z e. P~B /\ z e. {x | x ~~ C}))
58	48	elpw 1801	. . . . . . . 8 |- (z e. P~B <-> z (_ B)
59		breq1 2065	. . . . . . . . 9 |- (x = z -> (x ~~ C <-> z ~~ C))
60	48, 59	elab 1415	. . . . . . . 8 |- (z e. {x | x ~~ C} <-> z ~~ C)
61	58, 60	anbi12i 369	. . . . . . 7 |- ((z e. P~B /\ z e. {x | x ~~ C}) <-> (z (_ B /\ z ~~ C))
62	57, 61	bitr 151	. . . . . 6 |- (z e. (P~B i^i {x | x ~~ C}) <-> (z (_ B /\ z ~~ C))
63		elin 1635	. . . . . . 7 |- ((`'f"z) e. (P~A i^i {x | x ~~ C}) <-> ((`'f"z) e. P~A /\ (`'f"z) e. {x | x ~~ C}))
64	30	cnvex 2670	. . . . . . . . . 10 |- `'f e. V
65		imaexg 2612	. . . . . . . . . 10 |- (`'f e. V -> (`'f"z) e. V)
66	64, 65	ax-mp 6	. . . . . . . . 9 |- (`'f"z) e. V
67	66	elpw 1801	. . . . . . . 8 |- ((`'f"z) e. P~A <-> (`'f"z) (_ A)
68		breq1 2065	. . . . . . . . 9 |- (x = (`'f"z) -> (x ~~ C <-> (`'f"z) ~~ C))
69	66, 68	elab 1415	. . . . . . . 8 |- ((`'f"z) e. {x | x ~~ C} <-> (`'f"z) ~~ C)
70	67, 69	anbi12i 369	. . . . . . 7 |- (((`'f"z) e. P~A /\ (`'f"z) e. {x | x ~~ C}) <-> ((`'f"z) (_ A /\ (`'f"z) ~~ C))
71	63, 70	bitr 151	. . . . . 6 |- ((`'f"z) e. (P~A i^i {x | x ~~ C}) <-> ((`'f"z) (_ A /\ (`'f"z) ~~ C))
72	56, 62, 71	3imtr4g 426	. . . . 5 |- (f:A-1-1-onto->B -> (z e. (P~B i^i {x | x ~~ C}) -> (`'f"z) e. (P~A i^i {x | x ~~ C})))
73		imaeq2 2603	. . . . . . . . . . . 12 |- (y = (`'f"z) -> (f"y) = (f"(`'f"z)))
74		f1orel 2803	. . . . . . . . . . . . . . . 16 |- (f:A-1-1-onto->B -> Rel f)
75		dfrel2 2660	. . . . . . . . . . . . . . . 16 |- (Rel f <-> `'`'f = f)
76	74, 75	sylib 173	. . . . . . . . . . . . . . 15 |- (f:A-1-1-onto->B -> `'`'f = f)
77		imaeq1 2602	. . . . . . . . . . . . . . 15 |- (`'`'f = f -> (`'`'f"(`'f"z)) = (f"(`'f"z)))
78	76, 77	syl 12	. . . . . . . . . . . . . 14 |- (f:A-1-1-onto->B -> (`'`'f"(`'f"z)) = (f"(`'f"z)))
79	78	adantr 306	. . . . . . . . . . . . 13 |- ((f:A-1-1-onto->B /\ z (_ B) -> (`'`'f"(`'f"z)) = (f"(`'f"z)))
80		f1imacnv 2814	. . . . . . . . . . . . . 14 |- ((`'f:B-1-1->A /\ z (_ B) -> (`'`'f"(`'f"z)) = z)
81	39, 50	syl 12	. . . . . . . . . . . . . 14 |- (f:A-1-1-onto->B -> `'f:B-1-1->A)
82	80, 81	sylan 343	. . . . . . . . . . . . 13 |- ((f:A-1-1-onto->B /\ z (_ B) -> (`'`'f"(`'f"z)) = z)
83	79, 82	eqtr3d 1130	. . . . . . . . . . . 12 |- ((f:A-1-1-onto->B /\ z (_ B) -> (f"(`'f"z)) = z)
84	73, 83	sylan9eqr 1145	. . . . . . . . . . 11 |- (((f:A-1-1-onto->B