Description: A simplified version of the satisfaction predicate, using the standard membership relation and eliminating the extra variable n . (Contributed by Mario Carneiro, 14-Jul-2013)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-sate | |- SatE = ( m e. _V , u e. _V |-> ( ( ( m Sat ( _E i^i ( m X. m ) ) ) ` _om ) ` u ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | csate | |- SatE |
|
| 1 | vm | |- m |
|
| 2 | cvv | |- _V |
|
| 3 | vu | |- u |
|
| 4 | 1 | cv | |- m |
| 5 | csat | |- Sat |
|
| 6 | cep | |- _E |
|
| 7 | 4 4 | cxp | |- ( m X. m ) |
| 8 | 6 7 | cin | |- ( _E i^i ( m X. m ) ) |
| 9 | 4 8 5 | co | |- ( m Sat ( _E i^i ( m X. m ) ) ) |
| 10 | com | |- _om |
|
| 11 | 10 9 | cfv | |- ( ( m Sat ( _E i^i ( m X. m ) ) ) ` _om ) |
| 12 | 3 | cv | |- u |
| 13 | 12 11 | cfv | |- ( ( ( m Sat ( _E i^i ( m X. m ) ) ) ` _om ) ` u ) |
| 14 | 1 3 2 2 13 | cmpo | |- ( m e. _V , u e. _V |-> ( ( ( m Sat ( _E i^i ( m X. m ) ) ) ` _om ) ` u ) ) |
| 15 | 0 14 | wceq | |- SatE = ( m e. _V , u e. _V |-> ( ( ( m Sat ( _E i^i ( m X. m ) ) ) ` _om ) ` u ) ) |