sategoelfvb

Description: Characterization of a valuation S of a simplified satisfaction predicate for a Godel-set of membership. (Contributed by AV, 5-Nov-2023)

		Ref	Expression
	Hypothesis	sategoelfvb.s	⊢ 𝐸 = ( 𝑀 Sat_∈ ( 𝐴 ∈_𝑔 𝐵 ) )
	Assertion	sategoelfvb	⊢ ( ( 𝑀 ∈ 𝑉 ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) → ( 𝑆 ∈ 𝐸 ↔ ( 𝑆 ∈ ( 𝑀 ↑_m ω ) ∧ ( 𝑆 ‘ 𝐴 ) ∈ ( 𝑆 ‘ 𝐵 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		sategoelfvb.s	⊢ 𝐸 = ( 𝑀 Sat_∈ ( 𝐴 ∈_𝑔 𝐵 ) )
2		ovexd	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴 ∈_𝑔 𝐵 ) ∈ V )
3		simpl	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → 𝐴 ∈ ω )
4		opeq1	⊢ ( 𝑎 = 𝐴 → ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝐴 , 𝑏 ⟩ )
5	4	opeq2d	⊢ ( 𝑎 = 𝐴 → ⟨ ∅ , ⟨ 𝑎 , 𝑏 ⟩ ⟩ = ⟨ ∅ , ⟨ 𝐴 , 𝑏 ⟩ ⟩ )
6	5	eqeq2d	⊢ ( 𝑎 = 𝐴 → ( ⟨ ∅ , ⟨ 𝐴 , 𝐵 ⟩ ⟩ = ⟨ ∅ , ⟨ 𝑎 , 𝑏 ⟩ ⟩ ↔ ⟨ ∅ , ⟨ 𝐴 , 𝐵 ⟩ ⟩ = ⟨ ∅ , ⟨ 𝐴 , 𝑏 ⟩ ⟩ ) )
7	6	rexbidv	⊢ ( 𝑎 = 𝐴 → ( ∃ 𝑏 ∈ ω ⟨ ∅ , ⟨ 𝐴 , 𝐵 ⟩ ⟩ = ⟨ ∅ , ⟨ 𝑎 , 𝑏 ⟩ ⟩ ↔ ∃ 𝑏 ∈ ω ⟨ ∅ , ⟨ 𝐴 , 𝐵 ⟩ ⟩ = ⟨ ∅ , ⟨ 𝐴 , 𝑏 ⟩ ⟩ ) )
8	7	adantl	⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝑎 = 𝐴 ) → ( ∃ 𝑏 ∈ ω ⟨ ∅ , ⟨ 𝐴 , 𝐵 ⟩ ⟩ = ⟨ ∅ , ⟨ 𝑎 , 𝑏 ⟩ ⟩ ↔ ∃ 𝑏 ∈ ω ⟨ ∅ , ⟨ 𝐴 , 𝐵 ⟩ ⟩ = ⟨ ∅ , ⟨ 𝐴 , 𝑏 ⟩ ⟩ ) )
9		simpr	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → 𝐵 ∈ ω )
10		opeq2	⊢ ( 𝑏 = 𝐵 → ⟨ 𝐴 , 𝑏 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ )
11	10	opeq2d	⊢ ( 𝑏 = 𝐵 → ⟨ ∅ , ⟨ 𝐴 , 𝑏 ⟩ ⟩ = ⟨ ∅ , ⟨ 𝐴 , 𝐵 ⟩ ⟩ )
12	11	eqeq2d	⊢ ( 𝑏 = 𝐵 → ( ⟨ ∅ , ⟨ 𝐴 , 𝐵 ⟩ ⟩ = ⟨ ∅ , ⟨ 𝐴 , 𝑏 ⟩ ⟩ ↔ ⟨ ∅ , ⟨ 𝐴 , 𝐵 ⟩ ⟩ = ⟨ ∅ , ⟨ 𝐴 , 𝐵 ⟩ ⟩ ) )
13	12	adantl	⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝑏 = 𝐵 ) → ( ⟨ ∅ , ⟨ 𝐴 , 𝐵 ⟩ ⟩ = ⟨ ∅ , ⟨ 𝐴 , 𝑏 ⟩ ⟩ ↔ ⟨ ∅ , ⟨ 𝐴 , 𝐵 ⟩ ⟩ = ⟨ ∅ , ⟨ 𝐴 , 𝐵 ⟩ ⟩ ) )
14		eqidd	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ⟨ ∅ , ⟨ 𝐴 , 𝐵 ⟩ ⟩ = ⟨ ∅ , ⟨ 𝐴 , 𝐵 ⟩ ⟩ )
15	9 13 14	rspcedvd	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ∃ 𝑏 ∈ ω ⟨ ∅ , ⟨ 𝐴 , 𝐵 ⟩ ⟩ = ⟨ ∅ , ⟨ 𝐴 , 𝑏 ⟩ ⟩ )
16	3 8 15	rspcedvd	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ∃ 𝑎 ∈ ω ∃ 𝑏 ∈ ω ⟨ ∅ , ⟨ 𝐴 , 𝐵 ⟩ ⟩ = ⟨ ∅ , ⟨ 𝑎 , 𝑏 ⟩ ⟩ )
17		goel	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴 ∈_𝑔 𝐵 ) = ⟨ ∅ , ⟨ 𝐴 , 𝐵 ⟩ ⟩ )
18		goel	⊢ ( ( 𝑎 ∈ ω ∧ 𝑏 ∈ ω ) → ( 𝑎 ∈_𝑔 𝑏 ) = ⟨ ∅ , ⟨ 𝑎 , 𝑏 ⟩ ⟩ )
19	17 18	eqeqan12d	⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ ( 𝑎 ∈ ω ∧ 𝑏 ∈ ω ) ) → ( ( 𝐴 ∈_𝑔 𝐵 ) = ( 𝑎 ∈_𝑔 𝑏 ) ↔ ⟨ ∅ , ⟨ 𝐴 , 𝐵 ⟩ ⟩ = ⟨ ∅ , ⟨ 𝑎 , 𝑏 ⟩ ⟩ ) )
20	19	2rexbidva	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( ∃ 𝑎 ∈ ω ∃ 𝑏 ∈ ω ( 𝐴 ∈_𝑔 𝐵 ) = ( 𝑎 ∈_𝑔 𝑏 ) ↔ ∃ 𝑎 ∈ ω ∃ 𝑏 ∈ ω ⟨ ∅ , ⟨ 𝐴 , 𝐵 ⟩ ⟩ = ⟨ ∅ , ⟨ 𝑎 , 𝑏 ⟩ ⟩ ) )
21	16 20	mpbird	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ∃ 𝑎 ∈ ω ∃ 𝑏 ∈ ω ( 𝐴 ∈_𝑔 𝐵 ) = ( 𝑎 ∈_𝑔 𝑏 ) )
22		eqeq1	⊢ ( 𝑥 = ( 𝐴 ∈_𝑔 𝐵 ) → ( 𝑥 = ( 𝑎 ∈_𝑔 𝑏 ) ↔ ( 𝐴 ∈_𝑔 𝐵 ) = ( 𝑎 ∈_𝑔 𝑏 ) ) )
23	22	2rexbidv	⊢ ( 𝑥 = ( 𝐴 ∈_𝑔 𝐵 ) → ( ∃ 𝑎 ∈ ω ∃ 𝑏 ∈ ω 𝑥 = ( 𝑎 ∈_𝑔 𝑏 ) ↔ ∃ 𝑎 ∈ ω ∃ 𝑏 ∈ ω ( 𝐴 ∈_𝑔 𝐵 ) = ( 𝑎 ∈_𝑔 𝑏 ) ) )
24		fmla0	⊢ ( Fmla ‘ ∅ ) = { 𝑥 ∈ V ∣ ∃ 𝑎 ∈ ω ∃ 𝑏 ∈ ω 𝑥 = ( 𝑎 ∈_𝑔 𝑏 ) }
25	23 24	elrab2	⊢ ( ( 𝐴 ∈_𝑔 𝐵 ) ∈ ( Fmla ‘ ∅ ) ↔ ( ( 𝐴 ∈_𝑔 𝐵 ) ∈ V ∧ ∃ 𝑎 ∈ ω ∃ 𝑏 ∈ ω ( 𝐴 ∈_𝑔 𝐵 ) = ( 𝑎 ∈_𝑔 𝑏 ) ) )
26	2 21 25	sylanbrc	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴 ∈_𝑔 𝐵 ) ∈ ( Fmla ‘ ∅ ) )
27		satefvfmla0	⊢ ( ( 𝑀 ∈ 𝑉 ∧ ( 𝐴 ∈_𝑔 𝐵 ) ∈ ( Fmla ‘ ∅ ) ) → ( 𝑀 Sat_∈ ( 𝐴 ∈_𝑔 𝐵 ) ) = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ ( 1^st ‘ ( 2^nd ‘ ( 𝐴 ∈_𝑔 𝐵 ) ) ) ) ∈ ( 𝑎 ‘ ( 2^nd ‘ ( 2^nd ‘ ( 𝐴 ∈_𝑔 𝐵 ) ) ) ) } )
28	26 27	sylan2	⊢ ( ( 𝑀 ∈ 𝑉 ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) → ( 𝑀 Sat_∈ ( 𝐴 ∈_𝑔 𝐵 ) ) = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ ( 1^st ‘ ( 2^nd ‘ ( 𝐴 ∈_𝑔 𝐵 ) ) ) ) ∈ ( 𝑎 ‘ ( 2^nd ‘ ( 2^nd ‘ ( 𝐴 ∈_𝑔 𝐵 ) ) ) ) } )
29	1 28	syl5eq	⊢ ( ( 𝑀 ∈ 𝑉 ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) → 𝐸 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ ( 1^st ‘ ( 2^nd ‘ ( 𝐴 ∈_𝑔 𝐵 ) ) ) ) ∈ ( 𝑎 ‘ ( 2^nd ‘ ( 2^nd ‘ ( 𝐴 ∈_𝑔 𝐵 ) ) ) ) } )
30	29	eleq2d	⊢ ( ( 𝑀 ∈ 𝑉 ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) → ( 𝑆 ∈ 𝐸 ↔ 𝑆 ∈ { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ ( 1^st ‘ ( 2^nd ‘ ( 𝐴 ∈_𝑔 𝐵 ) ) ) ) ∈ ( 𝑎 ‘ ( 2^nd ‘ ( 2^nd ‘ ( 𝐴 ∈_𝑔 𝐵 ) ) ) ) } ) )
31		fveq1	⊢ ( 𝑎 = 𝑆 → ( 𝑎 ‘ ( 1^st ‘ ( 2^nd ‘ ( 𝐴 ∈_𝑔 𝐵 ) ) ) ) = ( 𝑆 ‘ ( 1^st ‘ ( 2^nd ‘ ( 𝐴 ∈_𝑔 𝐵 ) ) ) ) )
32		fveq1	⊢ ( 𝑎 = 𝑆 → ( 𝑎 ‘ ( 2^nd ‘ ( 2^nd ‘ ( 𝐴 ∈_𝑔 𝐵 ) ) ) ) = ( 𝑆 ‘ ( 2^nd ‘ ( 2^nd ‘ ( 𝐴 ∈_𝑔 𝐵 ) ) ) ) )
33	31 32	eleq12d	⊢ ( 𝑎 = 𝑆 → ( ( 𝑎 ‘ ( 1^st ‘ ( 2^nd ‘ ( 𝐴 ∈_𝑔 𝐵 ) ) ) ) ∈ ( 𝑎 ‘ ( 2^nd ‘ ( 2^nd ‘ ( 𝐴 ∈_𝑔 𝐵 ) ) ) ) ↔ ( 𝑆 ‘ ( 1^st ‘ ( 2^nd ‘ ( 𝐴 ∈_𝑔 𝐵 ) ) ) ) ∈ ( 𝑆 ‘ ( 2^nd ‘ ( 2^nd ‘ ( 𝐴 ∈_𝑔 𝐵 ) ) ) ) ) )
34	33	elrab	⊢ ( 𝑆 ∈ { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ ( 1^st ‘ ( 2^nd ‘ ( 𝐴 ∈_𝑔 𝐵 ) ) ) ) ∈ ( 𝑎 ‘ ( 2^nd ‘ ( 2^nd ‘ ( 𝐴 ∈_𝑔 𝐵 ) ) ) ) } ↔ ( 𝑆 ∈ ( 𝑀 ↑_m ω ) ∧ ( 𝑆 ‘ ( 1^st ‘ ( 2^nd ‘ ( 𝐴 ∈_𝑔 𝐵 ) ) ) ) ∈ ( 𝑆 ‘ ( 2^nd ‘ ( 2^nd ‘ ( 𝐴 ∈_𝑔 𝐵 ) ) ) ) ) )
35	30 34	bitrdi	⊢ ( ( 𝑀 ∈ 𝑉 ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) → ( 𝑆 ∈ 𝐸 ↔ ( 𝑆 ∈ ( 𝑀 ↑_m ω ) ∧ ( 𝑆 ‘ ( 1^st ‘ ( 2^nd ‘ ( 𝐴 ∈_𝑔 𝐵 ) ) ) ) ∈ ( 𝑆 ‘ ( 2^nd ‘ ( 2^nd ‘ ( 𝐴 ∈_𝑔 𝐵 ) ) ) ) ) ) )
36	17	fveq2d	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 2^nd ‘ ( 𝐴 ∈_𝑔 𝐵 ) ) = ( 2^nd ‘ ⟨ ∅ , ⟨ 𝐴 , 𝐵 ⟩ ⟩ ) )
37	36	fveq2d	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 1^st ‘ ( 2^nd ‘ ( 𝐴 ∈_𝑔 𝐵 ) ) ) = ( 1^st ‘ ( 2^nd ‘ ⟨ ∅ , ⟨ 𝐴 , 𝐵 ⟩ ⟩ ) ) )
38		0ex	⊢ ∅ ∈ V
39		opex	⊢ ⟨ 𝐴 , 𝐵 ⟩ ∈ V
40	38 39	op2nd	⊢ ( 2^nd ‘ ⟨ ∅ , ⟨ 𝐴 , 𝐵 ⟩ ⟩ ) = ⟨ 𝐴 , 𝐵 ⟩
41	40	fveq2i	⊢ ( 1^st ‘ ( 2^nd ‘ ⟨ ∅ , ⟨ 𝐴 , 𝐵 ⟩ ⟩ ) ) = ( 1^st ‘ ⟨ 𝐴 , 𝐵 ⟩ )
42		op1stg	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 1^st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝐴 )
43	41 42	syl5eq	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 1^st ‘ ( 2^nd ‘ ⟨ ∅ , ⟨ 𝐴 , 𝐵 ⟩ ⟩ ) ) = 𝐴 )
44	37 43	eqtrd	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 1^st ‘ ( 2^nd ‘ ( 𝐴 ∈_𝑔 𝐵 ) ) ) = 𝐴 )
45	44	fveq2d	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝑆 ‘ ( 1^st ‘ ( 2^nd ‘ ( 𝐴 ∈_𝑔 𝐵 ) ) ) ) = ( 𝑆 ‘ 𝐴 ) )
46	36	fveq2d	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 2^nd ‘ ( 2^nd ‘ ( 𝐴 ∈_𝑔 𝐵 ) ) ) = ( 2^nd ‘ ( 2^nd ‘ ⟨ ∅ , ⟨ 𝐴 , 𝐵 ⟩ ⟩ ) ) )
47	40	fveq2i	⊢ ( 2^nd ‘ ( 2^nd ‘ ⟨ ∅ , ⟨ 𝐴 , 𝐵 ⟩ ⟩ ) ) = ( 2^nd ‘ ⟨ 𝐴 , 𝐵 ⟩ )
48		op2ndg	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 2^nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝐵 )
49	47 48	syl5eq	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 2^nd ‘ ( 2^nd ‘ ⟨ ∅ , ⟨ 𝐴 , 𝐵 ⟩ ⟩ ) ) = 𝐵 )
50	46 49	eqtrd	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 2^nd ‘ ( 2^nd ‘ ( 𝐴 ∈_𝑔 𝐵 ) ) ) = 𝐵 )
51	50	fveq2d	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝑆 ‘ ( 2^nd ‘ ( 2^nd ‘ ( 𝐴 ∈_𝑔 𝐵 ) ) ) ) = ( 𝑆 ‘ 𝐵 ) )
52	45 51	eleq12d	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( ( 𝑆 ‘ ( 1^st ‘ ( 2^nd ‘ ( 𝐴 ∈_𝑔 𝐵 ) ) ) ) ∈ ( 𝑆 ‘ ( 2^nd ‘ ( 2^nd ‘ ( 𝐴 ∈_𝑔 𝐵 ) ) ) ) ↔ ( 𝑆 ‘ 𝐴 ) ∈ ( 𝑆 ‘ 𝐵 ) ) )
53	52	adantl	⊢ ( ( 𝑀 ∈ 𝑉 ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) → ( ( 𝑆 ‘ ( 1^st ‘ ( 2^nd ‘ ( 𝐴 ∈_𝑔 𝐵 ) ) ) ) ∈ ( 𝑆 ‘ ( 2^nd ‘ ( 2^nd ‘ ( 𝐴 ∈_𝑔 𝐵 ) ) ) ) ↔ ( 𝑆 ‘ 𝐴 ) ∈ ( 𝑆 ‘ 𝐵 ) ) )
54	53	anbi2d	⊢ ( ( 𝑀 ∈ 𝑉 ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) → ( ( 𝑆 ∈ ( 𝑀 ↑_m ω ) ∧ ( 𝑆 ‘ ( 1^st ‘ ( 2^nd ‘ ( 𝐴 ∈_𝑔 𝐵 ) ) ) ) ∈ ( 𝑆 ‘ ( 2^nd ‘ ( 2^nd ‘ ( 𝐴 ∈_𝑔 𝐵 ) ) ) ) ) ↔ ( 𝑆 ∈ ( 𝑀 ↑_m ω ) ∧ ( 𝑆 ‘ 𝐴 ) ∈ ( 𝑆 ‘ 𝐵 ) ) ) )
55	35 54	bitrd	⊢ ( ( 𝑀 ∈ 𝑉 ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) → ( 𝑆 ∈ 𝐸 ↔ ( 𝑆 ∈ ( 𝑀 ↑_m ω ) ∧ ( 𝑆 ‘ 𝐴 ) ∈ ( 𝑆 ‘ 𝐵 ) ) ) )

Metamath Proof Explorer

Theorem sategoelfvb

Proof