satf00

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

		Ref	Expression
	Assertion	satf00	$⊢ (\emptyset Sat \emptyset) (\emptyset) = \{⟨x, y⟩ \| (y = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)\}$

Proof

Step	Hyp	Ref	Expression
1		peano1	$⊢ \emptyset \in ω$
2		elelsuc	$⊢ \emptyset \in ω \to \emptyset \in suc ω$
3		satf0sucom	$⊢ \emptyset \in suc ω \to (\emptyset Sat \emptyset) (\emptyset) = 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)\}) (\emptyset)$
4	1 2 3	mp2b	$⊢ (\emptyset Sat \emptyset) (\emptyset) = 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)\}) (\emptyset)$
5		omex	$⊢ ω \in V$
6	5 5	xpex	$⊢ ω \times ω \in V$
7		xpexg	$⊢ (ω \in V \land ω \times ω \in V) \to ω \times (ω \times ω) \in V$
8		simpl	$⊢ (ω \in V \land ω \times ω \in V) \to ω \in V$
9		goelel3xp	$⊢ (i \in ω \land j \in ω) \to i \in_{𝑔} j \in (ω \times (ω \times ω))$
10		eleq1	$⊢ x = i \in_{𝑔} j \to (x \in (ω \times (ω \times ω)) \leftrightarrow i \in_{𝑔} j \in (ω \times (ω \times ω)))$
11	9 10	syl5ibrcom	$⊢ (i \in ω \land j \in ω) \to (x = i \in_{𝑔} j \to x \in (ω \times (ω \times ω)))$
12	11	rexlimivv	$⊢ \exists i \in ω \exists j \in ω x = i \in_{𝑔} j \to x \in (ω \times (ω \times ω))$
13	12	ad2antll	$⊢ ((ω \in V \land ω \times ω \in V) \land (y = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)) \to x \in (ω \times (ω \times ω))$
14		eleq1	$⊢ y = \emptyset \to (y \in ω \leftrightarrow \emptyset \in ω)$
15	1 14	mpbiri	$⊢ y = \emptyset \to y \in ω$
16	15	ad2antrl	$⊢ ((ω \in V \land ω \times ω \in V) \land (y = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)) \to y \in ω$
17	7 8 13 16	opabex2	$⊢ (ω \in V \land ω \times ω \in V) \to \{⟨x, y⟩ \| (y = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)\} \in V$
18	5 6 17	mp2an	$⊢ \{⟨x, y⟩ \| (y = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)\} \in V$
19	18	rdg0	$⊢ 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)\}) (\emptyset) = \{⟨x, y⟩ \| (y = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)\}$
20	4 19	eqtri	$⊢ (\emptyset Sat \emptyset) (\emptyset) = \{⟨x, y⟩ \| (y = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)\}$

Metamath Proof Explorer

Theorem satf00

Proof