Theorem fpwrelmapffs

Description: Define a canonical mapping between finite relations (finite subsets of a cartesian product) and functions with finite support into finite subsets. (Contributed by Thierry Arnoux, 28-Aug-2017) (Revised by Thierry Arnoux, 1-Sep-2019)

	Ref	Expression
Hypotheses	fpwrelmap.1	⊢ 𝐴 ∈ V
	fpwrelmap.2	⊢ 𝐵 ∈ V
	fpwrelmap.3	⊢ 𝑀 = ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ) } )
	fpwrelmapffs.1	⊢ 𝑆 = { 𝑓 ∈ ( ( 𝒫 𝐵 ∩ Fin ) ↑m 𝐴 ) ∣ ( 𝑓 supp ∅ ) ∈ Fin }
Assertion	fpwrelmapffs	⊢ ( 𝑀 ↾ 𝑆 ) : 𝑆 –1-1-onto→ ( 𝒫 ( 𝐴 × 𝐵 ) ∩ Fin )

Proof

Step	Hyp	Ref	Expression
1		fpwrelmap.1	⊢ 𝐴 ∈ V
2		fpwrelmap.2	⊢ 𝐵 ∈ V
3		fpwrelmap.3	⊢ 𝑀 = ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ) } )
4		fpwrelmapffs.1	⊢ 𝑆 = { 𝑓 ∈ ( ( 𝒫 𝐵 ∩ Fin ) ↑m 𝐴 ) ∣ ( 𝑓 supp ∅ ) ∈ Fin }
5	1 2 3	fpwrelmap	⊢ 𝑀 : ( 𝒫 𝐵 ↑m 𝐴 ) –1-1-onto→ 𝒫 ( 𝐴 × 𝐵 )
6	5	a1i	⊢ ( ⊤ → 𝑀 : ( 𝒫 𝐵 ↑m 𝐴 ) –1-1-onto→ 𝒫 ( 𝐴 × 𝐵 ) )
7	2	pwex	⊢ 𝒫 𝐵 ∈ V
8	7 1	elmap	⊢ ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ↔ 𝑓 : 𝐴 ⟶ 𝒫 𝐵 )
9	8	birani	⊢ ( ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ∧ 𝑟 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ) } ) → 𝑓 : 𝐴 ⟶ 𝒫 𝐵 )
10		simpr	⊢ ( ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ∧ 𝑟 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ) } ) → 𝑟 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ) } )
11	1 2 9 10	fpwrelmapffslem	⊢ ( ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ∧ 𝑟 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ) } ) → ( 𝑟 ∈ Fin ↔ ( ran 𝑓 ⊆ Fin ∧ ( 𝑓 supp ∅ ) ∈ Fin ) ) )
12	11	3adant1	⊢ ( ( ⊤ ∧ 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ∧ 𝑟 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ) } ) → ( 𝑟 ∈ Fin ↔ ( ran 𝑓 ⊆ Fin ∧ ( 𝑓 supp ∅ ) ∈ Fin ) ) )
13	3 6 12	f1oresrab	⊢ ( ⊤ → ( 𝑀 ↾ { 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ∣ ( ran 𝑓 ⊆ Fin ∧ ( 𝑓 supp ∅ ) ∈ Fin ) } ) : { 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ∣ ( ran 𝑓 ⊆ Fin ∧ ( 𝑓 supp ∅ ) ∈ Fin ) } –1-1-onto→ { 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∣ 𝑟 ∈ Fin } )
14	13	mptru	⊢ ( 𝑀 ↾ { 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ∣ ( ran 𝑓 ⊆ Fin ∧ ( 𝑓 supp ∅ ) ∈ Fin ) } ) : { 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ∣ ( ran 𝑓 ⊆ Fin ∧ ( 𝑓 supp ∅ ) ∈ Fin ) } –1-1-onto→ { 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∣ 𝑟 ∈ Fin }
15	1 7	maprnin	⊢ ( ( 𝒫 𝐵 ∩ Fin ) ↑m 𝐴 ) = { 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ∣ ran 𝑓 ⊆ Fin }
16		nfcv	⊢ Ⅎ 𝑓 ( ( 𝒫 𝐵 ∩ Fin ) ↑m 𝐴 )
17		nfrab1	⊢ Ⅎ 𝑓 { 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ∣ ran 𝑓 ⊆ Fin }
18	16 17	rabeqf	⊢ ( ( ( 𝒫 𝐵 ∩ Fin ) ↑m 𝐴 ) = { 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ∣ ran 𝑓 ⊆ Fin } → { 𝑓 ∈ ( ( 𝒫 𝐵 ∩ Fin ) ↑m 𝐴 ) ∣ ( 𝑓 supp ∅ ) ∈ Fin } = { 𝑓 ∈ { 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ∣ ran 𝑓 ⊆ Fin } ∣ ( 𝑓 supp ∅ ) ∈ Fin } )
19	15 18	ax-mp	⊢ { 𝑓 ∈ ( ( 𝒫 𝐵 ∩ Fin ) ↑m 𝐴 ) ∣ ( 𝑓 supp ∅ ) ∈ Fin } = { 𝑓 ∈ { 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ∣ ran 𝑓 ⊆ Fin } ∣ ( 𝑓 supp ∅ ) ∈ Fin }
20		rabrab	⊢ { 𝑓 ∈ { 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ∣ ran 𝑓 ⊆ Fin } ∣ ( 𝑓 supp ∅ ) ∈ Fin } = { 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ∣ ( ran 𝑓 ⊆ Fin ∧ ( 𝑓 supp ∅ ) ∈ Fin ) }
21	4 19 20	3eqtri	⊢ 𝑆 = { 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ∣ ( ran 𝑓 ⊆ Fin ∧ ( 𝑓 supp ∅ ) ∈ Fin ) }
22		dfin5	⊢ ( 𝒫 ( 𝐴 × 𝐵 ) ∩ Fin ) = { 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∣ 𝑟 ∈ Fin }
23		f1oeq23	⊢ ( ( 𝑆 = { 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ∣ ( ran 𝑓 ⊆ Fin ∧ ( 𝑓 supp ∅ ) ∈ Fin ) } ∧ ( 𝒫 ( 𝐴 × 𝐵 ) ∩ Fin ) = { 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∣ 𝑟 ∈ Fin } ) → ( ( 𝑀 ↾ 𝑆 ) : 𝑆 –1-1-onto→ ( 𝒫 ( 𝐴 × 𝐵 ) ∩ Fin ) ↔ ( 𝑀 ↾ 𝑆 ) : { 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ∣ ( ran 𝑓 ⊆ Fin ∧ ( 𝑓 supp ∅ ) ∈ Fin ) } –1-1-onto→ { 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∣ 𝑟 ∈ Fin } ) )
24	21 22 23	mp2an	⊢ ( ( 𝑀 ↾ 𝑆 ) : 𝑆 –1-1-onto→ ( 𝒫 ( 𝐴 × 𝐵 ) ∩ Fin ) ↔ ( 𝑀 ↾ 𝑆 ) : { 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ∣ ( ran 𝑓 ⊆ Fin ∧ ( 𝑓 supp ∅ ) ∈ Fin ) } –1-1-onto→ { 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∣ 𝑟 ∈ Fin } )
25	21	reseq2i	⊢ ( 𝑀 ↾ 𝑆 ) = ( 𝑀 ↾ { 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ∣ ( ran 𝑓 ⊆ Fin ∧ ( 𝑓 supp ∅ ) ∈ Fin ) } )
26		f1oeq1	⊢ ( ( 𝑀 ↾ 𝑆 ) = ( 𝑀 ↾ { 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ∣ ( ran 𝑓 ⊆ Fin ∧ ( 𝑓 supp ∅ ) ∈ Fin ) } ) → ( ( 𝑀 ↾ 𝑆 ) : { 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ∣ ( ran 𝑓 ⊆ Fin ∧ ( 𝑓 supp ∅ ) ∈ Fin ) } –1-1-onto→ { 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∣ 𝑟 ∈ Fin } ↔ ( 𝑀 ↾ { 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ∣ ( ran 𝑓 ⊆ Fin ∧ ( 𝑓 supp ∅ ) ∈ Fin ) } ) : { 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ∣ ( ran 𝑓 ⊆ Fin ∧ ( 𝑓 supp ∅ ) ∈ Fin ) } –1-1-onto→ { 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∣ 𝑟 ∈ Fin } ) )
27	25 26	ax-mp	⊢ ( ( 𝑀 ↾ 𝑆 ) : { 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ∣ ( ran 𝑓 ⊆ Fin ∧ ( 𝑓 supp ∅ ) ∈ Fin ) } –1-1-onto→ { 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∣ 𝑟 ∈ Fin } ↔ ( 𝑀 ↾ { 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ∣ ( ran 𝑓 ⊆ Fin ∧ ( 𝑓 supp ∅ ) ∈ Fin ) } ) : { 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ∣ ( ran 𝑓 ⊆ Fin ∧ ( 𝑓 supp ∅ ) ∈ Fin ) } –1-1-onto→ { 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∣ 𝑟 ∈ Fin } )
28	24 27	bitr2i	⊢ ( ( 𝑀 ↾ { 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ∣ ( ran 𝑓 ⊆ Fin ∧ ( 𝑓 supp ∅ ) ∈ Fin ) } ) : { 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ∣ ( ran 𝑓 ⊆ Fin ∧ ( 𝑓 supp ∅ ) ∈ Fin ) } –1-1-onto→ { 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∣ 𝑟 ∈ Fin } ↔ ( 𝑀 ↾ 𝑆 ) : 𝑆 –1-1-onto→ ( 𝒫 ( 𝐴 × 𝐵 ) ∩ Fin ) )
29	14 28	mpbi	⊢ ( 𝑀 ↾ 𝑆 ) : 𝑆 –1-1-onto→ ( 𝒫 ( 𝐴 × 𝐵 ) ∩ Fin )