fmla0xp

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, 15-Sep-2023)

		Ref	Expression
	Assertion	fmla0xp	$⊢ Fmla (\emptyset) = \{\emptyset\} \times (ω \times ω)$

Proof

Step	Hyp	Ref	Expression
1		fmla0	$⊢ Fmla (\emptyset) = \{x \in V \| \exists i \in ω \exists j \in ω x = i \in_{𝑔} j\}$
2		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\}$
3		eqabcb	$⊢ \{x \| \exists i \in ω \exists j \in ω x = i \in_{𝑔} j\} = \{\emptyset\} \times (ω \times ω) \leftrightarrow \forall x (\exists i \in ω \exists j \in ω x = i \in_{𝑔} j \leftrightarrow x \in (\{\emptyset\} \times (ω \times ω)))$
4		goel	$⊢ (i \in ω \land j \in ω) \to i \in_{𝑔} j = ⟨\emptyset, ⟨i, j⟩⟩$
5	4	eqeq2d	$⊢ (i \in ω \land j \in ω) \to (x = i \in_{𝑔} j \leftrightarrow x = ⟨\emptyset, ⟨i, j⟩⟩)$
6	5	2rexbiia	$⊢ \exists i \in ω \exists j \in ω x = i \in_{𝑔} j \leftrightarrow \exists i \in ω \exists j \in ω x = ⟨\emptyset, ⟨i, j⟩⟩$
7		0ex	$⊢ \emptyset \in V$
8	7	snid	$⊢ \emptyset \in \{\emptyset\}$
9	8	a1i	$⊢ (i \in ω \land j \in ω) \to \emptyset \in \{\emptyset\}$
10		opelxpi	$⊢ (i \in ω \land j \in ω) \to ⟨i, j⟩ \in (ω \times ω)$
11	9 10	opelxpd	$⊢ (i \in ω \land j \in ω) \to ⟨\emptyset, ⟨i, j⟩⟩ \in (\{\emptyset\} \times (ω \times ω))$
12		eleq1	$⊢ x = ⟨\emptyset, ⟨i, j⟩⟩ \to (x \in (\{\emptyset\} \times (ω \times ω)) \leftrightarrow ⟨\emptyset, ⟨i, j⟩⟩ \in (\{\emptyset\} \times (ω \times ω)))$
13	11 12	syl5ibrcom	$⊢ (i \in ω \land j \in ω) \to (x = ⟨\emptyset, ⟨i, j⟩⟩ \to x \in (\{\emptyset\} \times (ω \times ω)))$
14	13	rexlimivv	$⊢ \exists i \in ω \exists j \in ω x = ⟨\emptyset, ⟨i, j⟩⟩ \to x \in (\{\emptyset\} \times (ω \times ω))$
15		elxpi	$⊢ x \in (\{\emptyset\} \times (ω \times ω)) \to \exists y \exists z (x = ⟨y, z⟩ \land (y \in \{\emptyset\} \land z \in (ω \times ω)))$
16		elsni	$⊢ y \in \{\emptyset\} \to y = \emptyset$
17	16	opeq1d	$⊢ y \in \{\emptyset\} \to ⟨y, z⟩ = ⟨\emptyset, z⟩$
18	17	eqeq2d	$⊢ y \in \{\emptyset\} \to (x = ⟨y, z⟩ \leftrightarrow x = ⟨\emptyset, z⟩)$
19	18	adantr	$⊢ (y \in \{\emptyset\} \land z \in (ω \times ω)) \to (x = ⟨y, z⟩ \leftrightarrow x = ⟨\emptyset, z⟩)$
20		elxpi	$⊢ z \in (ω \times ω) \to \exists i \exists j (z = ⟨i, j⟩ \land (i \in ω \land j \in ω))$
21		simprr	$⊢ (x = ⟨\emptyset, z⟩ \land (z = ⟨i, j⟩ \land (i \in ω \land j \in ω))) \to (i \in ω \land j \in ω)$
22		simpl	$⊢ (x = ⟨\emptyset, z⟩ \land (z = ⟨i, j⟩ \land (i \in ω \land j \in ω))) \to x = ⟨\emptyset, z⟩$
23		opeq2	$⊢ z = ⟨i, j⟩ \to ⟨\emptyset, z⟩ = ⟨\emptyset, ⟨i, j⟩⟩$
24	23	adantr	$⊢ (z = ⟨i, j⟩ \land (i \in ω \land j \in ω)) \to ⟨\emptyset, z⟩ = ⟨\emptyset, ⟨i, j⟩⟩$
25	24	adantl	$⊢ (x = ⟨\emptyset, z⟩ \land (z = ⟨i, j⟩ \land (i \in ω \land j \in ω))) \to ⟨\emptyset, z⟩ = ⟨\emptyset, ⟨i, j⟩⟩$
26	22 25	eqtrd	$⊢ (x = ⟨\emptyset, z⟩ \land (z = ⟨i, j⟩ \land (i \in ω \land j \in ω))) \to x = ⟨\emptyset, ⟨i, j⟩⟩$
27	21 26	jca	$⊢ (x = ⟨\emptyset, z⟩ \land (z = ⟨i, j⟩ \land (i \in ω \land j \in ω))) \to ((i \in ω \land j \in ω) \land x = ⟨\emptyset, ⟨i, j⟩⟩)$
28	27	ex	$⊢ x = ⟨\emptyset, z⟩ \to ((z = ⟨i, j⟩ \land (i \in ω \land j \in ω)) \to ((i \in ω \land j \in ω) \land x = ⟨\emptyset, ⟨i, j⟩⟩))$
29	28	2eximdv	$⊢ x = ⟨\emptyset, z⟩ \to (\exists i \exists j (z = ⟨i, j⟩ \land (i \in ω \land j \in ω)) \to \exists i \exists j ((i \in ω \land j \in ω) \land x = ⟨\emptyset, ⟨i, j⟩⟩))$
30		r2ex	$⊢ \exists i \in ω \exists j \in ω x = ⟨\emptyset, ⟨i, j⟩⟩ \leftrightarrow \exists i \exists j ((i \in ω \land j \in ω) \land x = ⟨\emptyset, ⟨i, j⟩⟩)$
31	29 30	imbitrrdi	$⊢ x = ⟨\emptyset, z⟩ \to (\exists i \exists j (z = ⟨i, j⟩ \land (i \in ω \land j \in ω)) \to \exists i \in ω \exists j \in ω x = ⟨\emptyset, ⟨i, j⟩⟩)$
32	20 31	syl5com	$⊢ z \in (ω \times ω) \to (x = ⟨\emptyset, z⟩ \to \exists i \in ω \exists j \in ω x = ⟨\emptyset, ⟨i, j⟩⟩)$
33	32	adantl	$⊢ (y \in \{\emptyset\} \land z \in (ω \times ω)) \to (x = ⟨\emptyset, z⟩ \to \exists i \in ω \exists j \in ω x = ⟨\emptyset, ⟨i, j⟩⟩)$
34	19 33	sylbid	$⊢ (y \in \{\emptyset\} \land z \in (ω \times ω)) \to (x = ⟨y, z⟩ \to \exists i \in ω \exists j \in ω x = ⟨\emptyset, ⟨i, j⟩⟩)$
35	34	impcom	$⊢ (x = ⟨y, z⟩ \land (y \in \{\emptyset\} \land z \in (ω \times ω))) \to \exists i \in ω \exists j \in ω x = ⟨\emptyset, ⟨i, j⟩⟩$
36	35	exlimivv	$⊢ \exists y \exists z (x = ⟨y, z⟩ \land (y \in \{\emptyset\} \land z \in (ω \times ω))) \to \exists i \in ω \exists j \in ω x = ⟨\emptyset, ⟨i, j⟩⟩$
37	15 36	syl	$⊢ x \in (\{\emptyset\} \times (ω \times ω)) \to \exists i \in ω \exists j \in ω x = ⟨\emptyset, ⟨i, j⟩⟩$
38	14 37	impbii	$⊢ \exists i \in ω \exists j \in ω x = ⟨\emptyset, ⟨i, j⟩⟩ \leftrightarrow x \in (\{\emptyset\} \times (ω \times ω))$
39	6 38	bitri	$⊢ \exists i \in ω \exists j \in ω x = i \in_{𝑔} j \leftrightarrow x \in (\{\emptyset\} \times (ω \times ω))$
40	3 39	mpgbir	$⊢ \{x \| \exists i \in ω \exists j \in ω x = i \in_{𝑔} j\} = \{\emptyset\} \times (ω \times ω)$
41	1 2 40	3eqtri	$⊢ Fmla (\emptyset) = \{\emptyset\} \times (ω \times ω)$

Metamath Proof Explorer

Theorem fmla0xp

Proof