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