Metamath Proof Explorer

Theorem satf0sucom

Description: The satisfaction predicate as function over wff codes in the empty model with an empty binary relation at a successor of _om . (Contributed by AV, 14-Sep-2023)

Ref Expression
Assertion satf0sucom ⊢ N ∈ suc ⁡ ω → ∅ Sat ∅ ⁡ N = rec ⁡ f ∈ V ⟼ f ∪ x y | y = ∅ ∧ ∃ u ∈ f ∃ v ∈ f x = 1 st ⁡ u ⊼ 𝑔 1 st ⁡ v ∨ ∃ i ∈ ω x = ∀ 𝑔 i 1 st ⁡ u x y | y = ∅ ∧ ∃ i ∈ ω ∃ j ∈ ω x = i ∈ 𝑔 j ⁡ N

Proof

Step Hyp Ref Expression
1 satf0 ⊢ ∅ Sat ∅ = rec ⁡ f ∈ V ⟼ f ∪ x y | y = ∅ ∧ ∃ u ∈ f ∃ v ∈ f x = 1 st ⁡ u ⊼ 𝑔 1 st ⁡ v ∨ ∃ i ∈ ω x = ∀ 𝑔 i 1 st ⁡ u x y | y = ∅ ∧ ∃ i ∈ ω ∃ j ∈ ω x = i ∈ 𝑔 j ↾ suc ⁡ ω
2 1 fveq1i ⊢ ∅ Sat ∅ ⁡ N = rec ⁡ f ∈ V ⟼ f ∪ x y | y = ∅ ∧ ∃ u ∈ f ∃ v ∈ f x = 1 st ⁡ u ⊼ 𝑔 1 st ⁡ v ∨ ∃ i ∈ ω x = ∀ 𝑔 i 1 st ⁡ u x y | y = ∅ ∧ ∃ i ∈ ω ∃ j ∈ ω x = i ∈ 𝑔 j ↾ suc ⁡ ω ⁡ N
3 fvres ⊢ N ∈ suc ⁡ ω → rec ⁡ f ∈ V ⟼ f ∪ x y | y = ∅ ∧ ∃ u ∈ f ∃ v ∈ f x = 1 st ⁡ u ⊼ 𝑔 1 st ⁡ v ∨ ∃ i ∈ ω x = ∀ 𝑔 i 1 st ⁡ u x y | y = ∅ ∧ ∃ i ∈ ω ∃ j ∈ ω x = i ∈ 𝑔 j ↾ suc ⁡ ω ⁡ N = rec ⁡ f ∈ V ⟼ f ∪ x y | y = ∅ ∧ ∃ u ∈ f ∃ v ∈ f x = 1 st ⁡ u ⊼ 𝑔 1 st ⁡ v ∨ ∃ i ∈ ω x = ∀ 𝑔 i 1 st ⁡ u x y | y = ∅ ∧ ∃ i ∈ ω ∃ j ∈ ω x = i ∈ 𝑔 j ⁡ N
4 2 3 syl5eq ⊢ N ∈ suc ⁡ ω → ∅ Sat ∅ ⁡ N = rec ⁡ f ∈ V ⟼ f ∪ x y | y = ∅ ∧ ∃ u ∈ f ∃ v ∈ f x = 1 st ⁡ u ⊼ 𝑔 1 st ⁡ v ∨ ∃ i ∈ ω x = ∀ 𝑔 i 1 st ⁡ u x y | y = ∅ ∧ ∃ i ∈ ω ∃ j ∈ ω x = i ∈ 𝑔 j ⁡ N