satef

Description: The simplified satisfaction predicate as function over wff codes over an empty model. (Contributed by AV, 30-Oct-2023)

		Ref	Expression
	Assertion	satef	$⊢ (M \in V \land U \in Fmla (ω) \land S \in (M {Sat}_{\in} U)) \to S : ω ⟶ M$

Proof

Step	Hyp	Ref	Expression
1		satefv	$⊢ (M \in V \land U \in Fmla (ω)) \to M {Sat}_{\in} U = (M Sat (E \cap (M \times M))) (ω) (U)$
2	1	eleq2d	$⊢ (M \in V \land U \in Fmla (ω)) \to (S \in (M {Sat}_{\in} U) \leftrightarrow S \in (M Sat (E \cap (M \times M))) (ω) (U))$
3		simpl	$⊢ (M \in V \land U \in Fmla (ω)) \to M \in V$
4		incom	$⊢ E \cap (M \times M) = (M \times M) \cap E$
5		sqxpexg	$⊢ M \in V \to M \times M \in V$
6	5	adantr	$⊢ (M \in V \land U \in Fmla (ω)) \to M \times M \in V$
7		inex1g	$⊢ M \times M \in V \to (M \times M) \cap E \in V$
8	6 7	syl	$⊢ (M \in V \land U \in Fmla (ω)) \to (M \times M) \cap E \in V$
9	4 8	eqeltrid	$⊢ (M \in V \land U \in Fmla (ω)) \to E \cap (M \times M) \in V$
10	3 9	jca	$⊢ (M \in V \land U \in Fmla (ω)) \to (M \in V \land E \cap (M \times M) \in V)$
11	10	adantr	$⊢ ((M \in V \land U \in Fmla (ω)) \land S \in (M Sat (E \cap (M \times M))) (ω) (U)) \to (M \in V \land E \cap (M \times M) \in V)$
12		simpr	$⊢ (M \in V \land U \in Fmla (ω)) \to U \in Fmla (ω)$
13	12	adantr	$⊢ ((M \in V \land U \in Fmla (ω)) \land S \in (M Sat (E \cap (M \times M))) (ω) (U)) \to U \in Fmla (ω)$
14		simpr	$⊢ ((M \in V \land U \in Fmla (ω)) \land S \in (M Sat (E \cap (M \times M))) (ω) (U)) \to S \in (M Sat (E \cap (M \times M))) (ω) (U)$
15	11 13 14	3jca	$⊢ ((M \in V \land U \in Fmla (ω)) \land S \in (M Sat (E \cap (M \times M))) (ω) (U)) \to ((M \in V \land E \cap (M \times M) \in V) \land U \in Fmla (ω) \land S \in (M Sat (E \cap (M \times M))) (ω) (U))$
16	15	ex	$⊢ (M \in V \land U \in Fmla (ω)) \to (S \in (M Sat (E \cap (M \times M))) (ω) (U) \to ((M \in V \land E \cap (M \times M) \in V) \land U \in Fmla (ω) \land S \in (M Sat (E \cap (M \times M))) (ω) (U)))$
17	2 16	sylbid	$⊢ (M \in V \land U \in Fmla (ω)) \to (S \in (M {Sat}_{\in} U) \to ((M \in V \land E \cap (M \times M) \in V) \land U \in Fmla (ω) \land S \in (M Sat (E \cap (M \times M))) (ω) (U)))$
18	17	3impia	$⊢ (M \in V \land U \in Fmla (ω) \land S \in (M {Sat}_{\in} U)) \to ((M \in V \land E \cap (M \times M) \in V) \land U \in Fmla (ω) \land S \in (M Sat (E \cap (M \times M))) (ω) (U))$
19		satfvel	$⊢ ((M \in V \land E \cap (M \times M) \in V) \land U \in Fmla (ω) \land S \in (M Sat (E \cap (M \times M))) (ω) (U)) \to S : ω ⟶ M$
20	18 19	syl	$⊢ (M \in V \land U \in Fmla (ω) \land S \in (M {Sat}_{\in} U)) \to S : ω ⟶ M$

Metamath Proof Explorer

Theorem satef

Proof