satfv0fvfmla0

Description: The value of the satisfaction predicate as function over a wff code at (/) . (Contributed by AV, 2-Nov-2023)

		Ref	Expression
	Hypothesis	satfv0fv.s	⊢ 𝑆 = ( 𝑀 Sat 𝐸 )
	Assertion	satfv0fvfmla0	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑋 ∈ ( Fmla ‘ ∅ ) ) → ( ( 𝑆 ‘ ∅ ) ‘ 𝑋 ) = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ ( 1^st ‘ ( 2^nd ‘ 𝑋 ) ) ) 𝐸 ( 𝑎 ‘ ( 2^nd ‘ ( 2^nd ‘ 𝑋 ) ) ) } )

Proof

Step	Hyp	Ref	Expression
1		satfv0fv.s	⊢ 𝑆 = ( 𝑀 Sat 𝐸 )
2		satfv0fun	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → Fun ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) )
3	1	fveq1i	⊢ ( 𝑆 ‘ ∅ ) = ( ( 𝑀 Sat 𝐸 ) ‘ ∅ )
4	3	funeqi	⊢ ( Fun ( 𝑆 ‘ ∅ ) ↔ Fun ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) )
5	2 4	sylibr	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → Fun ( 𝑆 ‘ ∅ ) )
6	5	3adant3	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑋 ∈ ( Fmla ‘ ∅ ) ) → Fun ( 𝑆 ‘ ∅ ) )
7		fmla0	⊢ ( Fmla ‘ ∅ ) = { 𝑥 ∈ V ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) }
8	7	eleq2i	⊢ ( 𝑋 ∈ ( Fmla ‘ ∅ ) ↔ 𝑋 ∈ { 𝑥 ∈ V ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) } )
9		eqeq1	⊢ ( 𝑥 = 𝑋 → ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ↔ 𝑋 = ( 𝑖 ∈_𝑔 𝑗 ) ) )
10	9	2rexbidv	⊢ ( 𝑥 = 𝑋 → ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ↔ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑋 = ( 𝑖 ∈_𝑔 𝑗 ) ) )
11	10	elrab	⊢ ( 𝑋 ∈ { 𝑥 ∈ V ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) } ↔ ( 𝑋 ∈ V ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑋 = ( 𝑖 ∈_𝑔 𝑗 ) ) )
12	8 11	bitri	⊢ ( 𝑋 ∈ ( Fmla ‘ ∅ ) ↔ ( 𝑋 ∈ V ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑋 = ( 𝑖 ∈_𝑔 𝑗 ) ) )
13		simpr	⊢ ( ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) ∧ 𝑋 = ( 𝑖 ∈_𝑔 𝑗 ) ) → 𝑋 = ( 𝑖 ∈_𝑔 𝑗 ) )
14		goel	⊢ ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) → ( 𝑖 ∈_𝑔 𝑗 ) = ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ )
15	14	eqeq2d	⊢ ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) → ( 𝑋 = ( 𝑖 ∈_𝑔 𝑗 ) ↔ 𝑋 = ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ ) )
16		2fveq3	⊢ ( 𝑋 = ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ → ( 1^st ‘ ( 2^nd ‘ 𝑋 ) ) = ( 1^st ‘ ( 2^nd ‘ ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ ) ) )
17		0ex	⊢ ∅ ∈ V
18		opex	⊢ ⟨ 𝑖 , 𝑗 ⟩ ∈ V
19	17 18	op2nd	⊢ ( 2^nd ‘ ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ ) = ⟨ 𝑖 , 𝑗 ⟩
20	19	fveq2i	⊢ ( 1^st ‘ ( 2^nd ‘ ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ ) ) = ( 1^st ‘ ⟨ 𝑖 , 𝑗 ⟩ )
21		vex	⊢ 𝑖 ∈ V
22		vex	⊢ 𝑗 ∈ V
23	21 22	op1st	⊢ ( 1^st ‘ ⟨ 𝑖 , 𝑗 ⟩ ) = 𝑖
24	20 23	eqtri	⊢ ( 1^st ‘ ( 2^nd ‘ ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ ) ) = 𝑖
25	16 24	eqtrdi	⊢ ( 𝑋 = ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ → ( 1^st ‘ ( 2^nd ‘ 𝑋 ) ) = 𝑖 )
26	25	fveq2d	⊢ ( 𝑋 = ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ → ( 𝑎 ‘ ( 1^st ‘ ( 2^nd ‘ 𝑋 ) ) ) = ( 𝑎 ‘ 𝑖 ) )
27		2fveq3	⊢ ( 𝑋 = ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ → ( 2^nd ‘ ( 2^nd ‘ 𝑋 ) ) = ( 2^nd ‘ ( 2^nd ‘ ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ ) ) )
28	19	fveq2i	⊢ ( 2^nd ‘ ( 2^nd ‘ ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ ) ) = ( 2^nd ‘ ⟨ 𝑖 , 𝑗 ⟩ )
29	21 22	op2nd	⊢ ( 2^nd ‘ ⟨ 𝑖 , 𝑗 ⟩ ) = 𝑗
30	28 29	eqtri	⊢ ( 2^nd ‘ ( 2^nd ‘ ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ ) ) = 𝑗
31	27 30	eqtrdi	⊢ ( 𝑋 = ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ → ( 2^nd ‘ ( 2^nd ‘ 𝑋 ) ) = 𝑗 )
32	31	fveq2d	⊢ ( 𝑋 = ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ → ( 𝑎 ‘ ( 2^nd ‘ ( 2^nd ‘ 𝑋 ) ) ) = ( 𝑎 ‘ 𝑗 ) )
33	26 32	breq12d	⊢ ( 𝑋 = ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ → ( ( 𝑎 ‘ ( 1^st ‘ ( 2^nd ‘ 𝑋 ) ) ) 𝐸 ( 𝑎 ‘ ( 2^nd ‘ ( 2^nd ‘ 𝑋 ) ) ) ↔ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) )
34	15 33	syl6bi	⊢ ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) → ( 𝑋 = ( 𝑖 ∈_𝑔 𝑗 ) → ( ( 𝑎 ‘ ( 1^st ‘ ( 2^nd ‘ 𝑋 ) ) ) 𝐸 ( 𝑎 ‘ ( 2^nd ‘ ( 2^nd ‘ 𝑋 ) ) ) ↔ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) ) )
35	34	imp	⊢ ( ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) ∧ 𝑋 = ( 𝑖 ∈_𝑔 𝑗 ) ) → ( ( 𝑎 ‘ ( 1^st ‘ ( 2^nd ‘ 𝑋 ) ) ) 𝐸 ( 𝑎 ‘ ( 2^nd ‘ ( 2^nd ‘ 𝑋 ) ) ) ↔ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) )
36	35	rabbidv	⊢ ( ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) ∧ 𝑋 = ( 𝑖 ∈_𝑔 𝑗 ) ) → { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ ( 1^st ‘ ( 2^nd ‘ 𝑋 ) ) ) 𝐸 ( 𝑎 ‘ ( 2^nd ‘ ( 2^nd ‘ 𝑋 ) ) ) } = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } )
37	13 36	jca	⊢ ( ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) ∧ 𝑋 = ( 𝑖 ∈_𝑔 𝑗 ) ) → ( 𝑋 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ ( 1^st ‘ ( 2^nd ‘ 𝑋 ) ) ) 𝐸 ( 𝑎 ‘ ( 2^nd ‘ ( 2^nd ‘ 𝑋 ) ) ) } = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) )
38	37	ex	⊢ ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) → ( 𝑋 = ( 𝑖 ∈_𝑔 𝑗 ) → ( 𝑋 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ ( 1^st ‘ ( 2^nd ‘ 𝑋 ) ) ) 𝐸 ( 𝑎 ‘ ( 2^nd ‘ ( 2^nd ‘ 𝑋 ) ) ) } = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) ) )
39	38	reximdva	⊢ ( 𝑖 ∈ ω → ( ∃ 𝑗 ∈ ω 𝑋 = ( 𝑖 ∈_𝑔 𝑗 ) → ∃ 𝑗 ∈ ω ( 𝑋 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ ( 1^st ‘ ( 2^nd ‘ 𝑋 ) ) ) 𝐸 ( 𝑎 ‘ ( 2^nd ‘ ( 2^nd ‘ 𝑋 ) ) ) } = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) ) )
40	39	reximia	⊢ ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑋 = ( 𝑖 ∈_𝑔 𝑗 ) → ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑋 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ ( 1^st ‘ ( 2^nd ‘ 𝑋 ) ) ) 𝐸 ( 𝑎 ‘ ( 2^nd ‘ ( 2^nd ‘ 𝑋 ) ) ) } = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) )
41	12 40	simplbiim	⊢ ( 𝑋 ∈ ( Fmla ‘ ∅ ) → ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑋 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ ( 1^st ‘ ( 2^nd ‘ 𝑋 ) ) ) 𝐸 ( 𝑎 ‘ ( 2^nd ‘ ( 2^nd ‘ 𝑋 ) ) ) } = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) )
42	41	3ad2ant3	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑋 ∈ ( Fmla ‘ ∅ ) ) → ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑋 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ ( 1^st ‘ ( 2^nd ‘ 𝑋 ) ) ) 𝐸 ( 𝑎 ‘ ( 2^nd ‘ ( 2^nd ‘ 𝑋 ) ) ) } = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) )
43		simp3	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑋 ∈ ( Fmla ‘ ∅ ) ) → 𝑋 ∈ ( Fmla ‘ ∅ ) )
44		ovex	⊢ ( 𝑀 ↑_m ω ) ∈ V
45	44	rabex	⊢ { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ ( 1^st ‘ ( 2^nd ‘ 𝑋 ) ) ) 𝐸 ( 𝑎 ‘ ( 2^nd ‘ ( 2^nd ‘ 𝑋 ) ) ) } ∈ V
46		eqeq1	⊢ ( 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ ( 1^st ‘ ( 2^nd ‘ 𝑋 ) ) ) 𝐸 ( 𝑎 ‘ ( 2^nd ‘ ( 2^nd ‘ 𝑋 ) ) ) } → ( 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ↔ { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ ( 1^st ‘ ( 2^nd ‘ 𝑋 ) ) ) 𝐸 ( 𝑎 ‘ ( 2^nd ‘ ( 2^nd ‘ 𝑋 ) ) ) } = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) )
47	9 46	bi2anan9	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ ( 1^st ‘ ( 2^nd ‘ 𝑋 ) ) ) 𝐸 ( 𝑎 ‘ ( 2^nd ‘ ( 2^nd ‘ 𝑋 ) ) ) } ) → ( ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) ↔ ( 𝑋 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ ( 1^st ‘ ( 2^nd ‘ 𝑋 ) ) ) 𝐸 ( 𝑎 ‘ ( 2^nd ‘ ( 2^nd ‘ 𝑋 ) ) ) } = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) ) )
48	47	2rexbidv	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ ( 1^st ‘ ( 2^nd ‘ 𝑋 ) ) ) 𝐸 ( 𝑎 ‘ ( 2^nd ‘ ( 2^nd ‘ 𝑋 ) ) ) } ) → ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) ↔ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑋 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ ( 1^st ‘ ( 2^nd ‘ 𝑋 ) ) ) 𝐸 ( 𝑎 ‘ ( 2^nd ‘ ( 2^nd ‘ 𝑋 ) ) ) } = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) ) )
49	48	opelopabga	⊢ ( ( 𝑋 ∈ ( Fmla ‘ ∅ ) ∧ { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ ( 1^st ‘ ( 2^nd ‘ 𝑋 ) ) ) 𝐸 ( 𝑎 ‘ ( 2^nd ‘ ( 2^nd ‘ 𝑋 ) ) ) } ∈ V ) → ( ⟨ 𝑋 , { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ ( 1^st ‘ ( 2^nd ‘ 𝑋 ) ) ) 𝐸 ( 𝑎 ‘ ( 2^nd ‘ ( 2^nd ‘ 𝑋 ) ) ) } ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) } ↔ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑋 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ ( 1^st ‘ ( 2^nd ‘ 𝑋 ) ) ) 𝐸 ( 𝑎 ‘ ( 2^nd ‘ ( 2^nd ‘ 𝑋 ) ) ) } = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) ) )
50	43 45 49	sylancl	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑋 ∈ ( Fmla ‘ ∅ ) ) → ( ⟨ 𝑋 , { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ ( 1^st ‘ ( 2^nd ‘ 𝑋 ) ) ) 𝐸 ( 𝑎 ‘ ( 2^nd ‘ ( 2^nd ‘ 𝑋 ) ) ) } ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) } ↔ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑋 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ ( 1^st ‘ ( 2^nd ‘ 𝑋 ) ) ) 𝐸 ( 𝑎 ‘ ( 2^nd ‘ ( 2^nd ‘ 𝑋 ) ) ) } = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) ) )
51	42 50	mpbird	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑋 ∈ ( Fmla ‘ ∅ ) ) → ⟨ 𝑋 , { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ ( 1^st ‘ ( 2^nd ‘ 𝑋 ) ) ) 𝐸 ( 𝑎 ‘ ( 2^nd ‘ ( 2^nd ‘ 𝑋 ) ) ) } ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) } )
52	1	satfv0	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( 𝑆 ‘ ∅ ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) } )
53	52	eleq2d	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( ⟨ 𝑋 , { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ ( 1^st ‘ ( 2^nd ‘ 𝑋 ) ) ) 𝐸 ( 𝑎 ‘ ( 2^nd ‘ ( 2^nd ‘ 𝑋 ) ) ) } ⟩ ∈ ( 𝑆 ‘ ∅ ) ↔ ⟨ 𝑋 , { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ ( 1^st ‘ ( 2^nd ‘ 𝑋 ) ) ) 𝐸 ( 𝑎 ‘ ( 2^nd ‘ ( 2^nd ‘ 𝑋 ) ) ) } ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) } ) )
54	53	3adant3	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑋 ∈ ( Fmla ‘ ∅ ) ) → ( ⟨ 𝑋 , { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ ( 1^st ‘ ( 2^nd ‘ 𝑋 ) ) ) 𝐸 ( 𝑎 ‘ ( 2^nd ‘ ( 2^nd ‘ 𝑋 ) ) ) } ⟩ ∈ ( 𝑆 ‘ ∅ ) ↔ ⟨ 𝑋 , { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ ( 1^st ‘ ( 2^nd ‘ 𝑋 ) ) ) 𝐸 ( 𝑎 ‘ ( 2^nd ‘ ( 2^nd ‘ 𝑋 ) ) ) } ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) } ) )
55	51 54	mpbird	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑋 ∈ ( Fmla ‘ ∅ ) ) → ⟨ 𝑋 , { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ ( 1^st ‘ ( 2^nd ‘ 𝑋 ) ) ) 𝐸 ( 𝑎 ‘ ( 2^nd ‘ ( 2^nd ‘ 𝑋 ) ) ) } ⟩ ∈ ( 𝑆 ‘ ∅ ) )
56		funopfv	⊢ ( Fun ( 𝑆 ‘ ∅ ) → ( ⟨ 𝑋 , { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ ( 1^st ‘ ( 2^nd ‘ 𝑋 ) ) ) 𝐸 ( 𝑎 ‘ ( 2^nd ‘ ( 2^nd ‘ 𝑋 ) ) ) } ⟩ ∈ ( 𝑆 ‘ ∅ ) → ( ( 𝑆 ‘ ∅ ) ‘ 𝑋 ) = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ ( 1^st ‘ ( 2^nd ‘ 𝑋 ) ) ) 𝐸 ( 𝑎 ‘ ( 2^nd ‘ ( 2^nd ‘ 𝑋 ) ) ) } ) )
57	6 55 56	sylc	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑋 ∈ ( Fmla ‘ ∅ ) ) → ( ( 𝑆 ‘ ∅ ) ‘ 𝑋 ) = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ ( 1^st ‘ ( 2^nd ‘ 𝑋 ) ) ) 𝐸 ( 𝑎 ‘ ( 2^nd ‘ ( 2^nd ‘ 𝑋 ) ) ) } )

Metamath Proof Explorer

Theorem satfv0fvfmla0

Proof