ssenen - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
GIF version

Theorem ssenen 4510

Description: Equinumerosity of equinumerous subsets of a set.

**Hypotheses**
Ref	Expression
ssenen.1	⊢ A ∈ V
ssenen.2	⊢ B ∈ 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 ∈ V
2	1	bren 4383	. . 3 ⊢ (A ≈ B ↔ ∃f f:A–1-1-onto→B)
3		ssenen.1	. . . . . . . 8 ⊢ A ∈ V
4	3	pwex 2751	. . . . . . 7 ⊢ ℘A ∈ V
5	4	inex1 2721	. . . . . 6 ⊢ (℘A ∩ {x∣x ≈ C}) ∈ V
6	5	a1i 8	. . . . 5 ⊢ (f:A–1-1-onto→B → (℘A ∩ {x∣x ≈ C}) ∈ V)
7		entrt 4420	. . . . . . . . . 10 ⊢ (((f “ y) ≈ y ⋀ y ≈ C) → (f “ y) ≈ C)
8		visset 1816	. . . . . . . . . . . 12 ⊢ y ∈ V
9	8	f1imaen 4428	. . . . . . . . . . 11 ⊢ ((f:A–1-1→B ⋀ y ⊆ A) → (f “ y) ≈ y)
10		f1of1 3694	. . . . . . . . . . 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 378	. . . . . . . 8 ⊢ (f:A–1-1-onto→B → (y ⊆ A → (y ≈ C → (f “ y) ≈ C)))
14	13	imp3a 361	. . . . . . 7 ⊢ (f:A–1-1-onto→B → ((y ⊆ A ⋀ y ≈ C) → (f “ y) ≈ C))
15		f1ofo 3701	. . . . . . . 8 ⊢ (f:A–1-1-onto→B → f:A–onto→B)
16		imassrn 3421	. . . . . . . . 9 ⊢ (f “ y) ⊆ ran f
17		forn 3680	. . . . . . . . . 10 ⊢ (f:A–onto→B → ran f = B)
18	17	sseq2d 2092	. . . . . . . . 9 ⊢ (f:A–onto→B → ((f “ y) ⊆ ran f ↔ (f “ y) ⊆ B))
19	16, 18	mpbii 193	. . . . . . . 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 603	. . . . . 6 ⊢ (f:A–1-1-onto→B → ((y ⊆ A ⋀ y ≈ C) → ((f “ y) ⊆ B ⋀ (f “ y) ≈ C)))
22		elin 2210	. . . . . . 7 ⊢ (y ∈ (℘A ∩ {x∣x ≈ C}) ↔ (y ∈ ℘A ⋀ y ∈ {x∣x ≈ C}))
23	8	elpw 2408	. . . . . . . 8 ⊢ (y ∈ ℘A ↔ y ⊆ A)
24		breq1 2627	. . . . . . . . 9 ⊢ (x = y → (x ≈ C ↔ y ≈ C))
25	8, 24	elab 1900	. . . . . . . 8 ⊢ (y ∈ {x∣x ≈ C} ↔ y ≈ C)
26	23, 25	anbi12i 484	. . . . . . 7 ⊢ ((y ∈ ℘A ⋀ y ∈ {x∣x ≈ C}) ↔ (y ⊆ A ⋀ y ≈ C))
27	22, 26	bitr 173	. . . . . 6 ⊢ (y ∈ (℘A ∩ {x∣x ≈ C}) ↔ (y ⊆ A ⋀ y ≈ C))
28		elin 2210	. . . . . . 7 ⊢ ((f “ y) ∈ (℘B ∩ {x∣x ≈ C}) ↔ ((f “ y) ∈ ℘B ⋀ (f “ y) ∈ {x∣x ≈ C}))
29		visset 1816	. . . . . . . . . 10 ⊢ f ∈ V
30		imaexg 3422	. . . . . . . . . 10 ⊢ (f ∈ V → (f “ y) ∈ V)
31	29, 30	ax-mp 7	. . . . . . . . 9 ⊢ (f “ y) ∈ V
32	31	elpw 2408	. . . . . . . 8 ⊢ ((f “ y) ∈ ℘B ↔ (f “ y) ⊆ B)
33		breq1 2627	. . . . . . . . 9 ⊢ (x = (f “ y) → (x ≈ C ↔ (f “ y) ≈ C))
34	31, 33	elab 1900	. . . . . . . 8 ⊢ ((f “ y) ∈ {x∣x ≈ C} ↔ (f “ y) ≈ C)
35	32, 34	anbi12i 484	. . . . . . 7 ⊢ (((f “ y) ∈ ℘B ⋀ (f “ y) ∈ {x∣x ≈ C}) ↔ ((f “ y) ⊆ B ⋀ (f “ y) ≈ C))
36	28, 35	bitr 173	. . . . . 6 ⊢ ((f “ y) ∈ (℘B ∩ {x∣x ≈ C}) ↔ ((f “ y) ⊆ B ⋀ (f “ y) ≈ C))
37	21, 27, 36	3imtr4g 555	. . . . 5 ⊢ (f:A–1-1-onto→B → (y ∈ (℘A ∩ {x∣x ≈ C}) → (f “ y) ∈ (℘B ∩ {x∣x ≈ C})))
38		f1ocnv 3707	. . . . . . 7 ⊢ (f:A–1-1-onto→B → ^◡f:B–1-1-onto→A)
39		entrt 4420	. . . . . . . . . . 11 ⊢ (((^◡f “ z) ≈ z ⋀ z ≈ C) → (^◡f “ z) ≈ C)
40		visset 1816	. . . . . . . . . . . . 13 ⊢ z ∈ V
41	40	f1imaen 4428	. . . . . . . . . . . 12 ⊢ ((^◡f:B–1-1→A ⋀ z ⊆ B) → (^◡f “ z) ≈ z)
42		f1of1 3694	. . . . . . . . . . . 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 378	. . . . . . . . 9 ⊢ (^◡f:B–1-1-onto→A → (z ⊆ B → (z ≈ C → (^◡f “ z) ≈ C)))
46	45	imp3a 361	. . . . . . . 8 ⊢ (^◡f:B–1-1-onto→A → ((z ⊆ B ⋀ z ≈ C) → (^◡f “ z) ≈ C))
47		f1ofo 3701	. . . . . . . . 9 ⊢ (^◡f:B–1-1-onto→A → ^◡f:B–onto→A)
48		imassrn 3421	. . . . . . . . . 10 ⊢ (^◡f “ z) ⊆ ran ^◡ f
49		forn 3680	. . . . . . . . . . 11 ⊢ (^◡f:B–onto→A → ran ^◡ f = A)
50	49	sseq2d 2092	. . . . . . . . . 10 ⊢ (^◡f:B–onto→A → ((^◡f “ z) ⊆ ran ^◡ f ↔ (^◡f “ z) ⊆ A))
51	48, 50	mpbii 193	. . . . . . . . 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 603	. . . . . . 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 2210	. . . . . . 7 ⊢ (z ∈ (℘B ∩ {x∣x ≈ C}) ↔ (z ∈ ℘B ⋀ z ∈ {x∣x ≈ C}))
56	40	elpw 2408	. . . . . . . 8 ⊢ (z ∈ ℘B ↔ z ⊆ B)
57		breq1 2627	. . . . . . . . 9 ⊢ (x = z → (x ≈ C ↔ z ≈ C))
58	40, 57	elab 1900	. . . . . . . 8 ⊢ (z ∈ {x∣x ≈ C} ↔ z ≈ C)
59	56, 58	anbi12i 484	. . . . . . 7 ⊢ ((z ∈ ℘B ⋀ z ∈ {x∣x ≈ C}) ↔ (z ⊆ B ⋀ z ≈ C))
60	55, 59	bitr 173	. . . . . 6 ⊢ (z ∈ (℘B ∩ {x∣x ≈ C}) ↔ (z ⊆ B ⋀ z ≈ C))
61		elin 2210	. . . . . . 7 ⊢ ((^◡f “ z) ∈ (℘A ∩ {x∣x ≈ C}) ↔ ((^◡f “ z) ∈ ℘A ⋀ (^◡f “ z) ∈ {x∣x ≈ C}))
62	29	cnvex 3526	. . . . . . . . . 10 ⊢ ^◡f ∈ V
63		imaexg 3422	. . . . . . . . . 10 ⊢ (^◡f ∈ V → (^◡f “ z) ∈ V)
64	62, 63	ax-mp 7	. . . . . . . . 9 ⊢ (^◡f “ z) ∈ V
65	64	elpw 2408	. . . . . . . 8 ⊢ ((^◡f “ z) ∈ ℘A ↔ (^◡f “ z) ⊆ A)
66		breq1 2627	. . . . . . . . 9 ⊢ (x = (^◡f “ z) → (x ≈ C ↔ (^◡f “ z) ≈ C))
67	64, 66	elab 1900	. . . . . . . 8 ⊢ ((^◡f “ z) ∈ {x∣x ≈ C} ↔ (^◡f “ z) ≈ C)
68	65, 67	anbi12i 484	. . . . . . 7 ⊢ (((^◡f “ z) ∈ ℘A ⋀ (^◡f “ z) ∈ {x∣x ≈ C}) ↔ ((^◡f “ z) ⊆ A ⋀ (^◡f “ z) ≈ C))
69	61, 68	bitr 173	. . . . . 6 ⊢ ((^◡f “ z) ∈ (℘A ∩ {x∣x ≈ C}) ↔ ((^◡f “ z) ⊆ A ⋀ (^◡f “ z) ≈ C))
70	54, 60, 69	3imtr4g 555	. . . . 5 ⊢ (f:A–1-1-onto→B → (z ∈ (℘B ∩ {x∣x ≈ C}) → (^◡f “ z) ∈ (℘A ∩ {x∣x ≈ C})))
71		imaeq2 3408	. . . . . . . . . . . 12 ⊢ (y = (^◡f “ z) → (f “ y) = (f “ (^◡f “ z)))
72		f1orel 3698	. . . . . . . . . . . . . . . 16 ⊢ (f:A–1-1-onto→B → Rel f)
73		dfrel2 3491	. . . . . . . . . . . . . . . 16 ⊢ (Rel f ↔ ^◡^◡f = f)
74	72, 73	sylib 198	. . . . . . . . . . . . . . 15 ⊢ (f:A–1-1-onto→B → ^◡^◡f = f)
75	74	imaeq1d 3409	. . . . . . . . . . . . . 14 ⊢ (f:A–1-1-onto→B → (^◡^◡f “ (^◡f “ z)) = (f “ (^◡f “ z)))
76	75	adantr 391	. . . . . . . . . . . . 13 ⊢ ((f:A–1-1-onto→B ⋀ z ⊆ B) → (^◡^◡f “ (^◡f “ z)) = (f “ (^◡f “ z)))
77		f1imacnv 3711	. . . . . . . . . . . . . 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 1512	. . . . . . . . . . . 12 ⊢ ((f:A–1-1-onto→B ⋀ z ⊆ B) → (f “ (^◡f “ z)) = z)
81	71, 80	sylan9eqr 1532	. . . . . . . . . . 11 ⊢ (((f:A–1-1-onto→B ⋀ z ⊆ B) ⋀ y = (^◡f “ z)) → (f “ y) = z)
82	81	eqcomd 1483	. . . . . . . . . 10 ⊢ (((f:A–1-1-onto→B ⋀ z ⊆ B) ⋀ y = (^◡f “ z)) → z = (f “ y))
83	82	ex 373	. . . . . . . . 9 ⊢ ((f:A–1-1-onto→B ⋀ z ⊆ B) → (y = (^◡f “ z) → z = (f “ y)))
84		pm3.26 319	. . . . . . . . . . 11 ⊢ ((z ∈ ℘B ⋀ z ∈ {x∣x ≈ C}) → z ∈ ℘B)
85	84, 56	sylib 198	. . . . . . . . . 10 ⊢ ((z ∈ ℘B ⋀ z ∈ {x∣x ≈ C}) → z ⊆ B)
86	55, 85	sylbi 199	. . . . . . . . 9 ⊢ (z ∈ (℘B ∩ {x∣x ≈ C}) → z ⊆ B)
87	83, 86	sylan2 453	. . . . . . . 8 ⊢ ((f:A–1-1-onto→B ⋀ z ∈ (℘B ∩ {x∣x ≈ C})) → (y = (^◡f “ z) → z = (f “ y)))
88	87	adantrl 396	. . . . . . 7 ⊢ ((f:A–1-1-onto→B ⋀ (y ∈ (℘A ∩ {x∣x ≈ C}) ⋀ z ∈ (℘B ∩ {x∣x ≈ C}))) → (y = (^◡f “ z) → z = (f “ y)))
89		imaeq2 3408	. . . . . . . . . . . 12 ⊢ (z = (f “ y) → (^◡f “ z) = (^◡f “ (f “ y)))
90		f1imacnv 3711	. . . . . . . . . . . . 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 1532	. . . . . . . . . . 11 ⊢ (((f:A–1-1-onto→B ⋀ y ⊆ A) ⋀ z = (f “ y)) → (^◡f “ z) = y)
93	92	eqcomd 1483	. . . . . . . . . 10 ⊢ (((f:A–1-1-onto→B ⋀ y ⊆ A) ⋀ z = (f “ y)) → y = (^◡f “ z))
94	93	ex 373	. . . . . . . . 9 ⊢ ((f:A–1-1-onto→B ⋀ y ⊆ A) → (z = (f “ y) → y = (^◡f “ z)))
95		pm3.26 319	. . . . . . . . . . 11 ⊢ ((y ∈ ℘A ⋀ y ∈ {x∣x ≈ C}) → y ∈ ℘A)
96	95, 23	sylib 198	. . . . . . . . . 10 ⊢ ((y ∈ ℘A ⋀ y ∈ {x∣x ≈ C}) → y ⊆ A)
97	22, 96	sylbi 199	. . . . . . . . 9 ⊢ (y ∈ (℘A ∩ {x∣x ≈ C}) → y ⊆ A)
98	94, 97	sylan2 453	. . . . . . . 8 ⊢ ((f:A–1-1-onto→B ⋀ y ∈ (℘A ∩ {x∣x ≈ C})) → (z = (f “ y) → y = (^◡f “ z)))
99	98	adantrr 397	. . . . . . 7 ⊢ ((f:A–1-1-onto→B ⋀ (y ∈ (℘A ∩ {x∣x ≈ C}) ⋀ z ∈ (℘B ∩ {x∣x ≈ C}))) → (z = (f “ y) → y = (^◡f “ z)))
100	88, 99	impbid 518	. . . . . 6 ⊢ ((f:A–1-1-onto→B ⋀ (y ∈ (℘A ∩ {x∣x ≈ C}) ⋀ z ∈ (℘B ∩ {x∣x ≈ C}))) → (y = (^◡f “ z) ↔ z = (f “ y)))
101	100	ex 373	. . . . 5 ⊢ (f:A–1-1-onto→B → ((y ∈ (℘A ∩ {x∣x ≈ C}) ⋀ z ∈ (℘B ∩ {x∣x ≈ C})) → (y = (^◡f “ z) ↔ z = (f “ y))))
102	6, 37, 70, 101	en3d 4407	. . . 4 ⊢ (f:A–1-1-onto→B → (℘A ∩ {x∣x ≈ C}) ≈ (℘B ∩ {x∣x ≈ C}))
103	102	19.23aiv 1297	. . 3 ⊢ (∃f f:A–1-1-onto→B → (℘A ∩ {x∣x ≈ C}) ≈ (℘B ∩ {x∣x ≈ C}))
104	2, 103	sylbi 199	. 2 ⊢ (A ≈ B → (℘A ∩ {x∣x ≈ C}) ≈ (℘B ∩ {x∣x ≈ C}))
105		df-pw 2406	. . . 4 ⊢ ℘A = {x∣x ⊆ A}
106	105	ineq1i 2216	. . 3 ⊢ (℘A ∩ {x∣x ≈ C}) = ({x∣x ⊆ A} ∩ {x∣x ≈ C})
107		inab 2271	. . 3 ⊢ ({x∣x ⊆ A} ∩ {x∣x ≈ C}) = {x∣(x ⊆ A ⋀ x ≈ C)}
108	106, 107	eqtr 1498	. 2 ⊢ (℘A ∩ {x∣x ≈ C}) = {x∣(x ⊆ A ⋀ x ≈ C)}
109		df-pw 2406	. . . 4 ⊢ ℘B = {x∣x ⊆ B}
110	109	ineq1i 2216	. . 3 ⊢ (℘B ∩ {x∣x ≈ C}) = ({x∣x ⊆ B} ∩ {x∣x ≈ C})
111		inab 2271	. . 3 ⊢ ({x∣x ⊆ B} ∩ {x∣x ≈ C}) = {x∣(x ⊆ B ⋀ x ≈ C)}
112	110, 111	eqtr 1498	. 2 ⊢ (℘B ∩ {x∣x ≈ C}) = {x∣(x ⊆ B ⋀ x ≈ C)}
113	104, 108, 112	3brtr3g 2651	1 ⊢ (A ≈ B → {x∣(x ⊆ A ⋀ x ≈ C)} ≈ {x∣(x ⊆ B ⋀ x ≈ C)})

Colors of variables: wff set class

Syntax hints: → wi 3 ↔ wb 146 ⋀ wa 223 = wceq 958 ∈ wcel 960 ∃wex 982 {cab 1466 Vcvv 1814 ∩ cin 2049 ⊆ wss 2050 ℘cpw 2405 class class class wbr 2624 ^◡ccnv 3175 ran crn 3177 “ cima 3179 Rel wrel 3181 –1-1→wf1 3185 –onto→wfo 3186 –1-1-onto→wf1o 3187 ≈ cen 4370

This theorem is referenced by: infmap2 7583

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 964 ax-gen 965 ax-8 966 ax-9 967 ax-10 968 ax-11 969 ax-12 970 ax-13 971 ax-14 972 ax-17 973 ax-4 975 ax-5o 977 ax-6o 980 ax-9o 1125 ax-10o 1142 ax-16 1212 ax-11o 1220 ax-ext 1462 ax-rep 2698 ax-sep 2708 ax-pow 2748 ax-pr 2785 ax-un 2872

This theorem depends on definitions: df-bi 147 df-or 224 df-an 225 df-3an 779 df-ex 983 df-sb 1174 df-eu 1384 df-mo 1385 df-clab 1467 df-cleq 1472 df-clel 1475 df-ne 1590 df-ral 1652 df-rex 1653 df-v 1815 df-dif 2052 df-un 2053 df-in 2054 df-ss 2056 df-nul 2284 df-pw 2406 df-sn 2416 df-pr 2417 df-op 2420 df-uni 2508 df-br 2625 df-opab 2672 df-id 2841 df-xp 3190 df-rel 3191 df-cnv 3192 df-co 3193 df-dm 3194 df-rn 3195 df-res 3196 df-ima 3197 df-fun 3198 df-fn 3199 df-f 3200 df-f1 3201 df-fo 3202 df-f1o 3203 df-er 4267 df-en 4374