fmla0disjsuc

Description: The set of valid Godel formulas of height 0 is disjoint with the formulas constructed from Godel-sets for the Sheffer stroke NAND and Godel-set of universal quantification. (Contributed by AV, 20-Oct-2023)

		Ref	Expression
	Assertion	fmla0disjsuc	$⊢ Fmla (\emptyset) \cap \{x \| \exists u \in Fmla (\emptyset) (\exists v \in Fmla (\emptyset) x = u ⊼_{𝑔} v \lor \exists i \in ω x = [\forall_{𝑔} i u])\} = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		fmla0	$⊢ Fmla (\emptyset) = \{x \in V \| \exists j \in ω \exists k \in ω x = j \in_{𝑔} k\}$
2		rabab	$⊢ \{x \in V \| \exists j \in ω \exists k \in ω x = j \in_{𝑔} k\} = \{x \| \exists j \in ω \exists k \in ω x = j \in_{𝑔} k\}$
3	1 2	eqtri	$⊢ Fmla (\emptyset) = \{x \| \exists j \in ω \exists k \in ω x = j \in_{𝑔} k\}$
4	3	ineq1i	$⊢ Fmla (\emptyset) \cap \{x \| \exists u \in Fmla (\emptyset) (\exists v \in Fmla (\emptyset) x = u ⊼_{𝑔} v \lor \exists i \in ω x = [\forall_{𝑔} i u])\} = \{x \| \exists j \in ω \exists k \in ω x = j \in_{𝑔} k\} \cap \{x \| \exists u \in Fmla (\emptyset) (\exists v \in Fmla (\emptyset) x = u ⊼_{𝑔} v \lor \exists i \in ω x = [\forall_{𝑔} i u])\}$
5		inab	$⊢ \{x \| \exists j \in ω \exists k \in ω x = j \in_{𝑔} k\} \cap \{x \| \exists u \in Fmla (\emptyset) (\exists v \in Fmla (\emptyset) x = u ⊼_{𝑔} v \lor \exists i \in ω x = [\forall_{𝑔} i u])\} = \{x \| (\exists j \in ω \exists k \in ω x = j \in_{𝑔} k \land \exists u \in Fmla (\emptyset) (\exists v \in Fmla (\emptyset) x = u ⊼_{𝑔} v \lor \exists i \in ω x = [\forall_{𝑔} i u]))\}$
6		goel	$⊢ (j \in ω \land k \in ω) \to j \in_{𝑔} k = ⟨\emptyset, ⟨j, k⟩⟩$
7	6	eqeq2d	$⊢ (j \in ω \land k \in ω) \to (x = j \in_{𝑔} k \leftrightarrow x = ⟨\emptyset, ⟨j, k⟩⟩)$
8		1n0	$⊢ 1_{𝑜} \neq \emptyset$
9	8	nesymi	$⊢ \neg \emptyset = 1_{𝑜}$
10	9	intnanr	$⊢ \neg (\emptyset = 1_{𝑜} \land ⟨j, k⟩ = ⟨u, v⟩)$
11		gonafv	$⊢ (u \in V \land v \in V) \to u ⊼_{𝑔} v = ⟨1_{𝑜}, ⟨u, v⟩⟩$
12	11	el2v	$⊢ u ⊼_{𝑔} v = ⟨1_{𝑜}, ⟨u, v⟩⟩$
13	12	eqeq2i	$⊢ ⟨\emptyset, ⟨j, k⟩⟩ = u ⊼_{𝑔} v \leftrightarrow ⟨\emptyset, ⟨j, k⟩⟩ = ⟨1_{𝑜}, ⟨u, v⟩⟩$
14		0ex	$⊢ \emptyset \in V$
15		opex	$⊢ ⟨j, k⟩ \in V$
16	14 15	opth	$⊢ ⟨\emptyset, ⟨j, k⟩⟩ = ⟨1_{𝑜}, ⟨u, v⟩⟩ \leftrightarrow (\emptyset = 1_{𝑜} \land ⟨j, k⟩ = ⟨u, v⟩)$
17	13 16	bitri	$⊢ ⟨\emptyset, ⟨j, k⟩⟩ = u ⊼_{𝑔} v \leftrightarrow (\emptyset = 1_{𝑜} \land ⟨j, k⟩ = ⟨u, v⟩)$
18	10 17	mtbir	$⊢ \neg ⟨\emptyset, ⟨j, k⟩⟩ = u ⊼_{𝑔} v$
19		eqeq1	$⊢ x = ⟨\emptyset, ⟨j, k⟩⟩ \to (x = u ⊼_{𝑔} v \leftrightarrow ⟨\emptyset, ⟨j, k⟩⟩ = u ⊼_{𝑔} v)$
20	18 19	mtbiri	$⊢ x = ⟨\emptyset, ⟨j, k⟩⟩ \to \neg x = u ⊼_{𝑔} v$
21	7 20	syl6bi	$⊢ (j \in ω \land k \in ω) \to (x = j \in_{𝑔} k \to \neg x = u ⊼_{𝑔} v)$
22	21	imp	$⊢ ((j \in ω \land k \in ω) \land x = j \in_{𝑔} k) \to \neg x = u ⊼_{𝑔} v$
23	22	adantr	$⊢ (((j \in ω \land k \in ω) \land x = j \in_{𝑔} k) \land u \in Fmla (\emptyset)) \to \neg x = u ⊼_{𝑔} v$
24	23	ralrimivw	$⊢ (((j \in ω \land k \in ω) \land x = j \in_{𝑔} k) \land u \in Fmla (\emptyset)) \to \forall v \in Fmla (\emptyset) \neg x = u ⊼_{𝑔} v$
25		2on0	$⊢ 2_{𝑜} \neq \emptyset$
26	25	nesymi	$⊢ \neg \emptyset = 2_{𝑜}$
27	26	orci	$⊢ (\neg \emptyset = 2_{𝑜} \lor \neg ⟨j, k⟩ = ⟨i, u⟩)$
28	14 15	opth	$⊢ ⟨\emptyset, ⟨j, k⟩⟩ = ⟨2_{𝑜}, ⟨i, u⟩⟩ \leftrightarrow (\emptyset = 2_{𝑜} \land ⟨j, k⟩ = ⟨i, u⟩)$
29	28	notbii	$⊢ \neg ⟨\emptyset, ⟨j, k⟩⟩ = ⟨2_{𝑜}, ⟨i, u⟩⟩ \leftrightarrow \neg (\emptyset = 2_{𝑜} \land ⟨j, k⟩ = ⟨i, u⟩)$
30		ianor	$⊢ \neg (\emptyset = 2_{𝑜} \land ⟨j, k⟩ = ⟨i, u⟩) \leftrightarrow (\neg \emptyset = 2_{𝑜} \lor \neg ⟨j, k⟩ = ⟨i, u⟩)$
31	29 30	bitri	$⊢ \neg ⟨\emptyset, ⟨j, k⟩⟩ = ⟨2_{𝑜}, ⟨i, u⟩⟩ \leftrightarrow (\neg \emptyset = 2_{𝑜} \lor \neg ⟨j, k⟩ = ⟨i, u⟩)$
32	27 31	mpbir	$⊢ \neg ⟨\emptyset, ⟨j, k⟩⟩ = ⟨2_{𝑜}, ⟨i, u⟩⟩$
33		eqeq1	$⊢ x = ⟨\emptyset, ⟨j, k⟩⟩ \to (x = [\forall_{𝑔} i u] \leftrightarrow ⟨\emptyset, ⟨j, k⟩⟩ = [\forall_{𝑔} i u])$
34		df-goal	$⊢ [\forall_{𝑔} i u] = ⟨2_{𝑜}, ⟨i, u⟩⟩$
35	34	eqeq2i	$⊢ ⟨\emptyset, ⟨j, k⟩⟩ = [\forall_{𝑔} i u] \leftrightarrow ⟨\emptyset, ⟨j, k⟩⟩ = ⟨2_{𝑜}, ⟨i, u⟩⟩$
36	33 35	bitrdi	$⊢ x = ⟨\emptyset, ⟨j, k⟩⟩ \to (x = [\forall_{𝑔} i u] \leftrightarrow ⟨\emptyset, ⟨j, k⟩⟩ = ⟨2_{𝑜}, ⟨i, u⟩⟩)$
37	32 36	mtbiri	$⊢ x = ⟨\emptyset, ⟨j, k⟩⟩ \to \neg x = [\forall_{𝑔} i u]$
38	7 37	syl6bi	$⊢ (j \in ω \land k \in ω) \to (x = j \in_{𝑔} k \to \neg x = [\forall_{𝑔} i u])$
39	38	imp	$⊢ ((j \in ω \land k \in ω) \land x = j \in_{𝑔} k) \to \neg x = [\forall_{𝑔} i u]$
40	39	adantr	$⊢ (((j \in ω \land k \in ω) \land x = j \in_{𝑔} k) \land u \in Fmla (\emptyset)) \to \neg x = [\forall_{𝑔} i u]$
41	40	adantr	$⊢ ((((j \in ω \land k \in ω) \land x = j \in_{𝑔} k) \land u \in Fmla (\emptyset)) \land i \in ω) \to \neg x = [\forall_{𝑔} i u]$
42	41	ralrimiva	$⊢ (((j \in ω \land k \in ω) \land x = j \in_{𝑔} k) \land u \in Fmla (\emptyset)) \to \forall i \in ω \neg x = [\forall_{𝑔} i u]$
43	24 42	jca	$⊢ (((j \in ω \land k \in ω) \land x = j \in_{𝑔} k) \land u \in Fmla (\emptyset)) \to (\forall v \in Fmla (\emptyset) \neg x = u ⊼_{𝑔} v \land \forall i \in ω \neg x = [\forall_{𝑔} i u])$
44	43	ralrimiva	$⊢ ((j \in ω \land k \in ω) \land x = j \in_{𝑔} k) \to \forall u \in Fmla (\emptyset) (\forall v \in Fmla (\emptyset) \neg x = u ⊼_{𝑔} v \land \forall i \in ω \neg x = [\forall_{𝑔} i u])$
45		ralnex	$⊢ \forall v \in Fmla (\emptyset) \neg x = u ⊼_{𝑔} v \leftrightarrow \neg \exists v \in Fmla (\emptyset) x = u ⊼_{𝑔} v$
46		ralnex	$⊢ \forall i \in ω \neg x = [\forall_{𝑔} i u] \leftrightarrow \neg \exists i \in ω x = [\forall_{𝑔} i u]$
47	45 46	anbi12i	$⊢ (\forall v \in Fmla (\emptyset) \neg x = u ⊼_{𝑔} v \land \forall i \in ω \neg x = [\forall_{𝑔} i u]) \leftrightarrow (\neg \exists v \in Fmla (\emptyset) x = u ⊼_{𝑔} v \land \neg \exists i \in ω x = [\forall_{𝑔} i u])$
48		ioran	$⊢ \neg (\exists v \in Fmla (\emptyset) x = u ⊼_{𝑔} v \lor \exists i \in ω x = [\forall_{𝑔} i u]) \leftrightarrow (\neg \exists v \in Fmla (\emptyset) x = u ⊼_{𝑔} v \land \neg \exists i \in ω x = [\forall_{𝑔} i u])$
49	47 48	bitr4i	$⊢ (\forall v \in Fmla (\emptyset) \neg x = u ⊼_{𝑔} v \land \forall i \in ω \neg x = [\forall_{𝑔} i u]) \leftrightarrow \neg (\exists v \in Fmla (\emptyset) x = u ⊼_{𝑔} v \lor \exists i \in ω x = [\forall_{𝑔} i u])$
50	49	ralbii	$⊢ \forall u \in Fmla (\emptyset) (\forall v \in Fmla (\emptyset) \neg x = u ⊼_{𝑔} v \land \forall i \in ω \neg x = [\forall_{𝑔} i u]) \leftrightarrow \forall u \in Fmla (\emptyset) \neg (\exists v \in Fmla (\emptyset) x = u ⊼_{𝑔} v \lor \exists i \in ω x = [\forall_{𝑔} i u])$
51		ralnex	$⊢ \forall u \in Fmla (\emptyset) \neg (\exists v \in Fmla (\emptyset) x = u ⊼_{𝑔} v \lor \exists i \in ω x = [\forall_{𝑔} i u]) \leftrightarrow \neg \exists u \in Fmla (\emptyset) (\exists v \in Fmla (\emptyset) x = u ⊼_{𝑔} v \lor \exists i \in ω x = [\forall_{𝑔} i u])$
52	50 51	bitri	$⊢ \forall u \in Fmla (\emptyset) (\forall v \in Fmla (\emptyset) \neg x = u ⊼_{𝑔} v \land \forall i \in ω \neg x = [\forall_{𝑔} i u]) \leftrightarrow \neg \exists u \in Fmla (\emptyset) (\exists v \in Fmla (\emptyset) x = u ⊼_{𝑔} v \lor \exists i \in ω x = [\forall_{𝑔} i u])$
53	44 52	sylib	$⊢ ((j \in ω \land k \in ω) \land x = j \in_{𝑔} k) \to \neg \exists u \in Fmla (\emptyset) (\exists v \in Fmla (\emptyset) x = u ⊼_{𝑔} v \lor \exists i \in ω x = [\forall_{𝑔} i u])$
54	53	ex	$⊢ (j \in ω \land k \in ω) \to (x = j \in_{𝑔} k \to \neg \exists u \in Fmla (\emptyset) (\exists v \in Fmla (\emptyset) x = u ⊼_{𝑔} v \lor \exists i \in ω x = [\forall_{𝑔} i u]))$
55	54	rexlimdva	$⊢ j \in ω \to (\exists k \in ω x = j \in_{𝑔} k \to \neg \exists u \in Fmla (\emptyset) (\exists v \in Fmla (\emptyset) x = u ⊼_{𝑔} v \lor \exists i \in ω x = [\forall_{𝑔} i u]))$
56	55	rexlimiv	$⊢ \exists j \in ω \exists k \in ω x = j \in_{𝑔} k \to \neg \exists u \in Fmla (\emptyset) (\exists v \in Fmla (\emptyset) x = u ⊼_{𝑔} v \lor \exists i \in ω x = [\forall_{𝑔} i u])$
57	56	imori	$⊢ (\neg \exists j \in ω \exists k \in ω x = j \in_{𝑔} k \lor \neg \exists u \in Fmla (\emptyset) (\exists v \in Fmla (\emptyset) x = u ⊼_{𝑔} v \lor \exists i \in ω x = [\forall_{𝑔} i u]))$
58		ianor	$⊢ \neg (\exists j \in ω \exists k \in ω x = j \in_{𝑔} k \land \exists u \in Fmla (\emptyset) (\exists v \in Fmla (\emptyset) x = u ⊼_{𝑔} v \lor \exists i \in ω x = [\forall_{𝑔} i u])) \leftrightarrow (\neg \exists j \in ω \exists k \in ω x = j \in_{𝑔} k \lor \neg \exists u \in Fmla (\emptyset) (\exists v \in Fmla (\emptyset) x = u ⊼_{𝑔} v \lor \exists i \in ω x = [\forall_{𝑔} i u]))$
59	57 58	mpbir	$⊢ \neg (\exists j \in ω \exists k \in ω x = j \in_{𝑔} k \land \exists u \in Fmla (\emptyset) (\exists v \in Fmla (\emptyset) x = u ⊼_{𝑔} v \lor \exists i \in ω x = [\forall_{𝑔} i u]))$
60	59	abf	$⊢ \{x \| (\exists j \in ω \exists k \in ω x = j \in_{𝑔} k \land \exists u \in Fmla (\emptyset) (\exists v \in Fmla (\emptyset) x = u ⊼_{𝑔} v \lor \exists i \in ω x = [\forall_{𝑔} i u]))\} = \emptyset$
61	5 60	eqtri	$⊢ \{x \| \exists j \in ω \exists k \in ω x = j \in_{𝑔} k\} \cap \{x \| \exists u \in Fmla (\emptyset) (\exists v \in Fmla (\emptyset) x = u ⊼_{𝑔} v \lor \exists i \in ω x = [\forall_{𝑔} i u])\} = \emptyset$
62	4 61	eqtri	$⊢ Fmla (\emptyset) \cap \{x \| \exists u \in Fmla (\emptyset) (\exists v \in Fmla (\emptyset) x = u ⊼_{𝑔} v \lor \exists i \in ω x = [\forall_{𝑔} i u])\} = \emptyset$

Metamath Proof Explorer

Theorem fmla0disjsuc

Proof