indf1ofs

Description: The bijection between finite subsets and the indicator functions with finite support. (Contributed by Thierry Arnoux, 22-Aug-2017)

		Ref	Expression
	Assertion	indf1ofs	$⊢ O \in V \to ({𝟙_{O} ↾}_{Fin}) : 𝒫 O \cap Fin \underset{1-1 onto}{⟶} \{f \in ({\{0, 1\}}^{O}) \| f^{-1} [\{1\}] \in Fin\}$

Proof

Step	Hyp	Ref	Expression
1		indf1o	$⊢ O \in V \to 𝟙_{O} : 𝒫 O \underset{1-1 onto}{⟶} {\{0, 1\}}^{O}$
2		f1of1	$⊢ 𝟙_{O} : 𝒫 O \underset{1-1 onto}{⟶} {\{0, 1\}}^{O} \to 𝟙_{O} : 𝒫 O \underset{1-1}{⟶} {\{0, 1\}}^{O}$
3	1 2	syl	$⊢ O \in V \to 𝟙_{O} : 𝒫 O \underset{1-1}{⟶} {\{0, 1\}}^{O}$
4		inss1	$⊢ 𝒫 O \cap Fin \subseteq 𝒫 O$
5		f1ores	$⊢ (𝟙_{O} : 𝒫 O \underset{1-1}{⟶} {\{0, 1\}}^{O} \land 𝒫 O \cap Fin \subseteq 𝒫 O) \to ({𝟙_{O} ↾}_{(𝒫 O \cap Fin)}) : 𝒫 O \cap Fin \underset{1-1 onto}{⟶} 𝟙_{O} [𝒫 O \cap Fin]$
6	3 4 5	sylancl	$⊢ O \in V \to ({𝟙_{O} ↾}_{(𝒫 O \cap Fin)}) : 𝒫 O \cap Fin \underset{1-1 onto}{⟶} 𝟙_{O} [𝒫 O \cap Fin]$
7		resres	$⊢ {({𝟙_{O} ↾}_{𝒫 O}) ↾}_{Fin} = {𝟙_{O} ↾}_{(𝒫 O \cap Fin)}$
8		f1ofn	$⊢ 𝟙_{O} : 𝒫 O \underset{1-1 onto}{⟶} {\{0, 1\}}^{O} \to 𝟙_{O} Fn 𝒫 O$
9		fnresdm	$⊢ 𝟙_{O} Fn 𝒫 O \to {𝟙_{O} ↾}_{𝒫 O} = 𝟙_{O}$
10	1 8 9	3syl	$⊢ O \in V \to {𝟙_{O} ↾}_{𝒫 O} = 𝟙_{O}$
11	10	reseq1d	$⊢ O \in V \to {({𝟙_{O} ↾}_{𝒫 O}) ↾}_{Fin} = {𝟙_{O} ↾}_{Fin}$
12	7 11	eqtr3id	$⊢ O \in V \to {𝟙_{O} ↾}_{(𝒫 O \cap Fin)} = {𝟙_{O} ↾}_{Fin}$
13		eqidd	$⊢ O \in V \to 𝒫 O \cap Fin = 𝒫 O \cap Fin$
14		simpll	$⊢ ((O \in V \land a \in (𝒫 O \cap Fin)) \land 𝟙_{O} (a) = g) \to O \in V$
15		simpr	$⊢ (O \in V \land a \in (𝒫 O \cap Fin)) \to a \in (𝒫 O \cap Fin)$
16	4 15	sselid	$⊢ (O \in V \land a \in (𝒫 O \cap Fin)) \to a \in 𝒫 O$
17	16	elpwid	$⊢ (O \in V \land a \in (𝒫 O \cap Fin)) \to a \subseteq O$
18		indf	$⊢ (O \in V \land a \subseteq O) \to 𝟙_{O} (a) : O ⟶ \{0, 1\}$
19	17 18	syldan	$⊢ (O \in V \land a \in (𝒫 O \cap Fin)) \to 𝟙_{O} (a) : O ⟶ \{0, 1\}$
20	19	adantr	$⊢ ((O \in V \land a \in (𝒫 O \cap Fin)) \land 𝟙_{O} (a) = g) \to 𝟙_{O} (a) : O ⟶ \{0, 1\}$
21		simpr	$⊢ ((O \in V \land a \in (𝒫 O \cap Fin)) \land 𝟙_{O} (a) = g) \to 𝟙_{O} (a) = g$
22	21	feq1d	$⊢ ((O \in V \land a \in (𝒫 O \cap Fin)) \land 𝟙_{O} (a) = g) \to (𝟙_{O} (a) : O ⟶ \{0, 1\} \leftrightarrow g : O ⟶ \{0, 1\})$
23	20 22	mpbid	$⊢ ((O \in V \land a \in (𝒫 O \cap Fin)) \land 𝟙_{O} (a) = g) \to g : O ⟶ \{0, 1\}$
24		prex	$⊢ \{0, 1\} \in V$
25		elmapg	$⊢ (\{0, 1\} \in V \land O \in V) \to (g \in ({\{0, 1\}}^{O}) \leftrightarrow g : O ⟶ \{0, 1\})$
26	24 25	mpan	$⊢ O \in V \to (g \in ({\{0, 1\}}^{O}) \leftrightarrow g : O ⟶ \{0, 1\})$
27	26	biimpar	$⊢ (O \in V \land g : O ⟶ \{0, 1\}) \to g \in ({\{0, 1\}}^{O})$
28	14 23 27	syl2anc	$⊢ ((O \in V \land a \in (𝒫 O \cap Fin)) \land 𝟙_{O} (a) = g) \to g \in ({\{0, 1\}}^{O})$
29	21	cnveqd	$⊢ ((O \in V \land a \in (𝒫 O \cap Fin)) \land 𝟙_{O} (a) = g) \to {𝟙_{O} (a)}^{-1} = g^{-1}$
30	29	imaeq1d	$⊢ ((O \in V \land a \in (𝒫 O \cap Fin)) \land 𝟙_{O} (a) = g) \to {𝟙_{O} (a)}^{-1} [\{1\}] = g^{-1} [\{1\}]$
31		indpi1	$⊢ (O \in V \land a \subseteq O) \to {𝟙_{O} (a)}^{-1} [\{1\}] = a$
32	17 31	syldan	$⊢ (O \in V \land a \in (𝒫 O \cap Fin)) \to {𝟙_{O} (a)}^{-1} [\{1\}] = a$
33		inss2	$⊢ 𝒫 O \cap Fin \subseteq Fin$
34	33 15	sselid	$⊢ (O \in V \land a \in (𝒫 O \cap Fin)) \to a \in Fin$
35	32 34	eqeltrd	$⊢ (O \in V \land a \in (𝒫 O \cap Fin)) \to {𝟙_{O} (a)}^{-1} [\{1\}] \in Fin$
36	35	adantr	$⊢ ((O \in V \land a \in (𝒫 O \cap Fin)) \land 𝟙_{O} (a) = g) \to {𝟙_{O} (a)}^{-1} [\{1\}] \in Fin$
37	30 36	eqeltrrd	$⊢ ((O \in V \land a \in (𝒫 O \cap Fin)) \land 𝟙_{O} (a) = g) \to g^{-1} [\{1\}] \in Fin$
38	28 37	jca	$⊢ ((O \in V \land a \in (𝒫 O \cap Fin)) \land 𝟙_{O} (a) = g) \to (g \in ({\{0, 1\}}^{O}) \land g^{-1} [\{1\}] \in Fin)$
39	38	rexlimdva2	$⊢ O \in V \to (\exists a \in (𝒫 O \cap Fin) 𝟙_{O} (a) = g \to (g \in ({\{0, 1\}}^{O}) \land g^{-1} [\{1\}] \in Fin))$
40		cnvimass	$⊢ g^{-1} [\{1\}] \subseteq dom g$
41	26	biimpa	$⊢ (O \in V \land g \in ({\{0, 1\}}^{O})) \to g : O ⟶ \{0, 1\}$
42	41	fdmd	$⊢ (O \in V \land g \in ({\{0, 1\}}^{O})) \to dom g = O$
43	42	adantrr	$⊢ (O \in V \land (g \in ({\{0, 1\}}^{O}) \land g^{-1} [\{1\}] \in Fin)) \to dom g = O$
44	40 43	sseqtrid	$⊢ (O \in V \land (g \in ({\{0, 1\}}^{O}) \land g^{-1} [\{1\}] \in Fin)) \to g^{-1} [\{1\}] \subseteq O$
45		simprr	$⊢ (O \in V \land (g \in ({\{0, 1\}}^{O}) \land g^{-1} [\{1\}] \in Fin)) \to g^{-1} [\{1\}] \in Fin$
46		elfpw	$⊢ g^{-1} [\{1\}] \in (𝒫 O \cap Fin) \leftrightarrow (g^{-1} [\{1\}] \subseteq O \land g^{-1} [\{1\}] \in Fin)$
47	44 45 46	sylanbrc	$⊢ (O \in V \land (g \in ({\{0, 1\}}^{O}) \land g^{-1} [\{1\}] \in Fin)) \to g^{-1} [\{1\}] \in (𝒫 O \cap Fin)$
48		indpreima	$⊢ (O \in V \land g : O ⟶ \{0, 1\}) \to g = 𝟙_{O} (g^{-1} [\{1\}])$
49	48	eqcomd	$⊢ (O \in V \land g : O ⟶ \{0, 1\}) \to 𝟙_{O} (g^{-1} [\{1\}]) = g$
50	41 49	syldan	$⊢ (O \in V \land g \in ({\{0, 1\}}^{O})) \to 𝟙_{O} (g^{-1} [\{1\}]) = g$
51	50	adantrr	$⊢ (O \in V \land (g \in ({\{0, 1\}}^{O}) \land g^{-1} [\{1\}] \in Fin)) \to 𝟙_{O} (g^{-1} [\{1\}]) = g$
52		fveqeq2	$⊢ a = g^{-1} [\{1\}] \to (𝟙_{O} (a) = g \leftrightarrow 𝟙_{O} (g^{-1} [\{1\}]) = g)$
53	52	rspcev	$⊢ (g^{-1} [\{1\}] \in (𝒫 O \cap Fin) \land 𝟙_{O} (g^{-1} [\{1\}]) = g) \to \exists a \in (𝒫 O \cap Fin) 𝟙_{O} (a) = g$
54	47 51 53	syl2anc	$⊢ (O \in V \land (g \in ({\{0, 1\}}^{O}) \land g^{-1} [\{1\}] \in Fin)) \to \exists a \in (𝒫 O \cap Fin) 𝟙_{O} (a) = g$
55	54	ex	$⊢ O \in V \to ((g \in ({\{0, 1\}}^{O}) \land g^{-1} [\{1\}] \in Fin) \to \exists a \in (𝒫 O \cap Fin) 𝟙_{O} (a) = g)$
56	39 55	impbid	$⊢ O \in V \to (\exists a \in (𝒫 O \cap Fin) 𝟙_{O} (a) = g \leftrightarrow (g \in ({\{0, 1\}}^{O}) \land g^{-1} [\{1\}] \in Fin))$
57	1 8	syl	$⊢ O \in V \to 𝟙_{O} Fn 𝒫 O$
58		fvelimab	$⊢ (𝟙_{O} Fn 𝒫 O \land 𝒫 O \cap Fin \subseteq 𝒫 O) \to (g \in 𝟙_{O} [𝒫 O \cap Fin] \leftrightarrow \exists a \in (𝒫 O \cap Fin) 𝟙_{O} (a) = g)$
59	57 4 58	sylancl	$⊢ O \in V \to (g \in 𝟙_{O} [𝒫 O \cap Fin] \leftrightarrow \exists a \in (𝒫 O \cap Fin) 𝟙_{O} (a) = g)$
60		cnveq	$⊢ f = g \to f^{-1} = g^{-1}$
61	60	imaeq1d	$⊢ f = g \to f^{-1} [\{1\}] = g^{-1} [\{1\}]$
62	61	eleq1d	$⊢ f = g \to (f^{-1} [\{1\}] \in Fin \leftrightarrow g^{-1} [\{1\}] \in Fin)$
63	62	elrab	$⊢ g \in \{f \in ({\{0, 1\}}^{O}) \| f^{-1} [\{1\}] \in Fin\} \leftrightarrow (g \in ({\{0, 1\}}^{O}) \land g^{-1} [\{1\}] \in Fin)$
64	63	a1i	$⊢ O \in V \to (g \in \{f \in ({\{0, 1\}}^{O}) \| f^{-1} [\{1\}] \in Fin\} \leftrightarrow (g \in ({\{0, 1\}}^{O}) \land g^{-1} [\{1\}] \in Fin))$
65	56 59 64	3bitr4d	$⊢ O \in V \to (g \in 𝟙_{O} [𝒫 O \cap Fin] \leftrightarrow g \in \{f \in ({\{0, 1\}}^{O}) \| f^{-1} [\{1\}] \in Fin\})$
66	65	eqrdv	$⊢ O \in V \to 𝟙_{O} [𝒫 O \cap Fin] = \{f \in ({\{0, 1\}}^{O}) \| f^{-1} [\{1\}] \in Fin\}$
67	12 13 66	f1oeq123d	$⊢ O \in V \to (({𝟙_{O} ↾}_{(𝒫 O \cap Fin)}) : 𝒫 O \cap Fin \underset{1-1 onto}{⟶} 𝟙_{O} [𝒫 O \cap Fin] \leftrightarrow ({𝟙_{O} ↾}_{Fin}) : 𝒫 O \cap Fin \underset{1-1 onto}{⟶} \{f \in ({\{0, 1\}}^{O}) \| f^{-1} [\{1\}] \in Fin\})$
68	6 67	mpbid	$⊢ O \in V \to ({𝟙_{O} ↾}_{Fin}) : 𝒫 O \cap Fin \underset{1-1 onto}{⟶} \{f \in ({\{0, 1\}}^{O}) \| f^{-1} [\{1\}] \in Fin\}$

Metamath Proof Explorer

Theorem indf1ofs

Proof