goaln0

Description: The "Godel-set of universal quantification" is a Godel formula of at least height 1. (Contributed by AV, 22-Oct-2023)

		Ref	Expression
	Assertion	goaln0	$⊢ [\forall_{𝑔} i A] \in Fmla (N) \to N \neq \emptyset$

Proof

Step	Hyp	Ref	Expression
1		df-goal	$⊢ [\forall_{𝑔} i A] = ⟨2_{𝑜}, ⟨i, A⟩⟩$
2		2on0	$⊢ 2_{𝑜} \neq \emptyset$
3	2	neii	$⊢ \neg 2_{𝑜} = \emptyset$
4	3	intnanr	$⊢ \neg (2_{𝑜} = \emptyset \land ⟨i, A⟩ = ⟨k, j⟩)$
5		2oex	$⊢ 2_{𝑜} \in V$
6		opex	$⊢ ⟨i, A⟩ \in V$
7	5 6	opth	$⊢ ⟨2_{𝑜}, ⟨i, A⟩⟩ = ⟨\emptyset, ⟨k, j⟩⟩ \leftrightarrow (2_{𝑜} = \emptyset \land ⟨i, A⟩ = ⟨k, j⟩)$
8	4 7	mtbir	$⊢ \neg ⟨2_{𝑜}, ⟨i, A⟩⟩ = ⟨\emptyset, ⟨k, j⟩⟩$
9		goel	$⊢ (k \in ω \land j \in ω) \to k \in_{𝑔} j = ⟨\emptyset, ⟨k, j⟩⟩$
10	9	eqeq2d	$⊢ (k \in ω \land j \in ω) \to (⟨2_{𝑜}, ⟨i, A⟩⟩ = k \in_{𝑔} j \leftrightarrow ⟨2_{𝑜}, ⟨i, A⟩⟩ = ⟨\emptyset, ⟨k, j⟩⟩)$
11	8 10	mtbiri	$⊢ (k \in ω \land j \in ω) \to \neg ⟨2_{𝑜}, ⟨i, A⟩⟩ = k \in_{𝑔} j$
12	11	rgen2	$⊢ \forall k \in ω \forall j \in ω \neg ⟨2_{𝑜}, ⟨i, A⟩⟩ = k \in_{𝑔} j$
13		ralnex2	$⊢ \forall k \in ω \forall j \in ω \neg ⟨2_{𝑜}, ⟨i, A⟩⟩ = k \in_{𝑔} j \leftrightarrow \neg \exists k \in ω \exists j \in ω ⟨2_{𝑜}, ⟨i, A⟩⟩ = k \in_{𝑔} j$
14	12 13	mpbi	$⊢ \neg \exists k \in ω \exists j \in ω ⟨2_{𝑜}, ⟨i, A⟩⟩ = k \in_{𝑔} j$
15	14	intnan	$⊢ \neg (⟨2_{𝑜}, ⟨i, A⟩⟩ \in V \land \exists k \in ω \exists j \in ω ⟨2_{𝑜}, ⟨i, A⟩⟩ = k \in_{𝑔} j)$
16		eqeq1	$⊢ x = ⟨2_{𝑜}, ⟨i, A⟩⟩ \to (x = k \in_{𝑔} j \leftrightarrow ⟨2_{𝑜}, ⟨i, A⟩⟩ = k \in_{𝑔} j)$
17	16	2rexbidv	$⊢ x = ⟨2_{𝑜}, ⟨i, A⟩⟩ \to (\exists k \in ω \exists j \in ω x = k \in_{𝑔} j \leftrightarrow \exists k \in ω \exists j \in ω ⟨2_{𝑜}, ⟨i, A⟩⟩ = k \in_{𝑔} j)$
18		fmla0	$⊢ Fmla (\emptyset) = \{x \in V \| \exists k \in ω \exists j \in ω x = k \in_{𝑔} j\}$
19	17 18	elrab2	$⊢ ⟨2_{𝑜}, ⟨i, A⟩⟩ \in Fmla (\emptyset) \leftrightarrow (⟨2_{𝑜}, ⟨i, A⟩⟩ \in V \land \exists k \in ω \exists j \in ω ⟨2_{𝑜}, ⟨i, A⟩⟩ = k \in_{𝑔} j)$
20	15 19	mtbir	$⊢ \neg ⟨2_{𝑜}, ⟨i, A⟩⟩ \in Fmla (\emptyset)$
21	1 20	eqneltri	$⊢ \neg [\forall_{𝑔} i A] \in Fmla (\emptyset)$
22		fveq2	$⊢ N = \emptyset \to Fmla (N) = Fmla (\emptyset)$
23	22	eleq2d	$⊢ N = \emptyset \to ([\forall_{𝑔} i A] \in Fmla (N) \leftrightarrow [\forall_{𝑔} i A] \in Fmla (\emptyset))$
24	21 23	mtbiri	$⊢ N = \emptyset \to \neg [\forall_{𝑔} i A] \in Fmla (N)$
25	24	necon2ai	$⊢ [\forall_{𝑔} i A] \in Fmla (N) \to N \neq \emptyset$

Metamath Proof Explorer

Theorem goaln0

Proof