simp[Finset.subset_image_iff, Semiformula.domain]
L : Language
T : Theory L
A : FinSubtheory T → Type u
s : (i : FinSubtheory T) → Structure L (A i)
inst✝ : ∀ (t : FinSubtheory T), Nonempty (A t)
H : ∀ (i : FinSubtheory T), A i ⊧ₘ* ↑↑i
this : DecidableEq (Set (FinSubtheory T))
⊢ ∀ (T_1 : Finset (Set (FinSubtheory T))), ↑T_1 ⊆ Semiformula.domain A '' T → (⋂₀ ↑T_1).Nonempty
L : Language
T : Theory L
A : FinSubtheory T → Type u
s : (i : FinSubtheory T) → Structure L (A i)
inst✝ : ∀ (t : FinSubtheory T), Nonempty (A t)
H : ∀ (i : FinSubtheory T), A i ⊧ₘ* ↑↑i
this : DecidableEq (Set (FinSubtheory T))
⊢ ∀ (a : Finset (Sentence L)), ↑a ⊆ T → ∃ a_2, ∃ (h : ↑a_2 ⊆ T), ∀ a_3 ∈ a, A ⟨a_2, ⋯⟩ ⊧ₘ a_3