nqerf

Description: Corollary of nqereu : the function /Q is actually a function. (Contributed by Mario Carneiro, 6-May-2013) (New usage is discouraged.)

		Ref	Expression
	Assertion	nqerf	$⊢ /_{𝑸} : 𝑵 \times 𝑵 ⟶ 𝑸$

Proof

Step	Hyp	Ref	Expression
1		df-erq	$⊢ /_{𝑸} = ~_{𝑸} \cap ((𝑵 \times 𝑵) \times 𝑸)$
2		inss2	$⊢ ~_{𝑸} \cap ((𝑵 \times 𝑵) \times 𝑸) \subseteq (𝑵 \times 𝑵) \times 𝑸$
3	1 2	eqsstri	$⊢ /_{𝑸} \subseteq (𝑵 \times 𝑵) \times 𝑸$
4		xpss	$⊢ (𝑵 \times 𝑵) \times 𝑸 \subseteq V \times V$
5	3 4	sstri	$⊢ /_{𝑸} \subseteq V \times V$
6		df-rel	$⊢ Rel /_{𝑸} \leftrightarrow /_{𝑸} \subseteq V \times V$
7	5 6	mpbir	$⊢ Rel /_{𝑸}$
8		nqereu	$⊢ x \in (𝑵 \times 𝑵) \to \exists! y \in 𝑸 y ~_{𝑸} x$
9		df-reu	$⊢ \exists! y \in 𝑸 y ~_{𝑸} x \leftrightarrow \exists! y (y \in 𝑸 \land y ~_{𝑸} x)$
10		eumo	$⊢ \exists! y (y \in 𝑸 \land y ~_{𝑸} x) \to \exists^{*} y (y \in 𝑸 \land y ~_{𝑸} x)$
11	9 10	sylbi	$⊢ \exists! y \in 𝑸 y ~_{𝑸} x \to \exists^{*} y (y \in 𝑸 \land y ~_{𝑸} x)$
12	8 11	syl	$⊢ x \in (𝑵 \times 𝑵) \to \exists^{*} y (y \in 𝑸 \land y ~_{𝑸} x)$
13		moanimv	$⊢ \exists^{} y (x \in (𝑵 \times 𝑵) \land (y \in 𝑸 \land y ~_{𝑸} x)) \leftrightarrow (x \in (𝑵 \times 𝑵) \to \exists^{} y (y \in 𝑸 \land y ~_{𝑸} x))$
14	12 13	mpbir	$⊢ \exists^{*} y (x \in (𝑵 \times 𝑵) \land (y \in 𝑸 \land y ~_{𝑸} x))$
15	3	brel	$⊢ x /_{𝑸} y \to (x \in (𝑵 \times 𝑵) \land y \in 𝑸)$
16	15	simpld	$⊢ x /_{𝑸} y \to x \in (𝑵 \times 𝑵)$
17	15	simprd	$⊢ x /_{𝑸} y \to y \in 𝑸$
18		enqer	$⊢ ~_{𝑸} Er (𝑵 \times 𝑵)$
19	18	a1i	$⊢ x /_{𝑸} y \to ~_{𝑸} Er (𝑵 \times 𝑵)$
20		inss1	$⊢ ~_{𝑸} \cap ((𝑵 \times 𝑵) \times 𝑸) \subseteq ~_{𝑸}$
21	1 20	eqsstri	$⊢ /_{𝑸} \subseteq ~_{𝑸}$
22	21	ssbri	$⊢ x /_{𝑸} y \to x ~_{𝑸} y$
23	19 22	ersym	$⊢ x /_{𝑸} y \to y ~_{𝑸} x$
24	16 17 23	jca32	$⊢ x /_{𝑸} y \to (x \in (𝑵 \times 𝑵) \land (y \in 𝑸 \land y ~_{𝑸} x))$
25	24	moimi	$⊢ \exists^{} y (x \in (𝑵 \times 𝑵) \land (y \in 𝑸 \land y ~_{𝑸} x)) \to \exists^{} y x /_{𝑸} y$
26	14 25	ax-mp	$⊢ \exists^{*} y x /_{𝑸} y$
27	26	ax-gen	$⊢ \forall x \exists^{*} y x /_{𝑸} y$
28		dffun6	$⊢ Fun /_{𝑸} \leftrightarrow (Rel /_{𝑸} \land \forall x \exists^{*} y x /_{𝑸} y)$
29	7 27 28	mpbir2an	$⊢ Fun /_{𝑸}$
30		dmss	$⊢ /_{𝑸} \subseteq (𝑵 \times 𝑵) \times 𝑸 \to dom /_{𝑸} \subseteq dom ((𝑵 \times 𝑵) \times 𝑸)$
31	3 30	ax-mp	$⊢ dom /_{𝑸} \subseteq dom ((𝑵 \times 𝑵) \times 𝑸)$
32		1nq	$⊢ 1_{𝑸} \in 𝑸$
33		ne0i	$⊢ 1_{𝑸} \in 𝑸 \to 𝑸 \neq \emptyset$
34		dmxp	$⊢ 𝑸 \neq \emptyset \to dom ((𝑵 \times 𝑵) \times 𝑸) = 𝑵 \times 𝑵$
35	32 33 34	mp2b	$⊢ dom ((𝑵 \times 𝑵) \times 𝑸) = 𝑵 \times 𝑵$
36	31 35	sseqtri	$⊢ dom /_{𝑸} \subseteq 𝑵 \times 𝑵$
37		reurex	$⊢ \exists! y \in 𝑸 y ~_{𝑸} x \to \exists y \in 𝑸 y ~_{𝑸} x$
38		simpll	$⊢ ((x \in (𝑵 \times 𝑵) \land y \in 𝑸) \land y ~_{𝑸} x) \to x \in (𝑵 \times 𝑵)$
39		simplr	$⊢ ((x \in (𝑵 \times 𝑵) \land y \in 𝑸) \land y ~_{𝑸} x) \to y \in 𝑸$
40	18	a1i	$⊢ ((x \in (𝑵 \times 𝑵) \land y \in 𝑸) \land y ~_{𝑸} x) \to ~_{𝑸} Er (𝑵 \times 𝑵)$
41		simpr	$⊢ ((x \in (𝑵 \times 𝑵) \land y \in 𝑸) \land y ~_{𝑸} x) \to y ~_{𝑸} x$
42	40 41	ersym	$⊢ ((x \in (𝑵 \times 𝑵) \land y \in 𝑸) \land y ~_{𝑸} x) \to x ~_{𝑸} y$
43	1	breqi	$⊢ x /_{𝑸} y \leftrightarrow x (~_{𝑸} \cap ((𝑵 \times 𝑵) \times 𝑸)) y$
44		brinxp2	$⊢ x (~_{𝑸} \cap ((𝑵 \times 𝑵) \times 𝑸)) y \leftrightarrow ((x \in (𝑵 \times 𝑵) \land y \in 𝑸) \land x ~_{𝑸} y)$
45	43 44	bitri	$⊢ x /_{𝑸} y \leftrightarrow ((x \in (𝑵 \times 𝑵) \land y \in 𝑸) \land x ~_{𝑸} y)$
46	38 39 42 45	syl21anbrc	$⊢ ((x \in (𝑵 \times 𝑵) \land y \in 𝑸) \land y ~_{𝑸} x) \to x /_{𝑸} y$
47	46	ex	$⊢ (x \in (𝑵 \times 𝑵) \land y \in 𝑸) \to (y ~_{𝑸} x \to x /_{𝑸} y)$
48	47	reximdva	$⊢ x \in (𝑵 \times 𝑵) \to (\exists y \in 𝑸 y ~_{𝑸} x \to \exists y \in 𝑸 x /_{𝑸} y)$
49		rexex	$⊢ \exists y \in 𝑸 x /_{𝑸} y \to \exists y x /_{𝑸} y$
50	37 48 49	syl56	$⊢ x \in (𝑵 \times 𝑵) \to (\exists! y \in 𝑸 y ~_{𝑸} x \to \exists y x /_{𝑸} y)$
51	8 50	mpd	$⊢ x \in (𝑵 \times 𝑵) \to \exists y x /_{𝑸} y$
52		vex	$⊢ x \in V$
53	52	eldm	$⊢ x \in dom /_{𝑸} \leftrightarrow \exists y x /_{𝑸} y$
54	51 53	sylibr	$⊢ x \in (𝑵 \times 𝑵) \to x \in dom /_{𝑸}$
55	54	ssriv	$⊢ 𝑵 \times 𝑵 \subseteq dom /_{𝑸}$
56	36 55	eqssi	$⊢ dom /_{𝑸} = 𝑵 \times 𝑵$
57		df-fn	$⊢ /_{𝑸} Fn (𝑵 \times 𝑵) \leftrightarrow (Fun /_{𝑸} \land dom /_{𝑸} = 𝑵 \times 𝑵)$
58	29 56 57	mpbir2an	$⊢ /_{𝑸} Fn (𝑵 \times 𝑵)$
59	3	rnssi	$⊢ ran /_{𝑸} \subseteq ran ((𝑵 \times 𝑵) \times 𝑸)$
60		rnxpss	$⊢ ran ((𝑵 \times 𝑵) \times 𝑸) \subseteq 𝑸$
61	59 60	sstri	$⊢ ran /_{𝑸} \subseteq 𝑸$
62		df-f	$⊢ /_{𝑸} : 𝑵 \times 𝑵 ⟶ 𝑸 \leftrightarrow (/_{𝑸} Fn (𝑵 \times 𝑵) \land ran /_{𝑸} \subseteq 𝑸)$
63	58 61 62	mpbir2an	$⊢ /_{𝑸} : 𝑵 \times 𝑵 ⟶ 𝑸$

Metamath Proof Explorer

Theorem nqerf

Proof