This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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