xkocnv

Description: The inverse of the "currying" function F is the uncurrying function. (Contributed by Mario Carneiro, 13-Apr-2015)

	Ref	Expression
Hypotheses	xkohmeo.x	$⊢ φ \to J \in TopOn (X)$
	xkohmeo.y	$⊢ φ \to K \in TopOn (Y)$
	xkohmeo.f	$⊢ F = (f \in ((J \times_{t} K) Cn L) ⟼ (x \in X ⟼ (y \in Y ⟼ x f y)))$
	xkohmeo.j	$⊢ φ \to J \in N-LocallyComp$
	xkohmeo.k	$⊢ φ \to K \in N-LocallyComp$
	xkohmeo.l	$⊢ φ \to L \in Top$
Assertion	xkocnv	$⊢ φ \to F^{-1} = (g \in (J Cn (L^_{ko} K)) ⟼ (x \in X, y \in Y ⟼ g (x) (y)))$

Proof

Step	Hyp	Ref	Expression
1		xkohmeo.x	$⊢ φ \to J \in TopOn (X)$
2		xkohmeo.y	$⊢ φ \to K \in TopOn (Y)$
3		xkohmeo.f	$⊢ F = (f \in ((J \times_{t} K) Cn L) ⟼ (x \in X ⟼ (y \in Y ⟼ x f y)))$
4		xkohmeo.j	$⊢ φ \to J \in N-LocallyComp$
5		xkohmeo.k	$⊢ φ \to K \in N-LocallyComp$
6		xkohmeo.l	$⊢ φ \to L \in Top$
7		simprr	$⊢ (φ \land (f \in ((J \times_{t} K) Cn L) \land g = (x \in X ⟼ (y \in Y ⟼ x f y)))) \to g = (x \in X ⟼ (y \in Y ⟼ x f y))$
8	1	adantr	$⊢ (φ \land f \in ((J \times_{t} K) Cn L)) \to J \in TopOn (X)$
9	2	adantr	$⊢ (φ \land f \in ((J \times_{t} K) Cn L)) \to K \in TopOn (Y)$
10		txtopon	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to J \times_{t} K \in TopOn (X \times Y)$
11	1 2 10	syl2anc	$⊢ φ \to J \times_{t} K \in TopOn (X \times Y)$
12	11	adantr	$⊢ (φ \land f \in ((J \times_{t} K) Cn L)) \to J \times_{t} K \in TopOn (X \times Y)$
13		toptopon2	$⊢ L \in Top \leftrightarrow L \in TopOn (⋃ L)$
14	6 13	sylib	$⊢ φ \to L \in TopOn (⋃ L)$
15	14	adantr	$⊢ (φ \land f \in ((J \times_{t} K) Cn L)) \to L \in TopOn (⋃ L)$
16		simpr	$⊢ (φ \land f \in ((J \times_{t} K) Cn L)) \to f \in ((J \times_{t} K) Cn L)$
17		cnf2	$⊢ (J \times_{t} K \in TopOn (X \times Y) \land L \in TopOn (⋃ L) \land f \in ((J \times_{t} K) Cn L)) \to f : X \times Y ⟶ ⋃ L$
18	12 15 16 17	syl3anc	$⊢ (φ \land f \in ((J \times_{t} K) Cn L)) \to f : X \times Y ⟶ ⋃ L$
19	18	ffnd	$⊢ (φ \land f \in ((J \times_{t} K) Cn L)) \to f Fn (X \times Y)$
20		fnov	$⊢ f Fn (X \times Y) \leftrightarrow f = (x \in X, y \in Y ⟼ x f y)$
21	19 20	sylib	$⊢ (φ \land f \in ((J \times_{t} K) Cn L)) \to f = (x \in X, y \in Y ⟼ x f y)$
22	21 16	eqeltrrd	$⊢ (φ \land f \in ((J \times_{t} K) Cn L)) \to (x \in X, y \in Y ⟼ x f y) \in ((J \times_{t} K) Cn L)$
23	8 9 22	cnmpt2k	$⊢ (φ \land f \in ((J \times_{t} K) Cn L)) \to (x \in X ⟼ (y \in Y ⟼ x f y)) \in (J Cn (L^_{ko} K))$
24	23	adantrr	$⊢ (φ \land (f \in ((J \times_{t} K) Cn L) \land g = (x \in X ⟼ (y \in Y ⟼ x f y)))) \to (x \in X ⟼ (y \in Y ⟼ x f y)) \in (J Cn (L^_{ko} K))$
25	7 24	eqeltrd	$⊢ (φ \land (f \in ((J \times_{t} K) Cn L) \land g = (x \in X ⟼ (y \in Y ⟼ x f y)))) \to g \in (J Cn (L^_{ko} K))$
26	21	adantrr	$⊢ (φ \land (f \in ((J \times_{t} K) Cn L) \land g = (x \in X ⟼ (y \in Y ⟼ x f y)))) \to f = (x \in X, y \in Y ⟼ x f y)$
27		eqid	$⊢ X = X$
28		nfv	$⊢ Ⅎ x φ$
29		nfv	$⊢ Ⅎ x f \in ((J \times_{t} K) Cn L)$
30		nfmpt1	$⊢ \underline{Ⅎ} x (x \in X ⟼ (y \in Y ⟼ x f y))$
31	30	nfeq2	$⊢ Ⅎ x g = (x \in X ⟼ (y \in Y ⟼ x f y))$
32	29 31	nfan	$⊢ Ⅎ x (f \in ((J \times_{t} K) Cn L) \land g = (x \in X ⟼ (y \in Y ⟼ x f y)))$
33	28 32	nfan	$⊢ Ⅎ x (φ \land (f \in ((J \times_{t} K) Cn L) \land g = (x \in X ⟼ (y \in Y ⟼ x f y))))$
34		nfv	$⊢ Ⅎ y φ$
35		nfv	$⊢ Ⅎ y f \in ((J \times_{t} K) Cn L)$
36		nfcv	$⊢ \underline{Ⅎ} y X$
37		nfmpt1	$⊢ \underline{Ⅎ} y (y \in Y ⟼ x f y)$
38	36 37	nfmpt	$⊢ \underline{Ⅎ} y (x \in X ⟼ (y \in Y ⟼ x f y))$
39	38	nfeq2	$⊢ Ⅎ y g = (x \in X ⟼ (y \in Y ⟼ x f y))$
40	35 39	nfan	$⊢ Ⅎ y (f \in ((J \times_{t} K) Cn L) \land g = (x \in X ⟼ (y \in Y ⟼ x f y)))$
41	34 40	nfan	$⊢ Ⅎ y (φ \land (f \in ((J \times_{t} K) Cn L) \land g = (x \in X ⟼ (y \in Y ⟼ x f y))))$
42		nfv	$⊢ Ⅎ y x \in X$
43	41 42	nfan	$⊢ Ⅎ y ((φ \land (f \in ((J \times_{t} K) Cn L) \land g = (x \in X ⟼ (y \in Y ⟼ x f y)))) \land x \in X)$
44		simplrr	$⊢ ((φ \land (f \in ((J \times_{t} K) Cn L) \land g = (x \in X ⟼ (y \in Y ⟼ x f y)))) \land (x \in X \land y \in Y)) \to g = (x \in X ⟼ (y \in Y ⟼ x f y))$
45	44	fveq1d	$⊢ ((φ \land (f \in ((J \times_{t} K) Cn L) \land g = (x \in X ⟼ (y \in Y ⟼ x f y)))) \land (x \in X \land y \in Y)) \to g (x) = (x \in X ⟼ (y \in Y ⟼ x f y)) (x)$
46		simprl	$⊢ ((φ \land (f \in ((J \times_{t} K) Cn L) \land g = (x \in X ⟼ (y \in Y ⟼ x f y)))) \land (x \in X \land y \in Y)) \to x \in X$
47		toponmax	$⊢ K \in TopOn (Y) \to Y \in K$
48	2 47	syl	$⊢ φ \to Y \in K$
49	48	ad2antrr	$⊢ ((φ \land (f \in ((J \times_{t} K) Cn L) \land g = (x \in X ⟼ (y \in Y ⟼ x f y)))) \land (x \in X \land y \in Y)) \to Y \in K$
50	49	mptexd	$⊢ ((φ \land (f \in ((J \times_{t} K) Cn L) \land g = (x \in X ⟼ (y \in Y ⟼ x f y)))) \land (x \in X \land y \in Y)) \to (y \in Y ⟼ x f y) \in V$
51		eqid	$⊢ (x \in X ⟼ (y \in Y ⟼ x f y)) = (x \in X ⟼ (y \in Y ⟼ x f y))$
52	51	fvmpt2	$⊢ (x \in X \land (y \in Y ⟼ x f y) \in V) \to (x \in X ⟼ (y \in Y ⟼ x f y)) (x) = (y \in Y ⟼ x f y)$
53	46 50 52	syl2anc	$⊢ ((φ \land (f \in ((J \times_{t} K) Cn L) \land g = (x \in X ⟼ (y \in Y ⟼ x f y)))) \land (x \in X \land y \in Y)) \to (x \in X ⟼ (y \in Y ⟼ x f y)) (x) = (y \in Y ⟼ x f y)$
54	45 53	eqtrd	$⊢ ((φ \land (f \in ((J \times_{t} K) Cn L) \land g = (x \in X ⟼ (y \in Y ⟼ x f y)))) \land (x \in X \land y \in Y)) \to g (x) = (y \in Y ⟼ x f y)$
55	54	fveq1d	$⊢ ((φ \land (f \in ((J \times_{t} K) Cn L) \land g = (x \in X ⟼ (y \in Y ⟼ x f y)))) \land (x \in X \land y \in Y)) \to g (x) (y) = (y \in Y ⟼ x f y) (y)$
56		simprr	$⊢ ((φ \land (f \in ((J \times_{t} K) Cn L) \land g = (x \in X ⟼ (y \in Y ⟼ x f y)))) \land (x \in X \land y \in Y)) \to y \in Y$
57		ovex	$⊢ x f y \in V$
58		eqid	$⊢ (y \in Y ⟼ x f y) = (y \in Y ⟼ x f y)$
59	58	fvmpt2	$⊢ (y \in Y \land x f y \in V) \to (y \in Y ⟼ x f y) (y) = x f y$
60	56 57 59	sylancl	$⊢ ((φ \land (f \in ((J \times_{t} K) Cn L) \land g = (x \in X ⟼ (y \in Y ⟼ x f y)))) \land (x \in X \land y \in Y)) \to (y \in Y ⟼ x f y) (y) = x f y$
61	55 60	eqtrd	$⊢ ((φ \land (f \in ((J \times_{t} K) Cn L) \land g = (x \in X ⟼ (y \in Y ⟼ x f y)))) \land (x \in X \land y \in Y)) \to g (x) (y) = x f y$
62	61	expr	$⊢ ((φ \land (f \in ((J \times_{t} K) Cn L) \land g = (x \in X ⟼ (y \in Y ⟼ x f y)))) \land x \in X) \to (y \in Y \to g (x) (y) = x f y)$
63	43 62	ralrimi	$⊢ ((φ \land (f \in ((J \times_{t} K) Cn L) \land g = (x \in X ⟼ (y \in Y ⟼ x f y)))) \land x \in X) \to \forall y \in Y g (x) (y) = x f y$
64		eqid	$⊢ Y = Y$
65	63 64	jctil	$⊢ ((φ \land (f \in ((J \times_{t} K) Cn L) \land g = (x \in X ⟼ (y \in Y ⟼ x f y)))) \land x \in X) \to (Y = Y \land \forall y \in Y g (x) (y) = x f y)$
66	65	ex	$⊢ (φ \land (f \in ((J \times_{t} K) Cn L) \land g = (x \in X ⟼ (y \in Y ⟼ x f y)))) \to (x \in X \to (Y = Y \land \forall y \in Y g (x) (y) = x f y))$
67	33 66	ralrimi	$⊢ (φ \land (f \in ((J \times_{t} K) Cn L) \land g = (x \in X ⟼ (y \in Y ⟼ x f y)))) \to \forall x \in X (Y = Y \land \forall y \in Y g (x) (y) = x f y)$
68		mpoeq123	$⊢ (X = X \land \forall x \in X (Y = Y \land \forall y \in Y g (x) (y) = x f y)) \to (x \in X, y \in Y ⟼ g (x) (y)) = (x \in X, y \in Y ⟼ x f y)$
69	27 67 68	sylancr	$⊢ (φ \land (f \in ((J \times_{t} K) Cn L) \land g = (x \in X ⟼ (y \in Y ⟼ x f y)))) \to (x \in X, y \in Y ⟼ g (x) (y)) = (x \in X, y \in Y ⟼ x f y)$
70	26 69	eqtr4d	$⊢ (φ \land (f \in ((J \times_{t} K) Cn L) \land g = (x \in X ⟼ (y \in Y ⟼ x f y)))) \to f = (x \in X, y \in Y ⟼ g (x) (y))$
71	25 70	jca	$⊢ (φ \land (f \in ((J \times_{t} K) Cn L) \land g = (x \in X ⟼ (y \in Y ⟼ x f y)))) \to (g \in (J Cn (L^_{ko} K)) \land f = (x \in X, y \in Y ⟼ g (x) (y)))$
72		simprr	$⊢ (φ \land (g \in (J Cn (L^_{ko} K)) \land f = (x \in X, y \in Y ⟼ g (x) (y)))) \to f = (x \in X, y \in Y ⟼ g (x) (y))$
73	1	adantr	$⊢ (φ \land g \in (J Cn (L^_{ko} K))) \to J \in TopOn (X)$
74	2	adantr	$⊢ (φ \land g \in (J Cn (L^_{ko} K))) \to K \in TopOn (Y)$
75	14	adantr	$⊢ (φ \land g \in (J Cn (L^_{ko} K))) \to L \in TopOn (⋃ L)$
76	5	adantr	$⊢ (φ \land g \in (J Cn (L^_{ko} K))) \to K \in N-LocallyComp$
77		nllytop	$⊢ K \in N-LocallyComp\toK \in Top$
78	76 77	syl	$⊢ (φ \land g \in (J Cn (L^_{ko} K))) \to K \in Top$
79	6	adantr	$⊢ (φ \land g \in (J Cn (L^_{ko} K))) \to L \in Top$
80		eqid	$⊢ L^_{ko} K = L^_{ko} K$
81	80	xkotopon	$⊢ (K \in Top \land L \in Top) \to L^_{ko} K \in TopOn (K Cn L)$
82	78 79 81	syl2anc	$⊢ (φ \land g \in (J Cn (L^_{ko} K))) \to L^_{ko} K \in TopOn (K Cn L)$
83		simpr	$⊢ (φ \land g \in (J Cn (L^_{ko} K))) \to g \in (J Cn (L^_{ko} K))$
84		cnf2	$⊢ (J \in TopOn (X) \land L^_{ko} K \in TopOn (K Cn L) \land g \in (J Cn (L^_{ko} K))) \to g : X ⟶ K Cn L$
85	73 82 83 84	syl3anc	$⊢ (φ \land g \in (J Cn (L^_{ko} K))) \to g : X ⟶ K Cn L$
86	85	feqmptd	$⊢ (φ \land g \in (J Cn (L^_{ko} K))) \to g = (x \in X ⟼ g (x))$
87	2	ad2antrr	$⊢ ((φ \land g \in (J Cn (L^_{ko} K))) \land x \in X) \to K \in TopOn (Y)$
88	14	ad2antrr	$⊢ ((φ \land g \in (J Cn (L^_{ko} K))) \land x \in X) \to L \in TopOn (⋃ L)$
89	85	ffvelrnda	$⊢ ((φ \land g \in (J Cn (L^_{ko} K))) \land x \in X) \to g (x) \in (K Cn L)$
90		cnf2	$⊢ (K \in TopOn (Y) \land L \in TopOn (⋃ L) \land g (x) \in (K Cn L)) \to g (x) : Y ⟶ ⋃ L$
91	87 88 89 90	syl3anc	$⊢ ((φ \land g \in (J Cn (L^_{ko} K))) \land x \in X) \to g (x) : Y ⟶ ⋃ L$
92	91	feqmptd	$⊢ ((φ \land g \in (J Cn (L^_{ko} K))) \land x \in X) \to g (x) = (y \in Y ⟼ g (x) (y))$
93	92	mpteq2dva	$⊢ (φ \land g \in (J Cn (L^_{ko} K))) \to (x \in X ⟼ g (x)) = (x \in X ⟼ (y \in Y ⟼ g (x) (y)))$
94	86 93	eqtrd	$⊢ (φ \land g \in (J Cn (L^_{ko} K))) \to g = (x \in X ⟼ (y \in Y ⟼ g (x) (y)))$
95	94 83	eqeltrrd	$⊢ (φ \land g \in (J Cn (L^_{ko} K))) \to (x \in X ⟼ (y \in Y ⟼ g (x) (y))) \in (J Cn (L^_{ko} K))$
96	73 74 75 76 95	cnmptk2	$⊢ (φ \land g \in (J Cn (L^_{ko} K))) \to (x \in X, y \in Y ⟼ g (x) (y)) \in ((J \times_{t} K) Cn L)$
97	96	adantrr	$⊢ (φ \land (g \in (J Cn (L^_{ko} K)) \land f = (x \in X, y \in Y ⟼ g (x) (y)))) \to (x \in X, y \in Y ⟼ g (x) (y)) \in ((J \times_{t} K) Cn L)$
98	72 97	eqeltrd	$⊢ (φ \land (g \in (J Cn (L^_{ko} K)) \land f = (x \in X, y \in Y ⟼ g (x) (y)))) \to f \in ((J \times_{t} K) Cn L)$
99	94	adantrr	$⊢ (φ \land (g \in (J Cn (L^_{ko} K)) \land f = (x \in X, y \in Y ⟼ g (x) (y)))) \to g = (x \in X ⟼ (y \in Y ⟼ g (x) (y)))$
100		nfv	$⊢ Ⅎ x g \in (J Cn (L^_{ko} K))$
101		nfmpo1	$⊢ \underline{Ⅎ} x (x \in X, y \in Y ⟼ g (x) (y))$
102	101	nfeq2	$⊢ Ⅎ x f = (x \in X, y \in Y ⟼ g (x) (y))$
103	100 102	nfan	$⊢ Ⅎ x (g \in (J Cn (L^_{ko} K)) \land f = (x \in X, y \in Y ⟼ g (x) (y)))$
104	28 103	nfan	$⊢ Ⅎ x (φ \land (g \in (J Cn (L^_{ko} K)) \land f = (x \in X, y \in Y ⟼ g (x) (y))))$
105		nfv	$⊢ Ⅎ y g \in (J Cn (L^_{ko} K))$
106		nfmpo2	$⊢ \underline{Ⅎ} y (x \in X, y \in Y ⟼ g (x) (y))$
107	106	nfeq2	$⊢ Ⅎ y f = (x \in X, y \in Y ⟼ g (x) (y))$
108	105 107	nfan	$⊢ Ⅎ y (g \in (J Cn (L^_{ko} K)) \land f = (x \in X, y \in Y ⟼ g (x) (y)))$
109	34 108	nfan	$⊢ Ⅎ y (φ \land (g \in (J Cn (L^_{ko} K)) \land f = (x \in X, y \in Y ⟼ g (x) (y))))$
110	109 42	nfan	$⊢ Ⅎ y ((φ \land (g \in (J Cn (L^_{ko} K)) \land f = (x \in X, y \in Y ⟼ g (x) (y)))) \land x \in X)$
111	72	oveqd	$⊢ (φ \land (g \in (J Cn (L^_{ko} K)) \land f = (x \in X, y \in Y ⟼ g (x) (y)))) \to x f y = x (x \in X, y \in Y ⟼ g (x) (y)) y$
112		fvex	$⊢ g (x) (y) \in V$
113		eqid	$⊢ (x \in X, y \in Y ⟼ g (x) (y)) = (x \in X, y \in Y ⟼ g (x) (y))$
114	113	ovmpt4g	$⊢ (x \in X \land y \in Y \land g (x) (y) \in V) \to x (x \in X, y \in Y ⟼ g (x) (y)) y = g (x) (y)$
115	112 114	mp3an3	$⊢ (x \in X \land y \in Y) \to x (x \in X, y \in Y ⟼ g (x) (y)) y = g (x) (y)$
116	111 115	sylan9eq	$⊢ ((φ \land (g \in (J Cn (L^_{ko} K)) \land f = (x \in X, y \in Y ⟼ g (x) (y)))) \land (x \in X \land y \in Y)) \to x f y = g (x) (y)$
117	116	expr	$⊢ ((φ \land (g \in (J Cn (L^_{ko} K)) \land f = (x \in X, y \in Y ⟼ g (x) (y)))) \land x \in X) \to (y \in Y \to x f y = g (x) (y))$
118	110 117	ralrimi	$⊢ ((φ \land (g \in (J Cn (L^_{ko} K)) \land f = (x \in X, y \in Y ⟼ g (x) (y)))) \land x \in X) \to \forall y \in Y x f y = g (x) (y)$
119		mpteq12	$⊢ (Y = Y \land \forall y \in Y x f y = g (x) (y)) \to (y \in Y ⟼ x f y) = (y \in Y ⟼ g (x) (y))$
120	64 118 119	sylancr	$⊢ ((φ \land (g \in (J Cn (L^_{ko} K)) \land f = (x \in X, y \in Y ⟼ g (x) (y)))) \land x \in X) \to (y \in Y ⟼ x f y) = (y \in Y ⟼ g (x) (y))$
121	104 120	mpteq2da	$⊢ (φ \land (g \in (J Cn (L^_{ko} K)) \land f = (x \in X, y \in Y ⟼ g (x) (y)))) \to (x \in X ⟼ (y \in Y ⟼ x f y)) = (x \in X ⟼ (y \in Y ⟼ g (x) (y)))$
122	99 121	eqtr4d	$⊢ (φ \land (g \in (J Cn (L^_{ko} K)) \land f = (x \in X, y \in Y ⟼ g (x) (y)))) \to g = (x \in X ⟼ (y \in Y ⟼ x f y))$
123	98 122	jca	$⊢ (φ \land (g \in (J Cn (L^_{ko} K)) \land f = (x \in X, y \in Y ⟼ g (x) (y)))) \to (f \in ((J \times_{t} K) Cn L) \land g = (x \in X ⟼ (y \in Y ⟼ x f y)))$
124	71 123	impbida	$⊢ φ \to ((f \in ((J \times_{t} K) Cn L) \land g = (x \in X ⟼ (y \in Y ⟼ x f y))) \leftrightarrow (g \in (J Cn (L^_{ko} K)) \land f = (x \in X, y \in Y ⟼ g (x) (y))))$
125	124	opabbidv	$⊢ φ \to \{⟨g, f⟩ \| (f \in ((J \times_{t} K) Cn L) \land g = (x \in X ⟼ (y \in Y ⟼ x f y)))\} = \{⟨g, f⟩ \| (g \in (J Cn (L^_{ko} K)) \land f = (x \in X, y \in Y ⟼ g (x) (y)))\}$
126		df-mpt	$⊢ (f \in ((J \times_{t} K) Cn L) ⟼ (x \in X ⟼ (y \in Y ⟼ x f y))) = \{⟨f, g⟩ \| (f \in ((J \times_{t} K) Cn L) \land g = (x \in X ⟼ (y \in Y ⟼ x f y)))\}$
127	3 126	eqtri	$⊢ F = \{⟨f, g⟩ \| (f \in ((J \times_{t} K) Cn L) \land g = (x \in X ⟼ (y \in Y ⟼ x f y)))\}$
128	127	cnveqi	$⊢ F^{-1} = {\{⟨f, g⟩ \| (f \in ((J \times_{t} K) Cn L) \land g = (x \in X ⟼ (y \in Y ⟼ x f y)))\}}^{-1}$
129		cnvopab	$⊢ {\{⟨f, g⟩ \| (f \in ((J \times_{t} K) Cn L) \land g = (x \in X ⟼ (y \in Y ⟼ x f y)))\}}^{-1} = \{⟨g, f⟩ \| (f \in ((J \times_{t} K) Cn L) \land g = (x \in X ⟼ (y \in Y ⟼ x f y)))\}$
130	128 129	eqtri	$⊢ F^{-1} = \{⟨g, f⟩ \| (f \in ((J \times_{t} K) Cn L) \land g = (x \in X ⟼ (y \in Y ⟼ x f y)))\}$
131		df-mpt	$⊢ (g \in (J Cn (L^_{ko} K)) ⟼ (x \in X, y \in Y ⟼ g (x) (y))) = \{⟨g, f⟩ \| (g \in (J Cn (L^_{ko} K)) \land f = (x \in X, y \in Y ⟼ g (x) (y)))\}$
132	125 130 131	3eqtr4g	$⊢ φ \to F^{-1} = (g \in (J Cn (L^_{ko} K)) ⟼ (x \in X, y \in Y ⟼ g (x) (y)))$

Metamath Proof Explorer

Theorem xkocnv

Proof