Description: The converse of a Cartesian product. Exercise 11 of Suppes p. 67. (Contributed by NM, 14-Aug-1999) (Proof shortened by Andrew Salmon, 27-Aug-2011) Avoid ax-11 . (Revised by SN, 26-Aug-2026)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | cnvxp | ⊢ ◡ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | relcnv | ⊢ Rel ◡ ( 𝐴 × 𝐵 ) | |
| 2 | relxp | ⊢ Rel ( 𝐵 × 𝐴 ) | |
| 3 | vex | ⊢ 𝑥 ∈ V | |
| 4 | vex | ⊢ 𝑦 ∈ V | |
| 5 | 3 4 | brcnv | ⊢ ( 𝑥 ◡ ( 𝐴 × 𝐵 ) 𝑦 ↔ 𝑦 ( 𝐴 × 𝐵 ) 𝑥 ) |
| 6 | ancom | ⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ↔ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴 ) ) | |
| 7 | brxp | ⊢ ( 𝑦 ( 𝐴 × 𝐵 ) 𝑥 ↔ ( 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ) | |
| 8 | brxp | ⊢ ( 𝑥 ( 𝐵 × 𝐴 ) 𝑦 ↔ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴 ) ) | |
| 9 | 6 7 8 | 3bitr4i | ⊢ ( 𝑦 ( 𝐴 × 𝐵 ) 𝑥 ↔ 𝑥 ( 𝐵 × 𝐴 ) 𝑦 ) |
| 10 | 5 9 | bitri | ⊢ ( 𝑥 ◡ ( 𝐴 × 𝐵 ) 𝑦 ↔ 𝑥 ( 𝐵 × 𝐴 ) 𝑦 ) |
| 11 | 1 2 10 | eqbrriv | ⊢ ◡ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) |