gonan0

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

		Ref	Expression
	Assertion	gonan0	$⊢ A ⊼_{𝑔} B \in Fmla (N) \to N \neq \emptyset$

Proof

Step	Hyp	Ref	Expression
1		1n0	$⊢ 1_{𝑜} \neq \emptyset$
2	1	neii	$⊢ \neg 1_{𝑜} = \emptyset$
3	2	intnanr	$⊢ \neg (1_{𝑜} = \emptyset \land ⟨A, B⟩ = ⟨i, j⟩)$
4		1oex	$⊢ 1_{𝑜} \in V$
5		opex	$⊢ ⟨A, B⟩ \in V$
6	4 5	opth	$⊢ ⟨1_{𝑜}, ⟨A, B⟩⟩ = ⟨\emptyset, ⟨i, j⟩⟩ \leftrightarrow (1_{𝑜} = \emptyset \land ⟨A, B⟩ = ⟨i, j⟩)$
7	3 6	mtbir	$⊢ \neg ⟨1_{𝑜}, ⟨A, B⟩⟩ = ⟨\emptyset, ⟨i, j⟩⟩$
8		goel	$⊢ (i \in ω \land j \in ω) \to i \in_{𝑔} j = ⟨\emptyset, ⟨i, j⟩⟩$
9	8	eqeq2d	$⊢ (i \in ω \land j \in ω) \to (⟨1_{𝑜}, ⟨A, B⟩⟩ = i \in_{𝑔} j \leftrightarrow ⟨1_{𝑜}, ⟨A, B⟩⟩ = ⟨\emptyset, ⟨i, j⟩⟩)$
10	7 9	mtbiri	$⊢ (i \in ω \land j \in ω) \to \neg ⟨1_{𝑜}, ⟨A, B⟩⟩ = i \in_{𝑔} j$
11	10	rgen2	$⊢ \forall i \in ω \forall j \in ω \neg ⟨1_{𝑜}, ⟨A, B⟩⟩ = i \in_{𝑔} j$
12		ralnex2	$⊢ \forall i \in ω \forall j \in ω \neg ⟨1_{𝑜}, ⟨A, B⟩⟩ = i \in_{𝑔} j \leftrightarrow \neg \exists i \in ω \exists j \in ω ⟨1_{𝑜}, ⟨A, B⟩⟩ = i \in_{𝑔} j$
13	11 12	mpbi	$⊢ \neg \exists i \in ω \exists j \in ω ⟨1_{𝑜}, ⟨A, B⟩⟩ = i \in_{𝑔} j$
14	13	intnan	$⊢ \neg (⟨1_{𝑜}, ⟨A, B⟩⟩ \in V \land \exists i \in ω \exists j \in ω ⟨1_{𝑜}, ⟨A, B⟩⟩ = i \in_{𝑔} j)$
15		eqeq1	$⊢ x = ⟨1_{𝑜}, ⟨A, B⟩⟩ \to (x = i \in_{𝑔} j \leftrightarrow ⟨1_{𝑜}, ⟨A, B⟩⟩ = i \in_{𝑔} j)$
16	15	2rexbidv	$⊢ x = ⟨1_{𝑜}, ⟨A, B⟩⟩ \to (\exists i \in ω \exists j \in ω x = i \in_{𝑔} j \leftrightarrow \exists i \in ω \exists j \in ω ⟨1_{𝑜}, ⟨A, B⟩⟩ = i \in_{𝑔} j)$
17		fmla0	$⊢ Fmla (\emptyset) = \{x \in V \| \exists i \in ω \exists j \in ω x = i \in_{𝑔} j\}$
18	16 17	elrab2	$⊢ ⟨1_{𝑜}, ⟨A, B⟩⟩ \in Fmla (\emptyset) \leftrightarrow (⟨1_{𝑜}, ⟨A, B⟩⟩ \in V \land \exists i \in ω \exists j \in ω ⟨1_{𝑜}, ⟨A, B⟩⟩ = i \in_{𝑔} j)$
19	14 18	mtbir	$⊢ \neg ⟨1_{𝑜}, ⟨A, B⟩⟩ \in Fmla (\emptyset)$
20		gonafv	$⊢ (A \in V \land B \in V) \to A ⊼_{𝑔} B = ⟨1_{𝑜}, ⟨A, B⟩⟩$
21	20	eleq1d	$⊢ (A \in V \land B \in V) \to (A ⊼_{𝑔} B \in Fmla (\emptyset) \leftrightarrow ⟨1_{𝑜}, ⟨A, B⟩⟩ \in Fmla (\emptyset))$
22	19 21	mtbiri	$⊢ (A \in V \land B \in V) \to \neg A ⊼_{𝑔} B \in Fmla (\emptyset)$
23		eqid	$⊢ (x \in (V \times V) ⟼ ⟨1_{𝑜}, x⟩) = (x \in (V \times V) ⟼ ⟨1_{𝑜}, x⟩)$
24	23	dmmptss	$⊢ dom (x \in (V \times V) ⟼ ⟨1_{𝑜}, x⟩) \subseteq V \times V$
25		relxp	$⊢ Rel (V \times V)$
26		relss	$⊢ dom (x \in (V \times V) ⟼ ⟨1_{𝑜}, x⟩) \subseteq V \times V \to (Rel (V \times V) \to Rel dom (x \in (V \times V) ⟼ ⟨1_{𝑜}, x⟩))$
27	24 25 26	mp2	$⊢ Rel dom (x \in (V \times V) ⟼ ⟨1_{𝑜}, x⟩)$
28		df-gona	$⊢ ⊼_{𝑔} = (x \in (V \times V) ⟼ ⟨1_{𝑜}, x⟩)$
29	28	dmeqi	$⊢ dom ⊼_{𝑔} = dom (x \in (V \times V) ⟼ ⟨1_{𝑜}, x⟩)$
30	29	releqi	$⊢ Rel dom ⊼_{𝑔} \leftrightarrow Rel dom (x \in (V \times V) ⟼ ⟨1_{𝑜}, x⟩)$
31	27 30	mpbir	$⊢ Rel dom ⊼_{𝑔}$
32	31	ovprc	$⊢ \neg (A \in V \land B \in V) \to A ⊼_{𝑔} B = \emptyset$
33		peano1	$⊢ \emptyset \in ω$
34		fmlaomn0	$⊢ \emptyset \in ω \to \emptyset \notin Fmla (\emptyset)$
35	33 34	ax-mp	$⊢ \emptyset \notin Fmla (\emptyset)$
36	35	neli	$⊢ \neg \emptyset \in Fmla (\emptyset)$
37		eleq1	$⊢ A ⊼_{𝑔} B = \emptyset \to (A ⊼_{𝑔} B \in Fmla (\emptyset) \leftrightarrow \emptyset \in Fmla (\emptyset))$
38	36 37	mtbiri	$⊢ A ⊼_{𝑔} B = \emptyset \to \neg A ⊼_{𝑔} B \in Fmla (\emptyset)$
39	32 38	syl	$⊢ \neg (A \in V \land B \in V) \to \neg A ⊼_{𝑔} B \in Fmla (\emptyset)$
40	22 39	pm2.61i	$⊢ \neg A ⊼_{𝑔} B \in Fmla (\emptyset)$
41		fveq2	$⊢ N = \emptyset \to Fmla (N) = Fmla (\emptyset)$
42	41	eleq2d	$⊢ N = \emptyset \to (A ⊼_{𝑔} B \in Fmla (N) \leftrightarrow A ⊼_{𝑔} B \in Fmla (\emptyset))$
43	40 42	mtbiri	$⊢ N = \emptyset \to \neg A ⊼_{𝑔} B \in Fmla (N)$
44	43	necon2ai	$⊢ A ⊼_{𝑔} B \in Fmla (N) \to N \neq \emptyset$

Metamath Proof Explorer

Theorem gonan0

Proof