Theorem satefv

Description: The simplified satisfaction predicate as function over wff codes in the model M at the code U . (Contributed by AV, 30-Oct-2023)

	Ref	Expression
Assertion	satefv	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝑈 ∈ 𝑊 ) → ( 𝑀 Sat∈ 𝑈 ) = ( ( ( 𝑀 Sat ( E ∩ ( 𝑀 × 𝑀 ) ) ) ‘ ω ) ‘ 𝑈 ) )

Proof

Step	Hyp	Ref	Expression
1		df-sate	⊢ Sat∈ = ( 𝑚 ∈ V , 𝑢 ∈ V ↦ ( ( ( 𝑚 Sat ( E ∩ ( 𝑚 × 𝑚 ) ) ) ‘ ω ) ‘ 𝑢 ) )
2	1	a1i	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝑈 ∈ 𝑊 ) → Sat∈ = ( 𝑚 ∈ V , 𝑢 ∈ V ↦ ( ( ( 𝑚 Sat ( E ∩ ( 𝑚 × 𝑚 ) ) ) ‘ ω ) ‘ 𝑢 ) ) )
3		id	⊢ ( 𝑚 = 𝑀 → 𝑚 = 𝑀 )
4	3	sqxpeqd	⊢ ( 𝑚 = 𝑀 → ( 𝑚 × 𝑚 ) = ( 𝑀 × 𝑀 ) )
5	4	ineq2d	⊢ ( 𝑚 = 𝑀 → ( E ∩ ( 𝑚 × 𝑚 ) ) = ( E ∩ ( 𝑀 × 𝑀 ) ) )
6	3 5	oveq12d	⊢ ( 𝑚 = 𝑀 → ( 𝑚 Sat ( E ∩ ( 𝑚 × 𝑚 ) ) ) = ( 𝑀 Sat ( E ∩ ( 𝑀 × 𝑀 ) ) ) )
7	6	fveq1d	⊢ ( 𝑚 = 𝑀 → ( ( 𝑚 Sat ( E ∩ ( 𝑚 × 𝑚 ) ) ) ‘ ω ) = ( ( 𝑀 Sat ( E ∩ ( 𝑀 × 𝑀 ) ) ) ‘ ω ) )
8	7	adantr	⊢ ( ( 𝑚 = 𝑀 ∧ 𝑢 = 𝑈 ) → ( ( 𝑚 Sat ( E ∩ ( 𝑚 × 𝑚 ) ) ) ‘ ω ) = ( ( 𝑀 Sat ( E ∩ ( 𝑀 × 𝑀 ) ) ) ‘ ω ) )
9		simpr	⊢ ( ( 𝑚 = 𝑀 ∧ 𝑢 = 𝑈 ) → 𝑢 = 𝑈 )
10	8 9	fveq12d	⊢ ( ( 𝑚 = 𝑀 ∧ 𝑢 = 𝑈 ) → ( ( ( 𝑚 Sat ( E ∩ ( 𝑚 × 𝑚 ) ) ) ‘ ω ) ‘ 𝑢 ) = ( ( ( 𝑀 Sat ( E ∩ ( 𝑀 × 𝑀 ) ) ) ‘ ω ) ‘ 𝑈 ) )
11	10	adantl	⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝑈 ∈ 𝑊 ) ∧ ( 𝑚 = 𝑀 ∧ 𝑢 = 𝑈 ) ) → ( ( ( 𝑚 Sat ( E ∩ ( 𝑚 × 𝑚 ) ) ) ‘ ω ) ‘ 𝑢 ) = ( ( ( 𝑀 Sat ( E ∩ ( 𝑀 × 𝑀 ) ) ) ‘ ω ) ‘ 𝑈 ) )
12		elex	⊢ ( 𝑀 ∈ 𝑉 → 𝑀 ∈ V )
13	12	adantr	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝑈 ∈ 𝑊 ) → 𝑀 ∈ V )
14		elex	⊢ ( 𝑈 ∈ 𝑊 → 𝑈 ∈ V )
15	14	adantl	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝑈 ∈ 𝑊 ) → 𝑈 ∈ V )
16		fvexd	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝑈 ∈ 𝑊 ) → ( ( ( 𝑀 Sat ( E ∩ ( 𝑀 × 𝑀 ) ) ) ‘ ω ) ‘ 𝑈 ) ∈ V )
17	2 11 13 15 16	ovmpod	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝑈 ∈ 𝑊 ) → ( 𝑀 Sat∈ 𝑈 ) = ( ( ( 𝑀 Sat ( E ∩ ( 𝑀 × 𝑀 ) ) ) ‘ ω ) ‘ 𝑈 ) )