fmlaomn0

Description: The empty set is not a Godel formula of any height. (Contributed by AV, 21-Oct-2023)

		Ref	Expression
	Assertion	fmlaomn0	$⊢ N \in ω \to \emptyset \notin Fmla (N)$

Proof

Step	Hyp	Ref	Expression
1		fveq2	$⊢ x = \emptyset \to Fmla (x) = Fmla (\emptyset)$
2	1	eleq2d	$⊢ x = \emptyset \to (\emptyset \in Fmla (x) \leftrightarrow \emptyset \in Fmla (\emptyset))$
3	2	notbid	$⊢ x = \emptyset \to (\neg \emptyset \in Fmla (x) \leftrightarrow \neg \emptyset \in Fmla (\emptyset))$
4		fveq2	$⊢ x = y \to Fmla (x) = Fmla (y)$
5	4	eleq2d	$⊢ x = y \to (\emptyset \in Fmla (x) \leftrightarrow \emptyset \in Fmla (y))$
6	5	notbid	$⊢ x = y \to (\neg \emptyset \in Fmla (x) \leftrightarrow \neg \emptyset \in Fmla (y))$
7		fveq2	$⊢ x = suc y \to Fmla (x) = Fmla (suc y)$
8	7	eleq2d	$⊢ x = suc y \to (\emptyset \in Fmla (x) \leftrightarrow \emptyset \in Fmla (suc y))$
9	8	notbid	$⊢ x = suc y \to (\neg \emptyset \in Fmla (x) \leftrightarrow \neg \emptyset \in Fmla (suc y))$
10		fveq2	$⊢ x = N \to Fmla (x) = Fmla (N)$
11	10	eleq2d	$⊢ x = N \to (\emptyset \in Fmla (x) \leftrightarrow \emptyset \in Fmla (N))$
12	11	notbid	$⊢ x = N \to (\neg \emptyset \in Fmla (x) \leftrightarrow \neg \emptyset \in Fmla (N))$
13		0ex	$⊢ \emptyset \in V$
14		opex	$⊢ ⟨i, j⟩ \in V$
15	13 14	pm3.2i	$⊢ (\emptyset \in V \land ⟨i, j⟩ \in V)$
16	15	a1i	$⊢ (i \in ω \land j \in ω) \to (\emptyset \in V \land ⟨i, j⟩ \in V)$
17		necom	$⊢ \emptyset \neq ⟨\emptyset, ⟨i, j⟩⟩ \leftrightarrow ⟨\emptyset, ⟨i, j⟩⟩ \neq \emptyset$
18		opnz	$⊢ ⟨\emptyset, ⟨i, j⟩⟩ \neq \emptyset \leftrightarrow (\emptyset \in V \land ⟨i, j⟩ \in V)$
19	17 18	bitri	$⊢ \emptyset \neq ⟨\emptyset, ⟨i, j⟩⟩ \leftrightarrow (\emptyset \in V \land ⟨i, j⟩ \in V)$
20	16 19	sylibr	$⊢ (i \in ω \land j \in ω) \to \emptyset \neq ⟨\emptyset, ⟨i, j⟩⟩$
21	20	neneqd	$⊢ (i \in ω \land j \in ω) \to \neg \emptyset = ⟨\emptyset, ⟨i, j⟩⟩$
22		goel	$⊢ (i \in ω \land j \in ω) \to i \in_{𝑔} j = ⟨\emptyset, ⟨i, j⟩⟩$
23	22	eqeq2d	$⊢ (i \in ω \land j \in ω) \to (\emptyset = i \in_{𝑔} j \leftrightarrow \emptyset = ⟨\emptyset, ⟨i, j⟩⟩)$
24	21 23	mtbird	$⊢ (i \in ω \land j \in ω) \to \neg \emptyset = i \in_{𝑔} j$
25	24	rgen2	$⊢ \forall i \in ω \forall j \in ω \neg \emptyset = i \in_{𝑔} j$
26		ralnex2	$⊢ \forall i \in ω \forall j \in ω \neg \emptyset = i \in_{𝑔} j \leftrightarrow \neg \exists i \in ω \exists j \in ω \emptyset = i \in_{𝑔} j$
27	25 26	mpbi	$⊢ \neg \exists i \in ω \exists j \in ω \emptyset = i \in_{𝑔} j$
28	27	intnan	$⊢ \neg (\emptyset \in V \land \exists i \in ω \exists j \in ω \emptyset = i \in_{𝑔} j)$
29		fmla0	$⊢ Fmla (\emptyset) = \{x \in V \| \exists i \in ω \exists j \in ω x = i \in_{𝑔} j\}$
30	29	eleq2i	$⊢ \emptyset \in Fmla (\emptyset) \leftrightarrow \emptyset \in \{x \in V \| \exists i \in ω \exists j \in ω x = i \in_{𝑔} j\}$
31		eqeq1	$⊢ x = \emptyset \to (x = i \in_{𝑔} j \leftrightarrow \emptyset = i \in_{𝑔} j)$
32	31	2rexbidv	$⊢ x = \emptyset \to (\exists i \in ω \exists j \in ω x = i \in_{𝑔} j \leftrightarrow \exists i \in ω \exists j \in ω \emptyset = i \in_{𝑔} j)$
33	32	elrab	$⊢ \emptyset \in \{x \in V \| \exists i \in ω \exists j \in ω x = i \in_{𝑔} j\} \leftrightarrow (\emptyset \in V \land \exists i \in ω \exists j \in ω \emptyset = i \in_{𝑔} j)$
34	30 33	bitri	$⊢ \emptyset \in Fmla (\emptyset) \leftrightarrow (\emptyset \in V \land \exists i \in ω \exists j \in ω \emptyset = i \in_{𝑔} j)$
35	28 34	mtbir	$⊢ \neg \emptyset \in Fmla (\emptyset)$
36		simpr	$⊢ (y \in ω \land \neg \emptyset \in Fmla (y)) \to \neg \emptyset \in Fmla (y)$
37		1oex	$⊢ 1_{𝑜} \in V$
38		opex	$⊢ ⟨u, v⟩ \in V$
39	37 38	opnzi	$⊢ ⟨1_{𝑜}, ⟨u, v⟩⟩ \neq \emptyset$
40	39	nesymi	$⊢ \neg \emptyset = ⟨1_{𝑜}, ⟨u, v⟩⟩$
41		gonafv	$⊢ (u \in Fmla (y) \land v \in Fmla (y)) \to u ⊼_{𝑔} v = ⟨1_{𝑜}, ⟨u, v⟩⟩$
42	41	adantll	$⊢ ((y \in ω \land u \in Fmla (y)) \land v \in Fmla (y)) \to u ⊼_{𝑔} v = ⟨1_{𝑜}, ⟨u, v⟩⟩$
43	42	eqeq2d	$⊢ ((y \in ω \land u \in Fmla (y)) \land v \in Fmla (y)) \to (\emptyset = u ⊼_{𝑔} v \leftrightarrow \emptyset = ⟨1_{𝑜}, ⟨u, v⟩⟩)$
44	40 43	mtbiri	$⊢ ((y \in ω \land u \in Fmla (y)) \land v \in Fmla (y)) \to \neg \emptyset = u ⊼_{𝑔} v$
45	44	ralrimiva	$⊢ (y \in ω \land u \in Fmla (y)) \to \forall v \in Fmla (y) \neg \emptyset = u ⊼_{𝑔} v$
46		2oex	$⊢ 2_{𝑜} \in V$
47		opex	$⊢ ⟨i, u⟩ \in V$
48	46 47	opnzi	$⊢ ⟨2_{𝑜}, ⟨i, u⟩⟩ \neq \emptyset$
49	48	nesymi	$⊢ \neg \emptyset = ⟨2_{𝑜}, ⟨i, u⟩⟩$
50		df-goal	$⊢ [\forall_{𝑔} i u] = ⟨2_{𝑜}, ⟨i, u⟩⟩$
51	50	eqeq2i	$⊢ \emptyset = [\forall_{𝑔} i u] \leftrightarrow \emptyset = ⟨2_{𝑜}, ⟨i, u⟩⟩$
52	49 51	mtbir	$⊢ \neg \emptyset = [\forall_{𝑔} i u]$
53	52	a1i	$⊢ ((y \in ω \land u \in Fmla (y)) \land i \in ω) \to \neg \emptyset = [\forall_{𝑔} i u]$
54	53	ralrimiva	$⊢ (y \in ω \land u \in Fmla (y)) \to \forall i \in ω \neg \emptyset = [\forall_{𝑔} i u]$
55	45 54	jca	$⊢ (y \in ω \land u \in Fmla (y)) \to (\forall v \in Fmla (y) \neg \emptyset = u ⊼_{𝑔} v \land \forall i \in ω \neg \emptyset = [\forall_{𝑔} i u])$
56	55	ralrimiva	$⊢ y \in ω \to \forall u \in Fmla (y) (\forall v \in Fmla (y) \neg \emptyset = u ⊼_{𝑔} v \land \forall i \in ω \neg \emptyset = [\forall_{𝑔} i u])$
57	56	adantr	$⊢ (y \in ω \land \neg \emptyset \in Fmla (y)) \to \forall u \in Fmla (y) (\forall v \in Fmla (y) \neg \emptyset = u ⊼_{𝑔} v \land \forall i \in ω \neg \emptyset = [\forall_{𝑔} i u])$
58		ralnex	$⊢ \forall v \in Fmla (y) \neg \emptyset = u ⊼_{𝑔} v \leftrightarrow \neg \exists v \in Fmla (y) \emptyset = u ⊼_{𝑔} v$
59		ralnex	$⊢ \forall i \in ω \neg \emptyset = [\forall_{𝑔} i u] \leftrightarrow \neg \exists i \in ω \emptyset = [\forall_{𝑔} i u]$
60	58 59	anbi12i	$⊢ (\forall v \in Fmla (y) \neg \emptyset = u ⊼_{𝑔} v \land \forall i \in ω \neg \emptyset = [\forall_{𝑔} i u]) \leftrightarrow (\neg \exists v \in Fmla (y) \emptyset = u ⊼_{𝑔} v \land \neg \exists i \in ω \emptyset = [\forall_{𝑔} i u])$
61		ioran	$⊢ \neg (\exists v \in Fmla (y) \emptyset = u ⊼_{𝑔} v \lor \exists i \in ω \emptyset = [\forall_{𝑔} i u]) \leftrightarrow (\neg \exists v \in Fmla (y) \emptyset = u ⊼_{𝑔} v \land \neg \exists i \in ω \emptyset = [\forall_{𝑔} i u])$
62	60 61	bitr4i	$⊢ (\forall v \in Fmla (y) \neg \emptyset = u ⊼_{𝑔} v \land \forall i \in ω \neg \emptyset = [\forall_{𝑔} i u]) \leftrightarrow \neg (\exists v \in Fmla (y) \emptyset = u ⊼_{𝑔} v \lor \exists i \in ω \emptyset = [\forall_{𝑔} i u])$
63	62	ralbii	$⊢ \forall u \in Fmla (y) (\forall v \in Fmla (y) \neg \emptyset = u ⊼_{𝑔} v \land \forall i \in ω \neg \emptyset = [\forall_{𝑔} i u]) \leftrightarrow \forall u \in Fmla (y) \neg (\exists v \in Fmla (y) \emptyset = u ⊼_{𝑔} v \lor \exists i \in ω \emptyset = [\forall_{𝑔} i u])$
64		ralnex	$⊢ \forall u \in Fmla (y) \neg (\exists v \in Fmla (y) \emptyset = u ⊼_{𝑔} v \lor \exists i \in ω \emptyset = [\forall_{𝑔} i u]) \leftrightarrow \neg \exists u \in Fmla (y) (\exists v \in Fmla (y) \emptyset = u ⊼_{𝑔} v \lor \exists i \in ω \emptyset = [\forall_{𝑔} i u])$
65	63 64	bitri	$⊢ \forall u \in Fmla (y) (\forall v \in Fmla (y) \neg \emptyset = u ⊼_{𝑔} v \land \forall i \in ω \neg \emptyset = [\forall_{𝑔} i u]) \leftrightarrow \neg \exists u \in Fmla (y) (\exists v \in Fmla (y) \emptyset = u ⊼_{𝑔} v \lor \exists i \in ω \emptyset = [\forall_{𝑔} i u])$
66	57 65	sylib	$⊢ (y \in ω \land \neg \emptyset \in Fmla (y)) \to \neg \exists u \in Fmla (y) (\exists v \in Fmla (y) \emptyset = u ⊼_{𝑔} v \lor \exists i \in ω \emptyset = [\forall_{𝑔} i u])$
67		ioran	$⊢ \neg (\emptyset \in Fmla (y) \lor \exists u \in Fmla (y) (\exists v \in Fmla (y) \emptyset = u ⊼_{𝑔} v \lor \exists i \in ω \emptyset = [\forall_{𝑔} i u])) \leftrightarrow (\neg \emptyset \in Fmla (y) \land \neg \exists u \in Fmla (y) (\exists v \in Fmla (y) \emptyset = u ⊼_{𝑔} v \lor \exists i \in ω \emptyset = [\forall_{𝑔} i u]))$
68	36 66 67	sylanbrc	$⊢ (y \in ω \land \neg \emptyset \in Fmla (y)) \to \neg (\emptyset \in Fmla (y) \lor \exists u \in Fmla (y) (\exists v \in Fmla (y) \emptyset = u ⊼_{𝑔} v \lor \exists i \in ω \emptyset = [\forall_{𝑔} i u]))$
69		fmlasuc	$⊢ y \in ω \to Fmla (suc y) = Fmla (y) \cup \{x \| \exists u \in Fmla (y) (\exists v \in Fmla (y) x = u ⊼_{𝑔} v \lor \exists i \in ω x = [\forall_{𝑔} i u])\}$
70	69	eleq2d	$⊢ y \in ω \to (\emptyset \in Fmla (suc y) \leftrightarrow \emptyset \in (Fmla (y) \cup \{x \| \exists u \in Fmla (y) (\exists v \in Fmla (y) x = u ⊼_{𝑔} v \lor \exists i \in ω x = [\forall_{𝑔} i u])\}))$
71		elun	$⊢ \emptyset \in (Fmla (y) \cup \{x \| \exists u \in Fmla (y) (\exists v \in Fmla (y) x = u ⊼_{𝑔} v \lor \exists i \in ω x = [\forall_{𝑔} i u])\}) \leftrightarrow (\emptyset \in Fmla (y) \lor \emptyset \in \{x \| \exists u \in Fmla (y) (\exists v \in Fmla (y) x = u ⊼_{𝑔} v \lor \exists i \in ω x = [\forall_{𝑔} i u])\})$
72		eqeq1	$⊢ x = \emptyset \to (x = u ⊼_{𝑔} v \leftrightarrow \emptyset = u ⊼_{𝑔} v)$
73	72	rexbidv	$⊢ x = \emptyset \to (\exists v \in Fmla (y) x = u ⊼_{𝑔} v \leftrightarrow \exists v \in Fmla (y) \emptyset = u ⊼_{𝑔} v)$
74		eqeq1	$⊢ x = \emptyset \to (x = [\forall_{𝑔} i u] \leftrightarrow \emptyset = [\forall_{𝑔} i u])$
75	74	rexbidv	$⊢ x = \emptyset \to (\exists i \in ω x = [\forall_{𝑔} i u] \leftrightarrow \exists i \in ω \emptyset = [\forall_{𝑔} i u])$
76	73 75	orbi12d	$⊢ x = \emptyset \to ((\exists v \in Fmla (y) x = u ⊼_{𝑔} v \lor \exists i \in ω x = [\forall_{𝑔} i u]) \leftrightarrow (\exists v \in Fmla (y) \emptyset = u ⊼_{𝑔} v \lor \exists i \in ω \emptyset = [\forall_{𝑔} i u]))$
77	76	rexbidv	$⊢ x = \emptyset \to (\exists u \in Fmla (y) (\exists v \in Fmla (y) x = u ⊼_{𝑔} v \lor \exists i \in ω x = [\forall_{𝑔} i u]) \leftrightarrow \exists u \in Fmla (y) (\exists v \in Fmla (y) \emptyset = u ⊼_{𝑔} v \lor \exists i \in ω \emptyset = [\forall_{𝑔} i u]))$
78	13 77	elab	$⊢ \emptyset \in \{x \| \exists u \in Fmla (y) (\exists v \in Fmla (y) x = u ⊼_{𝑔} v \lor \exists i \in ω x = [\forall_{𝑔} i u])\} \leftrightarrow \exists u \in Fmla (y) (\exists v \in Fmla (y) \emptyset = u ⊼_{𝑔} v \lor \exists i \in ω \emptyset = [\forall_{𝑔} i u])$
79	78	orbi2i	$⊢ (\emptyset \in Fmla (y) \lor \emptyset \in \{x \| \exists u \in Fmla (y) (\exists v \in Fmla (y) x = u ⊼_{𝑔} v \lor \exists i \in ω x = [\forall_{𝑔} i u])\}) \leftrightarrow (\emptyset \in Fmla (y) \lor \exists u \in Fmla (y) (\exists v \in Fmla (y) \emptyset = u ⊼_{𝑔} v \lor \exists i \in ω \emptyset = [\forall_{𝑔} i u]))$
80	71 79	bitri	$⊢ \emptyset \in (Fmla (y) \cup \{x \| \exists u \in Fmla (y) (\exists v \in Fmla (y) x = u ⊼_{𝑔} v \lor \exists i \in ω x = [\forall_{𝑔} i u])\}) \leftrightarrow (\emptyset \in Fmla (y) \lor \exists u \in Fmla (y) (\exists v \in Fmla (y) \emptyset = u ⊼_{𝑔} v \lor \exists i \in ω \emptyset = [\forall_{𝑔} i u]))$
81	70 80	bitrdi	$⊢ y \in ω \to (\emptyset \in Fmla (suc y) \leftrightarrow (\emptyset \in Fmla (y) \lor \exists u \in Fmla (y) (\exists v \in Fmla (y) \emptyset = u ⊼_{𝑔} v \lor \exists i \in ω \emptyset = [\forall_{𝑔} i u])))$
82	81	adantr	$⊢ (y \in ω \land \neg \emptyset \in Fmla (y)) \to (\emptyset \in Fmla (suc y) \leftrightarrow (\emptyset \in Fmla (y) \lor \exists u \in Fmla (y) (\exists v \in Fmla (y) \emptyset = u ⊼_{𝑔} v \lor \exists i \in ω \emptyset = [\forall_{𝑔} i u])))$
83	68 82	mtbird	$⊢ (y \in ω \land \neg \emptyset \in Fmla (y)) \to \neg \emptyset \in Fmla (suc y)$
84	83	ex	$⊢ y \in ω \to (\neg \emptyset \in Fmla (y) \to \neg \emptyset \in Fmla (suc y))$
85	3 6 9 12 35 84	finds	$⊢ N \in ω \to \neg \emptyset \in Fmla (N)$
86		df-nel	$⊢ \emptyset \notin Fmla (N) \leftrightarrow \neg \emptyset \in Fmla (N)$
87	85 86	sylibr	$⊢ N \in ω \to \emptyset \notin Fmla (N)$

Metamath Proof Explorer

Theorem fmlaomn0

Proof