Metamath Proof Explorer

Theorem satfsucom

Description: The satisfaction predicate for wff codes in the model M and the binary relation E on M at an element of the successor of _om . (Contributed by AV, 22-Sep-2023)

Ref Expression
Assertion satfsucom ⊢ M ∈ V ∧ E ∈ W ∧ N ∈ suc ⁡ ω → M Sat E ⁡ N = rec ⁡ f ∈ V ⟼ f ∪ x y | ∃ u ∈ f ∃ v ∈ f x = 1 st ⁡ u ⊼ 𝑔 1 st ⁡ v ∧ y = M ω ∖ 2 nd ⁡ u ∩ 2 nd ⁡ v ∨ ∃ i ∈ ω x = ∀ 𝑔 i 1 st ⁡ u ∧ y = a ∈ M ω | ∀ z ∈ M i z ∪ a ↾ ω ∖ i ∈ 2 nd ⁡ u x y | ∃ i ∈ ω ∃ j ∈ ω x = i ∈ 𝑔 j ∧ y = a ∈ M ω | a ⁡ i E a ⁡ j ⁡ N

Proof

Step Hyp Ref Expression
1 satf ⊢ M ∈ V ∧ E ∈ W → M Sat E = rec ⁡ f ∈ V ⟼ f ∪ x y | ∃ u ∈ f ∃ v ∈ f x = 1 st ⁡ u ⊼ 𝑔 1 st ⁡ v ∧ y = M ω ∖ 2 nd ⁡ u ∩ 2 nd ⁡ v ∨ ∃ i ∈ ω x = ∀ 𝑔 i 1 st ⁡ u ∧ y = a ∈ M ω | ∀ z ∈ M i z ∪ a ↾ ω ∖ i ∈ 2 nd ⁡ u x y | ∃ i ∈ ω ∃ j ∈ ω x = i ∈ 𝑔 j ∧ y = a ∈ M ω | a ⁡ i E a ⁡ j ↾ suc ⁡ ω
2 1 fveq1d ⊢ M ∈ V ∧ E ∈ W → M Sat E ⁡ N = rec ⁡ f ∈ V ⟼ f ∪ x y | ∃ u ∈ f ∃ v ∈ f x = 1 st ⁡ u ⊼ 𝑔 1 st ⁡ v ∧ y = M ω ∖ 2 nd ⁡ u ∩ 2 nd ⁡ v ∨ ∃ i ∈ ω x = ∀ 𝑔 i 1 st ⁡ u ∧ y = a ∈ M ω | ∀ z ∈ M i z ∪ a ↾ ω ∖ i ∈ 2 nd ⁡ u x y | ∃ i ∈ ω ∃ j ∈ ω x = i ∈ 𝑔 j ∧ y = a ∈ M ω | a ⁡ i E a ⁡ j ↾ suc ⁡ ω ⁡ N
3 2 3adant3 ⊢ M ∈ V ∧ E ∈ W ∧ N ∈ suc ⁡ ω → M Sat E ⁡ N = rec ⁡ f ∈ V ⟼ f ∪ x y | ∃ u ∈ f ∃ v ∈ f x = 1 st ⁡ u ⊼ 𝑔 1 st ⁡ v ∧ y = M ω ∖ 2 nd ⁡ u ∩ 2 nd ⁡ v ∨ ∃ i ∈ ω x = ∀ 𝑔 i 1 st ⁡ u ∧ y = a ∈ M ω | ∀ z ∈ M i z ∪ a ↾ ω ∖ i ∈ 2 nd ⁡ u x y | ∃ i ∈ ω ∃ j ∈ ω x = i ∈ 𝑔 j ∧ y = a ∈ M ω | a ⁡ i E a ⁡ j ↾ suc ⁡ ω ⁡ N
4 fvres ⊢ N ∈ suc ⁡ ω → rec ⁡ f ∈ V ⟼ f ∪ x y | ∃ u ∈ f ∃ v ∈ f x = 1 st ⁡ u ⊼ 𝑔 1 st ⁡ v ∧ y = M ω ∖ 2 nd ⁡ u ∩ 2 nd ⁡ v ∨ ∃ i ∈ ω x = ∀ 𝑔 i 1 st ⁡ u ∧ y = a ∈ M ω | ∀ z ∈ M i z ∪ a ↾ ω ∖ i ∈ 2 nd ⁡ u x y | ∃ i ∈ ω ∃ j ∈ ω x = i ∈ 𝑔 j ∧ y = a ∈ M ω | a ⁡ i E a ⁡ j ↾ suc ⁡ ω ⁡ N = rec ⁡ f ∈ V ⟼ f ∪ x y | ∃ u ∈ f ∃ v ∈ f x = 1 st ⁡ u ⊼ 𝑔 1 st ⁡ v ∧ y = M ω ∖ 2 nd ⁡ u ∩ 2 nd ⁡ v ∨ ∃ i ∈ ω x = ∀ 𝑔 i 1 st ⁡ u ∧ y = a ∈ M ω | ∀ z ∈ M i z ∪ a ↾ ω ∖ i ∈ 2 nd ⁡ u x y | ∃ i ∈ ω ∃ j ∈ ω x = i ∈ 𝑔 j ∧ y = a ∈ M ω | a ⁡ i E a ⁡ j ⁡ N
5 4 3ad2ant3 ⊢ M ∈ V ∧ E ∈ W ∧ N ∈ suc ⁡ ω → rec ⁡ f ∈ V ⟼ f ∪ x y | ∃ u ∈ f ∃ v ∈ f x = 1 st ⁡ u ⊼ 𝑔 1 st ⁡ v ∧ y = M ω ∖ 2 nd ⁡ u ∩ 2 nd ⁡ v ∨ ∃ i ∈ ω x = ∀ 𝑔 i 1 st ⁡ u ∧ y = a ∈ M ω | ∀ z ∈ M i z ∪ a ↾ ω ∖ i ∈ 2 nd ⁡ u x y | ∃ i ∈ ω ∃ j ∈ ω x = i ∈ 𝑔 j ∧ y = a ∈ M ω | a ⁡ i E a ⁡ j ↾ suc ⁡ ω ⁡ N = rec ⁡ f ∈ V ⟼ f ∪ x y | ∃ u ∈ f ∃ v ∈ f x = 1 st ⁡ u ⊼ 𝑔 1 st ⁡ v ∧ y = M ω ∖ 2 nd ⁡ u ∩ 2 nd ⁡ v ∨ ∃ i ∈ ω x = ∀ 𝑔 i 1 st ⁡ u ∧ y = a ∈ M ω | ∀ z ∈ M i z ∪ a ↾ ω ∖ i ∈ 2 nd ⁡ u x y | ∃ i ∈ ω ∃ j ∈ ω x = i ∈ 𝑔 j ∧ y = a ∈ M ω | a ⁡ i E a ⁡ j ⁡ N
6 3 5 eqtrd ⊢ M ∈ V ∧ E ∈ W ∧ N ∈ suc ⁡ ω → M Sat E ⁡ N = rec ⁡ f ∈ V ⟼ f ∪ x y | ∃ u ∈ f ∃ v ∈ f x = 1 st ⁡ u ⊼ 𝑔 1 st ⁡ v ∧ y = M ω ∖ 2 nd ⁡ u ∩ 2 nd ⁡ v ∨ ∃ i ∈ ω x = ∀ 𝑔 i 1 st ⁡ u ∧ y = a ∈ M ω | ∀ z ∈ M i z ∪ a ↾ ω ∖ i ∈ 2 nd ⁡ u x y | ∃ i ∈ ω ∃ j ∈ ω x = i ∈ 𝑔 j ∧ y = a ∈ M ω | a ⁡ i E a ⁡ j ⁡ N