let f : (𝒫 (Set.univ : Set (ℕ × ℕ))) → (𝒫 (Set.univ : Set ℕ)) := by
  intro a_set_of_nxn
  exact {
    val := {2^x.1 * 3^x.2 | x ∈ a_set_of_nxn.val}
    property := by simp only [Set.powerset_univ, Set.mem_univ]
  }
⊢ ∃ fg, Function.Bijective fg
f : ↑(𝒫 Set.univ) → ↑(𝒫 Set.univ) :=
  fun a_set_of_nxn =>
    { val := {x | ∃ x_1 ∈ ↑a_set_of_nxn, 2 ^ x_1.1 * 3 ^ x_1.2 = x},
      property := (_ : {x | ∃ x_1 ∈ ↑a_set_of_nxn, 2 ^ x_1.1 * 3 ^ x_1.2 = x} ∈ 𝒫 Set.univ) }
⊢ ∃ fg, Function.Bijective fg