Description: Rewrite the universal property predicate with separated parts. (Contributed by Zhi Wang, 23-Oct-2025)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | up1st2nd2.1 | ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐹 ( 𝐷 UP 𝐸 ) 𝑊 ) ) | |
| Assertion | up1st2nd2 | ⊢ ( 𝜑 → ( 1st ‘ 𝑋 ) ( 𝐹 ( 𝐷 UP 𝐸 ) 𝑊 ) ( 2nd ‘ 𝑋 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | up1st2nd2.1 | ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐹 ( 𝐷 UP 𝐸 ) 𝑊 ) ) | |
| 2 | relup | ⊢ Rel ( 𝐹 ( 𝐷 UP 𝐸 ) 𝑊 ) | |
| 3 | 1st2ndbr | ⊢ ( ( Rel ( 𝐹 ( 𝐷 UP 𝐸 ) 𝑊 ) ∧ 𝑋 ∈ ( 𝐹 ( 𝐷 UP 𝐸 ) 𝑊 ) ) → ( 1st ‘ 𝑋 ) ( 𝐹 ( 𝐷 UP 𝐸 ) 𝑊 ) ( 2nd ‘ 𝑋 ) ) | |
| 4 | 2 1 3 | sylancr | ⊢ ( 𝜑 → ( 1st ‘ 𝑋 ) ( 𝐹 ( 𝐷 UP 𝐸 ) 𝑊 ) ( 2nd ‘ 𝑋 ) ) |