Description: A non-empty base set of the product category indicates the existence of the second factor of the product category. (Contributed by Zhi Wang, 8-Oct-2025) (Proof shortened by SN, 15-Oct-2025)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | elxpcbasex1.t | |- T = ( C Xc. D ) |
|
| elxpcbasex1.b | |- B = ( Base ` T ) |
||
| elxpcbasex1.x | |- ( ph -> X e. B ) |
||
| Assertion | elxpcbasex2 | |- ( ph -> D e. _V ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | elxpcbasex1.t | |- T = ( C Xc. D ) |
|
| 2 | elxpcbasex1.b | |- B = ( Base ` T ) |
|
| 3 | elxpcbasex1.x | |- ( ph -> X e. B ) |
|
| 4 | reldmxpc | |- Rel dom Xc. |
|
| 5 | 4 1 2 | elbasov | |- ( X e. B -> ( C e. _V /\ D e. _V ) ) |
| 6 | 3 5 | syl | |- ( ph -> ( C e. _V /\ D e. _V ) ) |
| 7 | 6 | simprd | |- ( ph -> D e. _V ) |