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 ( ( 𝑀 ∈ 𝑉 ∧ 𝑈 ∈ ( Fmla ‘ ω ) ∧ 𝑆 ∈ ( 𝑀 Sat∈ 𝑈 ) ) → 𝑆 : ω ⟶ 𝑀 )

Proof

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