Theorem 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=\left(x\in \mathrm{\omega }⟼if\left(x=2_{𝑜},1_{𝑜},2_{𝑜}\right)\right)$$
Assertion	ex-sategoelel12	$$⊢S\in \left(\left\{1_{𝑜},2_{𝑜}\right\}{\mathrm{Sat}}_{\in }\left(2_{𝑜}{\in }_{𝑔}{1}_{𝑜}\right)\right)$$

Proof

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