Theorem 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	⊢ 𝑆 = { 𝑦 ∈ ( 2o ↑m 𝐴 ) ∣ 𝑦 finSupp ∅ }
	pwfi2f1o.f	⊢ 𝐹 = ( 𝑥 ∈ 𝑆 ↦ ( ◡ 𝑥 “ { 1o } ) )
Assertion	pwfi2f1o	⊢ ( 𝐴 ∈ 𝑉 → 𝐹 : 𝑆 –1-1-onto→ ( 𝒫 𝐴 ∩ Fin ) )

Proof

Step	Hyp	Ref	Expression
1		pwfi2f1o.s	⊢ 𝑆 = { 𝑦 ∈ ( 2o ↑m 𝐴 ) ∣ 𝑦 finSupp ∅ }
2		pwfi2f1o.f	⊢ 𝐹 = ( 𝑥 ∈ 𝑆 ↦ ( ◡ 𝑥 “ { 1o } ) )
3		eqid	⊢ ( 𝑥 ∈ ( 2o ↑m 𝐴 ) ↦ ( ◡ 𝑥 “ { 1o } ) ) = ( 𝑥 ∈ ( 2o ↑m 𝐴 ) ↦ ( ◡ 𝑥 “ { 1o } ) )
4	3	pw2f1o2	⊢ ( 𝐴 ∈ 𝑉 → ( 𝑥 ∈ ( 2o ↑m 𝐴 ) ↦ ( ◡ 𝑥 “ { 1o } ) ) : ( 2o ↑m 𝐴 ) –1-1-onto→ 𝒫 𝐴 )
5		f1of1	⊢ ( ( 𝑥 ∈ ( 2o ↑m 𝐴 ) ↦ ( ◡ 𝑥 “ { 1o } ) ) : ( 2o ↑m 𝐴 ) –1-1-onto→ 𝒫 𝐴 → ( 𝑥 ∈ ( 2o ↑m 𝐴 ) ↦ ( ◡ 𝑥 “ { 1o } ) ) : ( 2o ↑m 𝐴 ) –1-1→ 𝒫 𝐴 )
6	4 5	syl	⊢ ( 𝐴 ∈ 𝑉 → ( 𝑥 ∈ ( 2o ↑m 𝐴 ) ↦ ( ◡ 𝑥 “ { 1o } ) ) : ( 2o ↑m 𝐴 ) –1-1→ 𝒫 𝐴 )
7		ssrab2	⊢ { 𝑦 ∈ ( 2o ↑m 𝐴 ) ∣ 𝑦 finSupp ∅ } ⊆ ( 2o ↑m 𝐴 )
8	1 7	eqsstri	⊢ 𝑆 ⊆ ( 2o ↑m 𝐴 )
9		f1ores	⊢ ( ( ( 𝑥 ∈ ( 2o ↑m 𝐴 ) ↦ ( ◡ 𝑥 “ { 1o } ) ) : ( 2o ↑m 𝐴 ) –1-1→ 𝒫 𝐴 ∧ 𝑆 ⊆ ( 2o ↑m 𝐴 ) ) → ( ( 𝑥 ∈ ( 2o ↑m 𝐴 ) ↦ ( ◡ 𝑥 “ { 1o } ) ) ↾ 𝑆 ) : 𝑆 –1-1-onto→ ( ( 𝑥 ∈ ( 2o ↑m 𝐴 ) ↦ ( ◡ 𝑥 “ { 1o } ) ) “ 𝑆 ) )
10	6 8 9	sylancl	⊢ ( 𝐴 ∈ 𝑉 → ( ( 𝑥 ∈ ( 2o ↑m 𝐴 ) ↦ ( ◡ 𝑥 “ { 1o } ) ) ↾ 𝑆 ) : 𝑆 –1-1-onto→ ( ( 𝑥 ∈ ( 2o ↑m 𝐴 ) ↦ ( ◡ 𝑥 “ { 1o } ) ) “ 𝑆 ) )
11		elmapfun	⊢ ( 𝑦 ∈ ( 2o ↑m 𝐴 ) → Fun 𝑦 )
12		id	⊢ ( 𝑦 ∈ ( 2o ↑m 𝐴 ) → 𝑦 ∈ ( 2o ↑m 𝐴 ) )
13		0ex	⊢ ∅ ∈ V
14	13	a1i	⊢ ( 𝑦 ∈ ( 2o ↑m 𝐴 ) → ∅ ∈ V )
15	11 12 14	3jca	⊢ ( 𝑦 ∈ ( 2o ↑m 𝐴 ) → ( Fun 𝑦 ∧ 𝑦 ∈ ( 2o ↑m 𝐴 ) ∧ ∅ ∈ V ) )
16	15	adantl	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑦 ∈ ( 2o ↑m 𝐴 ) ) → ( Fun 𝑦 ∧ 𝑦 ∈ ( 2o ↑m 𝐴 ) ∧ ∅ ∈ V ) )
17		funisfsupp	⊢ ( ( Fun 𝑦 ∧ 𝑦 ∈ ( 2o ↑m 𝐴 ) ∧ ∅ ∈ V ) → ( 𝑦 finSupp ∅ ↔ ( 𝑦 supp ∅ ) ∈ Fin ) )
18	16 17	syl	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑦 ∈ ( 2o ↑m 𝐴 ) ) → ( 𝑦 finSupp ∅ ↔ ( 𝑦 supp ∅ ) ∈ Fin ) )
19	14	anim2i	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑦 ∈ ( 2o ↑m 𝐴 ) ) → ( 𝐴 ∈ 𝑉 ∧ ∅ ∈ V ) )
20		elmapi	⊢ ( 𝑦 ∈ ( 2o ↑m 𝐴 ) → 𝑦 : 𝐴 ⟶ 2o )
21	20	adantl	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑦 ∈ ( 2o ↑m 𝐴 ) ) → 𝑦 : 𝐴 ⟶ 2o )
22		frnsuppeq	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∅ ∈ V ) → ( 𝑦 : 𝐴 ⟶ 2o → ( 𝑦 supp ∅ ) = ( ◡ 𝑦 “ ( 2o ∖ { ∅ } ) ) ) )
23	19 21 22	sylc	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑦 ∈ ( 2o ↑m 𝐴 ) ) → ( 𝑦 supp ∅ ) = ( ◡ 𝑦 “ ( 2o ∖ { ∅ } ) ) )
24		df-2o	⊢ 2o = suc 1o
25		df-suc	⊢ suc 1o = ( 1o ∪ { 1o } )
26	25	equncomi	⊢ suc 1o = ( { 1o } ∪ 1o )
27	24 26	eqtri	⊢ 2o = ( { 1o } ∪ 1o )
28		df1o2	⊢ 1o = { ∅ }
29	28	eqcomi	⊢ { ∅ } = 1o
30	27 29	difeq12i	⊢ ( 2o ∖ { ∅ } ) = ( ( { 1o } ∪ 1o ) ∖ 1o )
31		difun2	⊢ ( ( { 1o } ∪ 1o ) ∖ 1o ) = ( { 1o } ∖ 1o )
32		incom	⊢ ( { 1o } ∩ 1o ) = ( 1o ∩ { 1o } )
33		1on	⊢ 1o ∈ On
34	33	onordi	⊢ Ord 1o
35		orddisj	⊢ ( Ord 1o → ( 1o ∩ { 1o } ) = ∅ )
36	34 35	ax-mp	⊢ ( 1o ∩ { 1o } ) = ∅
37	32 36	eqtri	⊢ ( { 1o } ∩ 1o ) = ∅
38		disj3	⊢ ( ( { 1o } ∩ 1o ) = ∅ ↔ { 1o } = ( { 1o } ∖ 1o ) )
39	37 38	mpbi	⊢ { 1o } = ( { 1o } ∖ 1o )
40	31 39	eqtr4i	⊢ ( ( { 1o } ∪ 1o ) ∖ 1o ) = { 1o }
41	30 40	eqtri	⊢ ( 2o ∖ { ∅ } ) = { 1o }
42	41	imaeq2i	⊢ ( ◡ 𝑦 “ ( 2o ∖ { ∅ } ) ) = ( ◡ 𝑦 “ { 1o } )
43	23 42	eqtrdi	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑦 ∈ ( 2o ↑m 𝐴 ) ) → ( 𝑦 supp ∅ ) = ( ◡ 𝑦 “ { 1o } ) )
44	43	eleq1d	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑦 ∈ ( 2o ↑m 𝐴 ) ) → ( ( 𝑦 supp ∅ ) ∈ Fin ↔ ( ◡ 𝑦 “ { 1o } ) ∈ Fin ) )
45		cnvimass	⊢ ( ◡ 𝑦 “ { 1o } ) ⊆ dom 𝑦
46	45 21	fssdm	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑦 ∈ ( 2o ↑m 𝐴 ) ) → ( ◡ 𝑦 “ { 1o } ) ⊆ 𝐴 )
47	46	biantrurd	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑦 ∈ ( 2o ↑m 𝐴 ) ) → ( ( ◡ 𝑦 “ { 1o } ) ∈ Fin ↔ ( ( ◡ 𝑦 “ { 1o } ) ⊆ 𝐴 ∧ ( ◡ 𝑦 “ { 1o } ) ∈ Fin ) ) )
48	18 44 47	3bitrd	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑦 ∈ ( 2o ↑m 𝐴 ) ) → ( 𝑦 finSupp ∅ ↔ ( ( ◡ 𝑦 “ { 1o } ) ⊆ 𝐴 ∧ ( ◡ 𝑦 “ { 1o } ) ∈ Fin ) ) )
49		elfpw	⊢ ( ( ◡ 𝑦 “ { 1o } ) ∈ ( 𝒫 𝐴 ∩ Fin ) ↔ ( ( ◡ 𝑦 “ { 1o } ) ⊆ 𝐴 ∧ ( ◡ 𝑦 “ { 1o } ) ∈ Fin ) )
50	48 49	bitr4di	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑦 ∈ ( 2o ↑m 𝐴 ) ) → ( 𝑦 finSupp ∅ ↔ ( ◡ 𝑦 “ { 1o } ) ∈ ( 𝒫 𝐴 ∩ Fin ) ) )
51	50	rabbidva	⊢ ( 𝐴 ∈ 𝑉 → { 𝑦 ∈ ( 2o ↑m 𝐴 ) ∣ 𝑦 finSupp ∅ } = { 𝑦 ∈ ( 2o ↑m 𝐴 ) ∣ ( ◡ 𝑦 “ { 1o } ) ∈ ( 𝒫 𝐴 ∩ Fin ) } )
52		cnveq	⊢ ( 𝑥 = 𝑦 → ◡ 𝑥 = ◡ 𝑦 )
53	52	imaeq1d	⊢ ( 𝑥 = 𝑦 → ( ◡ 𝑥 “ { 1o } ) = ( ◡ 𝑦 “ { 1o } ) )
54	53	cbvmptv	⊢ ( 𝑥 ∈ ( 2o ↑m 𝐴 ) ↦ ( ◡ 𝑥 “ { 1o } ) ) = ( 𝑦 ∈ ( 2o ↑m 𝐴 ) ↦ ( ◡ 𝑦 “ { 1o } ) )
55	54	mptpreima	⊢ ( ◡ ( 𝑥 ∈ ( 2o ↑m 𝐴 ) ↦ ( ◡ 𝑥 “ { 1o } ) ) “ ( 𝒫 𝐴 ∩ Fin ) ) = { 𝑦 ∈ ( 2o ↑m 𝐴 ) ∣ ( ◡ 𝑦 “ { 1o } ) ∈ ( 𝒫 𝐴 ∩ Fin ) }
56	51 1 55	3eqtr4g	⊢ ( 𝐴 ∈ 𝑉 → 𝑆 = ( ◡ ( 𝑥 ∈ ( 2o ↑m 𝐴 ) ↦ ( ◡ 𝑥 “ { 1o } ) ) “ ( 𝒫 𝐴 ∩ Fin ) ) )
57	56	imaeq2d	⊢ ( 𝐴 ∈ 𝑉 → ( ( 𝑥 ∈ ( 2o ↑m 𝐴 ) ↦ ( ◡ 𝑥 “ { 1o } ) ) “ 𝑆 ) = ( ( 𝑥 ∈ ( 2o ↑m 𝐴 ) ↦ ( ◡ 𝑥 “ { 1o } ) ) “ ( ◡ ( 𝑥 ∈ ( 2o ↑m 𝐴 ) ↦ ( ◡ 𝑥 “ { 1o } ) ) “ ( 𝒫 𝐴 ∩ Fin ) ) ) )
58		f1ofo	⊢ ( ( 𝑥 ∈ ( 2o ↑m 𝐴 ) ↦ ( ◡ 𝑥 “ { 1o } ) ) : ( 2o ↑m 𝐴 ) –1-1-onto→ 𝒫 𝐴 → ( 𝑥 ∈ ( 2o ↑m 𝐴 ) ↦ ( ◡ 𝑥 “ { 1o } ) ) : ( 2o ↑m 𝐴 ) –onto→ 𝒫 𝐴 )
59	4 58	syl	⊢ ( 𝐴 ∈ 𝑉 → ( 𝑥 ∈ ( 2o ↑m 𝐴 ) ↦ ( ◡ 𝑥 “ { 1o } ) ) : ( 2o ↑m 𝐴 ) –onto→ 𝒫 𝐴 )
60		inss1	⊢ ( 𝒫 𝐴 ∩ Fin ) ⊆ 𝒫 𝐴
61		foimacnv	⊢ ( ( ( 𝑥 ∈ ( 2o ↑m 𝐴 ) ↦ ( ◡ 𝑥 “ { 1o } ) ) : ( 2o ↑m 𝐴 ) –onto→ 𝒫 𝐴 ∧ ( 𝒫 𝐴 ∩ Fin ) ⊆ 𝒫 𝐴 ) → ( ( 𝑥 ∈ ( 2o ↑m 𝐴 ) ↦ ( ◡ 𝑥 “ { 1o } ) ) “ ( ◡ ( 𝑥 ∈ ( 2o ↑m 𝐴 ) ↦ ( ◡ 𝑥 “ { 1o } ) ) “ ( 𝒫 𝐴 ∩ Fin ) ) ) = ( 𝒫 𝐴 ∩ Fin ) )
62	59 60 61	sylancl	⊢ ( 𝐴 ∈ 𝑉 → ( ( 𝑥 ∈ ( 2o ↑m 𝐴 ) ↦ ( ◡ 𝑥 “ { 1o } ) ) “ ( ◡ ( 𝑥 ∈ ( 2o ↑m 𝐴 ) ↦ ( ◡ 𝑥 “ { 1o } ) ) “ ( 𝒫 𝐴 ∩ Fin ) ) ) = ( 𝒫 𝐴 ∩ Fin ) )
63	57 62	eqtrd	⊢ ( 𝐴 ∈ 𝑉 → ( ( 𝑥 ∈ ( 2o ↑m 𝐴 ) ↦ ( ◡ 𝑥 “ { 1o } ) ) “ 𝑆 ) = ( 𝒫 𝐴 ∩ Fin ) )
64		f1oeq3	⊢ ( ( ( 𝑥 ∈ ( 2o ↑m 𝐴 ) ↦ ( ◡ 𝑥 “ { 1o } ) ) “ 𝑆 ) = ( 𝒫 𝐴 ∩ Fin ) → ( ( ( 𝑥 ∈ ( 2o ↑m 𝐴 ) ↦ ( ◡ 𝑥 “ { 1o } ) ) ↾ 𝑆 ) : 𝑆 –1-1-onto→ ( ( 𝑥 ∈ ( 2o ↑m 𝐴 ) ↦ ( ◡ 𝑥 “ { 1o } ) ) “ 𝑆 ) ↔ ( ( 𝑥 ∈ ( 2o ↑m 𝐴 ) ↦ ( ◡ 𝑥 “ { 1o } ) ) ↾ 𝑆 ) : 𝑆 –1-1-onto→ ( 𝒫 𝐴 ∩ Fin ) ) )
65	63 64	syl	⊢ ( 𝐴 ∈ 𝑉 → ( ( ( 𝑥 ∈ ( 2o ↑m 𝐴 ) ↦ ( ◡ 𝑥 “ { 1o } ) ) ↾ 𝑆 ) : 𝑆 –1-1-onto→ ( ( 𝑥 ∈ ( 2o ↑m 𝐴 ) ↦ ( ◡ 𝑥 “ { 1o } ) ) “ 𝑆 ) ↔ ( ( 𝑥 ∈ ( 2o ↑m 𝐴 ) ↦ ( ◡ 𝑥 “ { 1o } ) ) ↾ 𝑆 ) : 𝑆 –1-1-onto→ ( 𝒫 𝐴 ∩ Fin ) ) )
66		resmpt	⊢ ( 𝑆 ⊆ ( 2o ↑m 𝐴 ) → ( ( 𝑥 ∈ ( 2o ↑m 𝐴 ) ↦ ( ◡ 𝑥 “ { 1o } ) ) ↾ 𝑆 ) = ( 𝑥 ∈ 𝑆 ↦ ( ◡ 𝑥 “ { 1o } ) ) )
67	8 66	ax-mp	⊢ ( ( 𝑥 ∈ ( 2o ↑m 𝐴 ) ↦ ( ◡ 𝑥 “ { 1o } ) ) ↾ 𝑆 ) = ( 𝑥 ∈ 𝑆 ↦ ( ◡ 𝑥 “ { 1o } ) )
68	67 2	eqtr4i	⊢ ( ( 𝑥 ∈ ( 2o ↑m 𝐴 ) ↦ ( ◡ 𝑥 “ { 1o } ) ) ↾ 𝑆 ) = 𝐹
69		f1oeq1	⊢ ( ( ( 𝑥 ∈ ( 2o ↑m 𝐴 ) ↦ ( ◡ 𝑥 “ { 1o } ) ) ↾ 𝑆 ) = 𝐹 → ( ( ( 𝑥 ∈ ( 2o ↑m 𝐴 ) ↦ ( ◡ 𝑥 “ { 1o } ) ) ↾ 𝑆 ) : 𝑆 –1-1-onto→ ( 𝒫 𝐴 ∩ Fin ) ↔ 𝐹 : 𝑆 –1-1-onto→ ( 𝒫 𝐴 ∩ Fin ) ) )
70	68 69	mp1i	⊢ ( 𝐴 ∈ 𝑉 → ( ( ( 𝑥 ∈ ( 2o ↑m 𝐴 ) ↦ ( ◡ 𝑥 “ { 1o } ) ) ↾ 𝑆 ) : 𝑆 –1-1-onto→ ( 𝒫 𝐴 ∩ Fin ) ↔ 𝐹 : 𝑆 –1-1-onto→ ( 𝒫 𝐴 ∩ Fin ) ) )
71	65 70	bitrd	⊢ ( 𝐴 ∈ 𝑉 → ( ( ( 𝑥 ∈ ( 2o ↑m 𝐴 ) ↦ ( ◡ 𝑥 “ { 1o } ) ) ↾ 𝑆 ) : 𝑆 –1-1-onto→ ( ( 𝑥 ∈ ( 2o ↑m 𝐴 ) ↦ ( ◡ 𝑥 “ { 1o } ) ) “ 𝑆 ) ↔ 𝐹 : 𝑆 –1-1-onto→ ( 𝒫 𝐴 ∩ Fin ) ) )
72	10 71	mpbid	⊢ ( 𝐴 ∈ 𝑉 → 𝐹 : 𝑆 –1-1-onto→ ( 𝒫 𝐴 ∩ Fin ) )