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

Metamath Proof Explorer

Theorem nqereu

Description: There is a unique element of Q. equivalent to each element of N. X. N. . (Contributed by Mario Carneiro, 28-Apr-2013) (New usage is discouraged.)

Ref Expression
Assertion nqereu ( 𝐴 ∈ ( N × N ) → ∃! 𝑥 ∈ Q 𝑥 ~Q 𝐴 )

Proof

Step Hyp Ref Expression
1 elxp2 ⊢ ( 𝐴 ∈ ( N × N ) ↔ ∃ 𝑎 ∈ N ∃ 𝑏 ∈ N 𝐴 = ⟨ 𝑎 , 𝑏 ⟩ )
2 pion ⊢ ( 𝑏 ∈ N → 𝑏 ∈ On )
3 onsuc ⊢ ( 𝑏 ∈ On → suc 𝑏 ∈ On )
4 2 3 syl ⊢ ( 𝑏 ∈ N → suc 𝑏 ∈ On )
5 vex ⊢ 𝑏 ∈ V
6 5 sucid ⊢ 𝑏 ∈ suc 𝑏
7 eleq2 ⊢ ( 𝑦 = suc 𝑏 → ( 𝑏 ∈ 𝑦 ↔ 𝑏 ∈ suc 𝑏 ) )
8 7 rspcev ⊢ ( ( suc 𝑏 ∈ On ∧ 𝑏 ∈ suc 𝑏 ) → ∃ 𝑦 ∈ On 𝑏 ∈ 𝑦 )
9 4 6 8 sylancl ⊢ ( 𝑏 ∈ N → ∃ 𝑦 ∈ On 𝑏 ∈ 𝑦 )
10 9 adantl ⊢ ( ( 𝑎 ∈ N ∧ 𝑏 ∈ N ) → ∃ 𝑦 ∈ On 𝑏 ∈ 𝑦 )
11 elequ2 ⊢ ( 𝑦 = 𝑚 → ( 𝑏 ∈ 𝑦 ↔ 𝑏 ∈ 𝑚 ) )
12 11 imbi1d ⊢ ( 𝑦 = 𝑚 → ( ( 𝑏 ∈ 𝑦 → ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ 𝑎 , 𝑏 ⟩ ) ↔ ( 𝑏 ∈ 𝑚 → ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ 𝑎 , 𝑏 ⟩ ) ) )
13 12 2ralbidv ⊢ ( 𝑦 = 𝑚 → ( ∀ 𝑎 ∈ N ∀ 𝑏 ∈ N ( 𝑏 ∈ 𝑦 → ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ 𝑎 , 𝑏 ⟩ ) ↔ ∀ 𝑎 ∈ N ∀ 𝑏 ∈ N ( 𝑏 ∈ 𝑚 → ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ 𝑎 , 𝑏 ⟩ ) ) )
14 opeq1 ⊢ ( 𝑐 = 𝑎 → ⟨ 𝑐 , 𝑑 ⟩ = ⟨ 𝑎 , 𝑑 ⟩ )
15 14 breq2d ⊢ ( 𝑐 = 𝑎 → ( 𝑥 ~Q ⟨ 𝑐 , 𝑑 ⟩ ↔ 𝑥 ~Q ⟨ 𝑎 , 𝑑 ⟩ ) )
16 15 rexbidv ⊢ ( 𝑐 = 𝑎 → ( ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ 𝑐 , 𝑑 ⟩ ↔ ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ 𝑎 , 𝑑 ⟩ ) )
17 16 imbi2d ⊢ ( 𝑐 = 𝑎 → ( ( 𝑑 ∈ 𝑚 → ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ 𝑐 , 𝑑 ⟩ ) ↔ ( 𝑑 ∈ 𝑚 → ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ 𝑎 , 𝑑 ⟩ ) ) )
18 elequ1 ⊢ ( 𝑑 = 𝑏 → ( 𝑑 ∈ 𝑚 ↔ 𝑏 ∈ 𝑚 ) )
19 opeq2 ⊢ ( 𝑑 = 𝑏 → ⟨ 𝑎 , 𝑑 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ )
20 19 breq2d ⊢ ( 𝑑 = 𝑏 → ( 𝑥 ~Q ⟨ 𝑎 , 𝑑 ⟩ ↔ 𝑥 ~Q ⟨ 𝑎 , 𝑏 ⟩ ) )
21 20 rexbidv ⊢ ( 𝑑 = 𝑏 → ( ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ 𝑎 , 𝑑 ⟩ ↔ ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ 𝑎 , 𝑏 ⟩ ) )
22 18 21 imbi12d ⊢ ( 𝑑 = 𝑏 → ( ( 𝑑 ∈ 𝑚 → ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ 𝑎 , 𝑑 ⟩ ) ↔ ( 𝑏 ∈ 𝑚 → ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ 𝑎 , 𝑏 ⟩ ) ) )
23 17 22 cbvral2vw ⊢ ( ∀ 𝑐 ∈ N ∀ 𝑑 ∈ N ( 𝑑 ∈ 𝑚 → ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ 𝑐 , 𝑑 ⟩ ) ↔ ∀ 𝑎 ∈ N ∀ 𝑏 ∈ N ( 𝑏 ∈ 𝑚 → ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ 𝑎 , 𝑏 ⟩ ) )
24 23 ralbii ⊢ ( ∀ 𝑚 ∈ 𝑦 ∀ 𝑐 ∈ N ∀ 𝑑 ∈ N ( 𝑑 ∈ 𝑚 → ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ 𝑐 , 𝑑 ⟩ ) ↔ ∀ 𝑚 ∈ 𝑦 ∀ 𝑎 ∈ N ∀ 𝑏 ∈ N ( 𝑏 ∈ 𝑚 → ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ 𝑎 , 𝑏 ⟩ ) )
25 rexnal ⊢ ( ∃ 𝑧 ∈ ( N × N ) ¬ ( ⟨ 𝑎 , 𝑏 ⟩ ~Q 𝑧 → ¬ ( 2nd ‘ 𝑧 ) <N 𝑏 ) ↔ ¬ ∀ 𝑧 ∈ ( N × N ) ( ⟨ 𝑎 , 𝑏 ⟩ ~Q 𝑧 → ¬ ( 2nd ‘ 𝑧 ) <N 𝑏 ) )
26 pm4.63 ⊢ ( ¬ ( ⟨ 𝑎 , 𝑏 ⟩ ~Q 𝑧 → ¬ ( 2nd ‘ 𝑧 ) <N 𝑏 ) ↔ ( ⟨ 𝑎 , 𝑏 ⟩ ~Q 𝑧 ∧ ( 2nd ‘ 𝑧 ) <N 𝑏 ) )
27 xp2nd ⊢ ( 𝑧 ∈ ( N × N ) → ( 2nd ‘ 𝑧 ) ∈ N )
28 ltpiord ⊢ ( ( ( 2nd ‘ 𝑧 ) ∈ N ∧ 𝑏 ∈ N ) → ( ( 2nd ‘ 𝑧 ) <N 𝑏 ↔ ( 2nd ‘ 𝑧 ) ∈ 𝑏 ) )
29 28 ancoms ⊢ ( ( 𝑏 ∈ N ∧ ( 2nd ‘ 𝑧 ) ∈ N ) → ( ( 2nd ‘ 𝑧 ) <N 𝑏 ↔ ( 2nd ‘ 𝑧 ) ∈ 𝑏 ) )
30 27 29 sylan2 ⊢ ( ( 𝑏 ∈ N ∧ 𝑧 ∈ ( N × N ) ) → ( ( 2nd ‘ 𝑧 ) <N 𝑏 ↔ ( 2nd ‘ 𝑧 ) ∈ 𝑏 ) )
31 30 adantll ⊢ ( ( ( 𝑎 ∈ N ∧ 𝑏 ∈ N ) ∧ 𝑧 ∈ ( N × N ) ) → ( ( 2nd ‘ 𝑧 ) <N 𝑏 ↔ ( 2nd ‘ 𝑧 ) ∈ 𝑏 ) )
32 31 anbi2d ⊢ ( ( ( 𝑎 ∈ N ∧ 𝑏 ∈ N ) ∧ 𝑧 ∈ ( N × N ) ) → ( ( ⟨ 𝑎 , 𝑏 ⟩ ~Q 𝑧 ∧ ( 2nd ‘ 𝑧 ) <N 𝑏 ) ↔ ( ⟨ 𝑎 , 𝑏 ⟩ ~Q 𝑧 ∧ ( 2nd ‘ 𝑧 ) ∈ 𝑏 ) ) )
33 26 32 bitrid ⊢ ( ( ( 𝑎 ∈ N ∧ 𝑏 ∈ N ) ∧ 𝑧 ∈ ( N × N ) ) → ( ¬ ( ⟨ 𝑎 , 𝑏 ⟩ ~Q 𝑧 → ¬ ( 2nd ‘ 𝑧 ) <N 𝑏 ) ↔ ( ⟨ 𝑎 , 𝑏 ⟩ ~Q 𝑧 ∧ ( 2nd ‘ 𝑧 ) ∈ 𝑏 ) ) )
34 33 rexbidva ⊢ ( ( 𝑎 ∈ N ∧ 𝑏 ∈ N ) → ( ∃ 𝑧 ∈ ( N × N ) ¬ ( ⟨ 𝑎 , 𝑏 ⟩ ~Q 𝑧 → ¬ ( 2nd ‘ 𝑧 ) <N 𝑏 ) ↔ ∃ 𝑧 ∈ ( N × N ) ( ⟨ 𝑎 , 𝑏 ⟩ ~Q 𝑧 ∧ ( 2nd ‘ 𝑧 ) ∈ 𝑏 ) ) )
35 25 34 bitr3id ⊢ ( ( 𝑎 ∈ N ∧ 𝑏 ∈ N ) → ( ¬ ∀ 𝑧 ∈ ( N × N ) ( ⟨ 𝑎 , 𝑏 ⟩ ~Q 𝑧 → ¬ ( 2nd ‘ 𝑧 ) <N 𝑏 ) ↔ ∃ 𝑧 ∈ ( N × N ) ( ⟨ 𝑎 , 𝑏 ⟩ ~Q 𝑧 ∧ ( 2nd ‘ 𝑧 ) ∈ 𝑏 ) ) )
36 xp1st ⊢ ( 𝑧 ∈ ( N × N ) → ( 1st ‘ 𝑧 ) ∈ N )
37 elequ2 ⊢ ( 𝑚 = 𝑏 → ( 𝑑 ∈ 𝑚 ↔ 𝑑 ∈ 𝑏 ) )
38 37 imbi1d ⊢ ( 𝑚 = 𝑏 → ( ( 𝑑 ∈ 𝑚 → ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ 𝑐 , 𝑑 ⟩ ) ↔ ( 𝑑 ∈ 𝑏 → ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ 𝑐 , 𝑑 ⟩ ) ) )
39 38 2ralbidv ⊢ ( 𝑚 = 𝑏 → ( ∀ 𝑐 ∈ N ∀ 𝑑 ∈ N ( 𝑑 ∈ 𝑚 → ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ 𝑐 , 𝑑 ⟩ ) ↔ ∀ 𝑐 ∈ N ∀ 𝑑 ∈ N ( 𝑑 ∈ 𝑏 → ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ 𝑐 , 𝑑 ⟩ ) ) )
40 39 rspccv ⊢ ( ∀ 𝑚 ∈ 𝑦 ∀ 𝑐 ∈ N ∀ 𝑑 ∈ N ( 𝑑 ∈ 𝑚 → ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ 𝑐 , 𝑑 ⟩ ) → ( 𝑏 ∈ 𝑦 → ∀ 𝑐 ∈ N ∀ 𝑑 ∈ N ( 𝑑 ∈ 𝑏 → ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ 𝑐 , 𝑑 ⟩ ) ) )
41 opeq1 ⊢ ( 𝑐 = ( 1st ‘ 𝑧 ) → ⟨ 𝑐 , 𝑑 ⟩ = ⟨ ( 1st ‘ 𝑧 ) , 𝑑 ⟩ )
42 41 breq2d ⊢ ( 𝑐 = ( 1st ‘ 𝑧 ) → ( 𝑥 ~Q ⟨ 𝑐 , 𝑑 ⟩ ↔ 𝑥 ~Q ⟨ ( 1st ‘ 𝑧 ) , 𝑑 ⟩ ) )
43 42 rexbidv ⊢ ( 𝑐 = ( 1st ‘ 𝑧 ) → ( ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ 𝑐 , 𝑑 ⟩ ↔ ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ ( 1st ‘ 𝑧 ) , 𝑑 ⟩ ) )
44 43 imbi2d ⊢ ( 𝑐 = ( 1st ‘ 𝑧 ) → ( ( 𝑑 ∈ 𝑏 → ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ 𝑐 , 𝑑 ⟩ ) ↔ ( 𝑑 ∈ 𝑏 → ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ ( 1st ‘ 𝑧 ) , 𝑑 ⟩ ) ) )
45 44 ralbidv ⊢ ( 𝑐 = ( 1st ‘ 𝑧 ) → ( ∀ 𝑑 ∈ N ( 𝑑 ∈ 𝑏 → ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ 𝑐 , 𝑑 ⟩ ) ↔ ∀ 𝑑 ∈ N ( 𝑑 ∈ 𝑏 → ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ ( 1st ‘ 𝑧 ) , 𝑑 ⟩ ) ) )
46 45 rspccv ⊢ ( ∀ 𝑐 ∈ N ∀ 𝑑 ∈ N ( 𝑑 ∈ 𝑏 → ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ 𝑐 , 𝑑 ⟩ ) → ( ( 1st ‘ 𝑧 ) ∈ N → ∀ 𝑑 ∈ N ( 𝑑 ∈ 𝑏 → ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ ( 1st ‘ 𝑧 ) , 𝑑 ⟩ ) ) )
47 eleq1 ⊢ ( 𝑑 = ( 2nd ‘ 𝑧 ) → ( 𝑑 ∈ 𝑏 ↔ ( 2nd ‘ 𝑧 ) ∈ 𝑏 ) )
48 opeq2 ⊢ ( 𝑑 = ( 2nd ‘ 𝑧 ) → ⟨ ( 1st ‘ 𝑧 ) , 𝑑 ⟩ = ⟨ ( 1st ‘ 𝑧 ) , ( 2nd ‘ 𝑧 ) ⟩ )
49 48 breq2d ⊢ ( 𝑑 = ( 2nd ‘ 𝑧 ) → ( 𝑥 ~Q ⟨ ( 1st ‘ 𝑧 ) , 𝑑 ⟩ ↔ 𝑥 ~Q ⟨ ( 1st ‘ 𝑧 ) , ( 2nd ‘ 𝑧 ) ⟩ ) )
50 49 rexbidv ⊢ ( 𝑑 = ( 2nd ‘ 𝑧 ) → ( ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ ( 1st ‘ 𝑧 ) , 𝑑 ⟩ ↔ ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ ( 1st ‘ 𝑧 ) , ( 2nd ‘ 𝑧 ) ⟩ ) )
51 47 50 imbi12d ⊢ ( 𝑑 = ( 2nd ‘ 𝑧 ) → ( ( 𝑑 ∈ 𝑏 → ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ ( 1st ‘ 𝑧 ) , 𝑑 ⟩ ) ↔ ( ( 2nd ‘ 𝑧 ) ∈ 𝑏 → ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ ( 1st ‘ 𝑧 ) , ( 2nd ‘ 𝑧 ) ⟩ ) ) )
52 51 rspccv ⊢ ( ∀ 𝑑 ∈ N ( 𝑑 ∈ 𝑏 → ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ ( 1st ‘ 𝑧 ) , 𝑑 ⟩ ) → ( ( 2nd ‘ 𝑧 ) ∈ N → ( ( 2nd ‘ 𝑧 ) ∈ 𝑏 → ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ ( 1st ‘ 𝑧 ) , ( 2nd ‘ 𝑧 ) ⟩ ) ) )
53 46 52 syl6 ⊢ ( ∀ 𝑐 ∈ N ∀ 𝑑 ∈ N ( 𝑑 ∈ 𝑏 → ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ 𝑐 , 𝑑 ⟩ ) → ( ( 1st ‘ 𝑧 ) ∈ N → ( ( 2nd ‘ 𝑧 ) ∈ N → ( ( 2nd ‘ 𝑧 ) ∈ 𝑏 → ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ ( 1st ‘ 𝑧 ) , ( 2nd ‘ 𝑧 ) ⟩ ) ) ) )
54 40 53 syl6 ⊢ ( ∀ 𝑚 ∈ 𝑦 ∀ 𝑐 ∈ N ∀ 𝑑 ∈ N ( 𝑑 ∈ 𝑚 → ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ 𝑐 , 𝑑 ⟩ ) → ( 𝑏 ∈ 𝑦 → ( ( 1st ‘ 𝑧 ) ∈ N → ( ( 2nd ‘ 𝑧 ) ∈ N → ( ( 2nd ‘ 𝑧 ) ∈ 𝑏 → ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ ( 1st ‘ 𝑧 ) , ( 2nd ‘ 𝑧 ) ⟩ ) ) ) ) )
55 54 imp ⊢ ( ( ∀ 𝑚 ∈ 𝑦 ∀ 𝑐 ∈ N ∀ 𝑑 ∈ N ( 𝑑 ∈ 𝑚 → ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ 𝑐 , 𝑑 ⟩ ) ∧ 𝑏 ∈ 𝑦 ) → ( ( 1st ‘ 𝑧 ) ∈ N → ( ( 2nd ‘ 𝑧 ) ∈ N → ( ( 2nd ‘ 𝑧 ) ∈ 𝑏 → ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ ( 1st ‘ 𝑧 ) , ( 2nd ‘ 𝑧 ) ⟩ ) ) ) )
56 36 55 syl5 ⊢ ( ( ∀ 𝑚 ∈ 𝑦 ∀ 𝑐 ∈ N ∀ 𝑑 ∈ N ( 𝑑 ∈ 𝑚 → ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ 𝑐 , 𝑑 ⟩ ) ∧ 𝑏 ∈ 𝑦 ) → ( 𝑧 ∈ ( N × N ) → ( ( 2nd ‘ 𝑧 ) ∈ N → ( ( 2nd ‘ 𝑧 ) ∈ 𝑏 → ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ ( 1st ‘ 𝑧 ) , ( 2nd ‘ 𝑧 ) ⟩ ) ) ) )
57 27 56 mpdi ⊢ ( ( ∀ 𝑚 ∈ 𝑦 ∀ 𝑐 ∈ N ∀ 𝑑 ∈ N ( 𝑑 ∈ 𝑚 → ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ 𝑐 , 𝑑 ⟩ ) ∧ 𝑏 ∈ 𝑦 ) → ( 𝑧 ∈ ( N × N ) → ( ( 2nd ‘ 𝑧 ) ∈ 𝑏 → ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ ( 1st ‘ 𝑧 ) , ( 2nd ‘ 𝑧 ) ⟩ ) ) )
58 57 3imp ⊢ ( ( ( ∀ 𝑚 ∈ 𝑦 ∀ 𝑐 ∈ N ∀ 𝑑 ∈ N ( 𝑑 ∈ 𝑚 → ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ 𝑐 , 𝑑 ⟩ ) ∧ 𝑏 ∈ 𝑦 ) ∧ 𝑧 ∈ ( N × N ) ∧ ( 2nd ‘ 𝑧 ) ∈ 𝑏 ) → ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ ( 1st ‘ 𝑧 ) , ( 2nd ‘ 𝑧 ) ⟩ )
59 1st2nd2 ⊢ ( 𝑧 ∈ ( N × N ) → 𝑧 = ⟨ ( 1st ‘ 𝑧 ) , ( 2nd ‘ 𝑧 ) ⟩ )
60 59 breq2d ⊢ ( 𝑧 ∈ ( N × N ) → ( 𝑥 ~Q 𝑧 ↔ 𝑥 ~Q ⟨ ( 1st ‘ 𝑧 ) , ( 2nd ‘ 𝑧 ) ⟩ ) )
61 60 rexbidv ⊢ ( 𝑧 ∈ ( N × N ) → ( ∃ 𝑥 ∈ Q 𝑥 ~Q 𝑧 ↔ ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ ( 1st ‘ 𝑧 ) , ( 2nd ‘ 𝑧 ) ⟩ ) )
62 61 3ad2ant2 ⊢ ( ( ( ∀ 𝑚 ∈ 𝑦 ∀ 𝑐 ∈ N ∀ 𝑑 ∈ N ( 𝑑 ∈ 𝑚 → ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ 𝑐 , 𝑑 ⟩ ) ∧ 𝑏 ∈ 𝑦 ) ∧ 𝑧 ∈ ( N × N ) ∧ ( 2nd ‘ 𝑧 ) ∈ 𝑏 ) → ( ∃ 𝑥 ∈ Q 𝑥 ~Q 𝑧 ↔ ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ ( 1st ‘ 𝑧 ) , ( 2nd ‘ 𝑧 ) ⟩ ) )
63 58 62 mpbird ⊢ ( ( ( ∀ 𝑚 ∈ 𝑦 ∀ 𝑐 ∈ N ∀ 𝑑 ∈ N ( 𝑑 ∈ 𝑚 → ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ 𝑐 , 𝑑 ⟩ ) ∧ 𝑏 ∈ 𝑦 ) ∧ 𝑧 ∈ ( N × N ) ∧ ( 2nd ‘ 𝑧 ) ∈ 𝑏 ) → ∃ 𝑥 ∈ Q 𝑥 ~Q 𝑧 )
64 enqer ⊢ ~Q Er ( N × N )
65 64 a1i ⊢ ( ( ⟨ 𝑎 , 𝑏 ⟩ ~Q 𝑧 ∧ 𝑥 ~Q 𝑧 ) → ~Q Er ( N × N ) )
66 simpr ⊢ ( ( ⟨ 𝑎 , 𝑏 ⟩ ~Q 𝑧 ∧ 𝑥 ~Q 𝑧 ) → 𝑥 ~Q 𝑧 )
67 simpl ⊢ ( ( ⟨ 𝑎 , 𝑏 ⟩ ~Q 𝑧 ∧ 𝑥 ~Q 𝑧 ) → ⟨ 𝑎 , 𝑏 ⟩ ~Q 𝑧 )
68 65 66 67 ertr4d ⊢ ( ( ⟨ 𝑎 , 𝑏 ⟩ ~Q 𝑧 ∧ 𝑥 ~Q 𝑧 ) → 𝑥 ~Q ⟨ 𝑎 , 𝑏 ⟩ )
69 68 ex ⊢ ( ⟨ 𝑎 , 𝑏 ⟩ ~Q 𝑧 → ( 𝑥 ~Q 𝑧 → 𝑥 ~Q ⟨ 𝑎 , 𝑏 ⟩ ) )
70 69 reximdv ⊢ ( ⟨ 𝑎 , 𝑏 ⟩ ~Q 𝑧 → ( ∃ 𝑥 ∈ Q 𝑥 ~Q 𝑧 → ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ 𝑎 , 𝑏 ⟩ ) )
71 63 70 syl5com ⊢ ( ( ( ∀ 𝑚 ∈ 𝑦 ∀ 𝑐 ∈ N ∀ 𝑑 ∈ N ( 𝑑 ∈ 𝑚 → ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ 𝑐 , 𝑑 ⟩ ) ∧ 𝑏 ∈ 𝑦 ) ∧ 𝑧 ∈ ( N × N ) ∧ ( 2nd ‘ 𝑧 ) ∈ 𝑏 ) → ( ⟨ 𝑎 , 𝑏 ⟩ ~Q 𝑧 → ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ 𝑎 , 𝑏 ⟩ ) )
72 71 3expia ⊢ ( ( ( ∀ 𝑚 ∈ 𝑦 ∀ 𝑐 ∈ N ∀ 𝑑 ∈ N ( 𝑑 ∈ 𝑚 → ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ 𝑐 , 𝑑 ⟩ ) ∧ 𝑏 ∈ 𝑦 ) ∧ 𝑧 ∈ ( N × N ) ) → ( ( 2nd ‘ 𝑧 ) ∈ 𝑏 → ( ⟨ 𝑎 , 𝑏 ⟩ ~Q 𝑧 → ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ 𝑎 , 𝑏 ⟩ ) ) )
73 72 impcomd ⊢ ( ( ( ∀ 𝑚 ∈ 𝑦 ∀ 𝑐 ∈ N ∀ 𝑑 ∈ N ( 𝑑 ∈ 𝑚 → ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ 𝑐 , 𝑑 ⟩ ) ∧ 𝑏 ∈ 𝑦 ) ∧ 𝑧 ∈ ( N × N ) ) → ( ( ⟨ 𝑎 , 𝑏 ⟩ ~Q 𝑧 ∧ ( 2nd ‘ 𝑧 ) ∈ 𝑏 ) → ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ 𝑎 , 𝑏 ⟩ ) )
74 73 rexlimdva ⊢ ( ( ∀ 𝑚 ∈ 𝑦 ∀ 𝑐 ∈ N ∀ 𝑑 ∈ N ( 𝑑 ∈ 𝑚 → ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ 𝑐 , 𝑑 ⟩ ) ∧ 𝑏 ∈ 𝑦 ) → ( ∃ 𝑧 ∈ ( N × N ) ( ⟨ 𝑎 , 𝑏 ⟩ ~Q 𝑧 ∧ ( 2nd ‘ 𝑧 ) ∈ 𝑏 ) → ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ 𝑎 , 𝑏 ⟩ ) )
75 74 ex ⊢ ( ∀ 𝑚 ∈ 𝑦 ∀ 𝑐 ∈ N ∀ 𝑑 ∈ N ( 𝑑 ∈ 𝑚 → ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ 𝑐 , 𝑑 ⟩ ) → ( 𝑏 ∈ 𝑦 → ( ∃ 𝑧 ∈ ( N × N ) ( ⟨ 𝑎 , 𝑏 ⟩ ~Q 𝑧 ∧ ( 2nd ‘ 𝑧 ) ∈ 𝑏 ) → ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ 𝑎 , 𝑏 ⟩ ) ) )
76 75 com3r ⊢ ( ∃ 𝑧 ∈ ( N × N ) ( ⟨ 𝑎 , 𝑏 ⟩ ~Q 𝑧 ∧ ( 2nd ‘ 𝑧 ) ∈ 𝑏 ) → ( ∀ 𝑚 ∈ 𝑦 ∀ 𝑐 ∈ N ∀ 𝑑 ∈ N ( 𝑑 ∈ 𝑚 → ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ 𝑐 , 𝑑 ⟩ ) → ( 𝑏 ∈ 𝑦 → ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ 𝑎 , 𝑏 ⟩ ) ) )
77 35 76 biimtrdi ⊢ ( ( 𝑎 ∈ N ∧ 𝑏 ∈ N ) → ( ¬ ∀ 𝑧 ∈ ( N × N ) ( ⟨ 𝑎 , 𝑏 ⟩ ~Q 𝑧 → ¬ ( 2nd ‘ 𝑧 ) <N 𝑏 ) → ( ∀ 𝑚 ∈ 𝑦 ∀ 𝑐 ∈ N ∀ 𝑑 ∈ N ( 𝑑 ∈ 𝑚 → ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ 𝑐 , 𝑑 ⟩ ) → ( 𝑏 ∈ 𝑦 → ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ 𝑎 , 𝑏 ⟩ ) ) ) )
78 77 com13 ⊢ ( ∀ 𝑚 ∈ 𝑦 ∀ 𝑐 ∈ N ∀ 𝑑 ∈ N ( 𝑑 ∈ 𝑚 → ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ 𝑐 , 𝑑 ⟩ ) → ( ¬ ∀ 𝑧 ∈ ( N × N ) ( ⟨ 𝑎 , 𝑏 ⟩ ~Q 𝑧 → ¬ ( 2nd ‘ 𝑧 ) <N 𝑏 ) → ( ( 𝑎 ∈ N ∧ 𝑏 ∈ N ) → ( 𝑏 ∈ 𝑦 → ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ 𝑎 , 𝑏 ⟩ ) ) ) )
79 mulcompi ⊢ ( 𝑎 ·N 𝑏 ) = ( 𝑏 ·N 𝑎 )
80 enqbreq ⊢ ( ( ( 𝑎 ∈ N ∧ 𝑏 ∈ N ) ∧ ( 𝑎 ∈ N ∧ 𝑏 ∈ N ) ) → ( ⟨ 𝑎 , 𝑏 ⟩ ~Q ⟨ 𝑎 , 𝑏 ⟩ ↔ ( 𝑎 ·N 𝑏 ) = ( 𝑏 ·N 𝑎 ) ) )
81 80 anidms ⊢ ( ( 𝑎 ∈ N ∧ 𝑏 ∈ N ) → ( ⟨ 𝑎 , 𝑏 ⟩ ~Q ⟨ 𝑎 , 𝑏 ⟩ ↔ ( 𝑎 ·N 𝑏 ) = ( 𝑏 ·N 𝑎 ) ) )
82 79 81 mpbiri ⊢ ( ( 𝑎 ∈ N ∧ 𝑏 ∈ N ) → ⟨ 𝑎 , 𝑏 ⟩ ~Q ⟨ 𝑎 , 𝑏 ⟩ )
83 opelxpi ⊢ ( ( 𝑎 ∈ N ∧ 𝑏 ∈ N ) → ⟨ 𝑎 , 𝑏 ⟩ ∈ ( N × N ) )
84 breq1 ⊢ ( 𝑦 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝑦 ~Q 𝑧 ↔ ⟨ 𝑎 , 𝑏 ⟩ ~Q 𝑧 ) )
85 vex ⊢ 𝑎 ∈ V
86 85 5 op2ndd ⊢ ( 𝑦 = ⟨ 𝑎 , 𝑏 ⟩ → ( 2nd ‘ 𝑦 ) = 𝑏 )
87 86 breq2d ⊢ ( 𝑦 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( 2nd ‘ 𝑧 ) <N ( 2nd ‘ 𝑦 ) ↔ ( 2nd ‘ 𝑧 ) <N 𝑏 ) )
88 87 notbid ⊢ ( 𝑦 = ⟨ 𝑎 , 𝑏 ⟩ → ( ¬ ( 2nd ‘ 𝑧 ) <N ( 2nd ‘ 𝑦 ) ↔ ¬ ( 2nd ‘ 𝑧 ) <N 𝑏 ) )
89 84 88 imbi12d ⊢ ( 𝑦 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( 𝑦 ~Q 𝑧 → ¬ ( 2nd ‘ 𝑧 ) <N ( 2nd ‘ 𝑦 ) ) ↔ ( ⟨ 𝑎 , 𝑏 ⟩ ~Q 𝑧 → ¬ ( 2nd ‘ 𝑧 ) <N 𝑏 ) ) )
90 89 ralbidv ⊢ ( 𝑦 = ⟨ 𝑎 , 𝑏 ⟩ → ( ∀ 𝑧 ∈ ( N × N ) ( 𝑦 ~Q 𝑧 → ¬ ( 2nd ‘ 𝑧 ) <N ( 2nd ‘ 𝑦 ) ) ↔ ∀ 𝑧 ∈ ( N × N ) ( ⟨ 𝑎 , 𝑏 ⟩ ~Q 𝑧 → ¬ ( 2nd ‘ 𝑧 ) <N 𝑏 ) ) )
91 df-nq ⊢ Q = { 𝑦 ∈ ( N × N ) ∣ ∀ 𝑧 ∈ ( N × N ) ( 𝑦 ~Q 𝑧 → ¬ ( 2nd ‘ 𝑧 ) <N ( 2nd ‘ 𝑦 ) ) }
92 90 91 elrab2 ⊢ ( ⟨ 𝑎 , 𝑏 ⟩ ∈ Q ↔ ( ⟨ 𝑎 , 𝑏 ⟩ ∈ ( N × N ) ∧ ∀ 𝑧 ∈ ( N × N ) ( ⟨ 𝑎 , 𝑏 ⟩ ~Q 𝑧 → ¬ ( 2nd ‘ 𝑧 ) <N 𝑏 ) ) )
93 92 simplbi2 ⊢ ( ⟨ 𝑎 , 𝑏 ⟩ ∈ ( N × N ) → ( ∀ 𝑧 ∈ ( N × N ) ( ⟨ 𝑎 , 𝑏 ⟩ ~Q 𝑧 → ¬ ( 2nd ‘ 𝑧 ) <N 𝑏 ) → ⟨ 𝑎 , 𝑏 ⟩ ∈ Q ) )
94 83 93 syl ⊢ ( ( 𝑎 ∈ N ∧ 𝑏 ∈ N ) → ( ∀ 𝑧 ∈ ( N × N ) ( ⟨ 𝑎 , 𝑏 ⟩ ~Q 𝑧 → ¬ ( 2nd ‘ 𝑧 ) <N 𝑏 ) → ⟨ 𝑎 , 𝑏 ⟩ ∈ Q ) )
95 breq1 ⊢ ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝑥 ~Q ⟨ 𝑎 , 𝑏 ⟩ ↔ ⟨ 𝑎 , 𝑏 ⟩ ~Q ⟨ 𝑎 , 𝑏 ⟩ ) )
96 95 rspcev ⊢ ( ( ⟨ 𝑎 , 𝑏 ⟩ ∈ Q ∧ ⟨ 𝑎 , 𝑏 ⟩ ~Q ⟨ 𝑎 , 𝑏 ⟩ ) → ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ 𝑎 , 𝑏 ⟩ )
97 96 expcom ⊢ ( ⟨ 𝑎 , 𝑏 ⟩ ~Q ⟨ 𝑎 , 𝑏 ⟩ → ( ⟨ 𝑎 , 𝑏 ⟩ ∈ Q → ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ 𝑎 , 𝑏 ⟩ ) )
98 82 94 97 sylsyld ⊢ ( ( 𝑎 ∈ N ∧ 𝑏 ∈ N ) → ( ∀ 𝑧 ∈ ( N × N ) ( ⟨ 𝑎 , 𝑏 ⟩ ~Q 𝑧 → ¬ ( 2nd ‘ 𝑧 ) <N 𝑏 ) → ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ 𝑎 , 𝑏 ⟩ ) )
99 98 com12 ⊢ ( ∀ 𝑧 ∈ ( N × N ) ( ⟨ 𝑎 , 𝑏 ⟩ ~Q 𝑧 → ¬ ( 2nd ‘ 𝑧 ) <N 𝑏 ) → ( ( 𝑎 ∈ N ∧ 𝑏 ∈ N ) → ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ 𝑎 , 𝑏 ⟩ ) )
100 99 a1dd ⊢ ( ∀ 𝑧 ∈ ( N × N ) ( ⟨ 𝑎 , 𝑏 ⟩ ~Q 𝑧 → ¬ ( 2nd ‘ 𝑧 ) <N 𝑏 ) → ( ( 𝑎 ∈ N ∧ 𝑏 ∈ N ) → ( 𝑏 ∈ 𝑦 → ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ 𝑎 , 𝑏 ⟩ ) ) )
101 78 100 pm2.61d2 ⊢ ( ∀ 𝑚 ∈ 𝑦 ∀ 𝑐 ∈ N ∀ 𝑑 ∈ N ( 𝑑 ∈ 𝑚 → ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ 𝑐 , 𝑑 ⟩ ) → ( ( 𝑎 ∈ N ∧ 𝑏 ∈ N ) → ( 𝑏 ∈ 𝑦 → ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ 𝑎 , 𝑏 ⟩ ) ) )
102 101 ralrimivv ⊢ ( ∀ 𝑚 ∈ 𝑦 ∀ 𝑐 ∈ N ∀ 𝑑 ∈ N ( 𝑑 ∈ 𝑚 → ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ 𝑐 , 𝑑 ⟩ ) → ∀ 𝑎 ∈ N ∀ 𝑏 ∈ N ( 𝑏 ∈ 𝑦 → ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ 𝑎 , 𝑏 ⟩ ) )
103 24 102 sylbir ⊢ ( ∀ 𝑚 ∈ 𝑦 ∀ 𝑎 ∈ N ∀ 𝑏 ∈ N ( 𝑏 ∈ 𝑚 → ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ 𝑎 , 𝑏 ⟩ ) → ∀ 𝑎 ∈ N ∀ 𝑏 ∈ N ( 𝑏 ∈ 𝑦 → ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ 𝑎 , 𝑏 ⟩ ) )
104 103 a1i ⊢ ( 𝑦 ∈ On → ( ∀ 𝑚 ∈ 𝑦 ∀ 𝑎 ∈ N ∀ 𝑏 ∈ N ( 𝑏 ∈ 𝑚 → ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ 𝑎 , 𝑏 ⟩ ) → ∀ 𝑎 ∈ N ∀ 𝑏 ∈ N ( 𝑏 ∈ 𝑦 → ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ 𝑎 , 𝑏 ⟩ ) ) )
105 13 104 tfis2 ⊢ ( 𝑦 ∈ On → ∀ 𝑎 ∈ N ∀ 𝑏 ∈ N ( 𝑏 ∈ 𝑦 → ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ 𝑎 , 𝑏 ⟩ ) )
106 rsp ⊢ ( ∀ 𝑎 ∈ N ∀ 𝑏 ∈ N ( 𝑏 ∈ 𝑦 → ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ 𝑎 , 𝑏 ⟩ ) → ( 𝑎 ∈ N → ∀ 𝑏 ∈ N ( 𝑏 ∈ 𝑦 → ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ 𝑎 , 𝑏 ⟩ ) ) )
107 105 106 syl ⊢ ( 𝑦 ∈ On → ( 𝑎 ∈ N → ∀ 𝑏 ∈ N ( 𝑏 ∈ 𝑦 → ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ 𝑎 , 𝑏 ⟩ ) ) )
108 rsp ⊢ ( ∀ 𝑏 ∈ N ( 𝑏 ∈ 𝑦 → ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ 𝑎 , 𝑏 ⟩ ) → ( 𝑏 ∈ N → ( 𝑏 ∈ 𝑦 → ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ 𝑎 , 𝑏 ⟩ ) ) )
109 107 108 syl6 ⊢ ( 𝑦 ∈ On → ( 𝑎 ∈ N → ( 𝑏 ∈ N → ( 𝑏 ∈ 𝑦 → ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ 𝑎 , 𝑏 ⟩ ) ) ) )
110 109 impd ⊢ ( 𝑦 ∈ On → ( ( 𝑎 ∈ N ∧ 𝑏 ∈ N ) → ( 𝑏 ∈ 𝑦 → ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ 𝑎 , 𝑏 ⟩ ) ) )
111 110 com12 ⊢ ( ( 𝑎 ∈ N ∧ 𝑏 ∈ N ) → ( 𝑦 ∈ On → ( 𝑏 ∈ 𝑦 → ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ 𝑎 , 𝑏 ⟩ ) ) )
112 111 rexlimdv ⊢ ( ( 𝑎 ∈ N ∧ 𝑏 ∈ N ) → ( ∃ 𝑦 ∈ On 𝑏 ∈ 𝑦 → ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ 𝑎 , 𝑏 ⟩ ) )
113 10 112 mpd ⊢ ( ( 𝑎 ∈ N ∧ 𝑏 ∈ N ) → ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ 𝑎 , 𝑏 ⟩ )
114 breq2 ⊢ ( 𝐴 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝑥 ~Q 𝐴 ↔ 𝑥 ~Q ⟨ 𝑎 , 𝑏 ⟩ ) )
115 114 rexbidv ⊢ ( 𝐴 = ⟨ 𝑎 , 𝑏 ⟩ → ( ∃ 𝑥 ∈ Q 𝑥 ~Q 𝐴 ↔ ∃ 𝑥 ∈ Q 𝑥 ~Q ⟨ 𝑎 , 𝑏 ⟩ ) )
116 113 115 syl5ibrcom ⊢ ( ( 𝑎 ∈ N ∧ 𝑏 ∈ N ) → ( 𝐴 = ⟨ 𝑎 , 𝑏 ⟩ → ∃ 𝑥 ∈ Q 𝑥 ~Q 𝐴 ) )
117 116 rexlimivv ⊢ ( ∃ 𝑎 ∈ N ∃ 𝑏 ∈ N 𝐴 = ⟨ 𝑎 , 𝑏 ⟩ → ∃ 𝑥 ∈ Q 𝑥 ~Q 𝐴 )
118 1 117 sylbi ⊢ ( 𝐴 ∈ ( N × N ) → ∃ 𝑥 ∈ Q 𝑥 ~Q 𝐴 )
119 breq2 ⊢ ( 𝑎 = 𝐴 → ( 𝑥 ~Q 𝑎 ↔ 𝑥 ~Q 𝐴 ) )
120 breq2 ⊢ ( 𝑎 = 𝐴 → ( 𝑦 ~Q 𝑎 ↔ 𝑦 ~Q 𝐴 ) )
121 119 120 anbi12d ⊢ ( 𝑎 = 𝐴 → ( ( 𝑥 ~Q 𝑎 ∧ 𝑦 ~Q 𝑎 ) ↔ ( 𝑥 ~Q 𝐴 ∧ 𝑦 ~Q 𝐴 ) ) )
122 121 imbi1d ⊢ ( 𝑎 = 𝐴 → ( ( ( 𝑥 ~Q 𝑎 ∧ 𝑦 ~Q 𝑎 ) → 𝑥 = 𝑦 ) ↔ ( ( 𝑥 ~Q 𝐴 ∧ 𝑦 ~Q 𝐴 ) → 𝑥 = 𝑦 ) ) )
123 122 2ralbidv ⊢ ( 𝑎 = 𝐴 → ( ∀ 𝑥 ∈ Q ∀ 𝑦 ∈ Q ( ( 𝑥 ~Q 𝑎 ∧ 𝑦 ~Q 𝑎 ) → 𝑥 = 𝑦 ) ↔ ∀ 𝑥 ∈ Q ∀ 𝑦 ∈ Q ( ( 𝑥 ~Q 𝐴 ∧ 𝑦 ~Q 𝐴 ) → 𝑥 = 𝑦 ) ) )
124 64 a1i ⊢ ( ( 𝑥 ~Q 𝑎 ∧ 𝑦 ~Q 𝑎 ) → ~Q Er ( N × N ) )
125 simpl ⊢ ( ( 𝑥 ~Q 𝑎 ∧ 𝑦 ~Q 𝑎 ) → 𝑥 ~Q 𝑎 )
126 simpr ⊢ ( ( 𝑥 ~Q 𝑎 ∧ 𝑦 ~Q 𝑎 ) → 𝑦 ~Q 𝑎 )
127 124 125 126 ertr4d ⊢ ( ( 𝑥 ~Q 𝑎 ∧ 𝑦 ~Q 𝑎 ) → 𝑥 ~Q 𝑦 )
128 mulcompi ⊢ ( ( 2nd ‘ 𝑥 ) ·N ( 1st ‘ 𝑥 ) ) = ( ( 1st ‘ 𝑥 ) ·N ( 2nd ‘ 𝑥 ) )
129 elpqn ⊢ ( 𝑦 ∈ Q → 𝑦 ∈ ( N × N ) )
130 breq1 ⊢ ( 𝑦 = 𝑥 → ( 𝑦 ~Q 𝑧 ↔ 𝑥 ~Q 𝑧 ) )
131 fveq2 ⊢ ( 𝑦 = 𝑥 → ( 2nd ‘ 𝑦 ) = ( 2nd ‘ 𝑥 ) )
132 131 breq2d ⊢ ( 𝑦 = 𝑥 → ( ( 2nd ‘ 𝑧 ) <N ( 2nd ‘ 𝑦 ) ↔ ( 2nd ‘ 𝑧 ) <N ( 2nd ‘ 𝑥 ) ) )
133 132 notbid ⊢ ( 𝑦 = 𝑥 → ( ¬ ( 2nd ‘ 𝑧 ) <N ( 2nd ‘ 𝑦 ) ↔ ¬ ( 2nd ‘ 𝑧 ) <N ( 2nd ‘ 𝑥 ) ) )
134 130 133 imbi12d ⊢ ( 𝑦 = 𝑥 → ( ( 𝑦 ~Q 𝑧 → ¬ ( 2nd ‘ 𝑧 ) <N ( 2nd ‘ 𝑦 ) ) ↔ ( 𝑥 ~Q 𝑧 → ¬ ( 2nd ‘ 𝑧 ) <N ( 2nd ‘ 𝑥 ) ) ) )
135 134 ralbidv ⊢ ( 𝑦 = 𝑥 → ( ∀ 𝑧 ∈ ( N × N ) ( 𝑦 ~Q 𝑧 → ¬ ( 2nd ‘ 𝑧 ) <N ( 2nd ‘ 𝑦 ) ) ↔ ∀ 𝑧 ∈ ( N × N ) ( 𝑥 ~Q 𝑧 → ¬ ( 2nd ‘ 𝑧 ) <N ( 2nd ‘ 𝑥 ) ) ) )
136 135 91 elrab2 ⊢ ( 𝑥 ∈ Q ↔ ( 𝑥 ∈ ( N × N ) ∧ ∀ 𝑧 ∈ ( N × N ) ( 𝑥 ~Q 𝑧 → ¬ ( 2nd ‘ 𝑧 ) <N ( 2nd ‘ 𝑥 ) ) ) )
137 136 simprbi ⊢ ( 𝑥 ∈ Q → ∀ 𝑧 ∈ ( N × N ) ( 𝑥 ~Q 𝑧 → ¬ ( 2nd ‘ 𝑧 ) <N ( 2nd ‘ 𝑥 ) ) )
138 breq2 ⊢ ( 𝑧 = 𝑦 → ( 𝑥 ~Q 𝑧 ↔ 𝑥 ~Q 𝑦 ) )
139 fveq2 ⊢ ( 𝑧 = 𝑦 → ( 2nd ‘ 𝑧 ) = ( 2nd ‘ 𝑦 ) )
140 139 breq1d ⊢ ( 𝑧 = 𝑦 → ( ( 2nd ‘ 𝑧 ) <N ( 2nd ‘ 𝑥 ) ↔ ( 2nd ‘ 𝑦 ) <N ( 2nd ‘ 𝑥 ) ) )
141 140 notbid ⊢ ( 𝑧 = 𝑦 → ( ¬ ( 2nd ‘ 𝑧 ) <N ( 2nd ‘ 𝑥 ) ↔ ¬ ( 2nd ‘ 𝑦 ) <N ( 2nd ‘ 𝑥 ) ) )
142 138 141 imbi12d ⊢ ( 𝑧 = 𝑦 → ( ( 𝑥 ~Q 𝑧 → ¬ ( 2nd ‘ 𝑧 ) <N ( 2nd ‘ 𝑥 ) ) ↔ ( 𝑥 ~Q 𝑦 → ¬ ( 2nd ‘ 𝑦 ) <N ( 2nd ‘ 𝑥 ) ) ) )
143 142 rspcva ⊢ ( ( 𝑦 ∈ ( N × N ) ∧ ∀ 𝑧 ∈ ( N × N ) ( 𝑥 ~Q 𝑧 → ¬ ( 2nd ‘ 𝑧 ) <N ( 2nd ‘ 𝑥 ) ) ) → ( 𝑥 ~Q 𝑦 → ¬ ( 2nd ‘ 𝑦 ) <N ( 2nd ‘ 𝑥 ) ) )
144 129 137 143 syl2anr ⊢ ( ( 𝑥 ∈ Q ∧ 𝑦 ∈ Q ) → ( 𝑥 ~Q 𝑦 → ¬ ( 2nd ‘ 𝑦 ) <N ( 2nd ‘ 𝑥 ) ) )
145 144 imp ⊢ ( ( ( 𝑥 ∈ Q ∧ 𝑦 ∈ Q ) ∧ 𝑥 ~Q 𝑦 ) → ¬ ( 2nd ‘ 𝑦 ) <N ( 2nd ‘ 𝑥 ) )
146 elpqn ⊢ ( 𝑥 ∈ Q → 𝑥 ∈ ( N × N ) )
147 91 reqabi ⊢ ( 𝑦 ∈ Q ↔ ( 𝑦 ∈ ( N × N ) ∧ ∀ 𝑧 ∈ ( N × N ) ( 𝑦 ~Q 𝑧 → ¬ ( 2nd ‘ 𝑧 ) <N ( 2nd ‘ 𝑦 ) ) ) )
148 147 simprbi ⊢ ( 𝑦 ∈ Q → ∀ 𝑧 ∈ ( N × N ) ( 𝑦 ~Q 𝑧 → ¬ ( 2nd ‘ 𝑧 ) <N ( 2nd ‘ 𝑦 ) ) )
149 breq2 ⊢ ( 𝑧 = 𝑥 → ( 𝑦 ~Q 𝑧 ↔ 𝑦 ~Q 𝑥 ) )
150 fveq2 ⊢ ( 𝑧 = 𝑥 → ( 2nd ‘ 𝑧 ) = ( 2nd ‘ 𝑥 ) )
151 150 breq1d ⊢ ( 𝑧 = 𝑥 → ( ( 2nd ‘ 𝑧 ) <N ( 2nd ‘ 𝑦 ) ↔ ( 2nd ‘ 𝑥 ) <N ( 2nd ‘ 𝑦 ) ) )
152 151 notbid ⊢ ( 𝑧 = 𝑥 → ( ¬ ( 2nd ‘ 𝑧 ) <N ( 2nd ‘ 𝑦 ) ↔ ¬ ( 2nd ‘ 𝑥 ) <N ( 2nd ‘ 𝑦 ) ) )
153 149 152 imbi12d ⊢ ( 𝑧 = 𝑥 → ( ( 𝑦 ~Q 𝑧 → ¬ ( 2nd ‘ 𝑧 ) <N ( 2nd ‘ 𝑦 ) ) ↔ ( 𝑦 ~Q 𝑥 → ¬ ( 2nd ‘ 𝑥 ) <N ( 2nd ‘ 𝑦 ) ) ) )
154 153 rspcva ⊢ ( ( 𝑥 ∈ ( N × N ) ∧ ∀ 𝑧 ∈ ( N × N ) ( 𝑦 ~Q 𝑧 → ¬ ( 2nd ‘ 𝑧 ) <N ( 2nd ‘ 𝑦 ) ) ) → ( 𝑦 ~Q 𝑥 → ¬ ( 2nd ‘ 𝑥 ) <N ( 2nd ‘ 𝑦 ) ) )
155 146 148 154 syl2an ⊢ ( ( 𝑥 ∈ Q ∧ 𝑦 ∈ Q ) → ( 𝑦 ~Q 𝑥 → ¬ ( 2nd ‘ 𝑥 ) <N ( 2nd ‘ 𝑦 ) ) )
156 64 a1i ⊢ ( 𝑥 ~Q 𝑦 → ~Q Er ( N × N ) )
157 id ⊢ ( 𝑥 ~Q 𝑦 → 𝑥 ~Q 𝑦 )
158 156 157 ersym ⊢ ( 𝑥 ~Q 𝑦 → 𝑦 ~Q 𝑥 )
159 155 158 impel ⊢ ( ( ( 𝑥 ∈ Q ∧ 𝑦 ∈ Q ) ∧ 𝑥 ~Q 𝑦 ) → ¬ ( 2nd ‘ 𝑥 ) <N ( 2nd ‘ 𝑦 ) )
160 xp2nd ⊢ ( 𝑥 ∈ ( N × N ) → ( 2nd ‘ 𝑥 ) ∈ N )
161 146 160 syl ⊢ ( 𝑥 ∈ Q → ( 2nd ‘ 𝑥 ) ∈ N )
162 161 ad2antrr ⊢ ( ( ( 𝑥 ∈ Q ∧ 𝑦 ∈ Q ) ∧ 𝑥 ~Q 𝑦 ) → ( 2nd ‘ 𝑥 ) ∈ N )
163 xp2nd ⊢ ( 𝑦 ∈ ( N × N ) → ( 2nd ‘ 𝑦 ) ∈ N )
164 129 163 syl ⊢ ( 𝑦 ∈ Q → ( 2nd ‘ 𝑦 ) ∈ N )
165 164 ad2antlr ⊢ ( ( ( 𝑥 ∈ Q ∧ 𝑦 ∈ Q ) ∧ 𝑥 ~Q 𝑦 ) → ( 2nd ‘ 𝑦 ) ∈ N )
166 ltsopi ⊢ <N Or N
167 sotric ⊢ ( ( <N Or N ∧ ( ( 2nd ‘ 𝑥 ) ∈ N ∧ ( 2nd ‘ 𝑦 ) ∈ N ) ) → ( ( 2nd ‘ 𝑥 ) <N ( 2nd ‘ 𝑦 ) ↔ ¬ ( ( 2nd ‘ 𝑥 ) = ( 2nd ‘ 𝑦 ) ∨ ( 2nd ‘ 𝑦 ) <N ( 2nd ‘ 𝑥 ) ) ) )
168 166 167 mpan ⊢ ( ( ( 2nd ‘ 𝑥 ) ∈ N ∧ ( 2nd ‘ 𝑦 ) ∈ N ) → ( ( 2nd ‘ 𝑥 ) <N ( 2nd ‘ 𝑦 ) ↔ ¬ ( ( 2nd ‘ 𝑥 ) = ( 2nd ‘ 𝑦 ) ∨ ( 2nd ‘ 𝑦 ) <N ( 2nd ‘ 𝑥 ) ) ) )
169 168 notbid ⊢ ( ( ( 2nd ‘ 𝑥 ) ∈ N ∧ ( 2nd ‘ 𝑦 ) ∈ N ) → ( ¬ ( 2nd ‘ 𝑥 ) <N ( 2nd ‘ 𝑦 ) ↔ ¬ ¬ ( ( 2nd ‘ 𝑥 ) = ( 2nd ‘ 𝑦 ) ∨ ( 2nd ‘ 𝑦 ) <N ( 2nd ‘ 𝑥 ) ) ) )
170 notnotb ⊢ ( ( ( 2nd ‘ 𝑥 ) = ( 2nd ‘ 𝑦 ) ∨ ( 2nd ‘ 𝑦 ) <N ( 2nd ‘ 𝑥 ) ) ↔ ¬ ¬ ( ( 2nd ‘ 𝑥 ) = ( 2nd ‘ 𝑦 ) ∨ ( 2nd ‘ 𝑦 ) <N ( 2nd ‘ 𝑥 ) ) )
171 169 170 bitr4di ⊢ ( ( ( 2nd ‘ 𝑥 ) ∈ N ∧ ( 2nd ‘ 𝑦 ) ∈ N ) → ( ¬ ( 2nd ‘ 𝑥 ) <N ( 2nd ‘ 𝑦 ) ↔ ( ( 2nd ‘ 𝑥 ) = ( 2nd ‘ 𝑦 ) ∨ ( 2nd ‘ 𝑦 ) <N ( 2nd ‘ 𝑥 ) ) ) )
172 162 165 171 syl2anc ⊢ ( ( ( 𝑥 ∈ Q ∧ 𝑦 ∈ Q ) ∧ 𝑥 ~Q 𝑦 ) → ( ¬ ( 2nd ‘ 𝑥 ) <N ( 2nd ‘ 𝑦 ) ↔ ( ( 2nd ‘ 𝑥 ) = ( 2nd ‘ 𝑦 ) ∨ ( 2nd ‘ 𝑦 ) <N ( 2nd ‘ 𝑥 ) ) ) )
173 159 172 mpbid ⊢ ( ( ( 𝑥 ∈ Q ∧ 𝑦 ∈ Q ) ∧ 𝑥 ~Q 𝑦 ) → ( ( 2nd ‘ 𝑥 ) = ( 2nd ‘ 𝑦 ) ∨ ( 2nd ‘ 𝑦 ) <N ( 2nd ‘ 𝑥 ) ) )
174 173 ord ⊢ ( ( ( 𝑥 ∈ Q ∧ 𝑦 ∈ Q ) ∧ 𝑥 ~Q 𝑦 ) → ( ¬ ( 2nd ‘ 𝑥 ) = ( 2nd ‘ 𝑦 ) → ( 2nd ‘ 𝑦 ) <N ( 2nd ‘ 𝑥 ) ) )
175 145 174 mt3d ⊢ ( ( ( 𝑥 ∈ Q ∧ 𝑦 ∈ Q ) ∧ 𝑥 ~Q 𝑦 ) → ( 2nd ‘ 𝑥 ) = ( 2nd ‘ 𝑦 ) )
176 175 oveq2d ⊢ ( ( ( 𝑥 ∈ Q ∧ 𝑦 ∈ Q ) ∧ 𝑥 ~Q 𝑦 ) → ( ( 1st ‘ 𝑥 ) ·N ( 2nd ‘ 𝑥 ) ) = ( ( 1st ‘ 𝑥 ) ·N ( 2nd ‘ 𝑦 ) ) )
177 128 176 eqtrid ⊢ ( ( ( 𝑥 ∈ Q ∧ 𝑦 ∈ Q ) ∧ 𝑥 ~Q 𝑦 ) → ( ( 2nd ‘ 𝑥 ) ·N ( 1st ‘ 𝑥 ) ) = ( ( 1st ‘ 𝑥 ) ·N ( 2nd ‘ 𝑦 ) ) )
178 1st2nd2 ⊢ ( 𝑥 ∈ ( N × N ) → 𝑥 = ⟨ ( 1st ‘ 𝑥 ) , ( 2nd ‘ 𝑥 ) ⟩ )
179 1st2nd2 ⊢ ( 𝑦 ∈ ( N × N ) → 𝑦 = ⟨ ( 1st ‘ 𝑦 ) , ( 2nd ‘ 𝑦 ) ⟩ )
180 178 179 breqan12d ⊢ ( ( 𝑥 ∈ ( N × N ) ∧ 𝑦 ∈ ( N × N ) ) → ( 𝑥 ~Q 𝑦 ↔ ⟨ ( 1st ‘ 𝑥 ) , ( 2nd ‘ 𝑥 ) ⟩ ~Q ⟨ ( 1st ‘ 𝑦 ) , ( 2nd ‘ 𝑦 ) ⟩ ) )
181 xp1st ⊢ ( 𝑥 ∈ ( N × N ) → ( 1st ‘ 𝑥 ) ∈ N )
182 181 160 jca ⊢ ( 𝑥 ∈ ( N × N ) → ( ( 1st ‘ 𝑥 ) ∈ N ∧ ( 2nd ‘ 𝑥 ) ∈ N ) )
183 xp1st ⊢ ( 𝑦 ∈ ( N × N ) → ( 1st ‘ 𝑦 ) ∈ N )
184 183 163 jca ⊢ ( 𝑦 ∈ ( N × N ) → ( ( 1st ‘ 𝑦 ) ∈ N ∧ ( 2nd ‘ 𝑦 ) ∈ N ) )
185 enqbreq ⊢ ( ( ( ( 1st ‘ 𝑥 ) ∈ N ∧ ( 2nd ‘ 𝑥 ) ∈ N ) ∧ ( ( 1st ‘ 𝑦 ) ∈ N ∧ ( 2nd ‘ 𝑦 ) ∈ N ) ) → ( ⟨ ( 1st ‘ 𝑥 ) , ( 2nd ‘ 𝑥 ) ⟩ ~Q ⟨ ( 1st ‘ 𝑦 ) , ( 2nd ‘ 𝑦 ) ⟩ ↔ ( ( 1st ‘ 𝑥 ) ·N ( 2nd ‘ 𝑦 ) ) = ( ( 2nd ‘ 𝑥 ) ·N ( 1st ‘ 𝑦 ) ) ) )
186 182 184 185 syl2an ⊢ ( ( 𝑥 ∈ ( N × N ) ∧ 𝑦 ∈ ( N × N ) ) → ( ⟨ ( 1st ‘ 𝑥 ) , ( 2nd ‘ 𝑥 ) ⟩ ~Q ⟨ ( 1st ‘ 𝑦 ) , ( 2nd ‘ 𝑦 ) ⟩ ↔ ( ( 1st ‘ 𝑥 ) ·N ( 2nd ‘ 𝑦 ) ) = ( ( 2nd ‘ 𝑥 ) ·N ( 1st ‘ 𝑦 ) ) ) )
187 180 186 bitrd ⊢ ( ( 𝑥 ∈ ( N × N ) ∧ 𝑦 ∈ ( N × N ) ) → ( 𝑥 ~Q 𝑦 ↔ ( ( 1st ‘ 𝑥 ) ·N ( 2nd ‘ 𝑦 ) ) = ( ( 2nd ‘ 𝑥 ) ·N ( 1st ‘ 𝑦 ) ) ) )
188 146 129 187 syl2an ⊢ ( ( 𝑥 ∈ Q ∧ 𝑦 ∈ Q ) → ( 𝑥 ~Q 𝑦 ↔ ( ( 1st ‘ 𝑥 ) ·N ( 2nd ‘ 𝑦 ) ) = ( ( 2nd ‘ 𝑥 ) ·N ( 1st ‘ 𝑦 ) ) ) )
189 188 biimpa ⊢ ( ( ( 𝑥 ∈ Q ∧ 𝑦 ∈ Q ) ∧ 𝑥 ~Q 𝑦 ) → ( ( 1st ‘ 𝑥 ) ·N ( 2nd ‘ 𝑦 ) ) = ( ( 2nd ‘ 𝑥 ) ·N ( 1st ‘ 𝑦 ) ) )
190 177 189 eqtrd ⊢ ( ( ( 𝑥 ∈ Q ∧ 𝑦 ∈ Q ) ∧ 𝑥 ~Q 𝑦 ) → ( ( 2nd ‘ 𝑥 ) ·N ( 1st ‘ 𝑥 ) ) = ( ( 2nd ‘ 𝑥 ) ·N ( 1st ‘ 𝑦 ) ) )
191 146 ad2antrr ⊢ ( ( ( 𝑥 ∈ Q ∧ 𝑦 ∈ Q ) ∧ 𝑥 ~Q 𝑦 ) → 𝑥 ∈ ( N × N ) )
192 mulcanpi ⊢ ( ( ( 2nd ‘ 𝑥 ) ∈ N ∧ ( 1st ‘ 𝑥 ) ∈ N ) → ( ( ( 2nd ‘ 𝑥 ) ·N ( 1st ‘ 𝑥 ) ) = ( ( 2nd ‘ 𝑥 ) ·N ( 1st ‘ 𝑦 ) ) ↔ ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ) )
193 160 181 192 syl2anc ⊢ ( 𝑥 ∈ ( N × N ) → ( ( ( 2nd ‘ 𝑥 ) ·N ( 1st ‘ 𝑥 ) ) = ( ( 2nd ‘ 𝑥 ) ·N ( 1st ‘ 𝑦 ) ) ↔ ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ) )
194 191 193 syl ⊢ ( ( ( 𝑥 ∈ Q ∧ 𝑦 ∈ Q ) ∧ 𝑥 ~Q 𝑦 ) → ( ( ( 2nd ‘ 𝑥 ) ·N ( 1st ‘ 𝑥 ) ) = ( ( 2nd ‘ 𝑥 ) ·N ( 1st ‘ 𝑦 ) ) ↔ ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ) )
195 190 194 mpbid ⊢ ( ( ( 𝑥 ∈ Q ∧ 𝑦 ∈ Q ) ∧ 𝑥 ~Q 𝑦 ) → ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) )
196 195 175 opeq12d ⊢ ( ( ( 𝑥 ∈ Q ∧ 𝑦 ∈ Q ) ∧ 𝑥 ~Q 𝑦 ) → ⟨ ( 1st ‘ 𝑥 ) , ( 2nd ‘ 𝑥 ) ⟩ = ⟨ ( 1st ‘ 𝑦 ) , ( 2nd ‘ 𝑦 ) ⟩ )
197 191 178 syl ⊢ ( ( ( 𝑥 ∈ Q ∧ 𝑦 ∈ Q ) ∧ 𝑥 ~Q 𝑦 ) → 𝑥 = ⟨ ( 1st ‘ 𝑥 ) , ( 2nd ‘ 𝑥 ) ⟩ )
198 129 ad2antlr ⊢ ( ( ( 𝑥 ∈ Q ∧ 𝑦 ∈ Q ) ∧ 𝑥 ~Q 𝑦 ) → 𝑦 ∈ ( N × N ) )
199 198 179 syl ⊢ ( ( ( 𝑥 ∈ Q ∧ 𝑦 ∈ Q ) ∧ 𝑥 ~Q 𝑦 ) → 𝑦 = ⟨ ( 1st ‘ 𝑦 ) , ( 2nd ‘ 𝑦 ) ⟩ )
200 196 197 199 3eqtr4d ⊢ ( ( ( 𝑥 ∈ Q ∧ 𝑦 ∈ Q ) ∧ 𝑥 ~Q 𝑦 ) → 𝑥 = 𝑦 )
201 200 ex ⊢ ( ( 𝑥 ∈ Q ∧ 𝑦 ∈ Q ) → ( 𝑥 ~Q 𝑦 → 𝑥 = 𝑦 ) )
202 127 201 syl5 ⊢ ( ( 𝑥 ∈ Q ∧ 𝑦 ∈ Q ) → ( ( 𝑥 ~Q 𝑎 ∧ 𝑦 ~Q 𝑎 ) → 𝑥 = 𝑦 ) )
203 202 rgen2 ⊢ ∀ 𝑥 ∈ Q ∀ 𝑦 ∈ Q ( ( 𝑥 ~Q 𝑎 ∧ 𝑦 ~Q 𝑎 ) → 𝑥 = 𝑦 )
204 123 203 vtoclg ⊢ ( 𝐴 ∈ ( N × N ) → ∀ 𝑥 ∈ Q ∀ 𝑦 ∈ Q ( ( 𝑥 ~Q 𝐴 ∧ 𝑦 ~Q 𝐴 ) → 𝑥 = 𝑦 ) )
205 breq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ~Q 𝐴 ↔ 𝑦 ~Q 𝐴 ) )
206 205 reu4 ⊢ ( ∃! 𝑥 ∈ Q 𝑥 ~Q 𝐴 ↔ ( ∃ 𝑥 ∈ Q 𝑥 ~Q 𝐴 ∧ ∀ 𝑥 ∈ Q ∀ 𝑦 ∈ Q ( ( 𝑥 ~Q 𝐴 ∧ 𝑦 ~Q 𝐴 ) → 𝑥 = 𝑦 ) ) )
207 118 204 206 sylanbrc ⊢ ( 𝐴 ∈ ( N × N ) → ∃! 𝑥 ∈ Q 𝑥 ~Q 𝐴 )