cnmptcom

Description: The argument converse of a continuous function is continuous. (Contributed by Mario Carneiro, 6-Jun-2014)

	Ref	Expression
Hypotheses	cnmptcom.3	$⊢ φ \to J \in TopOn (X)$
	cnmptcom.4	$⊢ φ \to K \in TopOn (Y)$
	cnmptcom.6	$⊢ φ \to (x \in X, y \in Y ⟼ A) \in ((J \times_{t} K) Cn L)$
Assertion	cnmptcom	$⊢ φ \to (y \in Y, x \in X ⟼ A) \in ((K \times_{t} J) Cn L)$

Proof

Step	Hyp	Ref	Expression
1		cnmptcom.3	$⊢ φ \to J \in TopOn (X)$
2		cnmptcom.4	$⊢ φ \to K \in TopOn (Y)$
3		cnmptcom.6	$⊢ φ \to (x \in X, y \in Y ⟼ A) \in ((J \times_{t} K) Cn L)$
4		txtopon	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to J \times_{t} K \in TopOn (X \times Y)$
5	1 2 4	syl2anc	$⊢ φ \to J \times_{t} K \in TopOn (X \times Y)$
6		cntop2	$⊢ (x \in X, y \in Y ⟼ A) \in ((J \times_{t} K) Cn L) \to L \in Top$
7	3 6	syl	$⊢ φ \to L \in Top$
8		toptopon2	$⊢ L \in Top \leftrightarrow L \in TopOn (⋃ L)$
9	7 8	sylib	$⊢ φ \to L \in TopOn (⋃ L)$
10		cnf2	$⊢ (J \times_{t} K \in TopOn (X \times Y) \land L \in TopOn (⋃ L) \land (x \in X, y \in Y ⟼ A) \in ((J \times_{t} K) Cn L)) \to (x \in X, y \in Y ⟼ A) : X \times Y ⟶ ⋃ L$
11	5 9 3 10	syl3anc	$⊢ φ \to (x \in X, y \in Y ⟼ A) : X \times Y ⟶ ⋃ L$
12		eqid	$⊢ (x \in X, y \in Y ⟼ A) = (x \in X, y \in Y ⟼ A)$
13	12	fmpo	$⊢ \forall x \in X \forall y \in Y A \in ⋃ L \leftrightarrow (x \in X, y \in Y ⟼ A) : X \times Y ⟶ ⋃ L$
14		ralcom	$⊢ \forall x \in X \forall y \in Y A \in ⋃ L \leftrightarrow \forall y \in Y \forall x \in X A \in ⋃ L$
15	13 14	bitr3i	$⊢ (x \in X, y \in Y ⟼ A) : X \times Y ⟶ ⋃ L \leftrightarrow \forall y \in Y \forall x \in X A \in ⋃ L$
16	11 15	sylib	$⊢ φ \to \forall y \in Y \forall x \in X A \in ⋃ L$
17		eqid	$⊢ (y \in Y, x \in X ⟼ A) = (y \in Y, x \in X ⟼ A)$
18	17	fmpo	$⊢ \forall y \in Y \forall x \in X A \in ⋃ L \leftrightarrow (y \in Y, x \in X ⟼ A) : Y \times X ⟶ ⋃ L$
19	16 18	sylib	$⊢ φ \to (y \in Y, x \in X ⟼ A) : Y \times X ⟶ ⋃ L$
20	19	ffnd	$⊢ φ \to (y \in Y, x \in X ⟼ A) Fn (Y \times X)$
21		fnov	$⊢ (y \in Y, x \in X ⟼ A) Fn (Y \times X) \leftrightarrow (y \in Y, x \in X ⟼ A) = (z \in Y, w \in X ⟼ z (y \in Y, x \in X ⟼ A) w)$
22	20 21	sylib	$⊢ φ \to (y \in Y, x \in X ⟼ A) = (z \in Y, w \in X ⟼ z (y \in Y, x \in X ⟼ A) w)$
23		nfcv	$⊢ \underline{Ⅎ} y z$
24		nfcv	$⊢ \underline{Ⅎ} x z$
25		nfcv	$⊢ \underline{Ⅎ} x w$
26		nfv	$⊢ Ⅎ y φ$
27		nfcv	$⊢ \underline{Ⅎ} y x$
28		nfmpo2	$⊢ \underline{Ⅎ} y (x \in X, y \in Y ⟼ A)$
29	27 28 23	nfov	$⊢ \underline{Ⅎ} y (x (x \in X, y \in Y ⟼ A) z)$
30		nfmpo1	$⊢ \underline{Ⅎ} y (y \in Y, x \in X ⟼ A)$
31	23 30 27	nfov	$⊢ \underline{Ⅎ} y (z (y \in Y, x \in X ⟼ A) x)$
32	29 31	nfeq	$⊢ Ⅎ y x (x \in X, y \in Y ⟼ A) z = z (y \in Y, x \in X ⟼ A) x$
33	26 32	nfim	$⊢ Ⅎ y (φ \to x (x \in X, y \in Y ⟼ A) z = z (y \in Y, x \in X ⟼ A) x)$
34		nfv	$⊢ Ⅎ x φ$
35		nfmpo1	$⊢ \underline{Ⅎ} x (x \in X, y \in Y ⟼ A)$
36	25 35 24	nfov	$⊢ \underline{Ⅎ} x (w (x \in X, y \in Y ⟼ A) z)$
37		nfmpo2	$⊢ \underline{Ⅎ} x (y \in Y, x \in X ⟼ A)$
38	24 37 25	nfov	$⊢ \underline{Ⅎ} x (z (y \in Y, x \in X ⟼ A) w)$
39	36 38	nfeq	$⊢ Ⅎ x w (x \in X, y \in Y ⟼ A) z = z (y \in Y, x \in X ⟼ A) w$
40	34 39	nfim	$⊢ Ⅎ x (φ \to w (x \in X, y \in Y ⟼ A) z = z (y \in Y, x \in X ⟼ A) w)$
41		oveq2	$⊢ y = z \to x (x \in X, y \in Y ⟼ A) y = x (x \in X, y \in Y ⟼ A) z$
42		oveq1	$⊢ y = z \to y (y \in Y, x \in X ⟼ A) x = z (y \in Y, x \in X ⟼ A) x$
43	41 42	eqeq12d	$⊢ y = z \to (x (x \in X, y \in Y ⟼ A) y = y (y \in Y, x \in X ⟼ A) x \leftrightarrow x (x \in X, y \in Y ⟼ A) z = z (y \in Y, x \in X ⟼ A) x)$
44	43	imbi2d	$⊢ y = z \to ((φ \to x (x \in X, y \in Y ⟼ A) y = y (y \in Y, x \in X ⟼ A) x) \leftrightarrow (φ \to x (x \in X, y \in Y ⟼ A) z = z (y \in Y, x \in X ⟼ A) x))$
45		oveq1	$⊢ x = w \to x (x \in X, y \in Y ⟼ A) z = w (x \in X, y \in Y ⟼ A) z$
46		oveq2	$⊢ x = w \to z (y \in Y, x \in X ⟼ A) x = z (y \in Y, x \in X ⟼ A) w$
47	45 46	eqeq12d	$⊢ x = w \to (x (x \in X, y \in Y ⟼ A) z = z (y \in Y, x \in X ⟼ A) x \leftrightarrow w (x \in X, y \in Y ⟼ A) z = z (y \in Y, x \in X ⟼ A) w)$
48	47	imbi2d	$⊢ x = w \to ((φ \to x (x \in X, y \in Y ⟼ A) z = z (y \in Y, x \in X ⟼ A) x) \leftrightarrow (φ \to w (x \in X, y \in Y ⟼ A) z = z (y \in Y, x \in X ⟼ A) w))$
49		rsp2	$⊢ \forall y \in Y \forall x \in X A \in ⋃ L \to ((y \in Y \land x \in X) \to A \in ⋃ L)$
50	49 16	syl11	$⊢ (y \in Y \land x \in X) \to (φ \to A \in ⋃ L)$
51	12	ovmpt4g	$⊢ (x \in X \land y \in Y \land A \in ⋃ L) \to x (x \in X, y \in Y ⟼ A) y = A$
52	51	3com12	$⊢ (y \in Y \land x \in X \land A \in ⋃ L) \to x (x \in X, y \in Y ⟼ A) y = A$
53	17	ovmpt4g	$⊢ (y \in Y \land x \in X \land A \in ⋃ L) \to y (y \in Y, x \in X ⟼ A) x = A$
54	52 53	eqtr4d	$⊢ (y \in Y \land x \in X \land A \in ⋃ L) \to x (x \in X, y \in Y ⟼ A) y = y (y \in Y, x \in X ⟼ A) x$
55	54	3expia	$⊢ (y \in Y \land x \in X) \to (A \in ⋃ L \to x (x \in X, y \in Y ⟼ A) y = y (y \in Y, x \in X ⟼ A) x)$
56	50 55	syld	$⊢ (y \in Y \land x \in X) \to (φ \to x (x \in X, y \in Y ⟼ A) y = y (y \in Y, x \in X ⟼ A) x)$
57	23 24 25 33 40 44 48 56	vtocl2gaf	$⊢ (z \in Y \land w \in X) \to (φ \to w (x \in X, y \in Y ⟼ A) z = z (y \in Y, x \in X ⟼ A) w)$
58	57	com12	$⊢ φ \to ((z \in Y \land w \in X) \to w (x \in X, y \in Y ⟼ A) z = z (y \in Y, x \in X ⟼ A) w)$
59	58	3impib	$⊢ (φ \land z \in Y \land w \in X) \to w (x \in X, y \in Y ⟼ A) z = z (y \in Y, x \in X ⟼ A) w$
60	59	mpoeq3dva	$⊢ φ \to (z \in Y, w \in X ⟼ w (x \in X, y \in Y ⟼ A) z) = (z \in Y, w \in X ⟼ z (y \in Y, x \in X ⟼ A) w)$
61	22 60	eqtr4d	$⊢ φ \to (y \in Y, x \in X ⟼ A) = (z \in Y, w \in X ⟼ w (x \in X, y \in Y ⟼ A) z)$
62	2 1	cnmpt2nd	$⊢ φ \to (z \in Y, w \in X ⟼ w) \in ((K \times_{t} J) Cn J)$
63	2 1	cnmpt1st	$⊢ φ \to (z \in Y, w \in X ⟼ z) \in ((K \times_{t} J) Cn K)$
64	2 1 62 63 3	cnmpt22f	$⊢ φ \to (z \in Y, w \in X ⟼ w (x \in X, y \in Y ⟼ A) z) \in ((K \times_{t} J) Cn L)$
65	61 64	eqeltrd	$⊢ φ \to (y \in Y, x \in X ⟼ A) \in ((K \times_{t} J) Cn L)$

Metamath Proof Explorer

Theorem cnmptcom

Proof