fmlafvel

Description: A class is a valid Godel formula of height N iff it is the first component of a member of the value of the satisfaction predicate as function over wff codes in the empty model with an empty binary relation at N . (Contributed by AV, 19-Sep-2023)

		Ref	Expression
	Assertion	fmlafvel	$⊢ N \in ω \to (F \in Fmla (N) \leftrightarrow ⟨F, \emptyset⟩ \in (\emptyset Sat \emptyset) (N))$

Proof

Step	Hyp	Ref	Expression
1		fveq2	$⊢ x = \emptyset \to Fmla (x) = Fmla (\emptyset)$
2	1	eleq2d	$⊢ x = \emptyset \to (F \in Fmla (x) \leftrightarrow F \in Fmla (\emptyset))$
3		fveq2	$⊢ x = \emptyset \to (\emptyset Sat \emptyset) (x) = (\emptyset Sat \emptyset) (\emptyset)$
4	3	eleq2d	$⊢ x = \emptyset \to (⟨F, \emptyset⟩ \in (\emptyset Sat \emptyset) (x) \leftrightarrow ⟨F, \emptyset⟩ \in (\emptyset Sat \emptyset) (\emptyset))$
5	2 4	bibi12d	$⊢ x = \emptyset \to ((F \in Fmla (x) \leftrightarrow ⟨F, \emptyset⟩ \in (\emptyset Sat \emptyset) (x)) \leftrightarrow (F \in Fmla (\emptyset) \leftrightarrow ⟨F, \emptyset⟩ \in (\emptyset Sat \emptyset) (\emptyset)))$
6	5	imbi2d	$⊢ x = \emptyset \to ((F \in V \to (F \in Fmla (x) \leftrightarrow ⟨F, \emptyset⟩ \in (\emptyset Sat \emptyset) (x))) \leftrightarrow (F \in V \to (F \in Fmla (\emptyset) \leftrightarrow ⟨F, \emptyset⟩ \in (\emptyset Sat \emptyset) (\emptyset))))$
7		fveq2	$⊢ x = y \to Fmla (x) = Fmla (y)$
8	7	eleq2d	$⊢ x = y \to (F \in Fmla (x) \leftrightarrow F \in Fmla (y))$
9		fveq2	$⊢ x = y \to (\emptyset Sat \emptyset) (x) = (\emptyset Sat \emptyset) (y)$
10	9	eleq2d	$⊢ x = y \to (⟨F, \emptyset⟩ \in (\emptyset Sat \emptyset) (x) \leftrightarrow ⟨F, \emptyset⟩ \in (\emptyset Sat \emptyset) (y))$
11	8 10	bibi12d	$⊢ x = y \to ((F \in Fmla (x) \leftrightarrow ⟨F, \emptyset⟩ \in (\emptyset Sat \emptyset) (x)) \leftrightarrow (F \in Fmla (y) \leftrightarrow ⟨F, \emptyset⟩ \in (\emptyset Sat \emptyset) (y)))$
12	11	imbi2d	$⊢ x = y \to ((F \in V \to (F \in Fmla (x) \leftrightarrow ⟨F, \emptyset⟩ \in (\emptyset Sat \emptyset) (x))) \leftrightarrow (F \in V \to (F \in Fmla (y) \leftrightarrow ⟨F, \emptyset⟩ \in (\emptyset Sat \emptyset) (y))))$
13		fveq2	$⊢ x = suc y \to Fmla (x) = Fmla (suc y)$
14	13	eleq2d	$⊢ x = suc y \to (F \in Fmla (x) \leftrightarrow F \in Fmla (suc y))$
15		fveq2	$⊢ x = suc y \to (\emptyset Sat \emptyset) (x) = (\emptyset Sat \emptyset) (suc y)$
16	15	eleq2d	$⊢ x = suc y \to (⟨F, \emptyset⟩ \in (\emptyset Sat \emptyset) (x) \leftrightarrow ⟨F, \emptyset⟩ \in (\emptyset Sat \emptyset) (suc y))$
17	14 16	bibi12d	$⊢ x = suc y \to ((F \in Fmla (x) \leftrightarrow ⟨F, \emptyset⟩ \in (\emptyset Sat \emptyset) (x)) \leftrightarrow (F \in Fmla (suc y) \leftrightarrow ⟨F, \emptyset⟩ \in (\emptyset Sat \emptyset) (suc y)))$
18	17	imbi2d	$⊢ x = suc y \to ((F \in V \to (F \in Fmla (x) \leftrightarrow ⟨F, \emptyset⟩ \in (\emptyset Sat \emptyset) (x))) \leftrightarrow (F \in V \to (F \in Fmla (suc y) \leftrightarrow ⟨F, \emptyset⟩ \in (\emptyset Sat \emptyset) (suc y))))$
19		fveq2	$⊢ x = N \to Fmla (x) = Fmla (N)$
20	19	eleq2d	$⊢ x = N \to (F \in Fmla (x) \leftrightarrow F \in Fmla (N))$
21		fveq2	$⊢ x = N \to (\emptyset Sat \emptyset) (x) = (\emptyset Sat \emptyset) (N)$
22	21	eleq2d	$⊢ x = N \to (⟨F, \emptyset⟩ \in (\emptyset Sat \emptyset) (x) \leftrightarrow ⟨F, \emptyset⟩ \in (\emptyset Sat \emptyset) (N))$
23	20 22	bibi12d	$⊢ x = N \to ((F \in Fmla (x) \leftrightarrow ⟨F, \emptyset⟩ \in (\emptyset Sat \emptyset) (x)) \leftrightarrow (F \in Fmla (N) \leftrightarrow ⟨F, \emptyset⟩ \in (\emptyset Sat \emptyset) (N)))$
24	23	imbi2d	$⊢ x = N \to ((F \in V \to (F \in Fmla (x) \leftrightarrow ⟨F, \emptyset⟩ \in (\emptyset Sat \emptyset) (x))) \leftrightarrow (F \in V \to (F \in Fmla (N) \leftrightarrow ⟨F, \emptyset⟩ \in (\emptyset Sat \emptyset) (N))))$
25		eqeq1	$⊢ x = F \to (x = i \in_{𝑔} j \leftrightarrow F = i \in_{𝑔} j)$
26	25	2rexbidv	$⊢ x = F \to (\exists i \in ω \exists j \in ω x = i \in_{𝑔} j \leftrightarrow \exists i \in ω \exists j \in ω F = i \in_{𝑔} j)$
27	26	elrab	$⊢ F \in \{x \in V \| \exists i \in ω \exists j \in ω x = i \in_{𝑔} j\} \leftrightarrow (F \in V \land \exists i \in ω \exists j \in ω F = i \in_{𝑔} j)$
28		eqidd	$⊢ (F \in V \land \exists i \in ω \exists j \in ω F = i \in_{𝑔} j) \to \emptyset = \emptyset$
29		simpr	$⊢ (F \in V \land \exists i \in ω \exists j \in ω F = i \in_{𝑔} j) \to \exists i \in ω \exists j \in ω F = i \in_{𝑔} j$
30	28 29	jca	$⊢ (F \in V \land \exists i \in ω \exists j \in ω F = i \in_{𝑔} j) \to (\emptyset = \emptyset \land \exists i \in ω \exists j \in ω F = i \in_{𝑔} j)$
31		simpr	$⊢ (\emptyset = \emptyset \land \exists i \in ω \exists j \in ω F = i \in_{𝑔} j) \to \exists i \in ω \exists j \in ω F = i \in_{𝑔} j$
32	31	anim2i	$⊢ (F \in V \land (\emptyset = \emptyset \land \exists i \in ω \exists j \in ω F = i \in_{𝑔} j)) \to (F \in V \land \exists i \in ω \exists j \in ω F = i \in_{𝑔} j)$
33	32	ex	$⊢ F \in V \to ((\emptyset = \emptyset \land \exists i \in ω \exists j \in ω F = i \in_{𝑔} j) \to (F \in V \land \exists i \in ω \exists j \in ω F = i \in_{𝑔} j))$
34	30 33	impbid2	$⊢ F \in V \to ((F \in V \land \exists i \in ω \exists j \in ω F = i \in_{𝑔} j) \leftrightarrow (\emptyset = \emptyset \land \exists i \in ω \exists j \in ω F = i \in_{𝑔} j))$
35	27 34	syl5bb	$⊢ F \in V \to (F \in \{x \in V \| \exists i \in ω \exists j \in ω x = i \in_{𝑔} j\} \leftrightarrow (\emptyset = \emptyset \land \exists i \in ω \exists j \in ω F = i \in_{𝑔} j))$
36		fmla0	$⊢ Fmla (\emptyset) = \{x \in V \| \exists i \in ω \exists j \in ω x = i \in_{𝑔} j\}$
37	36	eleq2i	$⊢ F \in Fmla (\emptyset) \leftrightarrow F \in \{x \in V \| \exists i \in ω \exists j \in ω x = i \in_{𝑔} j\}$
38	37	a1i	$⊢ F \in V \to (F \in Fmla (\emptyset) \leftrightarrow F \in \{x \in V \| \exists i \in ω \exists j \in ω x = i \in_{𝑔} j\})$
39		satf00	$⊢ (\emptyset Sat \emptyset) (\emptyset) = \{⟨x, y⟩ \| (y = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)\}$
40	39	a1i	$⊢ F \in V \to (\emptyset Sat \emptyset) (\emptyset) = \{⟨x, y⟩ \| (y = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)\}$
41	40	eleq2d	$⊢ F \in V \to (⟨F, \emptyset⟩ \in (\emptyset Sat \emptyset) (\emptyset) \leftrightarrow ⟨F, \emptyset⟩ \in \{⟨x, y⟩ \| (y = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)\})$
42		0ex	$⊢ \emptyset \in V$
43		eqeq1	$⊢ y = \emptyset \to (y = \emptyset \leftrightarrow \emptyset = \emptyset)$
44	43 26	bi2anan9r	$⊢ (x = F \land y = \emptyset) \to ((y = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j) \leftrightarrow (\emptyset = \emptyset \land \exists i \in ω \exists j \in ω F = i \in_{𝑔} j))$
45	44	opelopabga	$⊢ (F \in V \land \emptyset \in V) \to (⟨F, \emptyset⟩ \in \{⟨x, y⟩ \| (y = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)\} \leftrightarrow (\emptyset = \emptyset \land \exists i \in ω \exists j \in ω F = i \in_{𝑔} j))$
46	42 45	mpan2	$⊢ F \in V \to (⟨F, \emptyset⟩ \in \{⟨x, y⟩ \| (y = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)\} \leftrightarrow (\emptyset = \emptyset \land \exists i \in ω \exists j \in ω F = i \in_{𝑔} j))$
47	41 46	bitrd	$⊢ F \in V \to (⟨F, \emptyset⟩ \in (\emptyset Sat \emptyset) (\emptyset) \leftrightarrow (\emptyset = \emptyset \land \exists i \in ω \exists j \in ω F = i \in_{𝑔} j))$
48	35 38 47	3bitr4d	$⊢ F \in V \to (F \in Fmla (\emptyset) \leftrightarrow ⟨F, \emptyset⟩ \in (\emptyset Sat \emptyset) (\emptyset))$
49		eqid	$⊢ \emptyset = \emptyset$
50	49	biantrur	$⊢ \exists u \in (\emptyset Sat \emptyset) (y) (\exists v \in (\emptyset Sat \emptyset) (y) F = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω F = [\forall_{𝑔} i 1^{st} (u)]) \leftrightarrow (\emptyset = \emptyset \land \exists u \in (\emptyset Sat \emptyset) (y) (\exists v \in (\emptyset Sat \emptyset) (y) F = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω F = [\forall_{𝑔} i 1^{st} (u)]))$
51	50	bicomi	$⊢ (\emptyset = \emptyset \land \exists u \in (\emptyset Sat \emptyset) (y) (\exists v \in (\emptyset Sat \emptyset) (y) F = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω F = [\forall_{𝑔} i 1^{st} (u)])) \leftrightarrow \exists u \in (\emptyset Sat \emptyset) (y) (\exists v \in (\emptyset Sat \emptyset) (y) F = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω F = [\forall_{𝑔} i 1^{st} (u)])$
52	51	a1i	$⊢ F \in V \to ((\emptyset = \emptyset \land \exists u \in (\emptyset Sat \emptyset) (y) (\exists v \in (\emptyset Sat \emptyset) (y) F = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω F = [\forall_{𝑔} i 1^{st} (u)])) \leftrightarrow \exists u \in (\emptyset Sat \emptyset) (y) (\exists v \in (\emptyset Sat \emptyset) (y) F = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω F = [\forall_{𝑔} i 1^{st} (u)]))$
53		eqeq1	$⊢ z = \emptyset \to (z = \emptyset \leftrightarrow \emptyset = \emptyset)$
54		eqeq1	$⊢ x = F \to (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \leftrightarrow F = 1^{st} (u) ⊼_{𝑔} 1^{st} (v))$
55	54	rexbidv	$⊢ x = F \to (\exists v \in (\emptyset Sat \emptyset) (y) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \leftrightarrow \exists v \in (\emptyset Sat \emptyset) (y) F = 1^{st} (u) ⊼_{𝑔} 1^{st} (v))$
56		eqeq1	$⊢ x = F \to (x = [\forall_{𝑔} i 1^{st} (u)] \leftrightarrow F = [\forall_{𝑔} i 1^{st} (u)])$
57	56	rexbidv	$⊢ x = F \to (\exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)] \leftrightarrow \exists i \in ω F = [\forall_{𝑔} i 1^{st} (u)])$
58	55 57	orbi12d	$⊢ x = F \to ((\exists v \in (\emptyset Sat \emptyset) (y) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]) \leftrightarrow (\exists v \in (\emptyset Sat \emptyset) (y) F = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω F = [\forall_{𝑔} i 1^{st} (u)]))$
59	58	rexbidv	$⊢ x = F \to (\exists u \in (\emptyset Sat \emptyset) (y) (\exists v \in (\emptyset Sat \emptyset) (y) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]) \leftrightarrow \exists u \in (\emptyset Sat \emptyset) (y) (\exists v \in (\emptyset Sat \emptyset) (y) F = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω F = [\forall_{𝑔} i 1^{st} (u)]))$
60	53 59	bi2anan9r	$⊢ (x = F \land z = \emptyset) \to ((z = \emptyset \land \exists u \in (\emptyset Sat \emptyset) (y) (\exists v \in (\emptyset Sat \emptyset) (y) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)])) \leftrightarrow (\emptyset = \emptyset \land \exists u \in (\emptyset Sat \emptyset) (y) (\exists v \in (\emptyset Sat \emptyset) (y) F = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω F = [\forall_{𝑔} i 1^{st} (u)])))$
61	60	opelopabga	$⊢ (F \in V \land \emptyset \in V) \to (⟨F, \emptyset⟩ \in \{⟨x, z⟩ \| (z = \emptyset \land \exists u \in (\emptyset Sat \emptyset) (y) (\exists v \in (\emptyset Sat \emptyset) (y) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\} \leftrightarrow (\emptyset = \emptyset \land \exists u \in (\emptyset Sat \emptyset) (y) (\exists v \in (\emptyset Sat \emptyset) (y) F = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω F = [\forall_{𝑔} i 1^{st} (u)])))$
62	42 61	mpan2	$⊢ F \in V \to (⟨F, \emptyset⟩ \in \{⟨x, z⟩ \| (z = \emptyset \land \exists u \in (\emptyset Sat \emptyset) (y) (\exists v \in (\emptyset Sat \emptyset) (y) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\} \leftrightarrow (\emptyset = \emptyset \land \exists u \in (\emptyset Sat \emptyset) (y) (\exists v \in (\emptyset Sat \emptyset) (y) F = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω F = [\forall_{𝑔} i 1^{st} (u)])))$
63	59	elabg	$⊢ F \in V \to (F \in \{x \| \exists u \in (\emptyset Sat \emptyset) (y) (\exists v \in (\emptyset Sat \emptyset) (y) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)])\} \leftrightarrow \exists u \in (\emptyset Sat \emptyset) (y) (\exists v \in (\emptyset Sat \emptyset) (y) F = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω F = [\forall_{𝑔} i 1^{st} (u)]))$
64	52 62 63	3bitr4d	$⊢ F \in V \to (⟨F, \emptyset⟩ \in \{⟨x, z⟩ \| (z = \emptyset \land \exists u \in (\emptyset Sat \emptyset) (y) (\exists v \in (\emptyset Sat \emptyset) (y) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\} \leftrightarrow F \in \{x \| \exists u \in (\emptyset Sat \emptyset) (y) (\exists v \in (\emptyset Sat \emptyset) (y) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)])\})$
65	64	adantl	$⊢ ((y \in ω \land (F \in V \to (F \in Fmla (y) \leftrightarrow ⟨F, \emptyset⟩ \in (\emptyset Sat \emptyset) (y)))) \land F \in V) \to (⟨F, \emptyset⟩ \in \{⟨x, z⟩ \| (z = \emptyset \land \exists u \in (\emptyset Sat \emptyset) (y) (\exists v \in (\emptyset Sat \emptyset) (y) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\} \leftrightarrow F \in \{x \| \exists u \in (\emptyset Sat \emptyset) (y) (\exists v \in (\emptyset Sat \emptyset) (y) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)])\})$
66	65	orbi2d	$⊢ ((y \in ω \land (F \in V \to (F \in Fmla (y) \leftrightarrow ⟨F, \emptyset⟩ \in (\emptyset Sat \emptyset) (y)))) \land F \in V) \to ((⟨F, \emptyset⟩ \in (\emptyset Sat \emptyset) (y) \lor ⟨F, \emptyset⟩ \in \{⟨x, z⟩ \| (z = \emptyset \land \exists u \in (\emptyset Sat \emptyset) (y) (\exists v \in (\emptyset Sat \emptyset) (y) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}) \leftrightarrow (⟨F, \emptyset⟩ \in (\emptyset Sat \emptyset) (y) \lor F \in \{x \| \exists u \in (\emptyset Sat \emptyset) (y) (\exists v \in (\emptyset Sat \emptyset) (y) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)])\}))$
67		eqid	$⊢ \emptyset Sat \emptyset = \emptyset Sat \emptyset$
68	67	satf0suc	$⊢ y \in ω \to (\emptyset Sat \emptyset) (suc y) = (\emptyset Sat \emptyset) (y) \cup \{⟨x, z⟩ \| (z = \emptyset \land \exists u \in (\emptyset Sat \emptyset) (y) (\exists v \in (\emptyset Sat \emptyset) (y) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}$
69	68	eleq2d	$⊢ y \in ω \to (⟨F, \emptyset⟩ \in (\emptyset Sat \emptyset) (suc y) \leftrightarrow ⟨F, \emptyset⟩ \in ((\emptyset Sat \emptyset) (y) \cup \{⟨x, z⟩ \| (z = \emptyset \land \exists u \in (\emptyset Sat \emptyset) (y) (\exists v \in (\emptyset Sat \emptyset) (y) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}))$
70		elun	$⊢ ⟨F, \emptyset⟩ \in ((\emptyset Sat \emptyset) (y) \cup \{⟨x, z⟩ \| (z = \emptyset \land \exists u \in (\emptyset Sat \emptyset) (y) (\exists v \in (\emptyset Sat \emptyset) (y) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}) \leftrightarrow (⟨F, \emptyset⟩ \in (\emptyset Sat \emptyset) (y) \lor ⟨F, \emptyset⟩ \in \{⟨x, z⟩ \| (z = \emptyset \land \exists u \in (\emptyset Sat \emptyset) (y) (\exists v \in (\emptyset Sat \emptyset) (y) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\})$
71	69 70	bitrdi	$⊢ y \in ω \to (⟨F, \emptyset⟩ \in (\emptyset Sat \emptyset) (suc y) \leftrightarrow (⟨F, \emptyset⟩ \in (\emptyset Sat \emptyset) (y) \lor ⟨F, \emptyset⟩ \in \{⟨x, z⟩ \| (z = \emptyset \land \exists u \in (\emptyset Sat \emptyset) (y) (\exists v \in (\emptyset Sat \emptyset) (y) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}))$
72	71	ad2antrr	$⊢ ((y \in ω \land (F \in V \to (F \in Fmla (y) \leftrightarrow ⟨F, \emptyset⟩ \in (\emptyset Sat \emptyset) (y)))) \land F \in V) \to (⟨F, \emptyset⟩ \in (\emptyset Sat \emptyset) (suc y) \leftrightarrow (⟨F, \emptyset⟩ \in (\emptyset Sat \emptyset) (y) \lor ⟨F, \emptyset⟩ \in \{⟨x, z⟩ \| (z = \emptyset \land \exists u \in (\emptyset Sat \emptyset) (y) (\exists v \in (\emptyset Sat \emptyset) (y) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}))$
73		fmlasuc0	$⊢ y \in ω \to Fmla (suc y) = Fmla (y) \cup \{x \| \exists u \in (\emptyset Sat \emptyset) (y) (\exists v \in (\emptyset Sat \emptyset) (y) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)])\}$
74	73	eleq2d	$⊢ y \in ω \to (F \in Fmla (suc y) \leftrightarrow F \in (Fmla (y) \cup \{x \| \exists u \in (\emptyset Sat \emptyset) (y) (\exists v \in (\emptyset Sat \emptyset) (y) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)])\}))$
75	74	ad2antrr	$⊢ ((y \in ω \land (F \in V \to (F \in Fmla (y) \leftrightarrow ⟨F, \emptyset⟩ \in (\emptyset Sat \emptyset) (y)))) \land F \in V) \to (F \in Fmla (suc y) \leftrightarrow F \in (Fmla (y) \cup \{x \| \exists u \in (\emptyset Sat \emptyset) (y) (\exists v \in (\emptyset Sat \emptyset) (y) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)])\}))$
76		elun	$⊢ F \in (Fmla (y) \cup \{x \| \exists u \in (\emptyset Sat \emptyset) (y) (\exists v \in (\emptyset Sat \emptyset) (y) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)])\}) \leftrightarrow (F \in Fmla (y) \lor F \in \{x \| \exists u \in (\emptyset Sat \emptyset) (y) (\exists v \in (\emptyset Sat \emptyset) (y) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)])\})$
77	76	a1i	$⊢ ((y \in ω \land (F \in V \to (F \in Fmla (y) \leftrightarrow ⟨F, \emptyset⟩ \in (\emptyset Sat \emptyset) (y)))) \land F \in V) \to (F \in (Fmla (y) \cup \{x \| \exists u \in (\emptyset Sat \emptyset) (y) (\exists v \in (\emptyset Sat \emptyset) (y) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)])\}) \leftrightarrow (F \in Fmla (y) \lor F \in \{x \| \exists u \in (\emptyset Sat \emptyset) (y) (\exists v \in (\emptyset Sat \emptyset) (y) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)])\}))$
78		simpr	$⊢ (y \in ω \land (F \in V \to (F \in Fmla (y) \leftrightarrow ⟨F, \emptyset⟩ \in (\emptyset Sat \emptyset) (y)))) \to (F \in V \to (F \in Fmla (y) \leftrightarrow ⟨F, \emptyset⟩ \in (\emptyset Sat \emptyset) (y)))$
79	78	imp	$⊢ ((y \in ω \land (F \in V \to (F \in Fmla (y) \leftrightarrow ⟨F, \emptyset⟩ \in (\emptyset Sat \emptyset) (y)))) \land F \in V) \to (F \in Fmla (y) \leftrightarrow ⟨F, \emptyset⟩ \in (\emptyset Sat \emptyset) (y))$
80	79	orbi1d	$⊢ ((y \in ω \land (F \in V \to (F \in Fmla (y) \leftrightarrow ⟨F, \emptyset⟩ \in (\emptyset Sat \emptyset) (y)))) \land F \in V) \to ((F \in Fmla (y) \lor F \in \{x \| \exists u \in (\emptyset Sat \emptyset) (y) (\exists v \in (\emptyset Sat \emptyset) (y) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)])\}) \leftrightarrow (⟨F, \emptyset⟩ \in (\emptyset Sat \emptyset) (y) \lor F \in \{x \| \exists u \in (\emptyset Sat \emptyset) (y) (\exists v \in (\emptyset Sat \emptyset) (y) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)])\}))$
81	75 77 80	3bitrd	$⊢ ((y \in ω \land (F \in V \to (F \in Fmla (y) \leftrightarrow ⟨F, \emptyset⟩ \in (\emptyset Sat \emptyset) (y)))) \land F \in V) \to (F \in Fmla (suc y) \leftrightarrow (⟨F, \emptyset⟩ \in (\emptyset Sat \emptyset) (y) \lor F \in \{x \| \exists u \in (\emptyset Sat \emptyset) (y) (\exists v \in (\emptyset Sat \emptyset) (y) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)])\}))$
82	66 72 81	3bitr4rd	$⊢ ((y \in ω \land (F \in V \to (F \in Fmla (y) \leftrightarrow ⟨F, \emptyset⟩ \in (\emptyset Sat \emptyset) (y)))) \land F \in V) \to (F \in Fmla (suc y) \leftrightarrow ⟨F, \emptyset⟩ \in (\emptyset Sat \emptyset) (suc y))$
83	82	exp31	$⊢ y \in ω \to ((F \in V \to (F \in Fmla (y) \leftrightarrow ⟨F, \emptyset⟩ \in (\emptyset Sat \emptyset) (y))) \to (F \in V \to (F \in Fmla (suc y) \leftrightarrow ⟨F, \emptyset⟩ \in (\emptyset Sat \emptyset) (suc y))))$
84	6 12 18 24 48 83	finds	$⊢ N \in ω \to (F \in V \to (F \in Fmla (N) \leftrightarrow ⟨F, \emptyset⟩ \in (\emptyset Sat \emptyset) (N)))$
85	84	com12	$⊢ F \in V \to (N \in ω \to (F \in Fmla (N) \leftrightarrow ⟨F, \emptyset⟩ \in (\emptyset Sat \emptyset) (N)))$
86		prcnel	$⊢ \neg F \in V \to \neg F \in Fmla (N)$
87	86	adantr	$⊢ (\neg F \in V \land N \in ω) \to \neg F \in Fmla (N)$
88		opprc1	$⊢ \neg F \in V \to ⟨F, \emptyset⟩ = \emptyset$
89	88	adantr	$⊢ (\neg F \in V \land N \in ω) \to ⟨F, \emptyset⟩ = \emptyset$
90		satf0n0	$⊢ N \in ω \to \emptyset \notin (\emptyset Sat \emptyset) (N)$
91		df-nel	$⊢ \emptyset \notin (\emptyset Sat \emptyset) (N) \leftrightarrow \neg \emptyset \in (\emptyset Sat \emptyset) (N)$
92	90 91	sylib	$⊢ N \in ω \to \neg \emptyset \in (\emptyset Sat \emptyset) (N)$
93	92	adantl	$⊢ (\neg F \in V \land N \in ω) \to \neg \emptyset \in (\emptyset Sat \emptyset) (N)$
94	89 93	eqneltrd	$⊢ (\neg F \in V \land N \in ω) \to \neg ⟨F, \emptyset⟩ \in (\emptyset Sat \emptyset) (N)$
95	87 94	2falsed	$⊢ (\neg F \in V \land N \in ω) \to (F \in Fmla (N) \leftrightarrow ⟨F, \emptyset⟩ \in (\emptyset Sat \emptyset) (N))$
96	95	ex	$⊢ \neg F \in V \to (N \in ω \to (F \in Fmla (N) \leftrightarrow ⟨F, \emptyset⟩ \in (\emptyset Sat \emptyset) (N)))$
97	85 96	pm2.61i	$⊢ N \in ω \to (F \in Fmla (N) \leftrightarrow ⟨F, \emptyset⟩ \in (\emptyset Sat \emptyset) (N))$

Metamath Proof Explorer

Theorem fmlafvel

Proof