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 | |- E = ( M SatE ( A e.g B ) ) |
|
| Assertion | sategoelfv | |- ( ( M e. V /\ ( A e. _om /\ B e. _om ) /\ S e. E ) -> ( S ` A ) e. ( S ` B ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | sategoelfvb.s | |- E = ( M SatE ( A e.g B ) ) |
|
| 2 | 1 | sategoelfvb | |- ( ( M e. V /\ ( A e. _om /\ B e. _om ) ) -> ( S e. E <-> ( S e. ( M ^m _om ) /\ ( S ` A ) e. ( S ` B ) ) ) ) |
| 3 | simpr | |- ( ( S e. ( M ^m _om ) /\ ( S ` A ) e. ( S ` B ) ) -> ( S ` A ) e. ( S ` B ) ) |
|
| 4 | 2 3 | syl6bi | |- ( ( M e. V /\ ( A e. _om /\ B e. _om ) ) -> ( S e. E -> ( S ` A ) e. ( S ` B ) ) ) |
| 5 | 4 | 3impia | |- ( ( M e. V /\ ( A e. _om /\ B e. _om ) /\ S e. E ) -> ( S ` A ) e. ( S ` B ) ) |