Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
GIF version

Theorem ssenen 3399

Description: Equinumerosity of equinumerous subsets of a set.

**Hypotheses**
Ref	Expression
ssenen.1	⊢ A ∈ V
ssenen.2	⊢ B ∈ V
ssenen.3	⊢ C ∈ 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 ∈ V
2	1	bren 3282	. . 3 ⊢ (A ≈ B ↔ ∃f f:A–1-1-onto→B)
3		ssenen.1	. . . . . . . 8 ⊢ A ∈ V
4	3	pwex 1806	. . . . . . 7 ⊢ ℘A ∈ V
5	4	inex1 1697	. . . . . 6 ⊢ (℘A ∩ {x∣x ≈ C}) ∈ V
6	5	a1i 7	. . . . 5 ⊢ (f:A–1-1-onto→B → (℘A ∩ {x∣x ≈ C}) ∈ 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 ∈ 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 ∈ (℘A ∩ {x∣x ≈ C}) ↔ (y ∈ ℘A ∧ y ∈ {x∣x ≈ C}))
24	15	elpw 1801	. . . . . . . 8 ⊢ (y ∈ ℘A ↔ y ⊆ A)
25		breq1 2065	. . . . . . . . 9 ⊢ (x = y → (x ≈ C ↔ y ≈ C))
26	15, 25	elab 1415	. . . . . . . 8 ⊢ (y ∈ {x∣x ≈ C} ↔ y ≈ C)
27	24, 26	anbi12i 369	. . . . . . 7 ⊢ ((y ∈ ℘A ∧ y ∈ {x∣x ≈ C}) ↔ (y ⊆ A ∧ y ≈ C))
28	23, 27	bitr 151	. . . . . 6 ⊢ (y ∈ (℘A ∩ {x∣x ≈ C}) ↔ (y ⊆ A ∧ y ≈ C))
29		elin 1635	. . . . . . 7 ⊢ ((f “ y) ∈ (℘B ∩ {x∣x ≈ C}) ↔ ((f “ y) ∈ ℘B ∧ (f “ y) ∈ {x∣x ≈ C}))
30		visset 1350	. . . . . . . . . 10 ⊢ f ∈ V
31		imaexg 2612	. . . . . . . . . 10 ⊢ (f ∈ V → (f “ y) ∈ V)
32	30, 31	ax-mp 6	. . . . . . . . 9 ⊢ (f “ y) ∈ V
33	32	elpw 1801	. . . . . . . 8 ⊢ ((f “ y) ∈ ℘B ↔ (f “ y) ⊆ B)
34		breq1 2065	. . . . . . . . 9 ⊢ (x = (f “ y) → (x ≈ C ↔ (f “ y) ≈ C))
35	32, 34	elab 1415	. . . . . . . 8 ⊢ ((f “ y) ∈ {x∣x ≈ C} ↔ (f “ y) ≈ C)
36	33, 35	anbi12i 369	. . . . . . 7 ⊢ (((f “ y) ∈ ℘B ∧ (f “ y) ∈ {x∣x ≈ C}) ↔ ((f “ y) ⊆ B ∧ (f “ y) ≈ C))
37	29, 36	bitr 151	. . . . . 6 ⊢ ((f “ y) ∈ (℘B ∩ {x∣x ≈ C}) ↔ ((f “ y) ⊆ B ∧ (f “ y) ≈ C))
38	22, 28, 37	3imtr4g 426	. . . . 5 ⊢ (f:A–1-1-onto→B → (y ∈ (℘A ∩ {x∣x ≈ C}) → (f “ y) ∈ (℘B ∩ {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 ∈ 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 ∈ (℘B ∩ {x∣x ≈ C}) ↔ (z ∈ ℘B ∧ z ∈ {x∣x ≈ C}))
58	48	elpw 1801	. . . . . . . 8 ⊢ (z ∈ ℘B ↔ z ⊆ B)
59		breq1 2065	. . . . . . . . 9 ⊢ (x = z → (x ≈ C ↔ z ≈ C))
60	48, 59	elab 1415	. . . . . . . 8 ⊢ (z ∈ {x∣x ≈ C} ↔ z ≈ C)
61	58, 60	anbi12i 369	. . . . . . 7 ⊢ ((z ∈ ℘B ∧ z ∈ {x∣x ≈ C}) ↔ (z ⊆ B ∧ z ≈ C))
62	57, 61	bitr 151	. . . . . 6 ⊢ (z ∈ (℘B ∩ {x∣x ≈ C}) ↔ (z ⊆ B ∧ z ≈ C))
63		elin 1635	. . . . . . 7 ⊢ ((^◡f “ z) ∈ (℘A ∩ {x∣x ≈ C}) ↔ ((^◡f “ z) ∈ ℘A ∧ (^◡f “ z) ∈ {x∣x ≈ C}))
64	30	cnvex 2670	. . . . . . . . . 10 ⊢ ^◡f ∈ V
65		imaexg 2612	. . . . . . . . . 10 ⊢ (^◡f ∈ V → (^◡f “ z) ∈ V)
66	64, 65	ax-mp 6	. . . . . . . . 9 ⊢ (^◡f “ z) ∈ V
67	66	elpw 1801	. . . . . . . 8 ⊢ ((^◡f “ z) ∈ ℘A ↔ (^◡f “ z) ⊆ A)
68		breq1 2065	. . . . . . . . 9 ⊢ (x = (^◡f “ z) → (x ≈ C ↔ (^◡f “ z) ≈ C))
69	66, 68	elab 1415	. . . . . . . 8 ⊢ ((^◡f “ z) ∈ {x∣x ≈ C} ↔ (^◡f “ z) ≈ C)
70	67, 69	anbi12i 369	. . . . . . 7 ⊢ (((^◡f “ z) ∈ ℘A ∧ (^◡f “ z) ∈ {x∣x ≈ C}) ↔ ((^◡f “ z) ⊆ A ∧ (^◡f “ z) ≈ C))
71	63, 70	bitr 151	. . . . . 6 ⊢ ((^◡f “ z) ∈ (℘A ∩ {x∣x ≈ C}) ↔ ((^◡f “ z) ⊆ A ∧ (^◡f “ z) ≈ C))
72	56, 62, 71	3imtr4g 426	. . . . 5 ⊢ (f:A–1-1-onto→B → (z ∈ (℘B ∩ {x∣x ≈ C}) → (^◡f “ z) ∈ (℘A ∩ {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 ∧ z ⊆ B) ∧ y = (^◡f “ z)) → (f “ y) = z)
85	84	cleqcomd 1106	. . . . . . . . . 10 ⊢ (((f:A–1-1-onto→B ∧ z ⊆ B) ∧ y = (^◡f “ z)) → z = (f “ y))
86	85	exp 291	. . . . . . . . 9 ⊢ ((f:A–1-1-onto→B ∧ z ⊆ B) → (y = (^◡f “ z) → z = (f “ y)))
87		pm3.26 256	. . . . . . . . . . 11 ⊢ ((z ∈ ℘B ∧ z ∈ {x∣x ≈ C}) → z ∈ ℘B)
88	87, 58	sylib 173	. . . . . . . . . 10 ⊢ ((z ∈ ℘B ∧ z ∈ {x∣x ≈ C}) → z ⊆ B)
89	57, 88	sylbi 174	. . . . . . . . 9 ⊢ (z ∈ (℘B ∩ {x∣x ≈ C}) → z ⊆ B)
90	86, 89	sylan2 346	. . . . . . . 8 ⊢ ((f:A–1-1-onto→B ∧ z ∈ (℘B ∩ {x∣x ≈ C})) → (y = (^◡f “ z) → z = (f “ y)))
91	90	adantrl 311	. . . . . . 7 ⊢ ((f:A–1-1-onto→B ∧ (y ∈ (℘A ∩ {x∣x ≈ C}) ∧ z ∈ (℘B ∩ {x∣x ≈ C}))) → (y = (^◡f “ z) → z = (f “ y)))
92		imaeq2 2603	. . . . . . . . . . . 12 ⊢ (z = (f “ y) → (^◡f “ z) = (^◡f “ (f “ y)))
93		f1imacnv 2814	. . . . . . . . . . . . 13 ⊢ ((f:A–1-1→B ∧ y ⊆ A) → (^◡f “ (f “ y)) = y)
94	93, 17	sylan 343	. . . . . . . . . . . 12 ⊢ ((f:A–1-1-onto→B ∧ y ⊆ A) → (^◡f “ (f “ y)) = y)
95	92, 94	sylan9eqr 1145	. . . . . . . . . . 11 ⊢ (((f:A–1-1-onto→B ∧ y ⊆ A) ∧ z = (f “ y)) → (^◡f “ z) = y)
96	95	cleqcomd 1106	. . . . . . . . . 10 ⊢ (((f:A–1-1-onto→B ∧ y ⊆ A) ∧ z = (f “ y)) → y = (^◡f “ z))
97	96	exp 291	. . . . . . . . 9 ⊢ ((f:A–1-1-onto→B ∧ y ⊆ A) → (z = (f “ y) → y = (^◡f “ z)))
98		pm3.26 256	. . . . . . . . . . 11 ⊢ ((y ∈ ℘A ∧ y ∈ {x∣x ≈ C}) → y ∈ ℘A)
99	98, 24	sylib 173	. . . . . . . . . 10 ⊢ ((y ∈ ℘A ∧ y ∈ {x∣x ≈ C}) → y ⊆ A)
100	23, 99	sylbi 174	. . . . . . . . 9 ⊢ (y ∈ (℘A ∩ {x∣x ≈ C}) → y ⊆ A)
101	97, 100	sylan2 346	. . . . . . . 8 ⊢ ((f:A–1-1-onto→B ∧ y ∈ (℘A ∩ {x∣x ≈ C})) → (z = (f “ y) → y = (^◡f “ z)))
102	101	adantrr 312	. . . . . . 7 ⊢ ((f:A–1-1-onto→B ∧ (y ∈ (℘A ∩ {x∣x ≈ C}) ∧ z ∈ (℘B ∩ {x∣x ≈ C}))) → (z = (f “ y) → y = (^◡f “ z)))
103	91, 102	impbid 397	. . . . . 6 ⊢ ((f:A–1-1-onto→B ∧ (y ∈ (℘A ∩ {x∣x ≈ C}) ∧ z ∈ (℘B ∩ {x∣x ≈ C}))) → (y = (^◡f “ z) ↔ z = (f “ y)))
104	103	exp 291	. . . . 5 ⊢ (f:A–1-1-onto→B → ((y ∈ (℘A ∩ {x∣x ≈ C}) ∧ z ∈ (℘B ∩ {x∣x ≈ C})) → (y = (^◡f “ z) ↔ z = (f “ y))))
105	6, 38, 72, 104	en3d 3304	. . . 4 ⊢ (f:A–1-1-onto→B → (℘A ∩ {x∣x ≈ C}) ≈ (℘B ∩ {x∣x ≈ C}))
106	105	19.23aiv 952	. . 3 ⊢ (∃f f:A–1-1-onto→B → (℘A ∩ {x∣x ≈ C}) ≈ (℘B ∩ {x∣x ≈ C}))
107	2, 106	sylbi 174	. 2 ⊢ (A ≈ B → (℘A ∩ {x∣x ≈ C}) ≈ (℘B ∩ {x∣x ≈ C}))
108		df-pw 1799	. . . 4 ⊢ ℘A = {x∣x ⊆ A}
109	108	ineq1i 1641	. . 3 ⊢ (℘A ∩ {x∣x ≈ C}) = ({x∣x ⊆ A} ∩ {x∣x ≈ C})
110		inab 1692	. . 3 ⊢ ({x∣x ⊆ A} ∩ {x∣x ≈ C}) = {x∣(x ⊆ A ∧ x ≈ C)}
111	109, 110	eqtr 1119	. 2 ⊢ (℘A ∩ {x∣x ≈ C}) = {x∣(x ⊆ A ∧ x ≈ C)}
112		df-pw 1799	. . . 4 ⊢ ℘B = {x∣x ⊆ B}
113	112	ineq1i 1641	. . 3 ⊢ (℘B ∩ {x∣x ≈ C}) = ({x∣x ⊆ B} ∩ {x∣x ≈ C})
114		inab 1692	. . 3 ⊢ ({x∣x ⊆ B} ∩ {x∣x ≈ C}) = {x∣(x ⊆ B ∧ x ≈ C)}
115	113, 114	eqtr 1119	. 2 ⊢ (℘B ∩ {x∣x ≈ C}) = {x∣(x ⊆ B ∧ x ≈ C)}
116	107, 111, 115	3brtr3g 2087	1 ⊢ (A ≈ B → {x∣(x ⊆ A ∧ x ≈ C)} ≈ {x∣(x ⊆ B ∧ x ≈ C)})

Colors of variables: wff set class

Syntax hints: → wi 2 ↔ wb 127 ∧ wa 196 ∃wex 678 {cab 1090 = wceq 1091 ∈ wcel 1092 Vcvv 1348 ∩ cin 1486 ⊆ wss 1487 ℘cpw 1798 class class class wbr 2054 ^◡ccnv 2409 ran crn 2411 “ cima 2413 Rel wrel 2415 –1-1→wf1 2419 –onto→wfo 2420 –1-1-onto→wf1o 2421 ≈ cen 3271

This theorem is referenced by: infmap2 4953

This theorem was proved from axioms: ax-1 3 ax-2 4 ax-3 5 ax-mp 6 ax-4 673 ax-5 674 ax-6 675 ax-7 676 ax-gen 677 ax-8 798 ax-9 799 ax-10 800 ax-11 801 ax-12 802 ax-13 804 ax-14 805 ax-16 922 ax-17 925 ax-ext 1074 ax-rep 1075 ax-un 1076 ax-pow 1077

This theorem depends on definitions: df-bi 128 df-or 197 df-an 198 df-3an 583 df-ex 679 df-sb 853 df-eu 1009 df-mo 1010 df-clab 1093 df-cleq 1097 df-clel 1099 df-ral 1205 df-rex 1206 df-v 1349 df-dif 1489 df-un 1490 df-in 1491 df-ss 1492 df-nul 1708 df-pw 1799 df-sn 1811 df-pr 1812 df-op 1815 df-uni 1920 df-br 2063 df-opab 2098 df-id 2125 df-xp 2424 df-rel 2425 df-cnv 2426 df-co 2427 df-dm 2428 df-rn 2429 df-res 2430 df-ima 2431 df-fun 2432 df-fn 2433 df-f 2434 df-f1 2435 df-fo 2436 df-f1o 2437 df-er 3200 df-en 3274

metamath.org