L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
S : Substructure (Language.sum L (skolem₁ L)) M
⊢ ∀ (n : ℕ) (φ : BoundedFormula L Empty (n + 1)) (x : Fin n → { x // x ∈ ↑(LHom.substructureReduct LHom.sumInl) S })
    (a : M),
    BoundedFormula.Realize φ default (Fin.snoc (Subtype.val ∘ x) a) →
      ∃ b, BoundedFormula.Realize φ default (Fin.snoc (Subtype.val ∘ x) ↑b)
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
S : Substructure (Language.sum L (skolem₁ L)) M
⊢ IsElementary (↑(LHom.substructureReduct LHom.sumInl) S)
apply (LHom.sumInl.substructureReduct S).isElementary_of_exists
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
S : Substructure (Language.sum L (skolem₁ L)) M
n : ℕ
φ : BoundedFormula L Empty (n + 1)
x : Fin n → { x // x ∈ ↑(LHom.substructureReduct LHom.sumInl) S }
a : M
h : BoundedFormula.Realize φ default (Fin.snoc (Subtype.val ∘ x) a)
⊢ ∃ b, BoundedFormula.Realize φ default (Fin.snoc (Subtype.val ∘ x) ↑b)
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
S : Substructure (Language.sum L (skolem₁ L)) M
⊢ ∀ (n : ℕ) (φ : BoundedFormula L Empty (n + 1)) (x : Fin n → { x // x ∈ ↑(LHom.substructureReduct LHom.sumInl) S })
    (a : M),
    BoundedFormula.Realize φ default (Fin.snoc (Subtype.val ∘ x) a) →
      ∃ b, BoundedFormula.Realize φ default (Fin.snoc (Subtype.val ∘ x) ↑b)
intro n φ x a h
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
S : Substructure (Language.sum L (skolem₁ L)) M
n : ℕ
φ : BoundedFormula L Empty (n + 1)
x : Fin n → { x // x ∈ ↑(LHom.substructureReduct LHom.sumInl) S }
a : M
h : BoundedFormula.Realize φ default (Fin.snoc (Subtype.val ∘ x) a)
φ' : Functions (Language.sum L (skolem₁ L)) n := LHom.onFunction LHom.sumInr φ
⊢ ∃ b, BoundedFormula.Realize φ default (Fin.snoc (Subtype.val ∘ x) ↑b)
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
S : Substructure (Language.sum L (skolem₁ L)) M
n : ℕ
φ : BoundedFormula L Empty (n + 1)
x : Fin n → { x // x ∈ ↑(LHom.substructureReduct LHom.sumInl) S }
a : M
h : BoundedFormula.Realize φ default (Fin.snoc (Subtype.val ∘ x) a)
⊢ ∃ b, BoundedFormula.Realize φ default (Fin.snoc (Subtype.val ∘ x) ↑b)
let φ' : (L.sum L.skolem₁).Functions n := LHom.sumInr.onFunction φ
no goals
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
S : Substructure (Language.sum L (skolem₁ L)) M
n : ℕ
φ : BoundedFormula L Empty (n + 1)
x : Fin n → { x // x ∈ ↑(LHom.substructureReduct LHom.sumInl) S }
a : M
h : BoundedFormula.Realize φ default (Fin.snoc (Subtype.val ∘ x) a)
φ' : Functions (Language.sum L (skolem₁ L)) n := LHom.onFunction LHom.sumInr φ
⊢ ∃ b, BoundedFormula.Realize φ default (Fin.snoc (Subtype.val ∘ x) ↑b)
exact
  ⟨⟨funMap φ' ((↑) ∘ x), S.fun_mem (LHom.sumInr.onFunction φ) ((↑) ∘ x) (by
    exact fun i => (x i).2)⟩,
    by exact Classical.epsilon_spec (p := fun a => BoundedFormula.Realize φ default
        (Fin.snoc (Subtype.val ∘ x) a)) ⟨a, h⟩⟩
no goals
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
S : Substructure (Language.sum L (skolem₁ L)) M
n : ℕ
φ : BoundedFormula L Empty (n + 1)
x : Fin n → { x // x ∈ ↑(LHom.substructureReduct LHom.sumInl) S }
a : M
h : BoundedFormula.Realize φ default (Fin.snoc (Subtype.val ∘ x) a)
φ' : Functions (Language.sum L (skolem₁ L)) n := LHom.onFunction LHom.sumInr φ
⊢ ∀ (i : Fin n), (Subtype.val ∘ x) i ∈ ↑S
exact fun i => (x i).2
no goals
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
S : Substructure (Language.sum L (skolem₁ L)) M
n : ℕ
φ : BoundedFormula L Empty (n + 1)
x : Fin n → { x // x ∈ ↑(LHom.substructureReduct LHom.sumInl) S }
a : M
h : BoundedFormula.Realize φ default (Fin.snoc (Subtype.val ∘ x) a)
φ' : Functions (Language.sum L (skolem₁ L)) n := LHom.onFunction LHom.sumInr φ
⊢ BoundedFormula.Realize φ default
    (Fin.snoc (Subtype.val ∘ x)
      ↑{ val := funMap φ' (Subtype.val ∘ x),
          property := (_ : funMap (LHom.onFunction LHom.sumInr φ) (Subtype.val ∘ x) ∈ ↑S) })
exact Classical.epsilon_spec (p := fun a => BoundedFormula.Realize φ default
 (Fin.snoc (Subtype.val ∘ x) a)) ⟨a, h⟩