txswaphmeolem

Description: Show inverse for the "swap components" operation on a Cartesian product. (Contributed by Mario Carneiro, 21-Mar-2015)

		Ref	Expression
	Assertion	txswaphmeolem	$⊢ (y \in Y, x \in X ⟼ ⟨x, y⟩) \circ (x \in X, y \in Y ⟼ ⟨y, x⟩) = {I ↾}_{(X \times Y)}$

Step	Hyp	Ref	Expression
1		id	$⊢ z = ⟨x, y⟩ \to z = ⟨x, y⟩$
2	1	mpompt	$⊢ (z \in (X \times Y) ⟼ z) = (x \in X, y \in Y ⟼ ⟨x, y⟩)$
3		mptresid	$⊢ {I ↾}_{(X \times Y)} = (z \in (X \times Y) ⟼ z)$
4		opelxpi	$⊢ (y \in Y \land x \in X) \to ⟨y, x⟩ \in (Y \times X)$
5	4	ancoms	$⊢ (x \in X \land y \in Y) \to ⟨y, x⟩ \in (Y \times X)$
6	5	adantl	$⊢ (⊤ \land (x \in X \land y \in Y)) \to ⟨y, x⟩ \in (Y \times X)$
7		eqidd	$⊢ ⊤ \to (x \in X, y \in Y ⟼ ⟨y, x⟩) = (x \in X, y \in Y ⟼ ⟨y, x⟩)$
8		sneq	$⊢ z = ⟨y, x⟩ \to \{z\} = \{⟨y, x⟩\}$
9	8	cnveqd	$⊢ z = ⟨y, x⟩ \to {\{z\}}^{-1} = {\{⟨y, x⟩\}}^{-1}$
10	9	unieqd	$⊢ z = ⟨y, x⟩ \to ⋃ {\{z\}}^{-1} = ⋃ {\{⟨y, x⟩\}}^{-1}$
11		opswap	$⊢ ⋃ {\{⟨y, x⟩\}}^{-1} = ⟨x, y⟩$
12	10 11	eqtrdi	$⊢ z = ⟨y, x⟩ \to ⋃ {\{z\}}^{-1} = ⟨x, y⟩$
13	12	mpompt	$⊢ (z \in (Y \times X) ⟼ ⋃ {\{z\}}^{-1}) = (y \in Y, x \in X ⟼ ⟨x, y⟩)$
14	13	eqcomi	$⊢ (y \in Y, x \in X ⟼ ⟨x, y⟩) = (z \in (Y \times X) ⟼ ⋃ {\{z\}}^{-1})$
15	14	a1i	$⊢ ⊤ \to (y \in Y, x \in X ⟼ ⟨x, y⟩) = (z \in (Y \times X) ⟼ ⋃ {\{z\}}^{-1})$
16	6 7 15 12	fmpoco	$⊢ ⊤ \to (y \in Y, x \in X ⟼ ⟨x, y⟩) \circ (x \in X, y \in Y ⟼ ⟨y, x⟩) = (x \in X, y \in Y ⟼ ⟨x, y⟩)$
17	16	mptru	$⊢ (y \in Y, x \in X ⟼ ⟨x, y⟩) \circ (x \in X, y \in Y ⟼ ⟨y, x⟩) = (x \in X, y \in Y ⟼ ⟨x, y⟩)$
18	2 3 17	3eqtr4ri	$⊢ (y \in Y, x \in X ⟼ ⟨x, y⟩) \circ (x \in X, y \in Y ⟼ ⟨y, x⟩) = {I ↾}_{(X \times Y)}$

Metamath Proof Explorer