Metamath Proof Explorer

Theorem fmla0

Description: The valid Godel formulas of height 0 is the set of all formulas of the form v_i e. v_j ("Godel-set of membership") coded as <. (/) , <. i , j >. >. . (Contributed by AV, 14-Sep-2023)

		Ref	Expression
	Assertion	fmla0	$⊢ Fmla (\emptyset) = \{x \in V \| \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		fmlafv	$⊢ \emptyset \in suc ω \to Fmla (\emptyset) = dom (\emptyset Sat \emptyset) (\emptyset)$
4	1 2 3	mp2b	$⊢ Fmla (\emptyset) = dom (\emptyset Sat \emptyset) (\emptyset)$
5		satf00	$⊢ (\emptyset Sat \emptyset) (\emptyset) = \{⟨x, y⟩ \| (y = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)\}$
6	5	dmeqi	$⊢ dom (\emptyset Sat \emptyset) (\emptyset) = dom \{⟨x, y⟩ \| (y = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)\}$
7		0ex	$⊢ \emptyset \in V$
8	7	isseti	$⊢ \exists y y = \emptyset$
9		19.41v	$⊢ \exists y (y = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j) \leftrightarrow (\exists y y = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)$
10	8 9	mpbiran	$⊢ \exists y (y = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j) \leftrightarrow \exists i \in ω \exists j \in ω x = i \in_{𝑔} j$
11	10	abbii	$⊢ \{x \| \exists y (y = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)\} = \{x \| \exists i \in ω \exists j \in ω x = i \in_{𝑔} j\}$
12		dmopab	$⊢ dom \{⟨x, y⟩ \| (y = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)\} = \{x \| \exists y (y = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)\}$
13		rabab	$⊢ \{x \in V \| \exists i \in ω \exists j \in ω x = i \in_{𝑔} j\} = \{x \| \exists i \in ω \exists j \in ω x = i \in_{𝑔} j\}$
14	11 12 13	3eqtr4i	$⊢ dom \{⟨x, y⟩ \| (y = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)\} = \{x \in V \| \exists i \in ω \exists j \in ω x = i \in_{𝑔} j\}$
15	4 6 14	3eqtri	$⊢ Fmla (\emptyset) = \{x \in V \| \exists i \in ω \exists j \in ω x = i \in_{𝑔} j\}$