fmlasuc0

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

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

Proof

Step	Hyp	Ref	Expression
1		df-fmla	$⊢ Fmla = (n \in suc ω ⟼ dom (\emptyset Sat \emptyset) (n))$
2		fveq2	$⊢ n = suc N \to (\emptyset Sat \emptyset) (n) = (\emptyset Sat \emptyset) (suc N)$
3	2	dmeqd	$⊢ n = suc N \to dom (\emptyset Sat \emptyset) (n) = dom (\emptyset Sat \emptyset) (suc N)$
4		omsucelsucb	$⊢ N \in ω \leftrightarrow suc N \in suc ω$
5	4	biimpi	$⊢ N \in ω \to suc N \in suc ω$
6		fvex	$⊢ (\emptyset Sat \emptyset) (suc N) \in V$
7	6	dmex	$⊢ dom (\emptyset Sat \emptyset) (suc N) \in V$
8	7	a1i	$⊢ N \in ω \to dom (\emptyset Sat \emptyset) (suc N) \in V$
9	1 3 5 8	fvmptd3	$⊢ N \in ω \to Fmla (suc N) = dom (\emptyset Sat \emptyset) (suc N)$
10		satf0sucom	$⊢ suc N \in suc ω \to (\emptyset Sat \emptyset) (suc N) = rec ((f \in V ⟼ f \cup \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}), \{⟨x, y⟩ \| (y = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)\}) (suc N)$
11	5 10	syl	$⊢ N \in ω \to (\emptyset Sat \emptyset) (suc N) = rec ((f \in V ⟼ f \cup \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}), \{⟨x, y⟩ \| (y = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)\}) (suc N)$
12		nnon	$⊢ N \in ω \to N \in On$
13		rdgsuc	$⊢ N \in On \to rec ((f \in V ⟼ f \cup \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}), \{⟨x, y⟩ \| (y = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)\}) (suc N) = (f \in V ⟼ f \cup \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}) (rec ((f \in V ⟼ f \cup \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}), \{⟨x, y⟩ \| (y = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)\}) (N))$
14	12 13	syl	$⊢ N \in ω \to rec ((f \in V ⟼ f \cup \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}), \{⟨x, y⟩ \| (y = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)\}) (suc N) = (f \in V ⟼ f \cup \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}) (rec ((f \in V ⟼ f \cup \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}), \{⟨x, y⟩ \| (y = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)\}) (N))$
15	11 14	eqtrd	$⊢ N \in ω \to (\emptyset Sat \emptyset) (suc N) = (f \in V ⟼ f \cup \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}) (rec ((f \in V ⟼ f \cup \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}), \{⟨x, y⟩ \| (y = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)\}) (N))$
16	15	dmeqd	$⊢ N \in ω \to dom (\emptyset Sat \emptyset) (suc N) = dom (f \in V ⟼ f \cup \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}) (rec ((f \in V ⟼ f \cup \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}), \{⟨x, y⟩ \| (y = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)\}) (N))$
17		elelsuc	$⊢ N \in ω \to N \in suc ω$
18		satf0sucom	$⊢ N \in suc ω \to (\emptyset Sat \emptyset) (N) = rec ((f \in V ⟼ f \cup \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}), \{⟨x, y⟩ \| (y = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)\}) (N)$
19	18	eqcomd	$⊢ N \in suc ω \to rec ((f \in V ⟼ f \cup \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}), \{⟨x, y⟩ \| (y = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)\}) (N) = (\emptyset Sat \emptyset) (N)$
20	17 19	syl	$⊢ N \in ω \to rec ((f \in V ⟼ f \cup \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}), \{⟨x, y⟩ \| (y = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)\}) (N) = (\emptyset Sat \emptyset) (N)$
21	20	fveq2d	$⊢ N \in ω \to (f \in V ⟼ f \cup \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}) (rec ((f \in V ⟼ f \cup \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}), \{⟨x, y⟩ \| (y = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)\}) (N)) = (f \in V ⟼ f \cup \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}) ((\emptyset Sat \emptyset) (N))$
22		eqidd	$⊢ N \in ω \to (f \in V ⟼ f \cup \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}) = (f \in V ⟼ f \cup \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\})$
23		id	$⊢ f = (\emptyset Sat \emptyset) (N) \to f = (\emptyset Sat \emptyset) (N)$
24		rexeq	$⊢ f = (\emptyset Sat \emptyset) (N) \to (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \leftrightarrow \exists v \in (\emptyset Sat \emptyset) (N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v))$
25	24	orbi1d	$⊢ f = (\emptyset Sat \emptyset) (N) \to ((\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]) \leftrightarrow (\exists v \in (\emptyset Sat \emptyset) (N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))$
26	25	rexeqbi1dv	$⊢ f = (\emptyset Sat \emptyset) (N) \to (\exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]) \leftrightarrow \exists u \in (\emptyset Sat \emptyset) (N) (\exists v \in (\emptyset Sat \emptyset) (N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))$
27	26	anbi2d	$⊢ f = (\emptyset Sat \emptyset) (N) \to ((y = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)])) \leftrightarrow (y = \emptyset \land \exists u \in (\emptyset Sat \emptyset) (N) (\exists v \in (\emptyset Sat \emptyset) (N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)])))$
28	27	opabbidv	$⊢ f = (\emptyset Sat \emptyset) (N) \to \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\} = \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in (\emptyset Sat \emptyset) (N) (\exists v \in (\emptyset Sat \emptyset) (N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}$
29	23 28	uneq12d	$⊢ f = (\emptyset Sat \emptyset) (N) \to f \cup \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\} = (\emptyset Sat \emptyset) (N) \cup \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in (\emptyset Sat \emptyset) (N) (\exists v \in (\emptyset Sat \emptyset) (N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}$
30	29	adantl	$⊢ (N \in ω \land f = (\emptyset Sat \emptyset) (N)) \to f \cup \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\} = (\emptyset Sat \emptyset) (N) \cup \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in (\emptyset Sat \emptyset) (N) (\exists v \in (\emptyset Sat \emptyset) (N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}$
31		fvex	$⊢ (\emptyset Sat \emptyset) (N) \in V$
32	31	a1i	$⊢ N \in ω \to (\emptyset Sat \emptyset) (N) \in V$
33		peano1	$⊢ \emptyset \in ω$
34		eleq1	$⊢ y = \emptyset \to (y \in ω \leftrightarrow \emptyset \in ω)$
35	33 34	mpbiri	$⊢ y = \emptyset \to y \in ω$
36	35	adantr	$⊢ (y = \emptyset \land \exists u \in (\emptyset Sat \emptyset) (N) (\exists v \in (\emptyset Sat \emptyset) (N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)])) \to y \in ω$
37	36	pm4.71ri	$⊢ (y = \emptyset \land \exists u \in (\emptyset Sat \emptyset) (N) (\exists v \in (\emptyset Sat \emptyset) (N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)])) \leftrightarrow (y \in ω \land (y = \emptyset \land \exists u \in (\emptyset Sat \emptyset) (N) (\exists v \in (\emptyset Sat \emptyset) (N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)])))$
38	37	opabbii	$⊢ \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in (\emptyset Sat \emptyset) (N) (\exists v \in (\emptyset Sat \emptyset) (N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\} = \{⟨x, y⟩ \| (y \in ω \land (y = \emptyset \land \exists u \in (\emptyset Sat \emptyset) (N) (\exists v \in (\emptyset Sat \emptyset) (N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)])))\}$
39		omex	$⊢ ω \in V$
40		id	$⊢ ω \in V \to ω \in V$
41		unab	$⊢ \{x \| \exists v \in (\emptyset Sat \emptyset) (N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v)\} \cup \{x \| \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]\} = \{x \| (\exists v \in (\emptyset Sat \emptyset) (N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)])\}$
42	31	abrexex	$⊢ \{x \| \exists v \in (\emptyset Sat \emptyset) (N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v)\} \in V$
43	39	abrexex	$⊢ \{x \| \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]\} \in V$
44	42 43	unex	$⊢ \{x \| \exists v \in (\emptyset Sat \emptyset) (N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v)\} \cup \{x \| \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]\} \in V$
45	41 44	eqeltrri	$⊢ \{x \| (\exists v \in (\emptyset Sat \emptyset) (N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)])\} \in V$
46	45	a1i	$⊢ ((ω \in V \land y \in ω) \land u \in (\emptyset Sat \emptyset) (N)) \to \{x \| (\exists v \in (\emptyset Sat \emptyset) (N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)])\} \in V$
47	46	ralrimiva	$⊢ (ω \in V \land y \in ω) \to \forall u \in (\emptyset Sat \emptyset) (N) \{x \| (\exists v \in (\emptyset Sat \emptyset) (N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)])\} \in V$
48		abrexex2g	$⊢ ((\emptyset Sat \emptyset) (N) \in V \land \forall u \in (\emptyset Sat \emptyset) (N) \{x \| (\exists v \in (\emptyset Sat \emptyset) (N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)])\} \in V) \to \{x \| \exists u \in (\emptyset Sat \emptyset) (N) (\exists v \in (\emptyset Sat \emptyset) (N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)])\} \in V$
49	31 47 48	sylancr	$⊢ (ω \in V \land y \in ω) \to \{x \| \exists u \in (\emptyset Sat \emptyset) (N) (\exists v \in (\emptyset Sat \emptyset) (N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)])\} \in V$
50	40 49	opabex3rd	$⊢ ω \in V \to \{⟨x, y⟩ \| (y \in ω \land \exists u \in (\emptyset Sat \emptyset) (N) (\exists v \in (\emptyset Sat \emptyset) (N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\} \in V$
51	39 50	ax-mp	$⊢ \{⟨x, y⟩ \| (y \in ω \land \exists u \in (\emptyset Sat \emptyset) (N) (\exists v \in (\emptyset Sat \emptyset) (N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\} \in V$
52		simpr	$⊢ (y = \emptyset \land \exists u \in (\emptyset Sat \emptyset) (N) (\exists v \in (\emptyset Sat \emptyset) (N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)])) \to \exists u \in (\emptyset Sat \emptyset) (N) (\exists v \in (\emptyset Sat \emptyset) (N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)])$
53	52	anim2i	$⊢ (y \in ω \land (y = \emptyset \land \exists u \in (\emptyset Sat \emptyset) (N) (\exists v \in (\emptyset Sat \emptyset) (N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))) \to (y \in ω \land \exists u \in (\emptyset Sat \emptyset) (N) (\exists v \in (\emptyset Sat \emptyset) (N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))$
54	53	ssopab2i	$⊢ \{⟨x, y⟩ \| (y \in ω \land (y = \emptyset \land \exists u \in (\emptyset Sat \emptyset) (N) (\exists v \in (\emptyset Sat \emptyset) (N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)])))\} \subseteq \{⟨x, y⟩ \| (y \in ω \land \exists u \in (\emptyset Sat \emptyset) (N) (\exists v \in (\emptyset Sat \emptyset) (N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}$
55	51 54	ssexi	$⊢ \{⟨x, y⟩ \| (y \in ω \land (y = \emptyset \land \exists u \in (\emptyset Sat \emptyset) (N) (\exists v \in (\emptyset Sat \emptyset) (N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)])))\} \in V$
56	55	a1i	$⊢ N \in ω \to \{⟨x, y⟩ \| (y \in ω \land (y = \emptyset \land \exists u \in (\emptyset Sat \emptyset) (N) (\exists v \in (\emptyset Sat \emptyset) (N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)])))\} \in V$
57	38 56	eqeltrid	$⊢ N \in ω \to \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in (\emptyset Sat \emptyset) (N) (\exists v \in (\emptyset Sat \emptyset) (N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\} \in V$
58		unexg	$⊢ ((\emptyset Sat \emptyset) (N) \in V \land \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in (\emptyset Sat \emptyset) (N) (\exists v \in (\emptyset Sat \emptyset) (N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\} \in V) \to (\emptyset Sat \emptyset) (N) \cup \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in (\emptyset Sat \emptyset) (N) (\exists v \in (\emptyset Sat \emptyset) (N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\} \in V$
59	31 57 58	sylancr	$⊢ N \in ω \to (\emptyset Sat \emptyset) (N) \cup \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in (\emptyset Sat \emptyset) (N) (\exists v \in (\emptyset Sat \emptyset) (N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\} \in V$
60	22 30 32 59	fvmptd	$⊢ N \in ω \to (f \in V ⟼ f \cup \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}) ((\emptyset Sat \emptyset) (N)) = (\emptyset Sat \emptyset) (N) \cup \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in (\emptyset Sat \emptyset) (N) (\exists v \in (\emptyset Sat \emptyset) (N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}$
61	21 60	eqtrd	$⊢ N \in ω \to (f \in V ⟼ f \cup \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}) (rec ((f \in V ⟼ f \cup \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}), \{⟨x, y⟩ \| (y = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)\}) (N)) = (\emptyset Sat \emptyset) (N) \cup \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in (\emptyset Sat \emptyset) (N) (\exists v \in (\emptyset Sat \emptyset) (N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}$
62	61	dmeqd	$⊢ N \in ω \to dom (f \in V ⟼ f \cup \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}) (rec ((f \in V ⟼ f \cup \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}), \{⟨x, y⟩ \| (y = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)\}) (N)) = dom ((\emptyset Sat \emptyset) (N) \cup \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in (\emptyset Sat \emptyset) (N) (\exists v \in (\emptyset Sat \emptyset) (N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\})$
63		dmun	$⊢ dom ((\emptyset Sat \emptyset) (N) \cup \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in (\emptyset Sat \emptyset) (N) (\exists v \in (\emptyset Sat \emptyset) (N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}) = dom (\emptyset Sat \emptyset) (N) \cup dom \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in (\emptyset Sat \emptyset) (N) (\exists v \in (\emptyset Sat \emptyset) (N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}$
64	62 63	eqtrdi	$⊢ N \in ω \to dom (f \in V ⟼ f \cup \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}) (rec ((f \in V ⟼ f \cup \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}), \{⟨x, y⟩ \| (y = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)\}) (N)) = dom (\emptyset Sat \emptyset) (N) \cup dom \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in (\emptyset Sat \emptyset) (N) (\exists v \in (\emptyset Sat \emptyset) (N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}$
65		fmlafv	$⊢ N \in suc ω \to Fmla (N) = dom (\emptyset Sat \emptyset) (N)$
66	17 65	syl	$⊢ N \in ω \to Fmla (N) = dom (\emptyset Sat \emptyset) (N)$
67	66	eqcomd	$⊢ N \in ω \to dom (\emptyset Sat \emptyset) (N) = Fmla (N)$
68		dmopab	$⊢ dom \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in (\emptyset Sat \emptyset) (N) (\exists v \in (\emptyset Sat \emptyset) (N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\} = \{x \| \exists y (y = \emptyset \land \exists u \in (\emptyset Sat \emptyset) (N) (\exists v \in (\emptyset Sat \emptyset) (N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}$
69	68	a1i	$⊢ N \in ω \to dom \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in (\emptyset Sat \emptyset) (N) (\exists v \in (\emptyset Sat \emptyset) (N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\} = \{x \| \exists y (y = \emptyset \land \exists u \in (\emptyset Sat \emptyset) (N) (\exists v \in (\emptyset Sat \emptyset) (N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}$
70		0ex	$⊢ \emptyset \in V$
71	70	isseti	$⊢ \exists y y = \emptyset$
72		19.41v	$⊢ \exists y (y = \emptyset \land \exists u \in (\emptyset Sat \emptyset) (N) (\exists v \in (\emptyset Sat \emptyset) (N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)])) \leftrightarrow (\exists y y = \emptyset \land \exists u \in (\emptyset Sat \emptyset) (N) (\exists v \in (\emptyset Sat \emptyset) (N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))$
73	71 72	mpbiran	$⊢ \exists y (y = \emptyset \land \exists u \in (\emptyset Sat \emptyset) (N) (\exists v \in (\emptyset Sat \emptyset) (N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)])) \leftrightarrow \exists u \in (\emptyset Sat \emptyset) (N) (\exists v \in (\emptyset Sat \emptyset) (N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)])$
74	73	abbii	$⊢ \{x \| \exists y (y = \emptyset \land \exists u \in (\emptyset Sat \emptyset) (N) (\exists v \in (\emptyset Sat \emptyset) (N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\} = \{x \| \exists u \in (\emptyset Sat \emptyset) (N) (\exists v \in (\emptyset Sat \emptyset) (N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)])\}$
75	69 74	eqtrdi	$⊢ N \in ω \to dom \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in (\emptyset Sat \emptyset) (N) (\exists v \in (\emptyset Sat \emptyset) (N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\} = \{x \| \exists u \in (\emptyset Sat \emptyset) (N) (\exists v \in (\emptyset Sat \emptyset) (N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)])\}$
76	67 75	uneq12d	$⊢ N \in ω \to dom (\emptyset Sat \emptyset) (N) \cup dom \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in (\emptyset Sat \emptyset) (N) (\exists v \in (\emptyset Sat \emptyset) (N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\} = Fmla (N) \cup \{x \| \exists u \in (\emptyset Sat \emptyset) (N) (\exists v \in (\emptyset Sat \emptyset) (N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)])\}$
77	64 76	eqtrd	$⊢ N \in ω \to dom (f \in V ⟼ f \cup \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}) (rec ((f \in V ⟼ f \cup \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}), \{⟨x, y⟩ \| (y = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)\}) (N)) = Fmla (N) \cup \{x \| \exists u \in (\emptyset Sat \emptyset) (N) (\exists v \in (\emptyset Sat \emptyset) (N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)])\}$
78	9 16 77	3eqtrd	$⊢ N \in ω \to Fmla (suc N) = Fmla (N) \cup \{x \| \exists u \in (\emptyset Sat \emptyset) (N) (\exists v \in (\emptyset Sat \emptyset) (N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)])\}$

Metamath Proof Explorer

Theorem fmlasuc0

Proof