f1opwfi

Description: A one-to-one mapping induces a one-to-one mapping on finite subsets. (Contributed by Mario Carneiro, 25-Jan-2015)

		Ref	Expression
	Assertion	f1opwfi	$⊢ F : A \underset{1-1 onto}{⟶} B \to (b \in (𝒫 A \cap Fin) ⟼ F [b]) : 𝒫 A \cap Fin \underset{1-1 onto}{⟶} 𝒫 B \cap Fin$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ (b \in (𝒫 A \cap Fin) ⟼ F [b]) = (b \in (𝒫 A \cap Fin) ⟼ F [b])$
2		simpr	$⊢ (F : A \underset{1-1 onto}{⟶} B \land b \in (𝒫 A \cap Fin)) \to b \in (𝒫 A \cap Fin)$
3	2	elin2d	$⊢ (F : A \underset{1-1 onto}{⟶} B \land b \in (𝒫 A \cap Fin)) \to b \in Fin$
4		f1ofun	$⊢ F : A \underset{1-1 onto}{⟶} B \to Fun F$
5		elinel1	$⊢ b \in (𝒫 A \cap Fin) \to b \in 𝒫 A$
6		elpwi	$⊢ b \in 𝒫 A \to b \subseteq A$
7	5 6	syl	$⊢ b \in (𝒫 A \cap Fin) \to b \subseteq A$
8	7	adantl	$⊢ (F : A \underset{1-1 onto}{⟶} B \land b \in (𝒫 A \cap Fin)) \to b \subseteq A$
9		f1odm	$⊢ F : A \underset{1-1 onto}{⟶} B \to dom F = A$
10	9	adantr	$⊢ (F : A \underset{1-1 onto}{⟶} B \land b \in (𝒫 A \cap Fin)) \to dom F = A$
11	8 10	sseqtrrd	$⊢ (F : A \underset{1-1 onto}{⟶} B \land b \in (𝒫 A \cap Fin)) \to b \subseteq dom F$
12		fores	$⊢ (Fun F \land b \subseteq dom F) \to ({F ↾}_{b}) : b \underset{onto}{⟶} F [b]$
13	4 11 12	syl2an2r	$⊢ (F : A \underset{1-1 onto}{⟶} B \land b \in (𝒫 A \cap Fin)) \to ({F ↾}_{b}) : b \underset{onto}{⟶} F [b]$
14		fofi	$⊢ (b \in Fin \land ({F ↾}_{b}) : b \underset{onto}{⟶} F [b]) \to F [b] \in Fin$
15	3 13 14	syl2anc	$⊢ (F : A \underset{1-1 onto}{⟶} B \land b \in (𝒫 A \cap Fin)) \to F [b] \in Fin$
16		imassrn	$⊢ F [b] \subseteq ran F$
17		f1ofo	$⊢ F : A \underset{1-1 onto}{⟶} B \to F : A \underset{onto}{⟶} B$
18		forn	$⊢ F : A \underset{onto}{⟶} B \to ran F = B$
19	17 18	syl	$⊢ F : A \underset{1-1 onto}{⟶} B \to ran F = B$
20	16 19	sseqtrid	$⊢ F : A \underset{1-1 onto}{⟶} B \to F [b] \subseteq B$
21	20	adantr	$⊢ (F : A \underset{1-1 onto}{⟶} B \land b \in (𝒫 A \cap Fin)) \to F [b] \subseteq B$
22	15 21	elpwd	$⊢ (F : A \underset{1-1 onto}{⟶} B \land b \in (𝒫 A \cap Fin)) \to F [b] \in 𝒫 B$
23	22 15	elind	$⊢ (F : A \underset{1-1 onto}{⟶} B \land b \in (𝒫 A \cap Fin)) \to F [b] \in (𝒫 B \cap Fin)$
24		simpr	$⊢ (F : A \underset{1-1 onto}{⟶} B \land a \in (𝒫 B \cap Fin)) \to a \in (𝒫 B \cap Fin)$
25	24	elin2d	$⊢ (F : A \underset{1-1 onto}{⟶} B \land a \in (𝒫 B \cap Fin)) \to a \in Fin$
26		dff1o3	$⊢ F : A \underset{1-1 onto}{⟶} B \leftrightarrow (F : A \underset{onto}{⟶} B \land Fun F^{-1})$
27	26	simprbi	$⊢ F : A \underset{1-1 onto}{⟶} B \to Fun F^{-1}$
28		elinel1	$⊢ a \in (𝒫 B \cap Fin) \to a \in 𝒫 B$
29	28	adantl	$⊢ (F : A \underset{1-1 onto}{⟶} B \land a \in (𝒫 B \cap Fin)) \to a \in 𝒫 B$
30		elpwi	$⊢ a \in 𝒫 B \to a \subseteq B$
31	29 30	syl	$⊢ (F : A \underset{1-1 onto}{⟶} B \land a \in (𝒫 B \cap Fin)) \to a \subseteq B$
32		f1ocnv	$⊢ F : A \underset{1-1 onto}{⟶} B \to F^{-1} : B \underset{1-1 onto}{⟶} A$
33	32	adantr	$⊢ (F : A \underset{1-1 onto}{⟶} B \land a \in (𝒫 B \cap Fin)) \to F^{-1} : B \underset{1-1 onto}{⟶} A$
34		f1odm	$⊢ F^{-1} : B \underset{1-1 onto}{⟶} A \to dom F^{-1} = B$
35	33 34	syl	$⊢ (F : A \underset{1-1 onto}{⟶} B \land a \in (𝒫 B \cap Fin)) \to dom F^{-1} = B$
36	31 35	sseqtrrd	$⊢ (F : A \underset{1-1 onto}{⟶} B \land a \in (𝒫 B \cap Fin)) \to a \subseteq dom F^{-1}$
37		fores	$⊢ (Fun F^{-1} \land a \subseteq dom F^{-1}) \to ({F^{-1} ↾}_{a}) : a \underset{onto}{⟶} F^{-1} [a]$
38	27 36 37	syl2an2r	$⊢ (F : A \underset{1-1 onto}{⟶} B \land a \in (𝒫 B \cap Fin)) \to ({F^{-1} ↾}_{a}) : a \underset{onto}{⟶} F^{-1} [a]$
39		fofi	$⊢ (a \in Fin \land ({F^{-1} ↾}_{a}) : a \underset{onto}{⟶} F^{-1} [a]) \to F^{-1} [a] \in Fin$
40	25 38 39	syl2anc	$⊢ (F : A \underset{1-1 onto}{⟶} B \land a \in (𝒫 B \cap Fin)) \to F^{-1} [a] \in Fin$
41		imassrn	$⊢ F^{-1} [a] \subseteq ran F^{-1}$
42		dfdm4	$⊢ dom F = ran F^{-1}$
43	42 9	eqtr3id	$⊢ F : A \underset{1-1 onto}{⟶} B \to ran F^{-1} = A$
44	41 43	sseqtrid	$⊢ F : A \underset{1-1 onto}{⟶} B \to F^{-1} [a] \subseteq A$
45	44	adantr	$⊢ (F : A \underset{1-1 onto}{⟶} B \land a \in (𝒫 B \cap Fin)) \to F^{-1} [a] \subseteq A$
46	40 45	elpwd	$⊢ (F : A \underset{1-1 onto}{⟶} B \land a \in (𝒫 B \cap Fin)) \to F^{-1} [a] \in 𝒫 A$
47	46 40	elind	$⊢ (F : A \underset{1-1 onto}{⟶} B \land a \in (𝒫 B \cap Fin)) \to F^{-1} [a] \in (𝒫 A \cap Fin)$
48	5 28	anim12i	$⊢ (b \in (𝒫 A \cap Fin) \land a \in (𝒫 B \cap Fin)) \to (b \in 𝒫 A \land a \in 𝒫 B)$
49	30	adantl	$⊢ (b \in 𝒫 A \land a \in 𝒫 B) \to a \subseteq B$
50		foimacnv	$⊢ (F : A \underset{onto}{⟶} B \land a \subseteq B) \to F [F^{-1} [a]] = a$
51	17 49 50	syl2an	$⊢ (F : A \underset{1-1 onto}{⟶} B \land (b \in 𝒫 A \land a \in 𝒫 B)) \to F [F^{-1} [a]] = a$
52	51	eqcomd	$⊢ (F : A \underset{1-1 onto}{⟶} B \land (b \in 𝒫 A \land a \in 𝒫 B)) \to a = F [F^{-1} [a]]$
53		imaeq2	$⊢ b = F^{-1} [a] \to F [b] = F [F^{-1} [a]]$
54	53	eqeq2d	$⊢ b = F^{-1} [a] \to (a = F [b] \leftrightarrow a = F [F^{-1} [a]])$
55	52 54	syl5ibrcom	$⊢ (F : A \underset{1-1 onto}{⟶} B \land (b \in 𝒫 A \land a \in 𝒫 B)) \to (b = F^{-1} [a] \to a = F [b])$
56		f1of1	$⊢ F : A \underset{1-1 onto}{⟶} B \to F : A \underset{1-1}{⟶} B$
57	6	adantr	$⊢ (b \in 𝒫 A \land a \in 𝒫 B) \to b \subseteq A$
58		f1imacnv	$⊢ (F : A \underset{1-1}{⟶} B \land b \subseteq A) \to F^{-1} [F [b]] = b$
59	56 57 58	syl2an	$⊢ (F : A \underset{1-1 onto}{⟶} B \land (b \in 𝒫 A \land a \in 𝒫 B)) \to F^{-1} [F [b]] = b$
60	59	eqcomd	$⊢ (F : A \underset{1-1 onto}{⟶} B \land (b \in 𝒫 A \land a \in 𝒫 B)) \to b = F^{-1} [F [b]]$
61		imaeq2	$⊢ a = F [b] \to F^{-1} [a] = F^{-1} [F [b]]$
62	61	eqeq2d	$⊢ a = F [b] \to (b = F^{-1} [a] \leftrightarrow b = F^{-1} [F [b]])$
63	60 62	syl5ibrcom	$⊢ (F : A \underset{1-1 onto}{⟶} B \land (b \in 𝒫 A \land a \in 𝒫 B)) \to (a = F [b] \to b = F^{-1} [a])$
64	55 63	impbid	$⊢ (F : A \underset{1-1 onto}{⟶} B \land (b \in 𝒫 A \land a \in 𝒫 B)) \to (b = F^{-1} [a] \leftrightarrow a = F [b])$
65	48 64	sylan2	$⊢ (F : A \underset{1-1 onto}{⟶} B \land (b \in (𝒫 A \cap Fin) \land a \in (𝒫 B \cap Fin))) \to (b = F^{-1} [a] \leftrightarrow a = F [b])$
66	1 23 47 65	f1o2d	$⊢ F : A \underset{1-1 onto}{⟶} B \to (b \in (𝒫 A \cap Fin) ⟼ F [b]) : 𝒫 A \cap Fin \underset{1-1 onto}{⟶} 𝒫 B \cap Fin$

Metamath Proof Explorer

Theorem f1opwfi

Proof