Metamath Proof Explorer


Theorem satfun

Description: The satisfaction predicate as function over wff codes in the model M and the binary relation E on M . (Contributed by AV, 29-Oct-2023)

Ref Expression
Assertion satfun ( ( 𝑀𝑉𝐸𝑊 ) → ( ( 𝑀 Sat 𝐸 ) ‘ ω ) : ( Fmla ‘ ω ) ⟶ 𝒫 ( 𝑀m ω ) )

Proof

Step Hyp Ref Expression
1 satff ( ( 𝑀𝑉𝐸𝑊𝑥 ∈ ω ) → ( ( 𝑀 Sat 𝐸 ) ‘ 𝑥 ) : ( Fmla ‘ 𝑥 ) ⟶ 𝒫 ( 𝑀m ω ) )
2 1 3expa ( ( ( 𝑀𝑉𝐸𝑊 ) ∧ 𝑥 ∈ ω ) → ( ( 𝑀 Sat 𝐸 ) ‘ 𝑥 ) : ( Fmla ‘ 𝑥 ) ⟶ 𝒫 ( 𝑀m ω ) )
3 entric ( ( 𝑥 ∈ ω ∧ 𝑦 ∈ ω ) → ( 𝑥𝑦𝑥𝑦𝑦𝑥 ) )
4 3 adantl ( ( ( 𝑀𝑉𝐸𝑊 ) ∧ ( 𝑥 ∈ ω ∧ 𝑦 ∈ ω ) ) → ( 𝑥𝑦𝑥𝑦𝑦𝑥 ) )
5 nnsdomo ( ( 𝑥 ∈ ω ∧ 𝑦 ∈ ω ) → ( 𝑥𝑦𝑥𝑦 ) )
6 5 adantl ( ( ( 𝑀𝑉𝐸𝑊 ) ∧ ( 𝑥 ∈ ω ∧ 𝑦 ∈ ω ) ) → ( 𝑥𝑦𝑥𝑦 ) )
7 pm3.22 ( ( 𝑥 ∈ ω ∧ 𝑦 ∈ ω ) → ( 𝑦 ∈ ω ∧ 𝑥 ∈ ω ) )
8 7 anim2i ( ( ( 𝑀𝑉𝐸𝑊 ) ∧ ( 𝑥 ∈ ω ∧ 𝑦 ∈ ω ) ) → ( ( 𝑀𝑉𝐸𝑊 ) ∧ ( 𝑦 ∈ ω ∧ 𝑥 ∈ ω ) ) )
9 pssss ( 𝑥𝑦𝑥𝑦 )
10 eqid ( 𝑀 Sat 𝐸 ) = ( 𝑀 Sat 𝐸 )
11 10 satfsschain ( ( ( 𝑀𝑉𝐸𝑊 ) ∧ ( 𝑦 ∈ ω ∧ 𝑥 ∈ ω ) ) → ( 𝑥𝑦 → ( ( 𝑀 Sat 𝐸 ) ‘ 𝑥 ) ⊆ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ) )
12 11 imp ( ( ( ( 𝑀𝑉𝐸𝑊 ) ∧ ( 𝑦 ∈ ω ∧ 𝑥 ∈ ω ) ) ∧ 𝑥𝑦 ) → ( ( 𝑀 Sat 𝐸 ) ‘ 𝑥 ) ⊆ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) )
13 8 9 12 syl2an ( ( ( ( 𝑀𝑉𝐸𝑊 ) ∧ ( 𝑥 ∈ ω ∧ 𝑦 ∈ ω ) ) ∧ 𝑥𝑦 ) → ( ( 𝑀 Sat 𝐸 ) ‘ 𝑥 ) ⊆ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) )
14 13 orcd ( ( ( ( 𝑀𝑉𝐸𝑊 ) ∧ ( 𝑥 ∈ ω ∧ 𝑦 ∈ ω ) ) ∧ 𝑥𝑦 ) → ( ( ( 𝑀 Sat 𝐸 ) ‘ 𝑥 ) ⊆ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ∨ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ⊆ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑥 ) ) )
15 14 ex ( ( ( 𝑀𝑉𝐸𝑊 ) ∧ ( 𝑥 ∈ ω ∧ 𝑦 ∈ ω ) ) → ( 𝑥𝑦 → ( ( ( 𝑀 Sat 𝐸 ) ‘ 𝑥 ) ⊆ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ∨ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ⊆ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑥 ) ) ) )
16 6 15 sylbid ( ( ( 𝑀𝑉𝐸𝑊 ) ∧ ( 𝑥 ∈ ω ∧ 𝑦 ∈ ω ) ) → ( 𝑥𝑦 → ( ( ( 𝑀 Sat 𝐸 ) ‘ 𝑥 ) ⊆ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ∨ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ⊆ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑥 ) ) ) )
17 nneneq ( ( 𝑥 ∈ ω ∧ 𝑦 ∈ ω ) → ( 𝑥𝑦𝑥 = 𝑦 ) )
18 17 adantl ( ( ( 𝑀𝑉𝐸𝑊 ) ∧ ( 𝑥 ∈ ω ∧ 𝑦 ∈ ω ) ) → ( 𝑥𝑦𝑥 = 𝑦 ) )
19 ssid ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ⊆ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 )
20 fveq2 ( 𝑥 = 𝑦 → ( ( 𝑀 Sat 𝐸 ) ‘ 𝑥 ) = ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) )
21 19 20 sseqtrrid ( 𝑥 = 𝑦 → ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ⊆ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑥 ) )
22 21 olcd ( 𝑥 = 𝑦 → ( ( ( 𝑀 Sat 𝐸 ) ‘ 𝑥 ) ⊆ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ∨ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ⊆ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑥 ) ) )
23 18 22 syl6bi ( ( ( 𝑀𝑉𝐸𝑊 ) ∧ ( 𝑥 ∈ ω ∧ 𝑦 ∈ ω ) ) → ( 𝑥𝑦 → ( ( ( 𝑀 Sat 𝐸 ) ‘ 𝑥 ) ⊆ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ∨ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ⊆ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑥 ) ) ) )
24 nnsdomo ( ( 𝑦 ∈ ω ∧ 𝑥 ∈ ω ) → ( 𝑦𝑥𝑦𝑥 ) )
25 24 ancoms ( ( 𝑥 ∈ ω ∧ 𝑦 ∈ ω ) → ( 𝑦𝑥𝑦𝑥 ) )
26 25 adantl ( ( ( 𝑀𝑉𝐸𝑊 ) ∧ ( 𝑥 ∈ ω ∧ 𝑦 ∈ ω ) ) → ( 𝑦𝑥𝑦𝑥 ) )
27 10 satfsschain ( ( ( 𝑀𝑉𝐸𝑊 ) ∧ ( 𝑥 ∈ ω ∧ 𝑦 ∈ ω ) ) → ( 𝑦𝑥 → ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ⊆ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑥 ) ) )
28 pssss ( 𝑦𝑥𝑦𝑥 )
29 27 28 impel ( ( ( ( 𝑀𝑉𝐸𝑊 ) ∧ ( 𝑥 ∈ ω ∧ 𝑦 ∈ ω ) ) ∧ 𝑦𝑥 ) → ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ⊆ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑥 ) )
30 29 olcd ( ( ( ( 𝑀𝑉𝐸𝑊 ) ∧ ( 𝑥 ∈ ω ∧ 𝑦 ∈ ω ) ) ∧ 𝑦𝑥 ) → ( ( ( 𝑀 Sat 𝐸 ) ‘ 𝑥 ) ⊆ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ∨ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ⊆ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑥 ) ) )
31 30 ex ( ( ( 𝑀𝑉𝐸𝑊 ) ∧ ( 𝑥 ∈ ω ∧ 𝑦 ∈ ω ) ) → ( 𝑦𝑥 → ( ( ( 𝑀 Sat 𝐸 ) ‘ 𝑥 ) ⊆ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ∨ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ⊆ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑥 ) ) ) )
32 26 31 sylbid ( ( ( 𝑀𝑉𝐸𝑊 ) ∧ ( 𝑥 ∈ ω ∧ 𝑦 ∈ ω ) ) → ( 𝑦𝑥 → ( ( ( 𝑀 Sat 𝐸 ) ‘ 𝑥 ) ⊆ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ∨ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ⊆ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑥 ) ) ) )
33 16 23 32 3jaod ( ( ( 𝑀𝑉𝐸𝑊 ) ∧ ( 𝑥 ∈ ω ∧ 𝑦 ∈ ω ) ) → ( ( 𝑥𝑦𝑥𝑦𝑦𝑥 ) → ( ( ( 𝑀 Sat 𝐸 ) ‘ 𝑥 ) ⊆ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ∨ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ⊆ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑥 ) ) ) )
34 4 33 mpd ( ( ( 𝑀𝑉𝐸𝑊 ) ∧ ( 𝑥 ∈ ω ∧ 𝑦 ∈ ω ) ) → ( ( ( 𝑀 Sat 𝐸 ) ‘ 𝑥 ) ⊆ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ∨ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ⊆ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑥 ) ) )
35 34 expr ( ( ( 𝑀𝑉𝐸𝑊 ) ∧ 𝑥 ∈ ω ) → ( 𝑦 ∈ ω → ( ( ( 𝑀 Sat 𝐸 ) ‘ 𝑥 ) ⊆ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ∨ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ⊆ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑥 ) ) ) )
36 35 ralrimiv ( ( ( 𝑀𝑉𝐸𝑊 ) ∧ 𝑥 ∈ ω ) → ∀ 𝑦 ∈ ω ( ( ( 𝑀 Sat 𝐸 ) ‘ 𝑥 ) ⊆ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ∨ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ⊆ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑥 ) ) )
37 2 36 jca ( ( ( 𝑀𝑉𝐸𝑊 ) ∧ 𝑥 ∈ ω ) → ( ( ( 𝑀 Sat 𝐸 ) ‘ 𝑥 ) : ( Fmla ‘ 𝑥 ) ⟶ 𝒫 ( 𝑀m ω ) ∧ ∀ 𝑦 ∈ ω ( ( ( 𝑀 Sat 𝐸 ) ‘ 𝑥 ) ⊆ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ∨ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ⊆ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑥 ) ) ) )
38 37 ralrimiva ( ( 𝑀𝑉𝐸𝑊 ) → ∀ 𝑥 ∈ ω ( ( ( 𝑀 Sat 𝐸 ) ‘ 𝑥 ) : ( Fmla ‘ 𝑥 ) ⟶ 𝒫 ( 𝑀m ω ) ∧ ∀ 𝑦 ∈ ω ( ( ( 𝑀 Sat 𝐸 ) ‘ 𝑥 ) ⊆ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ∨ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ⊆ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑥 ) ) ) )
39 fvex ( ( 𝑀 Sat 𝐸 ) ‘ 𝑥 ) ∈ V
40 20 39 fiun ( ∀ 𝑥 ∈ ω ( ( ( 𝑀 Sat 𝐸 ) ‘ 𝑥 ) : ( Fmla ‘ 𝑥 ) ⟶ 𝒫 ( 𝑀m ω ) ∧ ∀ 𝑦 ∈ ω ( ( ( 𝑀 Sat 𝐸 ) ‘ 𝑥 ) ⊆ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ∨ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ⊆ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑥 ) ) ) → 𝑥 ∈ ω ( ( 𝑀 Sat 𝐸 ) ‘ 𝑥 ) : 𝑥 ∈ ω ( Fmla ‘ 𝑥 ) ⟶ 𝒫 ( 𝑀m ω ) )
41 38 40 syl ( ( 𝑀𝑉𝐸𝑊 ) → 𝑥 ∈ ω ( ( 𝑀 Sat 𝐸 ) ‘ 𝑥 ) : 𝑥 ∈ ω ( Fmla ‘ 𝑥 ) ⟶ 𝒫 ( 𝑀m ω ) )
42 satom ( ( 𝑀𝑉𝐸𝑊 ) → ( ( 𝑀 Sat 𝐸 ) ‘ ω ) = 𝑥 ∈ ω ( ( 𝑀 Sat 𝐸 ) ‘ 𝑥 ) )
43 fmla ( Fmla ‘ ω ) = 𝑥 ∈ ω ( Fmla ‘ 𝑥 )
44 43 a1i ( ( 𝑀𝑉𝐸𝑊 ) → ( Fmla ‘ ω ) = 𝑥 ∈ ω ( Fmla ‘ 𝑥 ) )
45 42 44 feq12d ( ( 𝑀𝑉𝐸𝑊 ) → ( ( ( 𝑀 Sat 𝐸 ) ‘ ω ) : ( Fmla ‘ ω ) ⟶ 𝒫 ( 𝑀m ω ) ↔ 𝑥 ∈ ω ( ( 𝑀 Sat 𝐸 ) ‘ 𝑥 ) : 𝑥 ∈ ω ( Fmla ‘ 𝑥 ) ⟶ 𝒫 ( 𝑀m ω ) ) )
46 41 45 mpbird ( ( 𝑀𝑉𝐸𝑊 ) → ( ( 𝑀 Sat 𝐸 ) ‘ ω ) : ( Fmla ‘ ω ) ⟶ 𝒫 ( 𝑀m ω ) )