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	$⊢ (M \in V \land U \in W) \to M {Sat}_{\in} U = (M Sat (E \cap (M \times M))) (ω) (U)$

Step	Hyp	Ref	Expression
1		df-sate	$⊢ {Sat}_{\in} = (m \in V, u \in V ⟼ (m Sat (E \cap (m \times m))) (ω) (u))$
2	1	a1i	$⊢ (M \in V \land U \in W) \to {Sat}_{\in} = (m \in V, u \in V ⟼ (m Sat (E \cap (m \times m))) (ω) (u))$
3		id	$⊢ m = M \to m = M$
4	3	sqxpeqd	$⊢ m = M \to m \times m = M \times M$
5	4	ineq2d	$⊢ m = M \to E \cap (m \times m) = E \cap (M \times M)$
6	3 5	oveq12d	$⊢ m = M \to m Sat (E \cap (m \times m)) = M Sat (E \cap (M \times M))$
7	6	fveq1d	$⊢ m = M \to (m Sat (E \cap (m \times m))) (ω) = (M Sat (E \cap (M \times M))) (ω)$
8	7	adantr	$⊢ (m = M \land u = U) \to (m Sat (E \cap (m \times m))) (ω) = (M Sat (E \cap (M \times M))) (ω)$
9		simpr	$⊢ (m = M \land u = U) \to u = U$
10	8 9	fveq12d	$⊢ (m = M \land u = U) \to (m Sat (E \cap (m \times m))) (ω) (u) = (M Sat (E \cap (M \times M))) (ω) (U)$
11	10	adantl	$⊢ ((M \in V \land U \in W) \land (m = M \land u = U)) \to (m Sat (E \cap (m \times m))) (ω) (u) = (M Sat (E \cap (M \times M))) (ω) (U)$
12		elex	$⊢ M \in V \to M \in V$
13	12	adantr	$⊢ (M \in V \land U \in W) \to M \in V$
14		elex	$⊢ U \in W \to U \in V$
15	14	adantl	$⊢ (M \in V \land U \in W) \to U \in V$
16		fvexd	$⊢ (M \in V \land U \in W) \to (M Sat (E \cap (M \times M))) (ω) (U) \in V$
17	2 11 13 15 16	ovmpod	$⊢ (M \in V \land U \in W) \to M {Sat}_{\in} U = (M Sat (E \cap (M \times M))) (ω) (U)$

Metamath Proof Explorer