satf0n0

Description: The value of the satisfaction predicate as function over wff codes in the empty model and the empty binary relation does not contain the empty set. (Contributed by AV, 19-Sep-2023)

		Ref	Expression
	Assertion	satf0n0	$⊢ N \in ω \to \emptyset \notin (\emptyset Sat \emptyset) (N)$

Proof

Step	Hyp	Ref	Expression
1		fveq2	$⊢ x = \emptyset \to (\emptyset Sat \emptyset) (x) = (\emptyset Sat \emptyset) (\emptyset)$
2	1	eleq2d	$⊢ x = \emptyset \to (\emptyset \in (\emptyset Sat \emptyset) (x) \leftrightarrow \emptyset \in (\emptyset Sat \emptyset) (\emptyset))$
3	2	notbid	$⊢ x = \emptyset \to (\neg \emptyset \in (\emptyset Sat \emptyset) (x) \leftrightarrow \neg \emptyset \in (\emptyset Sat \emptyset) (\emptyset))$
4		fveq2	$⊢ x = y \to (\emptyset Sat \emptyset) (x) = (\emptyset Sat \emptyset) (y)$
5	4	eleq2d	$⊢ x = y \to (\emptyset \in (\emptyset Sat \emptyset) (x) \leftrightarrow \emptyset \in (\emptyset Sat \emptyset) (y))$
6	5	notbid	$⊢ x = y \to (\neg \emptyset \in (\emptyset Sat \emptyset) (x) \leftrightarrow \neg \emptyset \in (\emptyset Sat \emptyset) (y))$
7		fveq2	$⊢ x = suc y \to (\emptyset Sat \emptyset) (x) = (\emptyset Sat \emptyset) (suc y)$
8	7	eleq2d	$⊢ x = suc y \to (\emptyset \in (\emptyset Sat \emptyset) (x) \leftrightarrow \emptyset \in (\emptyset Sat \emptyset) (suc y))$
9	8	notbid	$⊢ x = suc y \to (\neg \emptyset \in (\emptyset Sat \emptyset) (x) \leftrightarrow \neg \emptyset \in (\emptyset Sat \emptyset) (suc y))$
10		fveq2	$⊢ x = N \to (\emptyset Sat \emptyset) (x) = (\emptyset Sat \emptyset) (N)$
11	10	eleq2d	$⊢ x = N \to (\emptyset \in (\emptyset Sat \emptyset) (x) \leftrightarrow \emptyset \in (\emptyset Sat \emptyset) (N))$
12	11	notbid	$⊢ x = N \to (\neg \emptyset \in (\emptyset Sat \emptyset) (x) \leftrightarrow \neg \emptyset \in (\emptyset Sat \emptyset) (N))$
13		0nelopab	$⊢ \neg \emptyset \in \{⟨x, y⟩ \| (y = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)\}$
14		satf00	$⊢ (\emptyset Sat \emptyset) (\emptyset) = \{⟨x, y⟩ \| (y = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)\}$
15	14	eleq2i	$⊢ \emptyset \in (\emptyset Sat \emptyset) (\emptyset) \leftrightarrow \emptyset \in \{⟨x, y⟩ \| (y = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)\}$
16	13 15	mtbir	$⊢ \neg \emptyset \in (\emptyset Sat \emptyset) (\emptyset)$
17		simpr	$⊢ (y \in ω \land \neg \emptyset \in (\emptyset Sat \emptyset) (y)) \to \neg \emptyset \in (\emptyset Sat \emptyset) (y)$
18		0nelopab	$⊢ \neg \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)]))\}$
19		ioran	$⊢ \neg (\emptyset \in (\emptyset Sat \emptyset) (y) \lor \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 (\neg \emptyset \in (\emptyset Sat \emptyset) (y) \land \neg \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)]))\})$
20	17 18 19	sylanblrc	$⊢ (y \in ω \land \neg \emptyset \in (\emptyset Sat \emptyset) (y)) \to \neg (\emptyset \in (\emptyset Sat \emptyset) (y) \lor \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)]))\})$
21		eqid	$⊢ \emptyset Sat \emptyset = \emptyset Sat \emptyset$
22	21	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)]))\}$
23	22	adantr	$⊢ (y \in ω \land \neg \emptyset \in (\emptyset Sat \emptyset) (y)) \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)]))\}$
24	23	eleq2d	$⊢ (y \in ω \land \neg \emptyset \in (\emptyset Sat \emptyset) (y)) \to (\emptyset \in (\emptyset Sat \emptyset) (suc y) \leftrightarrow \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)]))\}))$
25		elun	$⊢ \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 (\emptyset \in (\emptyset Sat \emptyset) (y) \lor \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)]))\})$
26	24 25	bitrdi	$⊢ (y \in ω \land \neg \emptyset \in (\emptyset Sat \emptyset) (y)) \to (\emptyset \in (\emptyset Sat \emptyset) (suc y) \leftrightarrow (\emptyset \in (\emptyset Sat \emptyset) (y) \lor \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)]))\}))$
27	20 26	mtbird	$⊢ (y \in ω \land \neg \emptyset \in (\emptyset Sat \emptyset) (y)) \to \neg \emptyset \in (\emptyset Sat \emptyset) (suc y)$
28	27	ex	$⊢ y \in ω \to (\neg \emptyset \in (\emptyset Sat \emptyset) (y) \to \neg \emptyset \in (\emptyset Sat \emptyset) (suc y))$
29	3 6 9 12 16 28	finds	$⊢ N \in ω \to \neg \emptyset \in (\emptyset Sat \emptyset) (N)$
30		df-nel	$⊢ \emptyset \notin (\emptyset Sat \emptyset) (N) \leftrightarrow \neg \emptyset \in (\emptyset Sat \emptyset) (N)$
31	29 30	sylibr	$⊢ N \in ω \to \emptyset \notin (\emptyset Sat \emptyset) (N)$

Metamath Proof Explorer

Theorem satf0n0

Proof