Theorem ssenen 4651

Description: Equinumerosity of equinumerous subsets of a set.

Hypotheses

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

Assertion

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

Distinct variable groups:   x,A   x,B   x,C

Proof of Theorem ssenen

Step	Hyp	Ref	Expression
1		ssenen.2	. . . 4 |- B e. V
2	1	bren 4518	. . 3 |- (A ~~ B <-> E.f f:A-1-1-onto->B)
3		ssenen.1	. . . . . . . 8 |- A e. V
4	3	pwex 2823	. . . . . . 7 |- P~A e. V
5	4	inex1 2790	. . . . . 6 |- (P~A i^i {x | x ~~ C}) e. V
6	5	a1i 8	. . . . 5 |- (f:A-1-1-onto->B -> (P~A i^i {x | x ~~ C}) e. V)
7		entr 4555	. . . . . . . . . 10 |- (((f"y) ~~ y /\ y ~~ C) -> (f"y) ~~ C)
8		visset 1859	. . . . . . . . . . . 12 |- y e. V
9	8	f1imaen 4563	. . . . . . . . . . 11 |- ((f:A-1-1->B /\ y (_ A) -> (f"y) ~~ y)
10		f1of1 3796	. . . . . . . . . . 11 |- (f:A-1-1-onto->B -> f:A-1-1->B)
11	9, 10	sylan 450	. . . . . . . . . 10 |- ((f:A-1-1-onto->B /\ y (_ A) -> (f"y) ~~ y)
12	7, 11	sylan 450	. . . . . . . . 9 |- (((f:A-1-1-onto->B /\ y (_ A) /\ y ~~ C) -> (f"y) ~~ C)
13	12	exp31 376	. . . . . . . 8 |- (f:A-1-1-onto->B -> (y (_ A -> (y ~~ C -> (f"y) ~~ C)))
14	13	imp3a 359	. . . . . . 7 |- (f:A-1-1-onto->B -> ((y (_ A /\ y ~~ C) -> (f"y) ~~ C))
15		f1ofo 3803	. . . . . . . 8 |- (f:A-1-1-onto->B -> f:A-onto->B)
16		imassrn 3507	. . . . . . . . 9 |- (f"y) (_ ran f
17		forn 3782	. . . . . . . . . 10 |- (f:A-onto->B -> ran f = B)
18	17	sseq2d 2141	. . . . . . . . 9 |- (f:A-onto->B -> ((f"y) (_ ran f <-> (f"y) (_ B))
19	16, 18	mpbii 191	. . . . . . . 8 |- (f:A-onto->B -> (f"y) (_ B)
20	15, 19	syl 10	. . . . . . 7 |- (f:A-1-1-onto->B -> (f"y) (_ B)
21	14, 20	jctild 604	. . . . . 6 |- (f:A-1-1-onto->B -> ((y (_ A /\ y ~~ C) -> ((f"y) (_ B /\ (f"y) ~~ C)))
22		elin 2259	. . . . . . 7 |- (y e. (P~A i^i {x | x ~~ C}) <-> (y e. P~A /\ y e. {x | x ~~ C}))
23	8	elpw 2461	. . . . . . . 8 |- (y e. P~A <-> y (_ A)
24		breq1 2695	. . . . . . . . 9 |- (x = y -> (x ~~ C <-> y ~~ C))
25	8, 24	elab 1943	. . . . . . . 8 |- (y e. {x | x ~~ C} <-> y ~~ C)
26	23, 25	anbi12i 485	. . . . . . 7 |- ((y e. P~A /\ y e. {x | x ~~ C}) <-> (y (_ A /\ y ~~ C))
27	22, 26	bitri 171	. . . . . 6 |- (y e. (P~A i^i {x | x ~~ C}) <-> (y (_ A /\ y ~~ C))
28		elin 2259	. . . . . . 7 |- ((f"y) e. (P~B i^i {x | x ~~ C}) <-> ((f"y) e. P~B /\ (f"y) e. {x | x ~~ C}))
29		visset 1859	. . . . . . . . . 10 |- f e. V
30		imaexg 3508	. . . . . . . . . 10 |- (f e. V -> (f"y) e. V)
31	29, 30	ax-mp 7	. . . . . . . . 9 |- (f"y) e. V
32	31	elpw 2461	. . . . . . . 8 |- ((f"y) e. P~B <-> (f"y) (_ B)
33		breq1 2695	. . . . . . . . 9 |- (x = (f"y) -> (x ~~ C <-> (f"y) ~~ C))
34	31, 33	elab 1943	. . . . . . . 8 |- ((f"y) e. {x | x ~~ C} <-> (f"y) ~~ C)
35	32, 34	anbi12i 485	. . . . . . 7 |- (((f"y) e. P~B /\ (f"y) e. {x | x ~~ C}) <-> ((f"y) (_ B /\ (f"y) ~~ C))
36	28, 35	bitri 171	. . . . . 6 |- ((f"y) e. (P~B i^i {x | x ~~ C}) <-> ((f"y) (_ B /\ (f"y) ~~ C))
37	21, 27, 36	3imtr4g 556	. . . . 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})))
38		f1ocnv 3809	. . . . . . 7 |- (f:A-1-1-onto->B -> `'f:B-1-1-onto->A)
39		entr 4555	. . . . . . . . . . 11 |- (((`'f"z) ~~ z /\ z ~~ C) -> (`'f"z) ~~ C)
40		visset 1859	. . . . . . . . . . . . 13 |- z e. V
41	40	f1imaen 4563	. . . . . . . . . . . 12 |- ((`'f:B-1-1->A /\ z (_ B) -> (`'f"z) ~~ z)
42		f1of1 3796	. . . . . . . . . . . 12 |- (`'f:B-1-1-onto->A -> `'f:B-1-1->A)
43	41, 42	sylan 450	. . . . . . . . . . 11 |- ((`'f:B-1-1-onto->A /\ z (_ B) -> (`'f"z) ~~ z)
44	39, 43	sylan 450	. . . . . . . . . 10 |- (((`'f:B-1-1-onto->A /\ z (_ B) /\ z ~~ C) -> (`'f"z) ~~ C)
45	44	exp31 376	. . . . . . . . 9 |- (`'f:B-1-1-onto->A -> (z (_ B -> (z ~~ C -> (`'f"z) ~~ C)))
46	45	imp3a 359	. . . . . . . 8 |- (`'f:B-1-1-onto->A -> ((z (_ B /\ z ~~ C) -> (`'f"z) ~~ C))
47		f1ofo 3803	. . . . . . . . 9 |- (`'f:B-1-1-onto->A -> `'f:B-onto->A)
48		imassrn 3507	. . . . . . . . . 10 |- (`'f"z) (_ ran `' f
49		forn 3782	. . . . . . . . . . 11 |- (`'f:B-onto->A -> ran `' f = A)
50	49	sseq2d 2141	. . . . . . . . . 10 |- (`'f:B-onto->A -> ((`'f"z) (_ ran `' f <-> (`'f"z) (_ A))
51	48, 50	mpbii 191	. . . . . . . . 9 |- (`'f:B-onto->A -> (`'f"z) (_ A)
52	47, 51	syl 10	. . . . . . . 8 |- (`'f:B-1-1-onto->A -> (`'f"z) (_ A)
53	46, 52	jctild 604	. . . . . . 7 |- (`'f:B-1-1-onto->A -> ((z (_ B /\ z ~~ C) -> ((`'f"z) (_ A /\ (`'f"z) ~~ C)))
54	38, 53	syl 10	. . . . . 6 |- (f:A-1-1-onto->B -> ((z (_ B /\ z ~~ C) -> ((`'f"z) (_ A /\ (`'f"z) ~~ C)))
55		elin 2259	. . . . . . 7 |- (z e. (P~B i^i {x | x ~~ C}) <-> (z e. P~B /\ z e. {x | x ~~ C}))
56	40	elpw 2461	. . . . . . . 8 |- (z e. P~B <-> z (_ B)
57		breq1 2695	. . . . . . . . 9 |- (x = z -> (x ~~ C <-> z ~~ C))
58	40, 57	elab 1943	. . . . . . . 8 |- (z e. {x | x ~~ C} <-> z ~~ C)
59	56, 58	anbi12i 485	. . . . . . 7 |- ((z e. P~B /\ z e. {x | x ~~ C}) <-> (z (_ B /\ z ~~ C))
60	55, 59	bitri 171	. . . . . 6 |- (z e. (P~B i^i {x | x ~~ C}) <-> (z (_ B /\ z ~~ C))
61		elin 2259	. . . . . . 7 |- ((`'f"z) e. (P~A i^i {x | x ~~ C}) <-> ((`'f"z) e. P~A /\ (`'f"z) e. {x | x ~~ C}))
62	29	cnvex 3625	. . . . . . . . . 10 |- `'f e. V
63		imaexg 3508	. . . . . . . . . 10 |- (`'f e. V -> (`'f"z) e. V)
64	62, 63	ax-mp 7	. . . . . . . . 9 |- (`'f"z) e. V
65	64	elpw 2461	. . . . . . . 8 |- ((`'f"z) e. P~A <-> (`'f"z) (_ A)
66		breq1 2695	. . . . . . . . 9 |- (x = (`'f"z) -> (x ~~ C <-> (`'f"z) ~~ C))
67	64, 66	elab 1943	. . . . . . . 8 |- ((`'f"z) e. {x | x ~~ C} <-> (`'f"z) ~~ C)
68	65, 67	anbi12i 485	. . . . . . 7 |- (((`'f"z) e. P~A /\ (`'f"z) e. {x | x ~~ C}) <-> ((`'f"z) (_ A /\ (`'f"z) ~~ C))
69	61, 68	bitri 171	. . . . . 6 |- ((`'f"z) e. (P~A i^i {x | x ~~ C}) <-> ((`'f"z) (_ A /\ (`'f"z) ~~ C))
70	54, 60, 69	3imtr4g 556	. . . . 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})))
71		imaeq2 3492	. . . . . . . . . . . 12 |- (y = (`'f"z) -> (f"y) = (f"(`'f"z)))
72		f1orel 3800	. . . . . . . . . . . . . . . 16 |- (f:A-1-1-onto->B -> Rel f)
73		dfrel2 3569	. . . . . . . . . . . . . . . 16 |- (Rel f <-> `'`'f = f)
74	72, 73	sylib 196	. . . . . . . . . . . . . . 15 |- (f:A-1-1-onto->B -> `'`'f = f)
75	74	imaeq1d 3495	. . . . . . . . . . . . . 14 |- (f:A-1-1-onto->B -> (`'`'f"(`'f"z)) = (f"(`'f"z)))
76	75	adantr 389	. . . . . . . . . . . . 13 |- ((f:A-1-1-onto->B /\ z (_ B) -> (`'`'f"(`'f"z)) = (f"(`'f"z)))
77		f1imacnv 3813	. . . . . . . . . . . . . 14 |- ((`'f:B-1-1->A /\ z (_ B) -> (`'`'f"(`'f"z)) = z)
78	38, 42	syl 10	. . . . . . . . . . . . . 14 |- (f:A-1-1-onto->B -> `'f:B-1-1->A)
79	77, 78	sylan 450	. . . . . . . . . . . . 13 |- ((f:A-1-1-onto->B /\ z (_ B) -> (`'`'f"(`'f"z)) = z)
80	76, 79	eqtr3d 1552	. . . . . . . . . . . 12 |- ((f:A-1-1-onto->B /\ z (_ B) -> (f"(`'f"z)) = z)
81	71, 80	sylan9eqr 1572	. . . . . . . . . . 11 |- (((f:A-1-1-onto->B /\ z (_ B) /\ y = (`'f"z)) -> (f"y) = z)
82	81	eqcomd 1523	. . . . . . . . . 10 |- (((f:A-1-1-onto->B /\ z (_ B) /\ y = (`'f"z)) -> z = (f"y))
83	82	ex 371	. . . . . . . . 9 |- ((f:A-1-1-onto->B /\ z (_ B) -> (y = (`'f"z) -> z = (f"y)))
84		pm3.26 317	. . . . . . . . . . 11 |- ((z e. P~B /\ z e. {x | x ~~ C}) -> z e. P~B)
85	84, 56	sylib 196	. . . . . . . . . 10 |- ((z e. P~B /\ z e. {x | x ~~ C}) -> z (_ B)
86	55, 85	sylbi 197	. . . . . . . . 9 |- (z e. (P~B i^i {x | x ~~ C}) -> z (_ B)
87	83, 86	sylan2 453	. . . . . . . 8 |- ((f:A-1-1-onto->B /\ z e. (P~B i^i {x | x ~~ C})) -> (y = (`'f"z) -> z = (f"y)))
88	87	adantrl 394	. . . . . . 7 |- ((f:A-1-1-onto->B /\ (y e. (P~A i^i {x | x ~~ C}) /\ z e. (P~B i^i {x | x ~~ C}))) -> (y = (`'f"z) -> z = (f"y)))
89		imaeq2 3492	. . . . . . . . . . . 12 |- (z = (f"y) -> (`'f"z) = (`'f"(f"y)))
90		f1imacnv 3813	. . . . . . . . . . . . 13 |- ((f:A-1-1->B /\ y (_ A) -> (`'f"(f"y)) = y)
91	90, 10	sylan 450	. . . . . . . . . . . 12 |- ((f:A-1-1-onto->B /\ y (_ A) -> (`'f"(f"y)) = y)
92	89, 91	sylan9eqr 1572	. . . . . . . . . . 11 |- (((f:A-1-1-onto->B /\ y (_ A) /\ z = (f"y)) -> (`'f"z) = y)
93	92	eqcomd 1523	. . . . . . . . . 10 |- (((f:A-1-1-onto->B /\ y (_ A) /\ z = (f"y)) -> y = (`'f"z))
94	93	ex 371	. . . . . . . . 9 |- ((f:A-1-1-onto->B /\ y (_ A) -> (z = (f"y) -> y = (`'f"z)))
95		pm3.26 317	. . . . . . . . . . 11 |- ((y e. P~A /\ y e. {x | x ~~ C}) -> y e. P~A)
96	95, 23	sylib 196	. . . . . . . . . 10 |- ((y e. P~A /\ y e. {x | x ~~ C}) -> y (_ A)
97	22, 96	sylbi 197	. . . . . . . . 9 |- (y e. (P~A i^i {x | x ~~ C}) -> y (_ A)
98	94, 97	sylan2 453	. . . . . . . 8 |- ((f:A-1-1-onto->B /\ y e. (P~A i^i {x | x ~~ C})) -> (z = (f"y) -> y = (`'f"z)))
99	98	adantrr 395	. . . . . . 7 |- ((f:A-1-1-onto->B /\ (y e. (P~A i^i {x | x ~~ C}) /\ z e. (P~B i^i {x | x ~~ C}))) -> (z = (f"y) -> y = (`'f"z)))
100	88, 99	impbid 519	. . . . . 6 |- ((f:A-1-1-onto->B /\ (y e. (P~A i^i {x | x ~~ C}) /\ z e. (P~B i^i {x | x ~~ C}))) -> (y = (`'f"z) <-> z = (f"y)))
101	100	ex 371	. . . . 5 |- (f:A-1-1-onto->B -> ((y e. (P~A i^i {x | x ~~ C}) /\ z e. (P~B i^i {x | x ~~ C})) -> (y = (`'f"z) <-> z = (f"y))))
102	6, 37, 70, 101	en3d 4542	. . . 4 |- (f:A-1-1-onto->B -> (P~A i^i {x | x ~~ C}) ~~ (P~B i^i {x | x ~~ C}))
103	102	19.23aiv 1333	. . 3 |- (E.f f:A-1-1-onto->B -> (P~A i^i {x | x ~~ C}) ~~ (P~B i^i {x | x ~~ C}))
104	2, 103	sylbi 197	. 2 |- (A ~~ B -> (P~A i^i {x | x ~~ C}) ~~ (P~B i^i {x | x ~~ C}))
105		df-pw 2459	. . . 4 |- P~A = {x | x (_ A}
106	105	ineq1i 2265	. . 3 |- (P~A i^i {x | x ~~ C}) = ({x | x (_ A} i^i {x | x ~~ C})
107		inab 2320	. . 3 |- ({x | x (_ A} i^i {x | x ~~ C}) = {x | (x (_ A /\ x ~~ C)}
108	106, 107	eqtri 1538	. 2 |- (P~A i^i {x | x ~~ C}) = {x | (x (_ A /\ x ~~ C)}
109		df-pw 2459	. . . 4 |- P~B = {x | x (_ B}
110	109	ineq1i 2265	. . 3 |- (P~B i^i {x | x ~~ C}) = ({x | x (_ B} i^i {x | x ~~ C})
111		inab 2320	. . 3 |- ({x | x (_ B} i^i {x | x ~~ C}) = {x | (x (_ B /\ x ~~ C)}
112	110, 111	eqtri 1538	. 2 |- (P~B i^i {x | x ~~ C}) = {x | (x (_ B /\ x ~~ C)}
113	104, 108, 112	3brtr3g 2719	1 |- (A ~~ B -> {x | (x (_ A /\ x ~~ C)} ~~ {x | (x (_ B /\ x ~~ C)})

Syntax hints:   -> wi 3   <-> wb 144   /\ wa 221   = wceq 992   e. wcel 994  E.wex 1016  {cab 1505  Vcvv 1857   i^i cin 2098   (_ wss 2099  P~cpw 2458   class class class wbr 2692  `'ccnv 3250  ran crn 3252  "cima 3254  Rel wrel 3256  -1-1->wf1 3260  -onto->wfo 3261  -1-1-onto->wf1o 3262   ~~ cen 4505

This theorem is referenced by:  infmap2 7793

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-9 1001  ax-10 1002  ax-11 1003  ax-12 1004  ax-13 1005  ax-14 1006  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500  ax-rep 2767  ax-sep 2777  ax-pow 2818  ax-pr 2855  ax-un 3089

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-3an 783  df-ex 1017  df-sb 1209  df-eu 1421  df-mo 1422  df-clab 1506  df-cleq 1511  df-clel 1514  df-ne 1630  df-ral 1695  df-rex 1696  df-v 1858  df-dif 2101  df-un 2102  df-in 2103  df-ss 2105  df-nul 2333  df-pw 2459  df-sn 2470  df-pr 2471  df-op 2474  df-uni 2570  df-br 2693  df-opab 2741  df-id 2913  df-xp 3265  df-rel 3266  df-cnv 3267  df-co 3268  df-dm 3269  df-rn 3270  df-res 3271  df-ima 3272  df-fun 3273  df-fn 3274  df-f 3275  df-f1 3276  df-fo 3277  df-f1o 3278  df-er 4401  df-en 4509

Copyright terms: Public domain