goalr

Description: If the "Godel-set of universal quantification" applied to a class is a Godel formula, the class is also a Godel formula. Remark: The reverse is not valid for A being of the same height as the "Godel-set of universal quantification". (Contributed by AV, 22-Oct-2023)

		Ref	Expression
	Assertion	goalr	$⊢ (N \in ω \land [\forall_{𝑔} i a] \in Fmla (N)) \to a \in Fmla (N)$

Proof

Step	Hyp	Ref	Expression
1		goaln0	$⊢ [\forall_{𝑔} i a] \in Fmla (N) \to N \neq \emptyset$
2	1	adantl	$⊢ (N \in ω \land [\forall_{𝑔} i a] \in Fmla (N)) \to N \neq \emptyset$
3		nnsuc	$⊢ (N \in ω \land N \neq \emptyset) \to \exists n \in ω N = suc n$
4		suceq	$⊢ x = \emptyset \to suc x = suc \emptyset$
5	4	fveq2d	$⊢ x = \emptyset \to Fmla (suc x) = Fmla (suc \emptyset)$
6	5	eleq2d	$⊢ x = \emptyset \to ([\forall_{𝑔} i a] \in Fmla (suc x) \leftrightarrow [\forall_{𝑔} i a] \in Fmla (suc \emptyset))$
7	5	eleq2d	$⊢ x = \emptyset \to (a \in Fmla (suc x) \leftrightarrow a \in Fmla (suc \emptyset))$
8	6 7	imbi12d	$⊢ x = \emptyset \to (([\forall_{𝑔} i a] \in Fmla (suc x) \to a \in Fmla (suc x)) \leftrightarrow ([\forall_{𝑔} i a] \in Fmla (suc \emptyset) \to a \in Fmla (suc \emptyset)))$
9		suceq	$⊢ x = y \to suc x = suc y$
10	9	fveq2d	$⊢ x = y \to Fmla (suc x) = Fmla (suc y)$
11	10	eleq2d	$⊢ x = y \to ([\forall_{𝑔} i a] \in Fmla (suc x) \leftrightarrow [\forall_{𝑔} i a] \in Fmla (suc y))$
12	10	eleq2d	$⊢ x = y \to (a \in Fmla (suc x) \leftrightarrow a \in Fmla (suc y))$
13	11 12	imbi12d	$⊢ x = y \to (([\forall_{𝑔} i a] \in Fmla (suc x) \to a \in Fmla (suc x)) \leftrightarrow ([\forall_{𝑔} i a] \in Fmla (suc y) \to a \in Fmla (suc y)))$
14		suceq	$⊢ x = suc y \to suc x = suc suc y$
15	14	fveq2d	$⊢ x = suc y \to Fmla (suc x) = Fmla (suc suc y)$
16	15	eleq2d	$⊢ x = suc y \to ([\forall_{𝑔} i a] \in Fmla (suc x) \leftrightarrow [\forall_{𝑔} i a] \in Fmla (suc suc y))$
17	15	eleq2d	$⊢ x = suc y \to (a \in Fmla (suc x) \leftrightarrow a \in Fmla (suc suc y))$
18	16 17	imbi12d	$⊢ x = suc y \to (([\forall_{𝑔} i a] \in Fmla (suc x) \to a \in Fmla (suc x)) \leftrightarrow ([\forall_{𝑔} i a] \in Fmla (suc suc y) \to a \in Fmla (suc suc y)))$
19		suceq	$⊢ x = n \to suc x = suc n$
20	19	fveq2d	$⊢ x = n \to Fmla (suc x) = Fmla (suc n)$
21	20	eleq2d	$⊢ x = n \to ([\forall_{𝑔} i a] \in Fmla (suc x) \leftrightarrow [\forall_{𝑔} i a] \in Fmla (suc n))$
22	20	eleq2d	$⊢ x = n \to (a \in Fmla (suc x) \leftrightarrow a \in Fmla (suc n))$
23	21 22	imbi12d	$⊢ x = n \to (([\forall_{𝑔} i a] \in Fmla (suc x) \to a \in Fmla (suc x)) \leftrightarrow ([\forall_{𝑔} i a] \in Fmla (suc n) \to a \in Fmla (suc n)))$
24		peano1	$⊢ \emptyset \in ω$
25		df-goal	$⊢ [\forall_{𝑔} i a] = ⟨2_{𝑜}, ⟨i, a⟩⟩$
26		opex	$⊢ ⟨2_{𝑜}, ⟨i, a⟩⟩ \in V$
27	25 26	eqeltri	$⊢ [\forall_{𝑔} i a] \in V$
28		isfmlasuc	$⊢ (\emptyset \in ω \land [\forall_{𝑔} i a] \in V) \to ([\forall_{𝑔} i a] \in Fmla (suc \emptyset) \leftrightarrow ([\forall_{𝑔} i a] \in Fmla (\emptyset) \lor \exists u \in Fmla (\emptyset) (\exists v \in Fmla (\emptyset) [\forall_{𝑔} i a] = u ⊼_{𝑔} v \lor \exists k \in ω [\forall_{𝑔} i a] = [\forall_{𝑔} k u])))$
29	24 27 28	mp2an	$⊢ [\forall_{𝑔} i a] \in Fmla (suc \emptyset) \leftrightarrow ([\forall_{𝑔} i a] \in Fmla (\emptyset) \lor \exists u \in Fmla (\emptyset) (\exists v \in Fmla (\emptyset) [\forall_{𝑔} i a] = u ⊼_{𝑔} v \lor \exists k \in ω [\forall_{𝑔} i a] = [\forall_{𝑔} k u]))$
30		eqeq1	$⊢ x = [\forall_{𝑔} i a] \to (x = k \in_{𝑔} j \leftrightarrow [\forall_{𝑔} i a] = k \in_{𝑔} j)$
31	30	2rexbidv	$⊢ x = [\forall_{𝑔} i a] \to (\exists k \in ω \exists j \in ω x = k \in_{𝑔} j \leftrightarrow \exists k \in ω \exists j \in ω [\forall_{𝑔} i a] = k \in_{𝑔} j)$
32		fmla0	$⊢ Fmla (\emptyset) = \{x \in V \| \exists k \in ω \exists j \in ω x = k \in_{𝑔} j\}$
33	31 32	elrab2	$⊢ [\forall_{𝑔} i a] \in Fmla (\emptyset) \leftrightarrow ([\forall_{𝑔} i a] \in V \land \exists k \in ω \exists j \in ω [\forall_{𝑔} i a] = k \in_{𝑔} j)$
34	25	a1i	$⊢ (k \in ω \land j \in ω) \to [\forall_{𝑔} i a] = ⟨2_{𝑜}, ⟨i, a⟩⟩$
35		goel	$⊢ (k \in ω \land j \in ω) \to k \in_{𝑔} j = ⟨\emptyset, ⟨k, j⟩⟩$
36	34 35	eqeq12d	$⊢ (k \in ω \land j \in ω) \to ([\forall_{𝑔} i a] = k \in_{𝑔} j \leftrightarrow ⟨2_{𝑜}, ⟨i, a⟩⟩ = ⟨\emptyset, ⟨k, j⟩⟩)$
37		2oex	$⊢ 2_{𝑜} \in V$
38		opex	$⊢ ⟨i, a⟩ \in V$
39	37 38	opth	$⊢ ⟨2_{𝑜}, ⟨i, a⟩⟩ = ⟨\emptyset, ⟨k, j⟩⟩ \leftrightarrow (2_{𝑜} = \emptyset \land ⟨i, a⟩ = ⟨k, j⟩)$
40		2on0	$⊢ 2_{𝑜} \neq \emptyset$
41		eqneqall	$⊢ 2_{𝑜} = \emptyset \to (2_{𝑜} \neq \emptyset \to a \in Fmla (suc \emptyset))$
42	40 41	mpi	$⊢ 2_{𝑜} = \emptyset \to a \in Fmla (suc \emptyset)$
43	42	adantr	$⊢ (2_{𝑜} = \emptyset \land ⟨i, a⟩ = ⟨k, j⟩) \to a \in Fmla (suc \emptyset)$
44	39 43	sylbi	$⊢ ⟨2_{𝑜}, ⟨i, a⟩⟩ = ⟨\emptyset, ⟨k, j⟩⟩ \to a \in Fmla (suc \emptyset)$
45	36 44	biimtrdi	$⊢ (k \in ω \land j \in ω) \to ([\forall_{𝑔} i a] = k \in_{𝑔} j \to a \in Fmla (suc \emptyset))$
46	45	rexlimdva	$⊢ k \in ω \to (\exists j \in ω [\forall_{𝑔} i a] = k \in_{𝑔} j \to a \in Fmla (suc \emptyset))$
47	46	rexlimiv	$⊢ \exists k \in ω \exists j \in ω [\forall_{𝑔} i a] = k \in_{𝑔} j \to a \in Fmla (suc \emptyset)$
48	33 47	simplbiim	$⊢ [\forall_{𝑔} i a] \in Fmla (\emptyset) \to a \in Fmla (suc \emptyset)$
49		gonanegoal	$⊢ u ⊼_{𝑔} v \neq [\forall_{𝑔} i a]$
50		eqneqall	$⊢ u ⊼_{𝑔} v = [\forall_{𝑔} i a] \to (u ⊼_{𝑔} v \neq [\forall_{𝑔} i a] \to a \in Fmla (suc \emptyset))$
51	49 50	mpi	$⊢ u ⊼_{𝑔} v = [\forall_{𝑔} i a] \to a \in Fmla (suc \emptyset)$
52	51	eqcoms	$⊢ [\forall_{𝑔} i a] = u ⊼_{𝑔} v \to a \in Fmla (suc \emptyset)$
53	52	a1i	$⊢ (u \in Fmla (\emptyset) \land v \in Fmla (\emptyset)) \to ([\forall_{𝑔} i a] = u ⊼_{𝑔} v \to a \in Fmla (suc \emptyset))$
54	53	rexlimdva	$⊢ u \in Fmla (\emptyset) \to (\exists v \in Fmla (\emptyset) [\forall_{𝑔} i a] = u ⊼_{𝑔} v \to a \in Fmla (suc \emptyset))$
55		df-goal	$⊢ [\forall_{𝑔} k u] = ⟨2_{𝑜}, ⟨k, u⟩⟩$
56	25 55	eqeq12i	$⊢ [\forall_{𝑔} i a] = [\forall_{𝑔} k u] \leftrightarrow ⟨2_{𝑜}, ⟨i, a⟩⟩ = ⟨2_{𝑜}, ⟨k, u⟩⟩$
57	37 38	opth	$⊢ ⟨2_{𝑜}, ⟨i, a⟩⟩ = ⟨2_{𝑜}, ⟨k, u⟩⟩ \leftrightarrow (2_{𝑜} = 2_{𝑜} \land ⟨i, a⟩ = ⟨k, u⟩)$
58		vex	$⊢ i \in V$
59		vex	$⊢ a \in V$
60	58 59	opth	$⊢ ⟨i, a⟩ = ⟨k, u⟩ \leftrightarrow (i = k \land a = u)$
61		eleq1w	$⊢ u = a \to (u \in Fmla (\emptyset) \leftrightarrow a \in Fmla (\emptyset))$
62		fmlasssuc	$⊢ \emptyset \in ω \to Fmla (\emptyset) \subseteq Fmla (suc \emptyset)$
63	24 62	ax-mp	$⊢ Fmla (\emptyset) \subseteq Fmla (suc \emptyset)$
64	63	sseli	$⊢ a \in Fmla (\emptyset) \to a \in Fmla (suc \emptyset)$
65	61 64	biimtrdi	$⊢ u = a \to (u \in Fmla (\emptyset) \to a \in Fmla (suc \emptyset))$
66	65	eqcoms	$⊢ a = u \to (u \in Fmla (\emptyset) \to a \in Fmla (suc \emptyset))$
67	60 66	simplbiim	$⊢ ⟨i, a⟩ = ⟨k, u⟩ \to (u \in Fmla (\emptyset) \to a \in Fmla (suc \emptyset))$
68	57 67	simplbiim	$⊢ ⟨2_{𝑜}, ⟨i, a⟩⟩ = ⟨2_{𝑜}, ⟨k, u⟩⟩ \to (u \in Fmla (\emptyset) \to a \in Fmla (suc \emptyset))$
69	68	com12	$⊢ u \in Fmla (\emptyset) \to (⟨2_{𝑜}, ⟨i, a⟩⟩ = ⟨2_{𝑜}, ⟨k, u⟩⟩ \to a \in Fmla (suc \emptyset))$
70	69	adantr	$⊢ (u \in Fmla (\emptyset) \land k \in ω) \to (⟨2_{𝑜}, ⟨i, a⟩⟩ = ⟨2_{𝑜}, ⟨k, u⟩⟩ \to a \in Fmla (suc \emptyset))$
71	56 70	biimtrid	$⊢ (u \in Fmla (\emptyset) \land k \in ω) \to ([\forall_{𝑔} i a] = [\forall_{𝑔} k u] \to a \in Fmla (suc \emptyset))$
72	71	rexlimdva	$⊢ u \in Fmla (\emptyset) \to (\exists k \in ω [\forall_{𝑔} i a] = [\forall_{𝑔} k u] \to a \in Fmla (suc \emptyset))$
73	54 72	jaod	$⊢ u \in Fmla (\emptyset) \to ((\exists v \in Fmla (\emptyset) [\forall_{𝑔} i a] = u ⊼_{𝑔} v \lor \exists k \in ω [\forall_{𝑔} i a] = [\forall_{𝑔} k u]) \to a \in Fmla (suc \emptyset))$
74	73	rexlimiv	$⊢ \exists u \in Fmla (\emptyset) (\exists v \in Fmla (\emptyset) [\forall_{𝑔} i a] = u ⊼_{𝑔} v \lor \exists k \in ω [\forall_{𝑔} i a] = [\forall_{𝑔} k u]) \to a \in Fmla (suc \emptyset)$
75	48 74	jaoi	$⊢ ([\forall_{𝑔} i a] \in Fmla (\emptyset) \lor \exists u \in Fmla (\emptyset) (\exists v \in Fmla (\emptyset) [\forall_{𝑔} i a] = u ⊼_{𝑔} v \lor \exists k \in ω [\forall_{𝑔} i a] = [\forall_{𝑔} k u])) \to a \in Fmla (suc \emptyset)$
76	29 75	sylbi	$⊢ [\forall_{𝑔} i a] \in Fmla (suc \emptyset) \to a \in Fmla (suc \emptyset)$
77		goalrlem	$⊢ y \in ω \to (([\forall_{𝑔} i a] \in Fmla (suc y) \to a \in Fmla (suc y)) \to ([\forall_{𝑔} i a] \in Fmla (suc suc y) \to a \in Fmla (suc suc y)))$
78	8 13 18 23 76 77	finds	$⊢ n \in ω \to ([\forall_{𝑔} i a] \in Fmla (suc n) \to a \in Fmla (suc n))$
79	78	adantr	$⊢ (n \in ω \land N = suc n) \to ([\forall_{𝑔} i a] \in Fmla (suc n) \to a \in Fmla (suc n))$
80		fveq2	$⊢ N = suc n \to Fmla (N) = Fmla (suc n)$
81	80	eleq2d	$⊢ N = suc n \to ([\forall_{𝑔} i a] \in Fmla (N) \leftrightarrow [\forall_{𝑔} i a] \in Fmla (suc n))$
82	80	eleq2d	$⊢ N = suc n \to (a \in Fmla (N) \leftrightarrow a \in Fmla (suc n))$
83	81 82	imbi12d	$⊢ N = suc n \to (([\forall_{𝑔} i a] \in Fmla (N) \to a \in Fmla (N)) \leftrightarrow ([\forall_{𝑔} i a] \in Fmla (suc n) \to a \in Fmla (suc n)))$
84	83	adantl	$⊢ (n \in ω \land N = suc n) \to (([\forall_{𝑔} i a] \in Fmla (N) \to a \in Fmla (N)) \leftrightarrow ([\forall_{𝑔} i a] \in Fmla (suc n) \to a \in Fmla (suc n)))$
85	79 84	mpbird	$⊢ (n \in ω \land N = suc n) \to ([\forall_{𝑔} i a] \in Fmla (N) \to a \in Fmla (N))$
86	85	rexlimiva	$⊢ \exists n \in ω N = suc n \to ([\forall_{𝑔} i a] \in Fmla (N) \to a \in Fmla (N))$
87	3 86	syl	$⊢ (N \in ω \land N \neq \emptyset) \to ([\forall_{𝑔} i a] \in Fmla (N) \to a \in Fmla (N))$
88	87	impancom	$⊢ (N \in ω \land [\forall_{𝑔} i a] \in Fmla (N)) \to (N \neq \emptyset \to a \in Fmla (N))$
89	2 88	mpd	$⊢ (N \in ω \land [\forall_{𝑔} i a] \in Fmla (N)) \to a \in Fmla (N)$

Metamath Proof Explorer

Theorem goalr

Proof