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 | ⊢ Sat∈ = ( 𝑚 ∈ V , 𝑢 ∈ V ↦ ( ( ( 𝑚 Sat ( E ∩ ( 𝑚 × 𝑚 ) ) ) ‘ ω ) ‘ 𝑢 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | csate | ⊢ Sat∈ | |
| 1 | vm | ⊢ 𝑚 | |
| 2 | cvv | ⊢ V | |
| 3 | vu | ⊢ 𝑢 | |
| 4 | 1 | cv | ⊢ 𝑚 |
| 5 | csat | ⊢ Sat | |
| 6 | cep | ⊢ E | |
| 7 | 4 4 | cxp | ⊢ ( 𝑚 × 𝑚 ) |
| 8 | 6 7 | cin | ⊢ ( E ∩ ( 𝑚 × 𝑚 ) ) |
| 9 | 4 8 5 | co | ⊢ ( 𝑚 Sat ( E ∩ ( 𝑚 × 𝑚 ) ) ) |
| 10 | com | ⊢ ω | |
| 11 | 10 9 | cfv | ⊢ ( ( 𝑚 Sat ( E ∩ ( 𝑚 × 𝑚 ) ) ) ‘ ω ) |
| 12 | 3 | cv | ⊢ 𝑢 |
| 13 | 12 11 | cfv | ⊢ ( ( ( 𝑚 Sat ( E ∩ ( 𝑚 × 𝑚 ) ) ) ‘ ω ) ‘ 𝑢 ) |
| 14 | 1 3 2 2 13 | cmpo | ⊢ ( 𝑚 ∈ V , 𝑢 ∈ V ↦ ( ( ( 𝑚 Sat ( E ∩ ( 𝑚 × 𝑚 ) ) ) ‘ ω ) ‘ 𝑢 ) ) |
| 15 | 0 14 | wceq | ⊢ Sat∈ = ( 𝑚 ∈ V , 𝑢 ∈ V ↦ ( ( ( 𝑚 Sat ( E ∩ ( 𝑚 × 𝑚 ) ) ) ‘ ω ) ‘ 𝑢 ) ) |