Description: A Cartesian product exists iff its converse does. Corollary 6.9(1) in TakeutiZaring p. 26. (Contributed by Andrew Salmon, 13-Nov-2011)
Ref | Expression | ||
---|---|---|---|
Assertion | xpexb | |- ( ( A X. B ) e. _V <-> ( B X. A ) e. _V ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cnvxp | |- `' ( A X. B ) = ( B X. A ) |
|
2 | cnvexg | |- ( ( A X. B ) e. _V -> `' ( A X. B ) e. _V ) |
|
3 | 1 2 | eqeltrrid | |- ( ( A X. B ) e. _V -> ( B X. A ) e. _V ) |
4 | cnvxp | |- `' ( B X. A ) = ( A X. B ) |
|
5 | cnvexg | |- ( ( B X. A ) e. _V -> `' ( B X. A ) e. _V ) |
|
6 | 4 5 | eqeltrrid | |- ( ( B X. A ) e. _V -> ( A X. B ) e. _V ) |
7 | 3 6 | impbii | |- ( ( A X. B ) e. _V <-> ( B X. A ) e. _V ) |