This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )