Description: Sufficient condition for the intersection of a range Cartesian product with a Cartesian product to be a set. (Contributed by Peter Mazsa, 12-Apr-2020)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | xrninxpex | |- ( ( A e. V /\ B e. W /\ C e. X ) -> ( ( R |X. S ) i^i ( A X. ( B X. C ) ) ) e. _V ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | xpexg | |- ( ( B e. W /\ C e. X ) -> ( B X. C ) e. _V ) |
|
| 2 | inxpex | |- ( ( ( R |X. S ) e. _V \/ ( A e. V /\ ( B X. C ) e. _V ) ) -> ( ( R |X. S ) i^i ( A X. ( B X. C ) ) ) e. _V ) |
|
| 3 | 2 | olcs | |- ( ( A e. V /\ ( B X. C ) e. _V ) -> ( ( R |X. S ) i^i ( A X. ( B X. C ) ) ) e. _V ) |
| 4 | 1 3 | sylan2 | |- ( ( A e. V /\ ( B e. W /\ C e. X ) ) -> ( ( R |X. S ) i^i ( A X. ( B X. C ) ) ) e. _V ) |
| 5 | 4 | 3impb | |- ( ( A e. V /\ B e. W /\ C e. X ) -> ( ( R |X. S ) i^i ( A X. ( B X. C ) ) ) e. _V ) |