Description: Condition of a valuation S of a simplified satisfaction predicate for a Godel-set of membership: The sets in model M corresponding to the variables A and B under the assignment of S are in a membership relation in M . (Contributed by AV, 5-Nov-2023)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | sategoelfvb.s | ⊢ 𝐸 = ( 𝑀 Sat∈ ( 𝐴 ∈𝑔 𝐵 ) ) | |
| Assertion | sategoelfv | ⊢ ( ( 𝑀 ∈ 𝑉 ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝑆 ∈ 𝐸 ) → ( 𝑆 ‘ 𝐴 ) ∈ ( 𝑆 ‘ 𝐵 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | sategoelfvb.s | ⊢ 𝐸 = ( 𝑀 Sat∈ ( 𝐴 ∈𝑔 𝐵 ) ) | |
| 2 | 1 | sategoelfvb | ⊢ ( ( 𝑀 ∈ 𝑉 ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) → ( 𝑆 ∈ 𝐸 ↔ ( 𝑆 ∈ ( 𝑀 ↑m ω ) ∧ ( 𝑆 ‘ 𝐴 ) ∈ ( 𝑆 ‘ 𝐵 ) ) ) ) |
| 3 | simpr | ⊢ ( ( 𝑆 ∈ ( 𝑀 ↑m ω ) ∧ ( 𝑆 ‘ 𝐴 ) ∈ ( 𝑆 ‘ 𝐵 ) ) → ( 𝑆 ‘ 𝐴 ) ∈ ( 𝑆 ‘ 𝐵 ) ) | |
| 4 | 2 3 | biimtrdi | ⊢ ( ( 𝑀 ∈ 𝑉 ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) → ( 𝑆 ∈ 𝐸 → ( 𝑆 ‘ 𝐴 ) ∈ ( 𝑆 ‘ 𝐵 ) ) ) |
| 5 | 4 | 3impia | ⊢ ( ( 𝑀 ∈ 𝑉 ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝑆 ∈ 𝐸 ) → ( 𝑆 ‘ 𝐴 ) ∈ ( 𝑆 ‘ 𝐵 ) ) |