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	⊢ 𝑆 = ( 𝑥 ∈ ω ↦ if ( 𝑥 = 2_o , 1_o , 2_o ) )
	Assertion	ex-sategoelel12	⊢ 𝑆 ∈ ( { 1_o , 2_o } Sat_∈ ( 2_o ∈_𝑔 1_o ) )

Proof

Step	Hyp	Ref	Expression
1		ex-sategoelel12.s	⊢ 𝑆 = ( 𝑥 ∈ ω ↦ if ( 𝑥 = 2_o , 1_o , 2_o ) )
2		1oex	⊢ 1_o ∈ V
3	2	prid1	⊢ 1_o ∈ { 1_o , 2_o }
4		2oex	⊢ 2_o ∈ V
5	4	prid2	⊢ 2_o ∈ { 1_o , 2_o }
6	3 5	ifcli	⊢ if ( 𝑥 = 2_o , 1_o , 2_o ) ∈ { 1_o , 2_o }
7	6	a1i	⊢ ( 𝑥 ∈ ω → if ( 𝑥 = 2_o , 1_o , 2_o ) ∈ { 1_o , 2_o } )
8	1 7	fmpti	⊢ 𝑆 : ω ⟶ { 1_o , 2_o }
9		prex	⊢ { 1_o , 2_o } ∈ V
10		omex	⊢ ω ∈ V
11	9 10	elmap	⊢ ( 𝑆 ∈ ( { 1_o , 2_o } ↑_m ω ) ↔ 𝑆 : ω ⟶ { 1_o , 2_o } )
12	8 11	mpbir	⊢ 𝑆 ∈ ( { 1_o , 2_o } ↑_m ω )
13	2	sucid	⊢ 1_o ∈ suc 1_o
14		df-2o	⊢ 2_o = suc 1_o
15	13 14	eleqtrri	⊢ 1_o ∈ 2_o
16		2onn	⊢ 2_o ∈ ω
17		1onn	⊢ 1_o ∈ ω
18		iftrue	⊢ ( 𝑥 = 2_o → if ( 𝑥 = 2_o , 1_o , 2_o ) = 1_o )
19	18 1	fvmptg	⊢ ( ( 2_o ∈ ω ∧ 1_o ∈ ω ) → ( 𝑆 ‘ 2_o ) = 1_o )
20	16 17 19	mp2an	⊢ ( 𝑆 ‘ 2_o ) = 1_o
21		1one2o	⊢ 1_o ≠ 2_o
22	21	neii	⊢ ¬ 1_o = 2_o
23		eqeq1	⊢ ( 𝑥 = 1_o → ( 𝑥 = 2_o ↔ 1_o = 2_o ) )
24	22 23	mtbiri	⊢ ( 𝑥 = 1_o → ¬ 𝑥 = 2_o )
25	24	iffalsed	⊢ ( 𝑥 = 1_o → if ( 𝑥 = 2_o , 1_o , 2_o ) = 2_o )
26	25 1	fvmptg	⊢ ( ( 1_o ∈ ω ∧ 2_o ∈ ω ) → ( 𝑆 ‘ 1_o ) = 2_o )
27	17 16 26	mp2an	⊢ ( 𝑆 ‘ 1_o ) = 2_o
28	15 20 27	3eltr4i	⊢ ( 𝑆 ‘ 2_o ) ∈ ( 𝑆 ‘ 1_o )
29	12 28	pm3.2i	⊢ ( 𝑆 ∈ ( { 1_o , 2_o } ↑_m ω ) ∧ ( 𝑆 ‘ 2_o ) ∈ ( 𝑆 ‘ 1_o ) )
30	16 17	pm3.2i	⊢ ( 2_o ∈ ω ∧ 1_o ∈ ω )
31		eqid	⊢ ( { 1_o , 2_o } Sat_∈ ( 2_o ∈_𝑔 1_o ) ) = ( { 1_o , 2_o } Sat_∈ ( 2_o ∈_𝑔 1_o ) )
32	31	sategoelfvb	⊢ ( ( { 1_o , 2_o } ∈ V ∧ ( 2_o ∈ ω ∧ 1_o ∈ ω ) ) → ( 𝑆 ∈ ( { 1_o , 2_o } Sat_∈ ( 2_o ∈_𝑔 1_o ) ) ↔ ( 𝑆 ∈ ( { 1_o , 2_o } ↑_m ω ) ∧ ( 𝑆 ‘ 2_o ) ∈ ( 𝑆 ‘ 1_o ) ) ) )
33	9 30 32	mp2an	⊢ ( 𝑆 ∈ ( { 1_o , 2_o } Sat_∈ ( 2_o ∈_𝑔 1_o ) ) ↔ ( 𝑆 ∈ ( { 1_o , 2_o } ↑_m ω ) ∧ ( 𝑆 ‘ 2_o ) ∈ ( 𝑆 ‘ 1_o ) ) )
34	29 33	mpbir	⊢ 𝑆 ∈ ( { 1_o , 2_o } Sat_∈ ( 2_o ∈_𝑔 1_o ) )

Metamath Proof Explorer

Theorem ex-sategoelel12

Proof