Theorem 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	⊢ [Q] : ( N × N ) ⟶ Q

Proof

Step	Hyp	Ref	Expression
1		df-erq	⊢ [Q] = ( ~Q ∩ ( ( N × N ) × Q ) )
2		inss2	⊢ ( ~Q ∩ ( ( N × N ) × Q ) ) ⊆ ( ( N × N ) × Q )
3	1 2	eqsstri	⊢ [Q] ⊆ ( ( N × N ) × Q )
4		xpss	⊢ ( ( N × N ) × Q ) ⊆ ( V × V )
5	3 4	sstri	⊢ [Q] ⊆ ( V × V )
6		df-rel	⊢ ( Rel [Q] ↔ [Q] ⊆ ( V × V ) )
7	5 6	mpbir	⊢ Rel [Q]
8		nqereu	⊢ ( 𝑥 ∈ ( N × N ) → ∃! 𝑦 ∈ Q 𝑦 ~Q 𝑥 )
9		df-reu	⊢ ( ∃! 𝑦 ∈ Q 𝑦 ~Q 𝑥 ↔ ∃! 𝑦 ( 𝑦 ∈ Q ∧ 𝑦 ~Q 𝑥 ) )
10		eumo	⊢ ( ∃! 𝑦 ( 𝑦 ∈ Q ∧ 𝑦 ~Q 𝑥 ) → ∃* 𝑦 ( 𝑦 ∈ Q ∧ 𝑦 ~Q 𝑥 ) )
11	9 10	sylbi	⊢ ( ∃! 𝑦 ∈ Q 𝑦 ~Q 𝑥 → ∃* 𝑦 ( 𝑦 ∈ Q ∧ 𝑦 ~Q 𝑥 ) )
12	8 11	syl	⊢ ( 𝑥 ∈ ( N × N ) → ∃* 𝑦 ( 𝑦 ∈ Q ∧ 𝑦 ~Q 𝑥 ) )
13		moanimv	⊢ ( ∃* 𝑦 ( 𝑥 ∈ ( N × N ) ∧ ( 𝑦 ∈ Q ∧ 𝑦 ~Q 𝑥 ) ) ↔ ( 𝑥 ∈ ( N × N ) → ∃* 𝑦 ( 𝑦 ∈ Q ∧ 𝑦 ~Q 𝑥 ) ) )
14	12 13	mpbir	⊢ ∃* 𝑦 ( 𝑥 ∈ ( N × N ) ∧ ( 𝑦 ∈ Q ∧ 𝑦 ~Q 𝑥 ) )
15	3	brel	⊢ ( 𝑥 [Q] 𝑦 → ( 𝑥 ∈ ( N × N ) ∧ 𝑦 ∈ Q ) )
16	15	simpld	⊢ ( 𝑥 [Q] 𝑦 → 𝑥 ∈ ( N × N ) )
17	15	simprd	⊢ ( 𝑥 [Q] 𝑦 → 𝑦 ∈ Q )
18		enqer	⊢ ~Q Er ( N × N )
19	18	a1i	⊢ ( 𝑥 [Q] 𝑦 → ~Q Er ( N × N ) )
20		inss1	⊢ ( ~Q ∩ ( ( N × N ) × Q ) ) ⊆ ~Q
21	1 20	eqsstri	⊢ [Q] ⊆ ~Q
22	21	ssbri	⊢ ( 𝑥 [Q] 𝑦 → 𝑥 ~Q 𝑦 )
23	19 22	ersym	⊢ ( 𝑥 [Q] 𝑦 → 𝑦 ~Q 𝑥 )
24	16 17 23	jca32	⊢ ( 𝑥 [Q] 𝑦 → ( 𝑥 ∈ ( N × N ) ∧ ( 𝑦 ∈ Q ∧ 𝑦 ~Q 𝑥 ) ) )
25	24	moimi	⊢ ( ∃* 𝑦 ( 𝑥 ∈ ( N × N ) ∧ ( 𝑦 ∈ Q ∧ 𝑦 ~Q 𝑥 ) ) → ∃* 𝑦 𝑥 [Q] 𝑦 )
26	14 25	ax-mp	⊢ ∃* 𝑦 𝑥 [Q] 𝑦
27	26	ax-gen	⊢ ∀ 𝑥 ∃* 𝑦 𝑥 [Q] 𝑦
28		dffun6	⊢ ( Fun [Q] ↔ ( Rel [Q] ∧ ∀ 𝑥 ∃* 𝑦 𝑥 [Q] 𝑦 ) )
29	7 27 28	mpbir2an	⊢ Fun [Q]
30		dmss	⊢ ( [Q] ⊆ ( ( N × N ) × Q ) → dom [Q] ⊆ dom ( ( N × N ) × Q ) )
31	3 30	ax-mp	⊢ dom [Q] ⊆ dom ( ( N × N ) × Q )
32		1nq	⊢ 1Q ∈ Q
33		ne0i	⊢ ( 1Q ∈ Q → Q ≠ ∅ )
34		dmxp	⊢ ( Q ≠ ∅ → dom ( ( N × N ) × Q ) = ( N × N ) )
35	32 33 34	mp2b	⊢ dom ( ( N × N ) × Q ) = ( N × N )
36	31 35	sseqtri	⊢ dom [Q] ⊆ ( N × N )
37		reurex	⊢ ( ∃! 𝑦 ∈ Q 𝑦 ~Q 𝑥 → ∃ 𝑦 ∈ Q 𝑦 ~Q 𝑥 )
38		simpll	⊢ ( ( ( 𝑥 ∈ ( N × N ) ∧ 𝑦 ∈ Q ) ∧ 𝑦 ~Q 𝑥 ) → 𝑥 ∈ ( N × N ) )
39		simplr	⊢ ( ( ( 𝑥 ∈ ( N × N ) ∧ 𝑦 ∈ Q ) ∧ 𝑦 ~Q 𝑥 ) → 𝑦 ∈ Q )
40	18	a1i	⊢ ( ( ( 𝑥 ∈ ( N × N ) ∧ 𝑦 ∈ Q ) ∧ 𝑦 ~Q 𝑥 ) → ~Q Er ( N × N ) )
41		simpr	⊢ ( ( ( 𝑥 ∈ ( N × N ) ∧ 𝑦 ∈ Q ) ∧ 𝑦 ~Q 𝑥 ) → 𝑦 ~Q 𝑥 )
42	40 41	ersym	⊢ ( ( ( 𝑥 ∈ ( N × N ) ∧ 𝑦 ∈ Q ) ∧ 𝑦 ~Q 𝑥 ) → 𝑥 ~Q 𝑦 )
43	1	breqi	⊢ ( 𝑥 [Q] 𝑦 ↔ 𝑥 ( ~Q ∩ ( ( N × N ) × Q ) ) 𝑦 )
44		brinxp2	⊢ ( 𝑥 ( ~Q ∩ ( ( N × N ) × Q ) ) 𝑦 ↔ ( ( 𝑥 ∈ ( N × N ) ∧ 𝑦 ∈ Q ) ∧ 𝑥 ~Q 𝑦 ) )
45	43 44	bitri	⊢ ( 𝑥 [Q] 𝑦 ↔ ( ( 𝑥 ∈ ( N × N ) ∧ 𝑦 ∈ Q ) ∧ 𝑥 ~Q 𝑦 ) )
46	38 39 42 45	syl21anbrc	⊢ ( ( ( 𝑥 ∈ ( N × N ) ∧ 𝑦 ∈ Q ) ∧ 𝑦 ~Q 𝑥 ) → 𝑥 [Q] 𝑦 )
47	46	ex	⊢ ( ( 𝑥 ∈ ( N × N ) ∧ 𝑦 ∈ Q ) → ( 𝑦 ~Q 𝑥 → 𝑥 [Q] 𝑦 ) )
48	47	reximdva	⊢ ( 𝑥 ∈ ( N × N ) → ( ∃ 𝑦 ∈ Q 𝑦 ~Q 𝑥 → ∃ 𝑦 ∈ Q 𝑥 [Q] 𝑦 ) )
49		rexex	⊢ ( ∃ 𝑦 ∈ Q 𝑥 [Q] 𝑦 → ∃ 𝑦 𝑥 [Q] 𝑦 )
50	37 48 49	syl56	⊢ ( 𝑥 ∈ ( N × N ) → ( ∃! 𝑦 ∈ Q 𝑦 ~Q 𝑥 → ∃ 𝑦 𝑥 [Q] 𝑦 ) )
51	8 50	mpd	⊢ ( 𝑥 ∈ ( N × N ) → ∃ 𝑦 𝑥 [Q] 𝑦 )
52		vex	⊢ 𝑥 ∈ V
53	52	eldm	⊢ ( 𝑥 ∈ dom [Q] ↔ ∃ 𝑦 𝑥 [Q] 𝑦 )
54	51 53	sylibr	⊢ ( 𝑥 ∈ ( N × N ) → 𝑥 ∈ dom [Q] )
55	54	ssriv	⊢ ( N × N ) ⊆ dom [Q]
56	36 55	eqssi	⊢ dom [Q] = ( N × N )
57		df-fn	⊢ ( [Q] Fn ( N × N ) ↔ ( Fun [Q] ∧ dom [Q] = ( N × N ) ) )
58	29 56 57	mpbir2an	⊢ [Q] Fn ( N × N )
59	3	rnssi	⊢ ran [Q] ⊆ ran ( ( N × N ) × Q )
60		rnxpss	⊢ ran ( ( N × N ) × Q ) ⊆ Q
61	59 60	sstri	⊢ ran [Q] ⊆ Q
62		df-f	⊢ ( [Q] : ( N × N ) ⟶ Q ↔ ( [Q] Fn ( N × N ) ∧ ran [Q] ⊆ Q ) )
63	58 61 62	mpbir2an	⊢ [Q] : ( N × N ) ⟶ Q