ex-sategoelel12

Description: Example of a valuation of a simplified satisfaction predicate over a proper pair (of ordinal numbers) as model for a Godel-set of membership using the properties of a successor: ( S2o ) = 1o e. 2o = ( S2o ) . Remark: the indices 1o and 2o are intentionally reversed to distinguish them from elements of the model: ( 2o e.g 1o ) should not be confused with 2o e. 1o , which is false. (Contributed by AV, 19-Nov-2023)

		Ref	Expression
	Hypothesis	ex-sategoelel12.s	$⊢ S = (x \in ω ⟼ if (x = 2_{𝑜}, 1_{𝑜}, 2_{𝑜}))$
	Assertion	ex-sategoelel12	$⊢ S \in (\{1_{𝑜}, 2_{𝑜}\} {Sat}_{\in} (2_{𝑜} \in_{𝑔} 1_{𝑜}))$

Proof

Step	Hyp	Ref	Expression
1		ex-sategoelel12.s	$⊢ S = (x \in ω ⟼ if (x = 2_{𝑜}, 1_{𝑜}, 2_{𝑜}))$
2		1oex	$⊢ 1_{𝑜} \in V$
3	2	prid1	$⊢ 1_{𝑜} \in \{1_{𝑜}, 2_{𝑜}\}$
4		2oex	$⊢ 2_{𝑜} \in V$
5	4	prid2	$⊢ 2_{𝑜} \in \{1_{𝑜}, 2_{𝑜}\}$
6	3 5	ifcli	$⊢ if (x = 2_{𝑜}, 1_{𝑜}, 2_{𝑜}) \in \{1_{𝑜}, 2_{𝑜}\}$
7	6	a1i	$⊢ x \in ω \to if (x = 2_{𝑜}, 1_{𝑜}, 2_{𝑜}) \in \{1_{𝑜}, 2_{𝑜}\}$
8	1 7	fmpti	$⊢ S : ω ⟶ \{1_{𝑜}, 2_{𝑜}\}$
9		prex	$⊢ \{1_{𝑜}, 2_{𝑜}\} \in V$
10		omex	$⊢ ω \in V$
11	9 10	elmap	$⊢ S \in ({\{1_{𝑜}, 2_{𝑜}\}}^{ω}) \leftrightarrow S : ω ⟶ \{1_{𝑜}, 2_{𝑜}\}$
12	8 11	mpbir	$⊢ S \in ({\{1_{𝑜}, 2_{𝑜}\}}^{ω})$
13	2	sucid	$⊢ 1_{𝑜} \in suc 1_{𝑜}$
14		df-2o	$⊢ 2_{𝑜} = suc 1_{𝑜}$
15	13 14	eleqtrri	$⊢ 1_{𝑜} \in 2_{𝑜}$
16		2onn	$⊢ 2_{𝑜} \in ω$
17		1onn	$⊢ 1_{𝑜} \in ω$
18		iftrue	$⊢ x = 2_{𝑜} \to if (x = 2_{𝑜}, 1_{𝑜}, 2_{𝑜}) = 1_{𝑜}$
19	18 1	fvmptg	$⊢ (2_{𝑜} \in ω \land 1_{𝑜} \in ω) \to S (2_{𝑜}) = 1_{𝑜}$
20	16 17 19	mp2an	$⊢ S (2_{𝑜}) = 1_{𝑜}$
21		1one2o	$⊢ 1_{𝑜} \neq 2_{𝑜}$
22	21	neii	$⊢ \neg 1_{𝑜} = 2_{𝑜}$
23		eqeq1	$⊢ x = 1_{𝑜} \to (x = 2_{𝑜} \leftrightarrow 1_{𝑜} = 2_{𝑜})$
24	22 23	mtbiri	$⊢ x = 1_{𝑜} \to \neg x = 2_{𝑜}$
25	24	iffalsed	$⊢ x = 1_{𝑜} \to if (x = 2_{𝑜}, 1_{𝑜}, 2_{𝑜}) = 2_{𝑜}$
26	25 1	fvmptg	$⊢ (1_{𝑜} \in ω \land 2_{𝑜} \in ω) \to S (1_{𝑜}) = 2_{𝑜}$
27	17 16 26	mp2an	$⊢ S (1_{𝑜}) = 2_{𝑜}$
28	15 20 27	3eltr4i	$⊢ S (2_{𝑜}) \in S (1_{𝑜})$
29	12 28	pm3.2i	$⊢ (S \in ({\{1_{𝑜}, 2_{𝑜}\}}^{ω}) \land S (2_{𝑜}) \in S (1_{𝑜}))$
30	16 17	pm3.2i	$⊢ (2_{𝑜} \in ω \land 1_{𝑜} \in ω)$
31		eqid	$⊢ \{1_{𝑜}, 2_{𝑜}\} {Sat}_{\in} (2_{𝑜} \in_{𝑔} 1_{𝑜}) = \{1_{𝑜}, 2_{𝑜}\} {Sat}_{\in} (2_{𝑜} \in_{𝑔} 1_{𝑜})$
32	31	sategoelfvb	$⊢ (\{1_{𝑜}, 2_{𝑜}\} \in V \land (2_{𝑜} \in ω \land 1_{𝑜} \in ω)) \to (S \in (\{1_{𝑜}, 2_{𝑜}\} {Sat}_{\in} (2_{𝑜} \in_{𝑔} 1_{𝑜})) \leftrightarrow (S \in ({\{1_{𝑜}, 2_{𝑜}\}}^{ω}) \land S (2_{𝑜}) \in S (1_{𝑜})))$
33	9 30 32	mp2an	$⊢ S \in (\{1_{𝑜}, 2_{𝑜}\} {Sat}_{\in} (2_{𝑜} \in_{𝑔} 1_{𝑜})) \leftrightarrow (S \in ({\{1_{𝑜}, 2_{𝑜}\}}^{ω}) \land S (2_{𝑜}) \in S (1_{𝑜}))$
34	29 33	mpbir	$⊢ S \in (\{1_{𝑜}, 2_{𝑜}\} {Sat}_{\in} (2_{𝑜} \in_{𝑔} 1_{𝑜}))$

Metamath Proof Explorer

Theorem ex-sategoelel12

Proof