fmla

Description: The set of all valid Godel formulas. (Contributed by AV, 20-Sep-2023)

		Ref	Expression
	Assertion	fmla	$⊢ Fmla (ω) = ⋃_{n \in ω} Fmla (n)$

Proof

Step	Hyp	Ref	Expression
1		df-fmla	$⊢ Fmla = (n \in suc ω ⟼ dom (\emptyset Sat \emptyset) (n))$
2	1	fveq1i	$⊢ Fmla (ω) = (n \in suc ω ⟼ dom (\emptyset Sat \emptyset) (n)) (ω)$
3		omex	$⊢ ω \in V$
4		eqidd	$⊢ ω \in V \to (n \in suc ω ⟼ dom (\emptyset Sat \emptyset) (n)) = (n \in suc ω ⟼ dom (\emptyset Sat \emptyset) (n))$
5		fveq2	$⊢ n = ω \to (\emptyset Sat \emptyset) (n) = (\emptyset Sat \emptyset) (ω)$
6	5	dmeqd	$⊢ n = ω \to dom (\emptyset Sat \emptyset) (n) = dom (\emptyset Sat \emptyset) (ω)$
7	6	adantl	$⊢ (ω \in V \land n = ω) \to dom (\emptyset Sat \emptyset) (n) = dom (\emptyset Sat \emptyset) (ω)$
8		sucidg	$⊢ ω \in V \to ω \in suc ω$
9		fvex	$⊢ (\emptyset Sat \emptyset) (ω) \in V$
10	9	dmex	$⊢ dom (\emptyset Sat \emptyset) (ω) \in V$
11	10	a1i	$⊢ ω \in V \to dom (\emptyset Sat \emptyset) (ω) \in V$
12	4 7 8 11	fvmptd	$⊢ ω \in V \to (n \in suc ω ⟼ dom (\emptyset Sat \emptyset) (n)) (ω) = dom (\emptyset Sat \emptyset) (ω)$
13	3 12	ax-mp	$⊢ (n \in suc ω ⟼ dom (\emptyset Sat \emptyset) (n)) (ω) = dom (\emptyset Sat \emptyset) (ω)$
14	3	sucid	$⊢ ω \in suc ω$
15		satf0sucom	$⊢ ω \in suc ω \to (\emptyset Sat \emptyset) (ω) = 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)\}) (ω)$
16	14 15	ax-mp	$⊢ (\emptyset Sat \emptyset) (ω) = 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)\}) (ω)$
17		limom	$⊢ Lim ω$
18		rdglim2a	$⊢ (ω \in V \land Lim ω) \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 \in ω} 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	3 17 18	mp2an	$⊢ 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 \in ω} 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)$
20	16 19	eqtri	$⊢ (\emptyset Sat \emptyset) (ω) = ⋃_{n \in ω} 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)$
21	20	dmeqi	$⊢ dom (\emptyset Sat \emptyset) (ω) = dom ⋃_{n \in ω} 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)$
22		dmiun	$⊢ dom ⋃_{n \in ω} 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) = ⋃_{n \in ω} dom 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)$
23		elelsuc	$⊢ n \in ω \to n \in suc ω$
24		fmlafv	$⊢ n \in suc ω \to Fmla (n) = dom (\emptyset Sat \emptyset) (n)$
25	23 24	syl	$⊢ n \in ω \to Fmla (n) = dom (\emptyset Sat \emptyset) (n)$
26		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)$
27	23 26	syl	$⊢ n \in ω \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)$
28	27	dmeqd	$⊢ n \in ω \to dom (\emptyset Sat \emptyset) (n) = dom 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)$
29	25 28	eqtr2d	$⊢ n \in ω \to dom 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)$
30	29	iuneq2i	$⊢ ⋃_{n \in ω} dom 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) = ⋃_{n \in ω} Fmla (n)$
31	21 22 30	3eqtri	$⊢ dom (\emptyset Sat \emptyset) (ω) = ⋃_{n \in ω} Fmla (n)$
32	2 13 31	3eqtri	$⊢ Fmla (ω) = ⋃_{n \in ω} Fmla (n)$

Metamath Proof Explorer

Theorem fmla

Proof