satf0suc

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

		Ref	Expression
	Hypothesis	satf0suc.s	$⊢ S = \emptyset Sat \emptyset$
	Assertion	satf0suc	$⊢ N \in ω \to S (suc N) = S (N) \cup \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in S (N) (\exists v \in S (N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}$

Proof

Step	Hyp	Ref	Expression
1		satf0suc.s	$⊢ S = \emptyset Sat \emptyset$
2	1	fveq1i	$⊢ S (suc N) = (\emptyset Sat \emptyset) (suc N)$
3	2	a1i	$⊢ N \in ω \to S (suc N) = (\emptyset Sat \emptyset) (suc N)$
4		omsucelsucb	$⊢ N \in ω \leftrightarrow suc N \in suc ω$
5		satf0sucom	$⊢ suc N \in suc ω \to (\emptyset Sat \emptyset) (suc N) = rec ((f \in V ⟼ f \cup \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}), \{⟨x, y⟩ \| (y = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)\}) (suc N)$
6	4 5	sylbi	$⊢ N \in ω \to (\emptyset Sat \emptyset) (suc N) = rec ((f \in V ⟼ f \cup \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}), \{⟨x, y⟩ \| (y = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)\}) (suc N)$
7		nnon	$⊢ N \in ω \to N \in On$
8		rdgsuc	$⊢ N \in On \to rec ((f \in V ⟼ f \cup \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}), \{⟨x, y⟩ \| (y = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)\}) (suc N) = (f \in V ⟼ f \cup \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}) (rec ((f \in V ⟼ f \cup \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}), \{⟨x, y⟩ \| (y = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)\}) (N))$
9	7 8	syl	$⊢ N \in ω \to rec ((f \in V ⟼ f \cup \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}), \{⟨x, y⟩ \| (y = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)\}) (suc N) = (f \in V ⟼ f \cup \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}) (rec ((f \in V ⟼ f \cup \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}), \{⟨x, y⟩ \| (y = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)\}) (N))$
10		elelsuc	$⊢ N \in ω \to N \in suc ω$
11		satf0sucom	$⊢ N \in suc ω \to (\emptyset Sat \emptyset) (N) = rec ((f \in V ⟼ f \cup \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}), \{⟨x, y⟩ \| (y = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)\}) (N)$
12	10 11	syl	$⊢ N \in ω \to (\emptyset Sat \emptyset) (N) = rec ((f \in V ⟼ f \cup \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}), \{⟨x, y⟩ \| (y = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)\}) (N)$
13	1	eqcomi	$⊢ \emptyset Sat \emptyset = S$
14	13	fveq1i	$⊢ (\emptyset Sat \emptyset) (N) = S (N)$
15	12 14	eqtr3di	$⊢ N \in ω \to rec ((f \in V ⟼ f \cup \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}), \{⟨x, y⟩ \| (y = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)\}) (N) = S (N)$
16	15	fveq2d	$⊢ N \in ω \to (f \in V ⟼ f \cup \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}) (rec ((f \in V ⟼ f \cup \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}), \{⟨x, y⟩ \| (y = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)\}) (N)) = (f \in V ⟼ f \cup \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}) (S (N))$
17		eqidd	$⊢ N \in ω \to (f \in V ⟼ f \cup \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}) = (f \in V ⟼ f \cup \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\})$
18		id	$⊢ f = S (N) \to f = S (N)$
19		rexeq	$⊢ f = S (N) \to (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \leftrightarrow \exists v \in S (N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v))$
20	19	orbi1d	$⊢ f = S (N) \to ((\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]) \leftrightarrow (\exists v \in S (N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))$
21	20	rexeqbi1dv	$⊢ f = S (N) \to (\exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]) \leftrightarrow \exists u \in S (N) (\exists v \in S (N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))$
22	21	anbi2d	$⊢ f = S (N) \to ((y = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)])) \leftrightarrow (y = \emptyset \land \exists u \in S (N) (\exists v \in S (N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)])))$
23	22	opabbidv	$⊢ f = S (N) \to \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\} = \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in S (N) (\exists v \in S (N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}$
24	18 23	uneq12d	$⊢ f = S (N) \to f \cup \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\} = S (N) \cup \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in S (N) (\exists v \in S (N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}$
25	24	adantl	$⊢ (N \in ω \land f = S (N)) \to f \cup \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\} = S (N) \cup \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in S (N) (\exists v \in S (N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}$
26		fvex	$⊢ S (N) \in V$
27	26	a1i	$⊢ N \in ω \to S (N) \in V$
28		omex	$⊢ ω \in V$
29		satf0suclem	$⊢ (S (N) \in V \land S (N) \in V \land ω \in V) \to \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in S (N) (\exists v \in S (N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\} \in V$
30	26 26 28 29	mp3an	$⊢ \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in S (N) (\exists v \in S (N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\} \in V$
31	26 30	unex	$⊢ S (N) \cup \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in S (N) (\exists v \in S (N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\} \in V$
32	31	a1i	$⊢ N \in ω \to S (N) \cup \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in S (N) (\exists v \in S (N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\} \in V$
33	17 25 27 32	fvmptd	$⊢ N \in ω \to (f \in V ⟼ f \cup \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}) (S (N)) = S (N) \cup \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in S (N) (\exists v \in S (N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}$
34	9 16 33	3eqtrd	$⊢ N \in ω \to rec ((f \in V ⟼ f \cup \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}), \{⟨x, y⟩ \| (y = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)\}) (suc N) = S (N) \cup \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in S (N) (\exists v \in S (N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}$
35	3 6 34	3eqtrd	$⊢ N \in ω \to S (suc N) = S (N) \cup \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in S (N) (\exists v \in S (N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}$

Metamath Proof Explorer

Theorem satf0suc

Proof