case intro
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type ?u.12600
B : Set M
s f g : Set (α → M)
hg : Definable A L g
φ : Formula (L[[↑A]]) α
hφ : f = setOf (Formula.Realize φ)
⊢ Definable A L (f ∪ g)
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type ?u.12600
B : Set M
s f g : Set (α → M)
hf : Definable A L f
hg : Definable A L g
⊢ Definable A L (f ∪ g)
rcases hf with ⟨φ, hφ⟩
case intro.intro
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type ?u.12600
B : Set M
s f g : Set (α → M)
φ : Formula (L[[↑A]]) α
hφ : f = setOf (Formula.Realize φ)
θ : Formula (L[[↑A]]) α
hθ : g = setOf (Formula.Realize θ)
⊢ Definable A L (f ∪ g)
case intro
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type ?u.12600
B : Set M
s f g : Set (α → M)
hg : Definable A L g
φ : Formula (L[[↑A]]) α
hφ : f = setOf (Formula.Realize φ)
⊢ Definable A L (f ∪ g)
rcases hg with ⟨θ, hθ⟩
case intro.intro
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type ?u.12600
B : Set M
s f g : Set (α → M)
φ : Formula (L[[↑A]]) α
hφ : f = setOf (Formula.Realize φ)
θ : Formula (L[[↑A]]) α
hθ : g = setOf (Formula.Realize θ)
⊢ f ∪ g = setOf (Formula.Realize (φ ⊔ θ))
case intro.intro
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type ?u.12600
B : Set M
s f g : Set (α → M)
φ : Formula (L[[↑A]]) α
hφ : f = setOf (Formula.Realize φ)
θ : Formula (L[[↑A]]) α
hθ : g = setOf (Formula.Realize θ)
⊢ Definable A L (f ∪ g)
refine' ⟨φ ⊔ θ, _⟩
case intro.intro.h
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type ?u.12600
B : Set M
s f g : Set (α → M)
φ : Formula (L[[↑A]]) α
hφ : f = setOf (Formula.Realize φ)
θ : Formula (L[[↑A]]) α
hθ : g = setOf (Formula.Realize θ)
x✝ : α → M
⊢ x✝ ∈ f ∪ g ↔ x✝ ∈ setOf (Formula.Realize (φ ⊔ θ))
case intro.intro
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type ?u.12600
B : Set M
s f g : Set (α → M)
φ : Formula (L[[↑A]]) α
hφ : f = setOf (Formula.Realize φ)
θ : Formula (L[[↑A]]) α
hθ : g = setOf (Formula.Realize θ)
⊢ f ∪ g = setOf (Formula.Realize (φ ⊔ θ))
ext
no goals
case intro.intro.h
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type ?u.12600
B : Set M
s f g : Set (α → M)
φ : Formula (L[[↑A]]) α
hφ : f = setOf (Formula.Realize φ)
θ : Formula (L[[↑A]]) α
hθ : g = setOf (Formula.Realize θ)
x✝ : α → M
⊢ x✝ ∈ f ∪ g ↔ x✝ ∈ setOf (Formula.Realize (φ ⊔ θ))
rw [hφ, hθ, mem_setOf_eq, Formula.realize_sup, mem_union, mem_setOf_eq, mem_setOf_eq]