fmlasuc

Description: The valid Godel formulas of height ( N + 1 ) , expressed by the valid Godel formulas of height N . (Contributed by AV, 20-Sep-2023)

		Ref	Expression
	Assertion	fmlasuc	$⊢ N \in ω \to Fmla (suc N) = Fmla (N) \cup \{x \| \exists u \in Fmla (N) (\exists v \in Fmla (N) x = u ⊼_{𝑔} v \lor \exists i \in ω x = [\forall_{𝑔} i u])\}$

Proof

Step	Hyp	Ref	Expression
1		fmlasuc0	$⊢ N \in ω \to Fmla (suc N) = Fmla (N) \cup \{x \| \exists y \in (\emptyset Sat \emptyset) (N) (\exists z \in (\emptyset Sat \emptyset) (N) x = 1^{st} (y) ⊼_{𝑔} 1^{st} (z) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (y)])\}$
2		eqid	$⊢ \emptyset Sat \emptyset = \emptyset Sat \emptyset$
3	2	satf0op	$⊢ N \in ω \to (y \in (\emptyset Sat \emptyset) (N) \leftrightarrow \exists z (y = ⟨z, \emptyset⟩ \land ⟨z, \emptyset⟩ \in (\emptyset Sat \emptyset) (N)))$
4		fveq2	$⊢ z = w \to 1^{st} (z) = 1^{st} (w)$
5	4	oveq2d	$⊢ z = w \to 1^{st} (y) ⊼_{𝑔} 1^{st} (z) = 1^{st} (y) ⊼_{𝑔} 1^{st} (w)$
6	5	eqeq2d	$⊢ z = w \to (x = 1^{st} (y) ⊼_{𝑔} 1^{st} (z) \leftrightarrow x = 1^{st} (y) ⊼_{𝑔} 1^{st} (w))$
7	6	cbvrexvw	$⊢ \exists z \in (\emptyset Sat \emptyset) (N) x = 1^{st} (y) ⊼_{𝑔} 1^{st} (z) \leftrightarrow \exists w \in (\emptyset Sat \emptyset) (N) x = 1^{st} (y) ⊼_{𝑔} 1^{st} (w)$
8	7	orbi1i	$⊢ (\exists z \in (\emptyset Sat \emptyset) (N) x = 1^{st} (y) ⊼_{𝑔} 1^{st} (z) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (y)]) \leftrightarrow (\exists w \in (\emptyset Sat \emptyset) (N) x = 1^{st} (y) ⊼_{𝑔} 1^{st} (w) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (y)])$
9		fmlafvel	$⊢ N \in ω \to (z \in Fmla (N) \leftrightarrow ⟨z, \emptyset⟩ \in (\emptyset Sat \emptyset) (N))$
10	9	biimprd	$⊢ N \in ω \to (⟨z, \emptyset⟩ \in (\emptyset Sat \emptyset) (N) \to z \in Fmla (N))$
11	10	adantld	$⊢ N \in ω \to ((y = ⟨z, \emptyset⟩ \land ⟨z, \emptyset⟩ \in (\emptyset Sat \emptyset) (N)) \to z \in Fmla (N))$
12	11	imp	$⊢ (N \in ω \land (y = ⟨z, \emptyset⟩ \land ⟨z, \emptyset⟩ \in (\emptyset Sat \emptyset) (N))) \to z \in Fmla (N)$
13		vex	$⊢ z \in V$
14		0ex	$⊢ \emptyset \in V$
15	13 14	op1std	$⊢ y = ⟨z, \emptyset⟩ \to 1^{st} (y) = z$
16	15	eleq1d	$⊢ y = ⟨z, \emptyset⟩ \to (1^{st} (y) \in Fmla (N) \leftrightarrow z \in Fmla (N))$
17	16	ad2antrl	$⊢ (N \in ω \land (y = ⟨z, \emptyset⟩ \land ⟨z, \emptyset⟩ \in (\emptyset Sat \emptyset) (N))) \to (1^{st} (y) \in Fmla (N) \leftrightarrow z \in Fmla (N))$
18	12 17	mpbird	$⊢ (N \in ω \land (y = ⟨z, \emptyset⟩ \land ⟨z, \emptyset⟩ \in (\emptyset Sat \emptyset) (N))) \to 1^{st} (y) \in Fmla (N)$
19	18	3adant3	$⊢ (N \in ω \land (y = ⟨z, \emptyset⟩ \land ⟨z, \emptyset⟩ \in (\emptyset Sat \emptyset) (N)) \land (\exists w \in (\emptyset Sat \emptyset) (N) x = 1^{st} (y) ⊼_{𝑔} 1^{st} (w) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (y)])) \to 1^{st} (y) \in Fmla (N)$
20		oveq1	$⊢ u = 1^{st} (y) \to u ⊼_{𝑔} v = 1^{st} (y) ⊼_{𝑔} v$
21	20	eqeq2d	$⊢ u = 1^{st} (y) \to (x = u ⊼_{𝑔} v \leftrightarrow x = 1^{st} (y) ⊼_{𝑔} v)$
22	21	rexbidv	$⊢ u = 1^{st} (y) \to (\exists v \in Fmla (N) x = u ⊼_{𝑔} v \leftrightarrow \exists v \in Fmla (N) x = 1^{st} (y) ⊼_{𝑔} v)$
23		eqidd	$⊢ u = 1^{st} (y) \to i = i$
24		id	$⊢ u = 1^{st} (y) \to u = 1^{st} (y)$
25	23 24	goaleq12d	$⊢ u = 1^{st} (y) \to [\forall_{𝑔} i u] = [\forall_{𝑔} i 1^{st} (y)]$
26	25	eqeq2d	$⊢ u = 1^{st} (y) \to (x = [\forall_{𝑔} i u] \leftrightarrow x = [\forall_{𝑔} i 1^{st} (y)])$
27	26	rexbidv	$⊢ u = 1^{st} (y) \to (\exists i \in ω x = [\forall_{𝑔} i u] \leftrightarrow \exists i \in ω x = [\forall_{𝑔} i 1^{st} (y)])$
28	22 27	orbi12d	$⊢ u = 1^{st} (y) \to ((\exists v \in Fmla (N) x = u ⊼_{𝑔} v \lor \exists i \in ω x = [\forall_{𝑔} i u]) \leftrightarrow (\exists v \in Fmla (N) x = 1^{st} (y) ⊼_{𝑔} v \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (y)]))$
29	28	adantl	$⊢ ((N \in ω \land (y = ⟨z, \emptyset⟩ \land ⟨z, \emptyset⟩ \in (\emptyset Sat \emptyset) (N)) \land (\exists w \in (\emptyset Sat \emptyset) (N) x = 1^{st} (y) ⊼_{𝑔} 1^{st} (w) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (y)])) \land u = 1^{st} (y)) \to ((\exists v \in Fmla (N) x = u ⊼_{𝑔} v \lor \exists i \in ω x = [\forall_{𝑔} i u]) \leftrightarrow (\exists v \in Fmla (N) x = 1^{st} (y) ⊼_{𝑔} v \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (y)]))$
30	2	satf0op	$⊢ N \in ω \to (w \in (\emptyset Sat \emptyset) (N) \leftrightarrow \exists y (w = ⟨y, \emptyset⟩ \land ⟨y, \emptyset⟩ \in (\emptyset Sat \emptyset) (N)))$
31		fmlafvel	$⊢ N \in ω \to (y \in Fmla (N) \leftrightarrow ⟨y, \emptyset⟩ \in (\emptyset Sat \emptyset) (N))$
32	31	biimprd	$⊢ N \in ω \to (⟨y, \emptyset⟩ \in (\emptyset Sat \emptyset) (N) \to y \in Fmla (N))$
33	32	adantld	$⊢ N \in ω \to ((w = ⟨y, \emptyset⟩ \land ⟨y, \emptyset⟩ \in (\emptyset Sat \emptyset) (N)) \to y \in Fmla (N))$
34	33	imp	$⊢ (N \in ω \land (w = ⟨y, \emptyset⟩ \land ⟨y, \emptyset⟩ \in (\emptyset Sat \emptyset) (N))) \to y \in Fmla (N)$
35		vex	$⊢ y \in V$
36	35 14	op1std	$⊢ w = ⟨y, \emptyset⟩ \to 1^{st} (w) = y$
37	36	eleq1d	$⊢ w = ⟨y, \emptyset⟩ \to (1^{st} (w) \in Fmla (N) \leftrightarrow y \in Fmla (N))$
38	37	ad2antrl	$⊢ (N \in ω \land (w = ⟨y, \emptyset⟩ \land ⟨y, \emptyset⟩ \in (\emptyset Sat \emptyset) (N))) \to (1^{st} (w) \in Fmla (N) \leftrightarrow y \in Fmla (N))$
39	34 38	mpbird	$⊢ (N \in ω \land (w = ⟨y, \emptyset⟩ \land ⟨y, \emptyset⟩ \in (\emptyset Sat \emptyset) (N))) \to 1^{st} (w) \in Fmla (N)$
40	39	adantr	$⊢ ((N \in ω \land (w = ⟨y, \emptyset⟩ \land ⟨y, \emptyset⟩ \in (\emptyset Sat \emptyset) (N))) \land x = z ⊼_{𝑔} 1^{st} (w)) \to 1^{st} (w) \in Fmla (N)$
41		oveq2	$⊢ v = 1^{st} (w) \to z ⊼_{𝑔} v = z ⊼_{𝑔} 1^{st} (w)$
42	41	eqeq2d	$⊢ v = 1^{st} (w) \to (x = z ⊼_{𝑔} v \leftrightarrow x = z ⊼_{𝑔} 1^{st} (w))$
43	42	adantl	$⊢ (((N \in ω \land (w = ⟨y, \emptyset⟩ \land ⟨y, \emptyset⟩ \in (\emptyset Sat \emptyset) (N))) \land x = z ⊼_{𝑔} 1^{st} (w)) \land v = 1^{st} (w)) \to (x = z ⊼_{𝑔} v \leftrightarrow x = z ⊼_{𝑔} 1^{st} (w))$
44		simpr	$⊢ ((N \in ω \land (w = ⟨y, \emptyset⟩ \land ⟨y, \emptyset⟩ \in (\emptyset Sat \emptyset) (N))) \land x = z ⊼_{𝑔} 1^{st} (w)) \to x = z ⊼_{𝑔} 1^{st} (w)$
45	40 43 44	rspcedvd	$⊢ ((N \in ω \land (w = ⟨y, \emptyset⟩ \land ⟨y, \emptyset⟩ \in (\emptyset Sat \emptyset) (N))) \land x = z ⊼_{𝑔} 1^{st} (w)) \to \exists v \in Fmla (N) x = z ⊼_{𝑔} v$
46	45	exp31	$⊢ N \in ω \to ((w = ⟨y, \emptyset⟩ \land ⟨y, \emptyset⟩ \in (\emptyset Sat \emptyset) (N)) \to (x = z ⊼_{𝑔} 1^{st} (w) \to \exists v \in Fmla (N) x = z ⊼_{𝑔} v))$
47	46	exlimdv	$⊢ N \in ω \to (\exists y (w = ⟨y, \emptyset⟩ \land ⟨y, \emptyset⟩ \in (\emptyset Sat \emptyset) (N)) \to (x = z ⊼_{𝑔} 1^{st} (w) \to \exists v \in Fmla (N) x = z ⊼_{𝑔} v))$
48	30 47	sylbid	$⊢ N \in ω \to (w \in (\emptyset Sat \emptyset) (N) \to (x = z ⊼_{𝑔} 1^{st} (w) \to \exists v \in Fmla (N) x = z ⊼_{𝑔} v))$
49	48	rexlimdv	$⊢ N \in ω \to (\exists w \in (\emptyset Sat \emptyset) (N) x = z ⊼_{𝑔} 1^{st} (w) \to \exists v \in Fmla (N) x = z ⊼_{𝑔} v)$
50	49	adantr	$⊢ (N \in ω \land (y = ⟨z, \emptyset⟩ \land ⟨z, \emptyset⟩ \in (\emptyset Sat \emptyset) (N))) \to (\exists w \in (\emptyset Sat \emptyset) (N) x = z ⊼_{𝑔} 1^{st} (w) \to \exists v \in Fmla (N) x = z ⊼_{𝑔} v)$
51	15	oveq1d	$⊢ y = ⟨z, \emptyset⟩ \to 1^{st} (y) ⊼_{𝑔} 1^{st} (w) = z ⊼_{𝑔} 1^{st} (w)$
52	51	eqeq2d	$⊢ y = ⟨z, \emptyset⟩ \to (x = 1^{st} (y) ⊼_{𝑔} 1^{st} (w) \leftrightarrow x = z ⊼_{𝑔} 1^{st} (w))$
53	52	rexbidv	$⊢ y = ⟨z, \emptyset⟩ \to (\exists w \in (\emptyset Sat \emptyset) (N) x = 1^{st} (y) ⊼_{𝑔} 1^{st} (w) \leftrightarrow \exists w \in (\emptyset Sat \emptyset) (N) x = z ⊼_{𝑔} 1^{st} (w))$
54	15	oveq1d	$⊢ y = ⟨z, \emptyset⟩ \to 1^{st} (y) ⊼_{𝑔} v = z ⊼_{𝑔} v$
55	54	eqeq2d	$⊢ y = ⟨z, \emptyset⟩ \to (x = 1^{st} (y) ⊼_{𝑔} v \leftrightarrow x = z ⊼_{𝑔} v)$
56	55	rexbidv	$⊢ y = ⟨z, \emptyset⟩ \to (\exists v \in Fmla (N) x = 1^{st} (y) ⊼_{𝑔} v \leftrightarrow \exists v \in Fmla (N) x = z ⊼_{𝑔} v)$
57	53 56	imbi12d	$⊢ y = ⟨z, \emptyset⟩ \to ((\exists w \in (\emptyset Sat \emptyset) (N) x = 1^{st} (y) ⊼_{𝑔} 1^{st} (w) \to \exists v \in Fmla (N) x = 1^{st} (y) ⊼_{𝑔} v) \leftrightarrow (\exists w \in (\emptyset Sat \emptyset) (N) x = z ⊼_{𝑔} 1^{st} (w) \to \exists v \in Fmla (N) x = z ⊼_{𝑔} v))$
58	57	ad2antrl	$⊢ (N \in ω \land (y = ⟨z, \emptyset⟩ \land ⟨z, \emptyset⟩ \in (\emptyset Sat \emptyset) (N))) \to ((\exists w \in (\emptyset Sat \emptyset) (N) x = 1^{st} (y) ⊼_{𝑔} 1^{st} (w) \to \exists v \in Fmla (N) x = 1^{st} (y) ⊼_{𝑔} v) \leftrightarrow (\exists w \in (\emptyset Sat \emptyset) (N) x = z ⊼_{𝑔} 1^{st} (w) \to \exists v \in Fmla (N) x = z ⊼_{𝑔} v))$
59	50 58	mpbird	$⊢ (N \in ω \land (y = ⟨z, \emptyset⟩ \land ⟨z, \emptyset⟩ \in (\emptyset Sat \emptyset) (N))) \to (\exists w \in (\emptyset Sat \emptyset) (N) x = 1^{st} (y) ⊼_{𝑔} 1^{st} (w) \to \exists v \in Fmla (N) x = 1^{st} (y) ⊼_{𝑔} v)$
60	59	orim1d	$⊢ (N \in ω \land (y = ⟨z, \emptyset⟩ \land ⟨z, \emptyset⟩ \in (\emptyset Sat \emptyset) (N))) \to ((\exists w \in (\emptyset Sat \emptyset) (N) x = 1^{st} (y) ⊼_{𝑔} 1^{st} (w) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (y)]) \to (\exists v \in Fmla (N) x = 1^{st} (y) ⊼_{𝑔} v \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (y)]))$
61	60	3impia	$⊢ (N \in ω \land (y = ⟨z, \emptyset⟩ \land ⟨z, \emptyset⟩ \in (\emptyset Sat \emptyset) (N)) \land (\exists w \in (\emptyset Sat \emptyset) (N) x = 1^{st} (y) ⊼_{𝑔} 1^{st} (w) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (y)])) \to (\exists v \in Fmla (N) x = 1^{st} (y) ⊼_{𝑔} v \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (y)])$
62	19 29 61	rspcedvd	$⊢ (N \in ω \land (y = ⟨z, \emptyset⟩ \land ⟨z, \emptyset⟩ \in (\emptyset Sat \emptyset) (N)) \land (\exists w \in (\emptyset Sat \emptyset) (N) x = 1^{st} (y) ⊼_{𝑔} 1^{st} (w) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (y)])) \to \exists u \in Fmla (N) (\exists v \in Fmla (N) x = u ⊼_{𝑔} v \lor \exists i \in ω x = [\forall_{𝑔} i u])$
63	62	3exp	$⊢ N \in ω \to ((y = ⟨z, \emptyset⟩ \land ⟨z, \emptyset⟩ \in (\emptyset Sat \emptyset) (N)) \to ((\exists w \in (\emptyset Sat \emptyset) (N) x = 1^{st} (y) ⊼_{𝑔} 1^{st} (w) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (y)]) \to \exists u \in Fmla (N) (\exists v \in Fmla (N) x = u ⊼_{𝑔} v \lor \exists i \in ω x = [\forall_{𝑔} i u])))$
64	63	exlimdv	$⊢ N \in ω \to (\exists z (y = ⟨z, \emptyset⟩ \land ⟨z, \emptyset⟩ \in (\emptyset Sat \emptyset) (N)) \to ((\exists w \in (\emptyset Sat \emptyset) (N) x = 1^{st} (y) ⊼_{𝑔} 1^{st} (w) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (y)]) \to \exists u \in Fmla (N) (\exists v \in Fmla (N) x = u ⊼_{𝑔} v \lor \exists i \in ω x = [\forall_{𝑔} i u])))$
65	8 64	syl7bi	$⊢ N \in ω \to (\exists z (y = ⟨z, \emptyset⟩ \land ⟨z, \emptyset⟩ \in (\emptyset Sat \emptyset) (N)) \to ((\exists z \in (\emptyset Sat \emptyset) (N) x = 1^{st} (y) ⊼_{𝑔} 1^{st} (z) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (y)]) \to \exists u \in Fmla (N) (\exists v \in Fmla (N) x = u ⊼_{𝑔} v \lor \exists i \in ω x = [\forall_{𝑔} i u])))$
66	3 65	sylbid	$⊢ N \in ω \to (y \in (\emptyset Sat \emptyset) (N) \to ((\exists z \in (\emptyset Sat \emptyset) (N) x = 1^{st} (y) ⊼_{𝑔} 1^{st} (z) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (y)]) \to \exists u \in Fmla (N) (\exists v \in Fmla (N) x = u ⊼_{𝑔} v \lor \exists i \in ω x = [\forall_{𝑔} i u])))$
67	66	rexlimdv	$⊢ N \in ω \to (\exists y \in (\emptyset Sat \emptyset) (N) (\exists z \in (\emptyset Sat \emptyset) (N) x = 1^{st} (y) ⊼_{𝑔} 1^{st} (z) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (y)]) \to \exists u \in Fmla (N) (\exists v \in Fmla (N) x = u ⊼_{𝑔} v \lor \exists i \in ω x = [\forall_{𝑔} i u]))$
68		fmlafvel	$⊢ N \in ω \to (u \in Fmla (N) \leftrightarrow ⟨u, \emptyset⟩ \in (\emptyset Sat \emptyset) (N))$
69	68	biimpa	$⊢ (N \in ω \land u \in Fmla (N)) \to ⟨u, \emptyset⟩ \in (\emptyset Sat \emptyset) (N)$
70	69	adantr	$⊢ ((N \in ω \land u \in Fmla (N)) \land (\exists v \in Fmla (N) x = u ⊼_{𝑔} v \lor \exists i \in ω x = [\forall_{𝑔} i u])) \to ⟨u, \emptyset⟩ \in (\emptyset Sat \emptyset) (N)$
71		vex	$⊢ u \in V$
72	71 14	op1std	$⊢ y = ⟨u, \emptyset⟩ \to 1^{st} (y) = u$
73	72	oveq1d	$⊢ y = ⟨u, \emptyset⟩ \to 1^{st} (y) ⊼_{𝑔} 1^{st} (z) = u ⊼_{𝑔} 1^{st} (z)$
74	73	eqeq2d	$⊢ y = ⟨u, \emptyset⟩ \to (x = 1^{st} (y) ⊼_{𝑔} 1^{st} (z) \leftrightarrow x = u ⊼_{𝑔} 1^{st} (z))$
75	74	rexbidv	$⊢ y = ⟨u, \emptyset⟩ \to (\exists z \in (\emptyset Sat \emptyset) (N) x = 1^{st} (y) ⊼_{𝑔} 1^{st} (z) \leftrightarrow \exists z \in (\emptyset Sat \emptyset) (N) x = u ⊼_{𝑔} 1^{st} (z))$
76		eqidd	$⊢ y = ⟨u, \emptyset⟩ \to i = i$
77	76 72	goaleq12d	$⊢ y = ⟨u, \emptyset⟩ \to [\forall_{𝑔} i 1^{st} (y)] = [\forall_{𝑔} i u]$
78	77	eqeq2d	$⊢ y = ⟨u, \emptyset⟩ \to (x = [\forall_{𝑔} i 1^{st} (y)] \leftrightarrow x = [\forall_{𝑔} i u])$
79	78	rexbidv	$⊢ y = ⟨u, \emptyset⟩ \to (\exists i \in ω x = [\forall_{𝑔} i 1^{st} (y)] \leftrightarrow \exists i \in ω x = [\forall_{𝑔} i u])$
80	75 79	orbi12d	$⊢ y = ⟨u, \emptyset⟩ \to ((\exists z \in (\emptyset Sat \emptyset) (N) x = 1^{st} (y) ⊼_{𝑔} 1^{st} (z) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (y)]) \leftrightarrow (\exists z \in (\emptyset Sat \emptyset) (N) x = u ⊼_{𝑔} 1^{st} (z) \lor \exists i \in ω x = [\forall_{𝑔} i u]))$
81	80	adantl	$⊢ (((N \in ω \land u \in Fmla (N)) \land (\exists v \in Fmla (N) x = u ⊼_{𝑔} v \lor \exists i \in ω x = [\forall_{𝑔} i u])) \land y = ⟨u, \emptyset⟩) \to ((\exists z \in (\emptyset Sat \emptyset) (N) x = 1^{st} (y) ⊼_{𝑔} 1^{st} (z) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (y)]) \leftrightarrow (\exists z \in (\emptyset Sat \emptyset) (N) x = u ⊼_{𝑔} 1^{st} (z) \lor \exists i \in ω x = [\forall_{𝑔} i u]))$
82		fmlafvel	$⊢ N \in ω \to (v \in Fmla (N) \leftrightarrow ⟨v, \emptyset⟩ \in (\emptyset Sat \emptyset) (N))$
83	82	biimpd	$⊢ N \in ω \to (v \in Fmla (N) \to ⟨v, \emptyset⟩ \in (\emptyset Sat \emptyset) (N))$
84	83	adantr	$⊢ (N \in ω \land u \in Fmla (N)) \to (v \in Fmla (N) \to ⟨v, \emptyset⟩ \in (\emptyset Sat \emptyset) (N))$
85	84	imp	$⊢ ((N \in ω \land u \in Fmla (N)) \land v \in Fmla (N)) \to ⟨v, \emptyset⟩ \in (\emptyset Sat \emptyset) (N)$
86	85	adantr	$⊢ (((N \in ω \land u \in Fmla (N)) \land v \in Fmla (N)) \land x = u ⊼_{𝑔} v) \to ⟨v, \emptyset⟩ \in (\emptyset Sat \emptyset) (N)$
87		vex	$⊢ v \in V$
88	87 14	op1std	$⊢ z = ⟨v, \emptyset⟩ \to 1^{st} (z) = v$
89	88	oveq2d	$⊢ z = ⟨v, \emptyset⟩ \to u ⊼_{𝑔} 1^{st} (z) = u ⊼_{𝑔} v$
90	89	eqeq2d	$⊢ z = ⟨v, \emptyset⟩ \to (x = u ⊼_{𝑔} 1^{st} (z) \leftrightarrow x = u ⊼_{𝑔} v)$
91	90	adantl	$⊢ ((((N \in ω \land u \in Fmla (N)) \land v \in Fmla (N)) \land x = u ⊼_{𝑔} v) \land z = ⟨v, \emptyset⟩) \to (x = u ⊼_{𝑔} 1^{st} (z) \leftrightarrow x = u ⊼_{𝑔} v)$
92		simpr	$⊢ (((N \in ω \land u \in Fmla (N)) \land v \in Fmla (N)) \land x = u ⊼_{𝑔} v) \to x = u ⊼_{𝑔} v$
93	86 91 92	rspcedvd	$⊢ (((N \in ω \land u \in Fmla (N)) \land v \in Fmla (N)) \land x = u ⊼_{𝑔} v) \to \exists z \in (\emptyset Sat \emptyset) (N) x = u ⊼_{𝑔} 1^{st} (z)$
94	93	rexlimdva2	$⊢ (N \in ω \land u \in Fmla (N)) \to (\exists v \in Fmla (N) x = u ⊼_{𝑔} v \to \exists z \in (\emptyset Sat \emptyset) (N) x = u ⊼_{𝑔} 1^{st} (z))$
95	94	orim1d	$⊢ (N \in ω \land u \in Fmla (N)) \to ((\exists v \in Fmla (N) x = u ⊼_{𝑔} v \lor \exists i \in ω x = [\forall_{𝑔} i u]) \to (\exists z \in (\emptyset Sat \emptyset) (N) x = u ⊼_{𝑔} 1^{st} (z) \lor \exists i \in ω x = [\forall_{𝑔} i u]))$
96	95	imp	$⊢ ((N \in ω \land u \in Fmla (N)) \land (\exists v \in Fmla (N) x = u ⊼_{𝑔} v \lor \exists i \in ω x = [\forall_{𝑔} i u])) \to (\exists z \in (\emptyset Sat \emptyset) (N) x = u ⊼_{𝑔} 1^{st} (z) \lor \exists i \in ω x = [\forall_{𝑔} i u])$
97	70 81 96	rspcedvd	$⊢ ((N \in ω \land u \in Fmla (N)) \land (\exists v \in Fmla (N) x = u ⊼_{𝑔} v \lor \exists i \in ω x = [\forall_{𝑔} i u])) \to \exists y \in (\emptyset Sat \emptyset) (N) (\exists z \in (\emptyset Sat \emptyset) (N) x = 1^{st} (y) ⊼_{𝑔} 1^{st} (z) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (y)])$
98	97	rexlimdva2	$⊢ N \in ω \to (\exists u \in Fmla (N) (\exists v \in Fmla (N) x = u ⊼_{𝑔} v \lor \exists i \in ω x = [\forall_{𝑔} i u]) \to \exists y \in (\emptyset Sat \emptyset) (N) (\exists z \in (\emptyset Sat \emptyset) (N) x = 1^{st} (y) ⊼_{𝑔} 1^{st} (z) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (y)]))$
99	67 98	impbid	$⊢ N \in ω \to (\exists y \in (\emptyset Sat \emptyset) (N) (\exists z \in (\emptyset Sat \emptyset) (N) x = 1^{st} (y) ⊼_{𝑔} 1^{st} (z) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (y)]) \leftrightarrow \exists u \in Fmla (N) (\exists v \in Fmla (N) x = u ⊼_{𝑔} v \lor \exists i \in ω x = [\forall_{𝑔} i u]))$
100	99	abbidv	$⊢ N \in ω \to \{x \| \exists y \in (\emptyset Sat \emptyset) (N) (\exists z \in (\emptyset Sat \emptyset) (N) x = 1^{st} (y) ⊼_{𝑔} 1^{st} (z) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (y)])\} = \{x \| \exists u \in Fmla (N) (\exists v \in Fmla (N) x = u ⊼_{𝑔} v \lor \exists i \in ω x = [\forall_{𝑔} i u])\}$
101	100	uneq2d	$⊢ N \in ω \to Fmla (N) \cup \{x \| \exists y \in (\emptyset Sat \emptyset) (N) (\exists z \in (\emptyset Sat \emptyset) (N) x = 1^{st} (y) ⊼_{𝑔} 1^{st} (z) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (y)])\} = Fmla (N) \cup \{x \| \exists u \in Fmla (N) (\exists v \in Fmla (N) x = u ⊼_{𝑔} v \lor \exists i \in ω x = [\forall_{𝑔} i u])\}$
102	1 101	eqtrd	$⊢ N \in ω \to Fmla (suc N) = Fmla (N) \cup \{x \| \exists u \in Fmla (N) (\exists v \in Fmla (N) x = u ⊼_{𝑔} v \lor \exists i \in ω x = [\forall_{𝑔} i u])\}$

Metamath Proof Explorer

Theorem fmlasuc

Proof