gonar

Description: If the "Godel-set of NAND" applied to classes is a Godel formula, the classes are also Godel formulas. Remark: The reverse is not valid for A or B being of the same height as the "Godel-set of NAND". (Contributed by AV, 21-Oct-2023)

		Ref	Expression
	Assertion	gonar	$⊢ (N \in ω \land a ⊼_{𝑔} b \in Fmla (N)) \to (a \in Fmla (N) \land b \in Fmla (N))$

Proof

Step	Hyp	Ref	Expression
1		gonan0	$⊢ a ⊼_{𝑔} b \in Fmla (N) \to N \neq \emptyset$
2	1	adantl	$⊢ (N \in ω \land a ⊼_{𝑔} b \in Fmla (N)) \to N \neq \emptyset$
3		nnsuc	$⊢ (N \in ω \land N \neq \emptyset) \to \exists x \in ω N = suc x$
4		suceq	$⊢ d = \emptyset \to suc d = suc \emptyset$
5	4	fveq2d	$⊢ d = \emptyset \to Fmla (suc d) = Fmla (suc \emptyset)$
6	5	eleq2d	$⊢ d = \emptyset \to (a ⊼_{𝑔} b \in Fmla (suc d) \leftrightarrow a ⊼_{𝑔} b \in Fmla (suc \emptyset))$
7	5	eleq2d	$⊢ d = \emptyset \to (a \in Fmla (suc d) \leftrightarrow a \in Fmla (suc \emptyset))$
8	5	eleq2d	$⊢ d = \emptyset \to (b \in Fmla (suc d) \leftrightarrow b \in Fmla (suc \emptyset))$
9	7 8	anbi12d	$⊢ d = \emptyset \to ((a \in Fmla (suc d) \land b \in Fmla (suc d)) \leftrightarrow (a \in Fmla (suc \emptyset) \land b \in Fmla (suc \emptyset)))$
10	6 9	imbi12d	$⊢ d = \emptyset \to ((a ⊼_{𝑔} b \in Fmla (suc d) \to (a \in Fmla (suc d) \land b \in Fmla (suc d))) \leftrightarrow (a ⊼_{𝑔} b \in Fmla (suc \emptyset) \to (a \in Fmla (suc \emptyset) \land b \in Fmla (suc \emptyset))))$
11		suceq	$⊢ d = c \to suc d = suc c$
12	11	fveq2d	$⊢ d = c \to Fmla (suc d) = Fmla (suc c)$
13	12	eleq2d	$⊢ d = c \to (a ⊼_{𝑔} b \in Fmla (suc d) \leftrightarrow a ⊼_{𝑔} b \in Fmla (suc c))$
14	12	eleq2d	$⊢ d = c \to (a \in Fmla (suc d) \leftrightarrow a \in Fmla (suc c))$
15	12	eleq2d	$⊢ d = c \to (b \in Fmla (suc d) \leftrightarrow b \in Fmla (suc c))$
16	14 15	anbi12d	$⊢ d = c \to ((a \in Fmla (suc d) \land b \in Fmla (suc d)) \leftrightarrow (a \in Fmla (suc c) \land b \in Fmla (suc c)))$
17	13 16	imbi12d	$⊢ d = c \to ((a ⊼_{𝑔} b \in Fmla (suc d) \to (a \in Fmla (suc d) \land b \in Fmla (suc d))) \leftrightarrow (a ⊼_{𝑔} b \in Fmla (suc c) \to (a \in Fmla (suc c) \land b \in Fmla (suc c))))$
18		suceq	$⊢ d = suc c \to suc d = suc suc c$
19	18	fveq2d	$⊢ d = suc c \to Fmla (suc d) = Fmla (suc suc c)$
20	19	eleq2d	$⊢ d = suc c \to (a ⊼_{𝑔} b \in Fmla (suc d) \leftrightarrow a ⊼_{𝑔} b \in Fmla (suc suc c))$
21	19	eleq2d	$⊢ d = suc c \to (a \in Fmla (suc d) \leftrightarrow a \in Fmla (suc suc c))$
22	19	eleq2d	$⊢ d = suc c \to (b \in Fmla (suc d) \leftrightarrow b \in Fmla (suc suc c))$
23	21 22	anbi12d	$⊢ d = suc c \to ((a \in Fmla (suc d) \land b \in Fmla (suc d)) \leftrightarrow (a \in Fmla (suc suc c) \land b \in Fmla (suc suc c)))$
24	20 23	imbi12d	$⊢ d = suc c \to ((a ⊼_{𝑔} b \in Fmla (suc d) \to (a \in Fmla (suc d) \land b \in Fmla (suc d))) \leftrightarrow (a ⊼_{𝑔} b \in Fmla (suc suc c) \to (a \in Fmla (suc suc c) \land b \in Fmla (suc suc c))))$
25		suceq	$⊢ d = x \to suc d = suc x$
26	25	fveq2d	$⊢ d = x \to Fmla (suc d) = Fmla (suc x)$
27	26	eleq2d	$⊢ d = x \to (a ⊼_{𝑔} b \in Fmla (suc d) \leftrightarrow a ⊼_{𝑔} b \in Fmla (suc x))$
28	26	eleq2d	$⊢ d = x \to (a \in Fmla (suc d) \leftrightarrow a \in Fmla (suc x))$
29	26	eleq2d	$⊢ d = x \to (b \in Fmla (suc d) \leftrightarrow b \in Fmla (suc x))$
30	28 29	anbi12d	$⊢ d = x \to ((a \in Fmla (suc d) \land b \in Fmla (suc d)) \leftrightarrow (a \in Fmla (suc x) \land b \in Fmla (suc x)))$
31	27 30	imbi12d	$⊢ d = x \to ((a ⊼_{𝑔} b \in Fmla (suc d) \to (a \in Fmla (suc d) \land b \in Fmla (suc d))) \leftrightarrow (a ⊼_{𝑔} b \in Fmla (suc x) \to (a \in Fmla (suc x) \land b \in Fmla (suc x))))$
32		peano1	$⊢ \emptyset \in ω$
33		ovex	$⊢ a ⊼_{𝑔} b \in V$
34		isfmlasuc	$⊢ (\emptyset \in ω \land a ⊼_{𝑔} b \in V) \to (a ⊼_{𝑔} b \in Fmla (suc \emptyset) \leftrightarrow (a ⊼_{𝑔} b \in Fmla (\emptyset) \lor \exists u \in Fmla (\emptyset) (\exists v \in Fmla (\emptyset) a ⊼_{𝑔} b = u ⊼_{𝑔} v \lor \exists i \in ω a ⊼_{𝑔} b = [\forall_{𝑔} i u])))$
35	32 33 34	mp2an	$⊢ a ⊼_{𝑔} b \in Fmla (suc \emptyset) \leftrightarrow (a ⊼_{𝑔} b \in Fmla (\emptyset) \lor \exists u \in Fmla (\emptyset) (\exists v \in Fmla (\emptyset) a ⊼_{𝑔} b = u ⊼_{𝑔} v \lor \exists i \in ω a ⊼_{𝑔} b = [\forall_{𝑔} i u]))$
36		eqeq1	$⊢ x = a ⊼_{𝑔} b \to (x = i \in_{𝑔} j \leftrightarrow a ⊼_{𝑔} b = i \in_{𝑔} j)$
37	36	2rexbidv	$⊢ x = a ⊼_{𝑔} b \to (\exists i \in ω \exists j \in ω x = i \in_{𝑔} j \leftrightarrow \exists i \in ω \exists j \in ω a ⊼_{𝑔} b = i \in_{𝑔} j)$
38		fmla0	$⊢ Fmla (\emptyset) = \{x \in V \| \exists i \in ω \exists j \in ω x = i \in_{𝑔} j\}$
39	37 38	elrab2	$⊢ a ⊼_{𝑔} b \in Fmla (\emptyset) \leftrightarrow (a ⊼_{𝑔} b \in V \land \exists i \in ω \exists j \in ω a ⊼_{𝑔} b = i \in_{𝑔} j)$
40		gonafv	$⊢ (a \in V \land b \in V) \to a ⊼_{𝑔} b = ⟨1_{𝑜}, ⟨a, b⟩⟩$
41	40	el2v	$⊢ a ⊼_{𝑔} b = ⟨1_{𝑜}, ⟨a, b⟩⟩$
42	41	a1i	$⊢ (i \in ω \land j \in ω) \to a ⊼_{𝑔} b = ⟨1_{𝑜}, ⟨a, b⟩⟩$
43		goel	$⊢ (i \in ω \land j \in ω) \to i \in_{𝑔} j = ⟨\emptyset, ⟨i, j⟩⟩$
44	42 43	eqeq12d	$⊢ (i \in ω \land j \in ω) \to (a ⊼_{𝑔} b = i \in_{𝑔} j \leftrightarrow ⟨1_{𝑜}, ⟨a, b⟩⟩ = ⟨\emptyset, ⟨i, j⟩⟩)$
45		1oex	$⊢ 1_{𝑜} \in V$
46		opex	$⊢ ⟨a, b⟩ \in V$
47	45 46	opth	$⊢ ⟨1_{𝑜}, ⟨a, b⟩⟩ = ⟨\emptyset, ⟨i, j⟩⟩ \leftrightarrow (1_{𝑜} = \emptyset \land ⟨a, b⟩ = ⟨i, j⟩)$
48		1n0	$⊢ 1_{𝑜} \neq \emptyset$
49		eqneqall	$⊢ 1_{𝑜} = \emptyset \to (1_{𝑜} \neq \emptyset \to (a \in Fmla (suc \emptyset) \land b \in Fmla (suc \emptyset)))$
50	48 49	mpi	$⊢ 1_{𝑜} = \emptyset \to (a \in Fmla (suc \emptyset) \land b \in Fmla (suc \emptyset))$
51	50	adantr	$⊢ (1_{𝑜} = \emptyset \land ⟨a, b⟩ = ⟨i, j⟩) \to (a \in Fmla (suc \emptyset) \land b \in Fmla (suc \emptyset))$
52	47 51	sylbi	$⊢ ⟨1_{𝑜}, ⟨a, b⟩⟩ = ⟨\emptyset, ⟨i, j⟩⟩ \to (a \in Fmla (suc \emptyset) \land b \in Fmla (suc \emptyset))$
53	44 52	biimtrdi	$⊢ (i \in ω \land j \in ω) \to (a ⊼_{𝑔} b = i \in_{𝑔} j \to (a \in Fmla (suc \emptyset) \land b \in Fmla (suc \emptyset)))$
54	53	rexlimdva	$⊢ i \in ω \to (\exists j \in ω a ⊼_{𝑔} b = i \in_{𝑔} j \to (a \in Fmla (suc \emptyset) \land b \in Fmla (suc \emptyset)))$
55	54	rexlimiv	$⊢ \exists i \in ω \exists j \in ω a ⊼_{𝑔} b = i \in_{𝑔} j \to (a \in Fmla (suc \emptyset) \land b \in Fmla (suc \emptyset))$
56	55	adantl	$⊢ (a ⊼_{𝑔} b \in V \land \exists i \in ω \exists j \in ω a ⊼_{𝑔} b = i \in_{𝑔} j) \to (a \in Fmla (suc \emptyset) \land b \in Fmla (suc \emptyset))$
57	39 56	sylbi	$⊢ a ⊼_{𝑔} b \in Fmla (\emptyset) \to (a \in Fmla (suc \emptyset) \land b \in Fmla (suc \emptyset))$
58	41	a1i	$⊢ (u \in Fmla (\emptyset) \land v \in Fmla (\emptyset)) \to a ⊼_{𝑔} b = ⟨1_{𝑜}, ⟨a, b⟩⟩$
59		gonafv	$⊢ (u \in Fmla (\emptyset) \land v \in Fmla (\emptyset)) \to u ⊼_{𝑔} v = ⟨1_{𝑜}, ⟨u, v⟩⟩$
60	58 59	eqeq12d	$⊢ (u \in Fmla (\emptyset) \land v \in Fmla (\emptyset)) \to (a ⊼_{𝑔} b = u ⊼_{𝑔} v \leftrightarrow ⟨1_{𝑜}, ⟨a, b⟩⟩ = ⟨1_{𝑜}, ⟨u, v⟩⟩)$
61	45 46	opth	$⊢ ⟨1_{𝑜}, ⟨a, b⟩⟩ = ⟨1_{𝑜}, ⟨u, v⟩⟩ \leftrightarrow (1_{𝑜} = 1_{𝑜} \land ⟨a, b⟩ = ⟨u, v⟩)$
62		vex	$⊢ a \in V$
63		vex	$⊢ b \in V$
64	62 63	opth	$⊢ ⟨a, b⟩ = ⟨u, v⟩ \leftrightarrow (a = u \land b = v)$
65		simpl	$⊢ (a = u \land b = v) \to a = u$
66	65	equcomd	$⊢ (a = u \land b = v) \to u = a$
67	66	eleq1d	$⊢ (a = u \land b = v) \to (u \in Fmla (\emptyset) \leftrightarrow a \in Fmla (\emptyset))$
68		simpr	$⊢ (a = u \land b = v) \to b = v$
69	68	equcomd	$⊢ (a = u \land b = v) \to v = b$
70	69	eleq1d	$⊢ (a = u \land b = v) \to (v \in Fmla (\emptyset) \leftrightarrow b \in Fmla (\emptyset))$
71	67 70	anbi12d	$⊢ (a = u \land b = v) \to ((u \in Fmla (\emptyset) \land v \in Fmla (\emptyset)) \leftrightarrow (a \in Fmla (\emptyset) \land b \in Fmla (\emptyset)))$
72	64 71	sylbi	$⊢ ⟨a, b⟩ = ⟨u, v⟩ \to ((u \in Fmla (\emptyset) \land v \in Fmla (\emptyset)) \leftrightarrow (a \in Fmla (\emptyset) \land b \in Fmla (\emptyset)))$
73	72	adantl	$⊢ (1_{𝑜} = 1_{𝑜} \land ⟨a, b⟩ = ⟨u, v⟩) \to ((u \in Fmla (\emptyset) \land v \in Fmla (\emptyset)) \leftrightarrow (a \in Fmla (\emptyset) \land b \in Fmla (\emptyset)))$
74	61 73	sylbi	$⊢ ⟨1_{𝑜}, ⟨a, b⟩⟩ = ⟨1_{𝑜}, ⟨u, v⟩⟩ \to ((u \in Fmla (\emptyset) \land v \in Fmla (\emptyset)) \leftrightarrow (a \in Fmla (\emptyset) \land b \in Fmla (\emptyset)))$
75		fmlasssuc	$⊢ \emptyset \in ω \to Fmla (\emptyset) \subseteq Fmla (suc \emptyset)$
76	32 75	ax-mp	$⊢ Fmla (\emptyset) \subseteq Fmla (suc \emptyset)$
77	76	sseli	$⊢ a \in Fmla (\emptyset) \to a \in Fmla (suc \emptyset)$
78	76	sseli	$⊢ b \in Fmla (\emptyset) \to b \in Fmla (suc \emptyset)$
79	77 78	anim12i	$⊢ (a \in Fmla (\emptyset) \land b \in Fmla (\emptyset)) \to (a \in Fmla (suc \emptyset) \land b \in Fmla (suc \emptyset))$
80	74 79	biimtrdi	$⊢ ⟨1_{𝑜}, ⟨a, b⟩⟩ = ⟨1_{𝑜}, ⟨u, v⟩⟩ \to ((u \in Fmla (\emptyset) \land v \in Fmla (\emptyset)) \to (a \in Fmla (suc \emptyset) \land b \in Fmla (suc \emptyset)))$
81	80	com12	$⊢ (u \in Fmla (\emptyset) \land v \in Fmla (\emptyset)) \to (⟨1_{𝑜}, ⟨a, b⟩⟩ = ⟨1_{𝑜}, ⟨u, v⟩⟩ \to (a \in Fmla (suc \emptyset) \land b \in Fmla (suc \emptyset)))$
82	60 81	sylbid	$⊢ (u \in Fmla (\emptyset) \land v \in Fmla (\emptyset)) \to (a ⊼_{𝑔} b = u ⊼_{𝑔} v \to (a \in Fmla (suc \emptyset) \land b \in Fmla (suc \emptyset)))$
83	82	rexlimdva	$⊢ u \in Fmla (\emptyset) \to (\exists v \in Fmla (\emptyset) a ⊼_{𝑔} b = u ⊼_{𝑔} v \to (a \in Fmla (suc \emptyset) \land b \in Fmla (suc \emptyset)))$
84		gonanegoal	$⊢ a ⊼_{𝑔} b \neq [\forall_{𝑔} i u]$
85		eqneqall	$⊢ a ⊼_{𝑔} b = [\forall_{𝑔} i u] \to (a ⊼_{𝑔} b \neq [\forall_{𝑔} i u] \to (a \in Fmla (suc \emptyset) \land b \in Fmla (suc \emptyset)))$
86	84 85	mpi	$⊢ a ⊼_{𝑔} b = [\forall_{𝑔} i u] \to (a \in Fmla (suc \emptyset) \land b \in Fmla (suc \emptyset))$
87	86	a1i	$⊢ (u \in Fmla (\emptyset) \land i \in ω) \to (a ⊼_{𝑔} b = [\forall_{𝑔} i u] \to (a \in Fmla (suc \emptyset) \land b \in Fmla (suc \emptyset)))$
88	87	rexlimdva	$⊢ u \in Fmla (\emptyset) \to (\exists i \in ω a ⊼_{𝑔} b = [\forall_{𝑔} i u] \to (a \in Fmla (suc \emptyset) \land b \in Fmla (suc \emptyset)))$
89	83 88	jaod	$⊢ u \in Fmla (\emptyset) \to ((\exists v \in Fmla (\emptyset) a ⊼_{𝑔} b = u ⊼_{𝑔} v \lor \exists i \in ω a ⊼_{𝑔} b = [\forall_{𝑔} i u]) \to (a \in Fmla (suc \emptyset) \land b \in Fmla (suc \emptyset)))$
90	89	rexlimiv	$⊢ \exists u \in Fmla (\emptyset) (\exists v \in Fmla (\emptyset) a ⊼_{𝑔} b = u ⊼_{𝑔} v \lor \exists i \in ω a ⊼_{𝑔} b = [\forall_{𝑔} i u]) \to (a \in Fmla (suc \emptyset) \land b \in Fmla (suc \emptyset))$
91	57 90	jaoi	$⊢ (a ⊼_{𝑔} b \in Fmla (\emptyset) \lor \exists u \in Fmla (\emptyset) (\exists v \in Fmla (\emptyset) a ⊼_{𝑔} b = u ⊼_{𝑔} v \lor \exists i \in ω a ⊼_{𝑔} b = [\forall_{𝑔} i u])) \to (a \in Fmla (suc \emptyset) \land b \in Fmla (suc \emptyset))$
92	35 91	sylbi	$⊢ a ⊼_{𝑔} b \in Fmla (suc \emptyset) \to (a \in Fmla (suc \emptyset) \land b \in Fmla (suc \emptyset))$
93		gonarlem	$⊢ c \in ω \to ((a ⊼_{𝑔} b \in Fmla (suc c) \to (a \in Fmla (suc c) \land b \in Fmla (suc c))) \to (a ⊼_{𝑔} b \in Fmla (suc suc c) \to (a \in Fmla (suc suc c) \land b \in Fmla (suc suc c))))$
94	10 17 24 31 92 93	finds	$⊢ x \in ω \to (a ⊼_{𝑔} b \in Fmla (suc x) \to (a \in Fmla (suc x) \land b \in Fmla (suc x)))$
95	94	adantr	$⊢ (x \in ω \land N = suc x) \to (a ⊼_{𝑔} b \in Fmla (suc x) \to (a \in Fmla (suc x) \land b \in Fmla (suc x)))$
96		fveq2	$⊢ N = suc x \to Fmla (N) = Fmla (suc x)$
97	96	eleq2d	$⊢ N = suc x \to (a ⊼_{𝑔} b \in Fmla (N) \leftrightarrow a ⊼_{𝑔} b \in Fmla (suc x))$
98	96	eleq2d	$⊢ N = suc x \to (a \in Fmla (N) \leftrightarrow a \in Fmla (suc x))$
99	96	eleq2d	$⊢ N = suc x \to (b \in Fmla (N) \leftrightarrow b \in Fmla (suc x))$
100	98 99	anbi12d	$⊢ N = suc x \to ((a \in Fmla (N) \land b \in Fmla (N)) \leftrightarrow (a \in Fmla (suc x) \land b \in Fmla (suc x)))$
101	97 100	imbi12d	$⊢ N = suc x \to ((a ⊼_{𝑔} b \in Fmla (N) \to (a \in Fmla (N) \land b \in Fmla (N))) \leftrightarrow (a ⊼_{𝑔} b \in Fmla (suc x) \to (a \in Fmla (suc x) \land b \in Fmla (suc x))))$
102	101	adantl	$⊢ (x \in ω \land N = suc x) \to ((a ⊼_{𝑔} b \in Fmla (N) \to (a \in Fmla (N) \land b \in Fmla (N))) \leftrightarrow (a ⊼_{𝑔} b \in Fmla (suc x) \to (a \in Fmla (suc x) \land b \in Fmla (suc x))))$
103	95 102	mpbird	$⊢ (x \in ω \land N = suc x) \to (a ⊼_{𝑔} b \in Fmla (N) \to (a \in Fmla (N) \land b \in Fmla (N)))$
104	103	rexlimiva	$⊢ \exists x \in ω N = suc x \to (a ⊼_{𝑔} b \in Fmla (N) \to (a \in Fmla (N) \land b \in Fmla (N)))$
105	3 104	syl	$⊢ (N \in ω \land N \neq \emptyset) \to (a ⊼_{𝑔} b \in Fmla (N) \to (a \in Fmla (N) \land b \in Fmla (N)))$
106	105	impancom	$⊢ (N \in ω \land a ⊼_{𝑔} b \in Fmla (N)) \to (N \neq \emptyset \to (a \in Fmla (N) \land b \in Fmla (N)))$
107	2 106	mpd	$⊢ (N \in ω \land a ⊼_{𝑔} b \in Fmla (N)) \to (a \in Fmla (N) \land b \in Fmla (N))$

Metamath Proof Explorer

Theorem gonar

Proof