txswaphmeo

Description: There is a homeomorphism from X X. Y to Y X. X . (Contributed by Mario Carneiro, 21-Mar-2015)

		Ref	Expression
	Assertion	txswaphmeo	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to (x \in X, y \in Y ⟼ ⟨y, x⟩) \in ((J \times_{t} K) Homeo (K \times_{t} J))$

Proof

Step	Hyp	Ref	Expression
1		simpl	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to J \in TopOn (X)$
2		simpr	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to K \in TopOn (Y)$
3	1 2	cnmpt2nd	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to (x \in X, y \in Y ⟼ y) \in ((J \times_{t} K) Cn K)$
4	1 2	cnmpt1st	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to (x \in X, y \in Y ⟼ x) \in ((J \times_{t} K) Cn J)$
5	1 2 3 4	cnmpt2t	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to (x \in X, y \in Y ⟼ ⟨y, x⟩) \in ((J \times_{t} K) Cn (K \times_{t} J))$
6		opelxpi	$⊢ (y \in Y \land x \in X) \to ⟨y, x⟩ \in (Y \times X)$
7	6	ancoms	$⊢ (x \in X \land y \in Y) \to ⟨y, x⟩ \in (Y \times X)$
8	7	adantl	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land (x \in X \land y \in Y)) \to ⟨y, x⟩ \in (Y \times X)$
9	8	ralrimivva	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to \forall x \in X \forall y \in Y ⟨y, x⟩ \in (Y \times X)$
10		eqid	$⊢ (x \in X, y \in Y ⟼ ⟨y, x⟩) = (x \in X, y \in Y ⟼ ⟨y, x⟩)$
11	10	fmpo	$⊢ \forall x \in X \forall y \in Y ⟨y, x⟩ \in (Y \times X) \leftrightarrow (x \in X, y \in Y ⟼ ⟨y, x⟩) : X \times Y ⟶ Y \times X$
12	9 11	sylib	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to (x \in X, y \in Y ⟼ ⟨y, x⟩) : X \times Y ⟶ Y \times X$
13		opelxpi	$⊢ (x \in X \land y \in Y) \to ⟨x, y⟩ \in (X \times Y)$
14	13	ancoms	$⊢ (y \in Y \land x \in X) \to ⟨x, y⟩ \in (X \times Y)$
15	14	adantl	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land (y \in Y \land x \in X)) \to ⟨x, y⟩ \in (X \times Y)$
16	15	ralrimivva	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to \forall y \in Y \forall x \in X ⟨x, y⟩ \in (X \times Y)$
17		eqid	$⊢ (y \in Y, x \in X ⟼ ⟨x, y⟩) = (y \in Y, x \in X ⟼ ⟨x, y⟩)$
18	17	fmpo	$⊢ \forall y \in Y \forall x \in X ⟨x, y⟩ \in (X \times Y) \leftrightarrow (y \in Y, x \in X ⟼ ⟨x, y⟩) : Y \times X ⟶ X \times Y$
19	16 18	sylib	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to (y \in Y, x \in X ⟼ ⟨x, y⟩) : Y \times X ⟶ X \times Y$
20		txswaphmeolem	$⊢ (x \in X, y \in Y ⟼ ⟨y, x⟩) \circ (y \in Y, x \in X ⟼ ⟨x, y⟩) = {I ↾}_{(Y \times X)}$
21		txswaphmeolem	$⊢ (y \in Y, x \in X ⟼ ⟨x, y⟩) \circ (x \in X, y \in Y ⟼ ⟨y, x⟩) = {I ↾}_{(X \times Y)}$
22		fcof1o	$⊢ (((x \in X, y \in Y ⟼ ⟨y, x⟩) : X \times Y ⟶ Y \times X \land (y \in Y, x \in X ⟼ ⟨x, y⟩) : Y \times X ⟶ X \times Y) \land ((x \in X, y \in Y ⟼ ⟨y, x⟩) \circ (y \in Y, x \in X ⟼ ⟨x, y⟩) = {I ↾}_{(Y \times X)} \land (y \in Y, x \in X ⟼ ⟨x, y⟩) \circ (x \in X, y \in Y ⟼ ⟨y, x⟩) = {I ↾}_{(X \times Y)})) \to ((x \in X, y \in Y ⟼ ⟨y, x⟩) : X \times Y \underset{1-1 onto}{⟶} Y \times X \land {(x \in X, y \in Y ⟼ ⟨y, x⟩)}^{-1} = (y \in Y, x \in X ⟼ ⟨x, y⟩))$
23	20 21 22	mpanr12	$⊢ ((x \in X, y \in Y ⟼ ⟨y, x⟩) : X \times Y ⟶ Y \times X \land (y \in Y, x \in X ⟼ ⟨x, y⟩) : Y \times X ⟶ X \times Y) \to ((x \in X, y \in Y ⟼ ⟨y, x⟩) : X \times Y \underset{1-1 onto}{⟶} Y \times X \land {(x \in X, y \in Y ⟼ ⟨y, x⟩)}^{-1} = (y \in Y, x \in X ⟼ ⟨x, y⟩))$
24	12 19 23	syl2anc	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to ((x \in X, y \in Y ⟼ ⟨y, x⟩) : X \times Y \underset{1-1 onto}{⟶} Y \times X \land {(x \in X, y \in Y ⟼ ⟨y, x⟩)}^{-1} = (y \in Y, x \in X ⟼ ⟨x, y⟩))$
25	24	simprd	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to {(x \in X, y \in Y ⟼ ⟨y, x⟩)}^{-1} = (y \in Y, x \in X ⟼ ⟨x, y⟩)$
26	2 1	cnmpt2nd	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to (y \in Y, x \in X ⟼ x) \in ((K \times_{t} J) Cn J)$
27	2 1	cnmpt1st	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to (y \in Y, x \in X ⟼ y) \in ((K \times_{t} J) Cn K)$
28	2 1 26 27	cnmpt2t	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to (y \in Y, x \in X ⟼ ⟨x, y⟩) \in ((K \times_{t} J) Cn (J \times_{t} K))$
29	25 28	eqeltrd	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to {(x \in X, y \in Y ⟼ ⟨y, x⟩)}^{-1} \in ((K \times_{t} J) Cn (J \times_{t} K))$
30		ishmeo	$⊢ (x \in X, y \in Y ⟼ ⟨y, x⟩) \in ((J \times_{t} K) Homeo (K \times_{t} J)) \leftrightarrow ((x \in X, y \in Y ⟼ ⟨y, x⟩) \in ((J \times_{t} K) Cn (K \times_{t} J)) \land {(x \in X, y \in Y ⟼ ⟨y, x⟩)}^{-1} \in ((K \times_{t} J) Cn (J \times_{t} K)))$
31	5 29 30	sylanbrc	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to (x \in X, y \in Y ⟼ ⟨y, x⟩) \in ((J \times_{t} K) Homeo (K \times_{t} J))$

Metamath Proof Explorer

Theorem txswaphmeo

Proof