ssenen

Description: Equinumerosity of equinumerous subsets of a set. (Contributed by NM, 30-Sep-2004) (Revised by Mario Carneiro, 16-Nov-2014)

		Ref	Expression
	Assertion	ssenen	$⊢ A \approx B \to \{x \| (x \subseteq A \land x \approx C)\} \approx \{x \| (x \subseteq B \land x \approx C)\}$

Proof

Step	Hyp	Ref	Expression
1		bren	$⊢ A \approx B \leftrightarrow \exists f f : A \underset{1-1 onto}{⟶} B$
2		f1odm	$⊢ f : A \underset{1-1 onto}{⟶} B \to dom f = A$
3		vex	$⊢ f \in V$
4	3	dmex	$⊢ dom f \in V$
5	2 4	eqeltrrdi	$⊢ f : A \underset{1-1 onto}{⟶} B \to A \in V$
6		pwexg	$⊢ A \in V \to 𝒫 A \in V$
7		inex1g	$⊢ 𝒫 A \in V \to 𝒫 A \cap \{x \| x \approx C\} \in V$
8	5 6 7	3syl	$⊢ f : A \underset{1-1 onto}{⟶} B \to 𝒫 A \cap \{x \| x \approx C\} \in V$
9		f1ofo	$⊢ f : A \underset{1-1 onto}{⟶} B \to f : A \underset{onto}{⟶} B$
10		forn	$⊢ f : A \underset{onto}{⟶} B \to ran f = B$
11	9 10	syl	$⊢ f : A \underset{1-1 onto}{⟶} B \to ran f = B$
12	3	rnex	$⊢ ran f \in V$
13	11 12	eqeltrrdi	$⊢ f : A \underset{1-1 onto}{⟶} B \to B \in V$
14		pwexg	$⊢ B \in V \to 𝒫 B \in V$
15		inex1g	$⊢ 𝒫 B \in V \to 𝒫 B \cap \{x \| x \approx C\} \in V$
16	13 14 15	3syl	$⊢ f : A \underset{1-1 onto}{⟶} B \to 𝒫 B \cap \{x \| x \approx C\} \in V$
17		f1of1	$⊢ f : A \underset{1-1 onto}{⟶} B \to f : A \underset{1-1}{⟶} B$
18	17	adantr	$⊢ (f : A \underset{1-1 onto}{⟶} B \land y \subseteq A) \to f : A \underset{1-1}{⟶} B$
19	13	adantr	$⊢ (f : A \underset{1-1 onto}{⟶} B \land y \subseteq A) \to B \in V$
20		simpr	$⊢ (f : A \underset{1-1 onto}{⟶} B \land y \subseteq A) \to y \subseteq A$
21		vex	$⊢ y \in V$
22	21	a1i	$⊢ (f : A \underset{1-1 onto}{⟶} B \land y \subseteq A) \to y \in V$
23		f1imaen2g	$⊢ ((f : A \underset{1-1}{⟶} B \land B \in V) \land (y \subseteq A \land y \in V)) \to f [y] \approx y$
24	18 19 20 22 23	syl22anc	$⊢ (f : A \underset{1-1 onto}{⟶} B \land y \subseteq A) \to f [y] \approx y$
25		entr	$⊢ (f [y] \approx y \land y \approx C) \to f [y] \approx C$
26	24 25	sylan	$⊢ ((f : A \underset{1-1 onto}{⟶} B \land y \subseteq A) \land y \approx C) \to f [y] \approx C$
27	26	expl	$⊢ f : A \underset{1-1 onto}{⟶} B \to ((y \subseteq A \land y \approx C) \to f [y] \approx C)$
28		imassrn	$⊢ f [y] \subseteq ran f$
29	28 10	sseqtrid	$⊢ f : A \underset{onto}{⟶} B \to f [y] \subseteq B$
30	9 29	syl	$⊢ f : A \underset{1-1 onto}{⟶} B \to f [y] \subseteq B$
31	27 30	jctild	$⊢ f : A \underset{1-1 onto}{⟶} B \to ((y \subseteq A \land y \approx C) \to (f [y] \subseteq B \land f [y] \approx C))$
32		elin	$⊢ y \in (𝒫 A \cap \{x \| x \approx C\}) \leftrightarrow (y \in 𝒫 A \land y \in \{x \| x \approx C\})$
33	21	elpw	$⊢ y \in 𝒫 A \leftrightarrow y \subseteq A$
34		breq1	$⊢ x = y \to (x \approx C \leftrightarrow y \approx C)$
35	21 34	elab	$⊢ y \in \{x \| x \approx C\} \leftrightarrow y \approx C$
36	33 35	anbi12i	$⊢ (y \in 𝒫 A \land y \in \{x \| x \approx C\}) \leftrightarrow (y \subseteq A \land y \approx C)$
37	32 36	bitri	$⊢ y \in (𝒫 A \cap \{x \| x \approx C\}) \leftrightarrow (y \subseteq A \land y \approx C)$
38		elin	$⊢ f [y] \in (𝒫 B \cap \{x \| x \approx C\}) \leftrightarrow (f [y] \in 𝒫 B \land f [y] \in \{x \| x \approx C\})$
39	3	imaex	$⊢ f [y] \in V$
40	39	elpw	$⊢ f [y] \in 𝒫 B \leftrightarrow f [y] \subseteq B$
41		breq1	$⊢ x = f [y] \to (x \approx C \leftrightarrow f [y] \approx C)$
42	39 41	elab	$⊢ f [y] \in \{x \| x \approx C\} \leftrightarrow f [y] \approx C$
43	40 42	anbi12i	$⊢ (f [y] \in 𝒫 B \land f [y] \in \{x \| x \approx C\}) \leftrightarrow (f [y] \subseteq B \land f [y] \approx C)$
44	38 43	bitri	$⊢ f [y] \in (𝒫 B \cap \{x \| x \approx C\}) \leftrightarrow (f [y] \subseteq B \land f [y] \approx C)$
45	31 37 44	3imtr4g	$⊢ f : A \underset{1-1 onto}{⟶} B \to (y \in (𝒫 A \cap \{x \| x \approx C\}) \to f [y] \in (𝒫 B \cap \{x \| x \approx C\}))$
46		f1ocnv	$⊢ f : A \underset{1-1 onto}{⟶} B \to f^{-1} : B \underset{1-1 onto}{⟶} A$
47		f1of1	$⊢ f^{-1} : B \underset{1-1 onto}{⟶} A \to f^{-1} : B \underset{1-1}{⟶} A$
48		f1f1orn	$⊢ f^{-1} : B \underset{1-1}{⟶} A \to f^{-1} : B \underset{1-1 onto}{⟶} ran f^{-1}$
49		f1of1	$⊢ f^{-1} : B \underset{1-1 onto}{⟶} ran f^{-1} \to f^{-1} : B \underset{1-1}{⟶} ran f^{-1}$
50	47 48 49	3syl	$⊢ f^{-1} : B \underset{1-1 onto}{⟶} A \to f^{-1} : B \underset{1-1}{⟶} ran f^{-1}$
51		vex	$⊢ z \in V$
52	51	f1imaen	$⊢ (f^{-1} : B \underset{1-1}{⟶} ran f^{-1} \land z \subseteq B) \to f^{-1} [z] \approx z$
53	50 52	sylan	$⊢ (f^{-1} : B \underset{1-1 onto}{⟶} A \land z \subseteq B) \to f^{-1} [z] \approx z$
54		entr	$⊢ (f^{-1} [z] \approx z \land z \approx C) \to f^{-1} [z] \approx C$
55	53 54	sylan	$⊢ ((f^{-1} : B \underset{1-1 onto}{⟶} A \land z \subseteq B) \land z \approx C) \to f^{-1} [z] \approx C$
56	55	expl	$⊢ f^{-1} : B \underset{1-1 onto}{⟶} A \to ((z \subseteq B \land z \approx C) \to f^{-1} [z] \approx C)$
57		f1ofo	$⊢ f^{-1} : B \underset{1-1 onto}{⟶} A \to f^{-1} : B \underset{onto}{⟶} A$
58		imassrn	$⊢ f^{-1} [z] \subseteq ran f^{-1}$
59		forn	$⊢ f^{-1} : B \underset{onto}{⟶} A \to ran f^{-1} = A$
60	58 59	sseqtrid	$⊢ f^{-1} : B \underset{onto}{⟶} A \to f^{-1} [z] \subseteq A$
61	57 60	syl	$⊢ f^{-1} : B \underset{1-1 onto}{⟶} A \to f^{-1} [z] \subseteq A$
62	56 61	jctild	$⊢ f^{-1} : B \underset{1-1 onto}{⟶} A \to ((z \subseteq B \land z \approx C) \to (f^{-1} [z] \subseteq A \land f^{-1} [z] \approx C))$
63	46 62	syl	$⊢ f : A \underset{1-1 onto}{⟶} B \to ((z \subseteq B \land z \approx C) \to (f^{-1} [z] \subseteq A \land f^{-1} [z] \approx C))$
64		elin	$⊢ z \in (𝒫 B \cap \{x \| x \approx C\}) \leftrightarrow (z \in 𝒫 B \land z \in \{x \| x \approx C\})$
65	51	elpw	$⊢ z \in 𝒫 B \leftrightarrow z \subseteq B$
66		breq1	$⊢ x = z \to (x \approx C \leftrightarrow z \approx C)$
67	51 66	elab	$⊢ z \in \{x \| x \approx C\} \leftrightarrow z \approx C$
68	65 67	anbi12i	$⊢ (z \in 𝒫 B \land z \in \{x \| x \approx C\}) \leftrightarrow (z \subseteq B \land z \approx C)$
69	64 68	bitri	$⊢ z \in (𝒫 B \cap \{x \| x \approx C\}) \leftrightarrow (z \subseteq B \land z \approx C)$
70		elin	$⊢ f^{-1} [z] \in (𝒫 A \cap \{x \| x \approx C\}) \leftrightarrow (f^{-1} [z] \in 𝒫 A \land f^{-1} [z] \in \{x \| x \approx C\})$
71	3	cnvex	$⊢ f^{-1} \in V$
72	71	imaex	$⊢ f^{-1} [z] \in V$
73	72	elpw	$⊢ f^{-1} [z] \in 𝒫 A \leftrightarrow f^{-1} [z] \subseteq A$
74		breq1	$⊢ x = f^{-1} [z] \to (x \approx C \leftrightarrow f^{-1} [z] \approx C)$
75	72 74	elab	$⊢ f^{-1} [z] \in \{x \| x \approx C\} \leftrightarrow f^{-1} [z] \approx C$
76	73 75	anbi12i	$⊢ (f^{-1} [z] \in 𝒫 A \land f^{-1} [z] \in \{x \| x \approx C\}) \leftrightarrow (f^{-1} [z] \subseteq A \land f^{-1} [z] \approx C)$
77	70 76	bitri	$⊢ f^{-1} [z] \in (𝒫 A \cap \{x \| x \approx C\}) \leftrightarrow (f^{-1} [z] \subseteq A \land f^{-1} [z] \approx C)$
78	63 69 77	3imtr4g	$⊢ f : A \underset{1-1 onto}{⟶} B \to (z \in (𝒫 B \cap \{x \| x \approx C\}) \to f^{-1} [z] \in (𝒫 A \cap \{x \| x \approx C\}))$
79		simpl	$⊢ (z \in 𝒫 B \land z \in \{x \| x \approx C\}) \to z \in 𝒫 B$
80	79	elpwid	$⊢ (z \in 𝒫 B \land z \in \{x \| x \approx C\}) \to z \subseteq B$
81	64 80	sylbi	$⊢ z \in (𝒫 B \cap \{x \| x \approx C\}) \to z \subseteq B$
82		imaeq2	$⊢ y = f^{-1} [z] \to f [y] = f [f^{-1} [z]]$
83		f1orel	$⊢ f : A \underset{1-1 onto}{⟶} B \to Rel f$
84		dfrel2	$⊢ Rel f \leftrightarrow {f^{-1}}^{-1} = f$
85	83 84	sylib	$⊢ f : A \underset{1-1 onto}{⟶} B \to {f^{-1}}^{-1} = f$
86	85	imaeq1d	$⊢ f : A \underset{1-1 onto}{⟶} B \to {f^{-1}}^{-1} [f^{-1} [z]] = f [f^{-1} [z]]$
87	86	adantr	$⊢ (f : A \underset{1-1 onto}{⟶} B \land z \subseteq B) \to {f^{-1}}^{-1} [f^{-1} [z]] = f [f^{-1} [z]]$
88	46 47	syl	$⊢ f : A \underset{1-1 onto}{⟶} B \to f^{-1} : B \underset{1-1}{⟶} A$
89		f1imacnv	$⊢ (f^{-1} : B \underset{1-1}{⟶} A \land z \subseteq B) \to {f^{-1}}^{-1} [f^{-1} [z]] = z$
90	88 89	sylan	$⊢ (f : A \underset{1-1 onto}{⟶} B \land z \subseteq B) \to {f^{-1}}^{-1} [f^{-1} [z]] = z$
91	87 90	eqtr3d	$⊢ (f : A \underset{1-1 onto}{⟶} B \land z \subseteq B) \to f [f^{-1} [z]] = z$
92	82 91	sylan9eqr	$⊢ ((f : A \underset{1-1 onto}{⟶} B \land z \subseteq B) \land y = f^{-1} [z]) \to f [y] = z$
93	92	eqcomd	$⊢ ((f : A \underset{1-1 onto}{⟶} B \land z \subseteq B) \land y = f^{-1} [z]) \to z = f [y]$
94	93	ex	$⊢ (f : A \underset{1-1 onto}{⟶} B \land z \subseteq B) \to (y = f^{-1} [z] \to z = f [y])$
95	81 94	sylan2	$⊢ (f : A \underset{1-1 onto}{⟶} B \land z \in (𝒫 B \cap \{x \| x \approx C\})) \to (y = f^{-1} [z] \to z = f [y])$
96	95	adantrl	$⊢ (f : A \underset{1-1 onto}{⟶} B \land (y \in (𝒫 A \cap \{x \| x \approx C\}) \land z \in (𝒫 B \cap \{x \| x \approx C\}))) \to (y = f^{-1} [z] \to z = f [y])$
97		simpl	$⊢ (y \in 𝒫 A \land y \in \{x \| x \approx C\}) \to y \in 𝒫 A$
98	97	elpwid	$⊢ (y \in 𝒫 A \land y \in \{x \| x \approx C\}) \to y \subseteq A$
99	32 98	sylbi	$⊢ y \in (𝒫 A \cap \{x \| x \approx C\}) \to y \subseteq A$
100		imaeq2	$⊢ z = f [y] \to f^{-1} [z] = f^{-1} [f [y]]$
101		f1imacnv	$⊢ (f : A \underset{1-1}{⟶} B \land y \subseteq A) \to f^{-1} [f [y]] = y$
102	17 101	sylan	$⊢ (f : A \underset{1-1 onto}{⟶} B \land y \subseteq A) \to f^{-1} [f [y]] = y$
103	100 102	sylan9eqr	$⊢ ((f : A \underset{1-1 onto}{⟶} B \land y \subseteq A) \land z = f [y]) \to f^{-1} [z] = y$
104	103	eqcomd	$⊢ ((f : A \underset{1-1 onto}{⟶} B \land y \subseteq A) \land z = f [y]) \to y = f^{-1} [z]$
105	104	ex	$⊢ (f : A \underset{1-1 onto}{⟶} B \land y \subseteq A) \to (z = f [y] \to y = f^{-1} [z])$
106	99 105	sylan2	$⊢ (f : A \underset{1-1 onto}{⟶} B \land y \in (𝒫 A \cap \{x \| x \approx C\})) \to (z = f [y] \to y = f^{-1} [z])$
107	106	adantrr	$⊢ (f : A \underset{1-1 onto}{⟶} B \land (y \in (𝒫 A \cap \{x \| x \approx C\}) \land z \in (𝒫 B \cap \{x \| x \approx C\}))) \to (z = f [y] \to y = f^{-1} [z])$
108	96 107	impbid	$⊢ (f : A \underset{1-1 onto}{⟶} B \land (y \in (𝒫 A \cap \{x \| x \approx C\}) \land z \in (𝒫 B \cap \{x \| x \approx C\}))) \to (y = f^{-1} [z] \leftrightarrow z = f [y])$
109	108	ex	$⊢ f : A \underset{1-1 onto}{⟶} B \to ((y \in (𝒫 A \cap \{x \| x \approx C\}) \land z \in (𝒫 B \cap \{x \| x \approx C\})) \to (y = f^{-1} [z] \leftrightarrow z = f [y]))$
110	8 16 45 78 109	en3d	$⊢ f : A \underset{1-1 onto}{⟶} B \to (𝒫 A \cap \{x \| x \approx C\}) \approx (𝒫 B \cap \{x \| x \approx C\})$
111	110	exlimiv	$⊢ \exists f f : A \underset{1-1 onto}{⟶} B \to (𝒫 A \cap \{x \| x \approx C\}) \approx (𝒫 B \cap \{x \| x \approx C\})$
112	1 111	sylbi	$⊢ A \approx B \to (𝒫 A \cap \{x \| x \approx C\}) \approx (𝒫 B \cap \{x \| x \approx C\})$
113		df-pw	$⊢ 𝒫 A = \{x \| x \subseteq A\}$
114	113	ineq1i	$⊢ 𝒫 A \cap \{x \| x \approx C\} = \{x \| x \subseteq A\} \cap \{x \| x \approx C\}$
115		inab	$⊢ \{x \| x \subseteq A\} \cap \{x \| x \approx C\} = \{x \| (x \subseteq A \land x \approx C)\}$
116	114 115	eqtri	$⊢ 𝒫 A \cap \{x \| x \approx C\} = \{x \| (x \subseteq A \land x \approx C)\}$
117		df-pw	$⊢ 𝒫 B = \{x \| x \subseteq B\}$
118	117	ineq1i	$⊢ 𝒫 B \cap \{x \| x \approx C\} = \{x \| x \subseteq B\} \cap \{x \| x \approx C\}$
119		inab	$⊢ \{x \| x \subseteq B\} \cap \{x \| x \approx C\} = \{x \| (x \subseteq B \land x \approx C)\}$
120	118 119	eqtri	$⊢ 𝒫 B \cap \{x \| x \approx C\} = \{x \| (x \subseteq B \land x \approx C)\}$
121	112 116 120	3brtr3g	$⊢ A \approx B \to \{x \| (x \subseteq A \land x \approx C)\} \approx \{x \| (x \subseteq B \land x \approx C)\}$

Metamath Proof Explorer

Theorem ssenen

Proof