rw [sq_rel, Set.subset_def] at is_fn
is_fn : sq_rel ⊆ Set.univ ×ˢ Set.univ ∧ ∀ (x : ℝ), ∃! y, (x, y) ∈ sq_rel
⊢ False
is_fn :
  (∀ x ∈ {x | ∃ x_1, (x_1 ^ 2, x_1) = x}, x ∈ Set.univ ×ˢ Set.univ) ∧
    ∀ (x : ℝ), ∃! y, (x, y) ∈ {x | ∃ x_1, (x_1 ^ 2, x_1) = x}
⊢ False