Metamath Proof Explorer

Theorem 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 ∈ V ∧ U ∈ Fmla ⁡ ω ∧ S ∈ M Sat ∈ U → S : ω ⟶ M

Proof

Step Hyp Ref Expression
1 satefv ⊢ M ∈ V ∧ U ∈ Fmla ⁡ ω → M Sat ∈ U = M Sat E ∩ M × M ⁡ ω ⁡ U
2 1 eleq2d ⊢ M ∈ V ∧ U ∈ Fmla ⁡ ω → S ∈ M Sat ∈ U ↔ S ∈ M Sat E ∩ M × M ⁡ ω ⁡ U
3 simpl ⊢ M ∈ V ∧ U ∈ Fmla ⁡ ω → M ∈ V
4 incom ⊢ E ∩ M × M = M × M ∩ E
5 sqxpexg ⊢ M ∈ V → M × M ∈ V
6 5 adantr ⊢ M ∈ V ∧ U ∈ Fmla ⁡ ω → M × M ∈ V
7 inex1g ⊢ M × M ∈ V → M × M ∩ E ∈ V
8 6 7 syl ⊢ M ∈ V ∧ U ∈ Fmla ⁡ ω → M × M ∩ E ∈ V
9 4 8 eqeltrid ⊢ M ∈ V ∧ U ∈ Fmla ⁡ ω → E ∩ M × M ∈ V
10 3 9 jca ⊢ M ∈ V ∧ U ∈ Fmla ⁡ ω → M ∈ V ∧ E ∩ M × M ∈ V
11 10 adantr ⊢ M ∈ V ∧ U ∈ Fmla ⁡ ω ∧ S ∈ M Sat E ∩ M × M ⁡ ω ⁡ U → M ∈ V ∧ E ∩ M × M ∈ V
12 simpr ⊢ M ∈ V ∧ U ∈ Fmla ⁡ ω → U ∈ Fmla ⁡ ω
13 12 adantr ⊢ M ∈ V ∧ U ∈ Fmla ⁡ ω ∧ S ∈ M Sat E ∩ M × M ⁡ ω ⁡ U → U ∈ Fmla ⁡ ω
14 simpr ⊢ M ∈ V ∧ U ∈ Fmla ⁡ ω ∧ S ∈ M Sat E ∩ M × M ⁡ ω ⁡ U → S ∈ M Sat E ∩ M × M ⁡ ω ⁡ U
15 11 13 14 3jca ⊢ M ∈ V ∧ U ∈ Fmla ⁡ ω ∧ S ∈ M Sat E ∩ M × M ⁡ ω ⁡ U → M ∈ V ∧ E ∩ M × M ∈ V ∧ U ∈ Fmla ⁡ ω ∧ S ∈ M Sat E ∩ M × M ⁡ ω ⁡ U
16 15 ex ⊢ M ∈ V ∧ U ∈ Fmla ⁡ ω → S ∈ M Sat E ∩ M × M ⁡ ω ⁡ U → M ∈ V ∧ E ∩ M × M ∈ V ∧ U ∈ Fmla ⁡ ω ∧ S ∈ M Sat E ∩ M × M ⁡ ω ⁡ U
17 2 16 sylbid ⊢ M ∈ V ∧ U ∈ Fmla ⁡ ω → S ∈ M Sat ∈ U → M ∈ V ∧ E ∩ M × M ∈ V ∧ U ∈ Fmla ⁡ ω ∧ S ∈ M Sat E ∩ M × M ⁡ ω ⁡ U
18 17 3impia ⊢ M ∈ V ∧ U ∈ Fmla ⁡ ω ∧ S ∈ M Sat ∈ U → M ∈ V ∧ E ∩ M × M ∈ V ∧ U ∈ Fmla ⁡ ω ∧ S ∈ M Sat E ∩ M × M ⁡ ω ⁡ U
19 satfvel ⊢ M ∈ V ∧ E ∩ M × M ∈ V ∧ U ∈ Fmla ⁡ ω ∧ S ∈ M Sat E ∩ M × M ⁡ ω ⁡ U → S : ω ⟶ M
20 18 19 syl ⊢ M ∈ V ∧ U ∈ Fmla ⁡ ω ∧ S ∈ M Sat ∈ U → S : ω ⟶ M