This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∩ ( 𝑀 × 𝑀 ) ) ) ‘ ω ) ‘ 𝑈 ) )