pwfi2f1o

Description: The pw2f1o bijection relates finitely supported indicator functions on a two-element set to finite subsets.MOVABLE (Contributed by Stefan O'Rear, 10-Jul-2015) (Revised by AV, 14-Jun-2020)

	Ref	Expression
Hypotheses	pwfi2f1o.s	$⊢ S = \{y \in ({2_{𝑜}}^{A}) \| {finSupp}_{\emptyset} (y)\}$
	pwfi2f1o.f	$⊢ F = (x \in S ⟼ x^{-1} [\{1_{𝑜}\}])$
Assertion	pwfi2f1o	$⊢ A \in V \to F : S \underset{1-1 onto}{⟶} 𝒫 A \cap Fin$

Proof

Step	Hyp	Ref	Expression
1		pwfi2f1o.s	$⊢ S = \{y \in ({2_{𝑜}}^{A}) \| {finSupp}_{\emptyset} (y)\}$
2		pwfi2f1o.f	$⊢ F = (x \in S ⟼ x^{-1} [\{1_{𝑜}\}])$
3		eqid	$⊢ (x \in ({2_{𝑜}}^{A}) ⟼ x^{-1} [\{1_{𝑜}\}]) = (x \in ({2_{𝑜}}^{A}) ⟼ x^{-1} [\{1_{𝑜}\}])$
4	3	pw2f1o2	$⊢ A \in V \to (x \in ({2_{𝑜}}^{A}) ⟼ x^{-1} [\{1_{𝑜}\}]) : {2_{𝑜}}^{A} \underset{1-1 onto}{⟶} 𝒫 A$
5		f1of1	$⊢ (x \in ({2_{𝑜}}^{A}) ⟼ x^{-1} [\{1_{𝑜}\}]) : {2_{𝑜}}^{A} \underset{1-1 onto}{⟶} 𝒫 A \to (x \in ({2_{𝑜}}^{A}) ⟼ x^{-1} [\{1_{𝑜}\}]) : {2_{𝑜}}^{A} \underset{1-1}{⟶} 𝒫 A$
6	4 5	syl	$⊢ A \in V \to (x \in ({2_{𝑜}}^{A}) ⟼ x^{-1} [\{1_{𝑜}\}]) : {2_{𝑜}}^{A} \underset{1-1}{⟶} 𝒫 A$
7		ssrab2	$⊢ \{y \in ({2_{𝑜}}^{A}) \| {finSupp}_{\emptyset} (y)\} \subseteq {2_{𝑜}}^{A}$
8	1 7	eqsstri	$⊢ S \subseteq {2_{𝑜}}^{A}$
9		f1ores	$⊢ ((x \in ({2_{𝑜}}^{A}) ⟼ x^{-1} [\{1_{𝑜}\}]) : {2_{𝑜}}^{A} \underset{1-1}{⟶} 𝒫 A \land S \subseteq {2_{𝑜}}^{A}) \to ({(x \in ({2_{𝑜}}^{A}) ⟼ x^{-1} [\{1_{𝑜}\}]) ↾}_{S}) : S \underset{1-1 onto}{⟶} (x \in ({2_{𝑜}}^{A}) ⟼ x^{-1} [\{1_{𝑜}\}]) [S]$
10	6 8 9	sylancl	$⊢ A \in V \to ({(x \in ({2_{𝑜}}^{A}) ⟼ x^{-1} [\{1_{𝑜}\}]) ↾}_{S}) : S \underset{1-1 onto}{⟶} (x \in ({2_{𝑜}}^{A}) ⟼ x^{-1} [\{1_{𝑜}\}]) [S]$
11		elmapfun	$⊢ y \in ({2_{𝑜}}^{A}) \to Fun y$
12		id	$⊢ y \in ({2_{𝑜}}^{A}) \to y \in ({2_{𝑜}}^{A})$
13		0ex	$⊢ \emptyset \in V$
14	13	a1i	$⊢ y \in ({2_{𝑜}}^{A}) \to \emptyset \in V$
15	11 12 14	3jca	$⊢ y \in ({2_{𝑜}}^{A}) \to (Fun y \land y \in ({2_{𝑜}}^{A}) \land \emptyset \in V)$
16	15	adantl	$⊢ (A \in V \land y \in ({2_{𝑜}}^{A})) \to (Fun y \land y \in ({2_{𝑜}}^{A}) \land \emptyset \in V)$
17		funisfsupp	$⊢ (Fun y \land y \in ({2_{𝑜}}^{A}) \land \emptyset \in V) \to ({finSupp}_{\emptyset} (y) \leftrightarrow y supp \emptyset \in Fin)$
18	16 17	syl	$⊢ (A \in V \land y \in ({2_{𝑜}}^{A})) \to ({finSupp}_{\emptyset} (y) \leftrightarrow y supp \emptyset \in Fin)$
19	14	anim2i	$⊢ (A \in V \land y \in ({2_{𝑜}}^{A})) \to (A \in V \land \emptyset \in V)$
20		elmapi	$⊢ y \in ({2_{𝑜}}^{A}) \to y : A ⟶ 2_{𝑜}$
21	20	adantl	$⊢ (A \in V \land y \in ({2_{𝑜}}^{A})) \to y : A ⟶ 2_{𝑜}$
22		frnsuppeq	$⊢ (A \in V \land \emptyset \in V) \to (y : A ⟶ 2_{𝑜} \to y supp \emptyset = y^{-1} [2_{𝑜} ∖ \{\emptyset\}])$
23	19 21 22	sylc	$⊢ (A \in V \land y \in ({2_{𝑜}}^{A})) \to y supp \emptyset = y^{-1} [2_{𝑜} ∖ \{\emptyset\}]$
24		df-2o	$⊢ 2_{𝑜} = suc 1_{𝑜}$
25		df-suc	$⊢ suc 1_{𝑜} = 1_{𝑜} \cup \{1_{𝑜}\}$
26	25	equncomi	$⊢ suc 1_{𝑜} = \{1_{𝑜}\} \cup 1_{𝑜}$
27	24 26	eqtri	$⊢ 2_{𝑜} = \{1_{𝑜}\} \cup 1_{𝑜}$
28		df1o2	$⊢ 1_{𝑜} = \{\emptyset\}$
29	28	eqcomi	$⊢ \{\emptyset\} = 1_{𝑜}$
30	27 29	difeq12i	$⊢ 2_{𝑜} ∖ \{\emptyset\} = (\{1_{𝑜}\} \cup 1_{𝑜}) ∖ 1_{𝑜}$
31		difun2	$⊢ (\{1_{𝑜}\} \cup 1_{𝑜}) ∖ 1_{𝑜} = \{1_{𝑜}\} ∖ 1_{𝑜}$
32		incom	$⊢ \{1_{𝑜}\} \cap 1_{𝑜} = 1_{𝑜} \cap \{1_{𝑜}\}$
33		1on	$⊢ 1_{𝑜} \in On$
34	33	onordi	$⊢ Ord 1_{𝑜}$
35		orddisj	$⊢ Ord 1_{𝑜} \to 1_{𝑜} \cap \{1_{𝑜}\} = \emptyset$
36	34 35	ax-mp	$⊢ 1_{𝑜} \cap \{1_{𝑜}\} = \emptyset$
37	32 36	eqtri	$⊢ \{1_{𝑜}\} \cap 1_{𝑜} = \emptyset$
38		disj3	$⊢ \{1_{𝑜}\} \cap 1_{𝑜} = \emptyset \leftrightarrow \{1_{𝑜}\} = \{1_{𝑜}\} ∖ 1_{𝑜}$
39	37 38	mpbi	$⊢ \{1_{𝑜}\} = \{1_{𝑜}\} ∖ 1_{𝑜}$
40	31 39	eqtr4i	$⊢ (\{1_{𝑜}\} \cup 1_{𝑜}) ∖ 1_{𝑜} = \{1_{𝑜}\}$
41	30 40	eqtri	$⊢ 2_{𝑜} ∖ \{\emptyset\} = \{1_{𝑜}\}$
42	41	imaeq2i	$⊢ y^{-1} [2_{𝑜} ∖ \{\emptyset\}] = y^{-1} [\{1_{𝑜}\}]$
43	23 42	eqtrdi	$⊢ (A \in V \land y \in ({2_{𝑜}}^{A})) \to y supp \emptyset = y^{-1} [\{1_{𝑜}\}]$
44	43	eleq1d	$⊢ (A \in V \land y \in ({2_{𝑜}}^{A})) \to (y supp \emptyset \in Fin \leftrightarrow y^{-1} [\{1_{𝑜}\}] \in Fin)$
45		cnvimass	$⊢ y^{-1} [\{1_{𝑜}\}] \subseteq dom y$
46	45 21	fssdm	$⊢ (A \in V \land y \in ({2_{𝑜}}^{A})) \to y^{-1} [\{1_{𝑜}\}] \subseteq A$
47	46	biantrurd	$⊢ (A \in V \land y \in ({2_{𝑜}}^{A})) \to (y^{-1} [\{1_{𝑜}\}] \in Fin \leftrightarrow (y^{-1} [\{1_{𝑜}\}] \subseteq A \land y^{-1} [\{1_{𝑜}\}] \in Fin))$
48	18 44 47	3bitrd	$⊢ (A \in V \land y \in ({2_{𝑜}}^{A})) \to ({finSupp}_{\emptyset} (y) \leftrightarrow (y^{-1} [\{1_{𝑜}\}] \subseteq A \land y^{-1} [\{1_{𝑜}\}] \in Fin))$
49		elfpw	$⊢ y^{-1} [\{1_{𝑜}\}] \in (𝒫 A \cap Fin) \leftrightarrow (y^{-1} [\{1_{𝑜}\}] \subseteq A \land y^{-1} [\{1_{𝑜}\}] \in Fin)$
50	48 49	bitr4di	$⊢ (A \in V \land y \in ({2_{𝑜}}^{A})) \to ({finSupp}_{\emptyset} (y) \leftrightarrow y^{-1} [\{1_{𝑜}\}] \in (𝒫 A \cap Fin))$
51	50	rabbidva	$⊢ A \in V \to \{y \in ({2_{𝑜}}^{A}) \| {finSupp}_{\emptyset} (y)\} = \{y \in ({2_{𝑜}}^{A}) \| y^{-1} [\{1_{𝑜}\}] \in (𝒫 A \cap Fin)\}$
52		cnveq	$⊢ x = y \to x^{-1} = y^{-1}$
53	52	imaeq1d	$⊢ x = y \to x^{-1} [\{1_{𝑜}\}] = y^{-1} [\{1_{𝑜}\}]$
54	53	cbvmptv	$⊢ (x \in ({2_{𝑜}}^{A}) ⟼ x^{-1} [\{1_{𝑜}\}]) = (y \in ({2_{𝑜}}^{A}) ⟼ y^{-1} [\{1_{𝑜}\}])$
55	54	mptpreima	$⊢ {(x \in ({2_{𝑜}}^{A}) ⟼ x^{-1} [\{1_{𝑜}\}])}^{-1} [𝒫 A \cap Fin] = \{y \in ({2_{𝑜}}^{A}) \| y^{-1} [\{1_{𝑜}\}] \in (𝒫 A \cap Fin)\}$
56	51 1 55	3eqtr4g	$⊢ A \in V \to S = {(x \in ({2_{𝑜}}^{A}) ⟼ x^{-1} [\{1_{𝑜}\}])}^{-1} [𝒫 A \cap Fin]$
57	56	imaeq2d	$⊢ A \in V \to (x \in ({2_{𝑜}}^{A}) ⟼ x^{-1} [\{1_{𝑜}\}]) [S] = (x \in ({2_{𝑜}}^{A}) ⟼ x^{-1} [\{1_{𝑜}\}]) [{(x \in ({2_{𝑜}}^{A}) ⟼ x^{-1} [\{1_{𝑜}\}])}^{-1} [𝒫 A \cap Fin]]$
58		f1ofo	$⊢ (x \in ({2_{𝑜}}^{A}) ⟼ x^{-1} [\{1_{𝑜}\}]) : {2_{𝑜}}^{A} \underset{1-1 onto}{⟶} 𝒫 A \to (x \in ({2_{𝑜}}^{A}) ⟼ x^{-1} [\{1_{𝑜}\}]) : {2_{𝑜}}^{A} \underset{onto}{⟶} 𝒫 A$
59	4 58	syl	$⊢ A \in V \to (x \in ({2_{𝑜}}^{A}) ⟼ x^{-1} [\{1_{𝑜}\}]) : {2_{𝑜}}^{A} \underset{onto}{⟶} 𝒫 A$
60		inss1	$⊢ 𝒫 A \cap Fin \subseteq 𝒫 A$
61		foimacnv	$⊢ ((x \in ({2_{𝑜}}^{A}) ⟼ x^{-1} [\{1_{𝑜}\}]) : {2_{𝑜}}^{A} \underset{onto}{⟶} 𝒫 A \land 𝒫 A \cap Fin \subseteq 𝒫 A) \to (x \in ({2_{𝑜}}^{A}) ⟼ x^{-1} [\{1_{𝑜}\}]) [{(x \in ({2_{𝑜}}^{A}) ⟼ x^{-1} [\{1_{𝑜}\}])}^{-1} [𝒫 A \cap Fin]] = 𝒫 A \cap Fin$
62	59 60 61	sylancl	$⊢ A \in V \to (x \in ({2_{𝑜}}^{A}) ⟼ x^{-1} [\{1_{𝑜}\}]) [{(x \in ({2_{𝑜}}^{A}) ⟼ x^{-1} [\{1_{𝑜}\}])}^{-1} [𝒫 A \cap Fin]] = 𝒫 A \cap Fin$
63	57 62	eqtrd	$⊢ A \in V \to (x \in ({2_{𝑜}}^{A}) ⟼ x^{-1} [\{1_{𝑜}\}]) [S] = 𝒫 A \cap Fin$
64		f1oeq3	$⊢ (x \in ({2_{𝑜}}^{A}) ⟼ x^{-1} [\{1_{𝑜}\}]) [S] = 𝒫 A \cap Fin \to (({(x \in ({2_{𝑜}}^{A}) ⟼ x^{-1} [\{1_{𝑜}\}]) ↾}_{S}) : S \underset{1-1 onto}{⟶} (x \in ({2_{𝑜}}^{A}) ⟼ x^{-1} [\{1_{𝑜}\}]) [S] \leftrightarrow ({(x \in ({2_{𝑜}}^{A}) ⟼ x^{-1} [\{1_{𝑜}\}]) ↾}_{S}) : S \underset{1-1 onto}{⟶} 𝒫 A \cap Fin)$
65	63 64	syl	$⊢ A \in V \to (({(x \in ({2_{𝑜}}^{A}) ⟼ x^{-1} [\{1_{𝑜}\}]) ↾}_{S}) : S \underset{1-1 onto}{⟶} (x \in ({2_{𝑜}}^{A}) ⟼ x^{-1} [\{1_{𝑜}\}]) [S] \leftrightarrow ({(x \in ({2_{𝑜}}^{A}) ⟼ x^{-1} [\{1_{𝑜}\}]) ↾}_{S}) : S \underset{1-1 onto}{⟶} 𝒫 A \cap Fin)$
66		resmpt	$⊢ S \subseteq {2_{𝑜}}^{A} \to {(x \in ({2_{𝑜}}^{A}) ⟼ x^{-1} [\{1_{𝑜}\}]) ↾}_{S} = (x \in S ⟼ x^{-1} [\{1_{𝑜}\}])$
67	8 66	ax-mp	$⊢ {(x \in ({2_{𝑜}}^{A}) ⟼ x^{-1} [\{1_{𝑜}\}]) ↾}_{S} = (x \in S ⟼ x^{-1} [\{1_{𝑜}\}])$
68	67 2	eqtr4i	$⊢ {(x \in ({2_{𝑜}}^{A}) ⟼ x^{-1} [\{1_{𝑜}\}]) ↾}_{S} = F$
69		f1oeq1	$⊢ {(x \in ({2_{𝑜}}^{A}) ⟼ x^{-1} [\{1_{𝑜}\}]) ↾}_{S} = F \to (({(x \in ({2_{𝑜}}^{A}) ⟼ x^{-1} [\{1_{𝑜}\}]) ↾}_{S}) : S \underset{1-1 onto}{⟶} 𝒫 A \cap Fin \leftrightarrow F : S \underset{1-1 onto}{⟶} 𝒫 A \cap Fin)$
70	68 69	mp1i	$⊢ A \in V \to (({(x \in ({2_{𝑜}}^{A}) ⟼ x^{-1} [\{1_{𝑜}\}]) ↾}_{S}) : S \underset{1-1 onto}{⟶} 𝒫 A \cap Fin \leftrightarrow F : S \underset{1-1 onto}{⟶} 𝒫 A \cap Fin)$
71	65 70	bitrd	$⊢ A \in V \to (({(x \in ({2_{𝑜}}^{A}) ⟼ x^{-1} [\{1_{𝑜}\}]) ↾}_{S}) : S \underset{1-1 onto}{⟶} (x \in ({2_{𝑜}}^{A}) ⟼ x^{-1} [\{1_{𝑜}\}]) [S] \leftrightarrow F : S \underset{1-1 onto}{⟶} 𝒫 A \cap Fin)$
72	10 71	mpbid	$⊢ A \in V \to F : S \underset{1-1 onto}{⟶} 𝒫 A \cap Fin$

Metamath Proof Explorer

Theorem pwfi2f1o

Proof