This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem satfvsucom

Description: The satisfaction predicate as function over wff codes at a successor of _om . (Contributed by AV, 22-Sep-2023)

Ref Expression
Hypothesis satfvsucom.s ⊢ S = M Sat E
Assertion satfvsucom ⊢ M ∈ V ∧ E ∈ W ∧ N ∈ suc ⁡ ω → S ⁡ 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 satfvsucom.s ⊢ S = M Sat E
2 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 ⁡ ω
3 2 3adant3 ⊢ M ∈ V ∧ E ∈ W ∧ N ∈ suc ⁡ ω → 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 ⁡ ω
4 1 3 eqtrid ⊢ M ∈ V ∧ E ∈ W ∧ N ∈ suc ⁡ ω → S = 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 ⁡ ω
5 4 fveq1d ⊢ M ∈ V ∧ E ∈ W ∧ N ∈ suc ⁡ ω → S ⁡ 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
6 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
7 6 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
8 5 7 eqtrd ⊢ M ∈ V ∧ E ∈ W ∧ N ∈ suc ⁡ ω → S ⁡ 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