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 biimtrdi ⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( 𝑥 ∈ ω ∧ 𝑦 ∈ ω ) ) → ( 𝑥 ≈ 𝑦 → ( ( ( 𝑀 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 ω ) )