L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
⊢ (#(n : ℕ) × BoundedFormula L Empty (n + 1)) ≤ max ℵ₀ (card L)
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
⊢ (#(n : ℕ) × Functions (Language.sum L (skolem₁ L)) n) ≤ max ℵ₀ (card L)
rw [card_functions_sum_skolem₁]
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
⊢ (#(n : ℕ) × BoundedFormula L Empty (n + 1)) ≤ (#(n : ℕ) × BoundedFormula L Empty n)

L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
⊢ (#(n : ℕ) × BoundedFormula L Empty n) ≤ max ℵ₀ (card L)
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
⊢ (#(n : ℕ) × BoundedFormula L Empty (n + 1)) ≤ max ℵ₀ (card L)
trans #Σ n, L.BoundedFormula Empty n
no goals
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
⊢ (#(n : ℕ) × BoundedFormula L Empty (n + 1)) ≤ (#(n : ℕ) × BoundedFormula L Empty n)
exact
  ⟨⟨Sigma.map Nat.succ fun _ => id,
      Nat.succ_injective.sigma_map fun _ => Function.injective_id⟩⟩
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
⊢ lift (max ℵ₀ (lift (#Empty) + lift (card L))) ≤ lift (max ℵ₀ (card L))
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
⊢ (#(n : ℕ) × BoundedFormula L Empty n) ≤ max ℵ₀ (card L)
refine' _root_.trans BoundedFormula.card_le (lift_le.{_, max u v}.1 _)
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
⊢ lift (max ℵ₀ (card L)) ≤ lift (max ℵ₀ (card L))
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
⊢ lift (max ℵ₀ (lift (#Empty) + lift (card L))) ≤ lift (max ℵ₀ (card L))
simp only [mk_empty, lift_zero, lift_uzero, zero_add]
no goals
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
⊢ lift (max ℵ₀ (card L)) ≤ lift (max ℵ₀ (card L))
rfl