Metamath Proof Explorer

Theorem enqeq

Description: Corollary of nqereu : if two fractions are both reduced and equivalent, then they are equal. (Contributed by Mario Carneiro, 6-May-2013) (New usage is discouraged.)

Ref Expression
Assertion enqeq ⊢ A ∈ 𝑸 ∧ B ∈ 𝑸 ∧ A ~ 𝑸 B → A = B

Proof

Step Hyp Ref Expression
1 3simpa ⊢ A ∈ 𝑸 ∧ B ∈ 𝑸 ∧ A ~ 𝑸 B → A ∈ 𝑸 ∧ B ∈ 𝑸
2 elpqn ⊢ B ∈ 𝑸 → B ∈ 𝑵 × 𝑵
3 2 3ad2ant2 ⊢ A ∈ 𝑸 ∧ B ∈ 𝑸 ∧ A ~ 𝑸 B → B ∈ 𝑵 × 𝑵
4 nqereu ⊢ B ∈ 𝑵 × 𝑵 → ∃! x ∈ 𝑸 x ~ 𝑸 B
5 reurmo ⊢ ∃! x ∈ 𝑸 x ~ 𝑸 B → ∃* x ∈ 𝑸 x ~ 𝑸 B
6 3 4 5 3syl ⊢ A ∈ 𝑸 ∧ B ∈ 𝑸 ∧ A ~ 𝑸 B → ∃* x ∈ 𝑸 x ~ 𝑸 B
7 df-rmo ⊢ ∃* x ∈ 𝑸 x ~ 𝑸 B ↔ ∃* x x ∈ 𝑸 ∧ x ~ 𝑸 B
8 6 7 sylib ⊢ A ∈ 𝑸 ∧ B ∈ 𝑸 ∧ A ~ 𝑸 B → ∃* x x ∈ 𝑸 ∧ x ~ 𝑸 B
9 3simpb ⊢ A ∈ 𝑸 ∧ B ∈ 𝑸 ∧ A ~ 𝑸 B → A ∈ 𝑸 ∧ A ~ 𝑸 B
10 simp2 ⊢ A ∈ 𝑸 ∧ B ∈ 𝑸 ∧ A ~ 𝑸 B → B ∈ 𝑸
11 enqer ⊢ ~ 𝑸 Er 𝑵 × 𝑵
12 11 a1i ⊢ A ∈ 𝑸 ∧ B ∈ 𝑸 ∧ A ~ 𝑸 B → ~ 𝑸 Er 𝑵 × 𝑵
13 12 3 erref ⊢ A ∈ 𝑸 ∧ B ∈ 𝑸 ∧ A ~ 𝑸 B → B ~ 𝑸 B
14 10 13 jca ⊢ A ∈ 𝑸 ∧ B ∈ 𝑸 ∧ A ~ 𝑸 B → B ∈ 𝑸 ∧ B ~ 𝑸 B
15 eleq1 ⊢ x = A → x ∈ 𝑸 ↔ A ∈ 𝑸
16 breq1 ⊢ x = A → x ~ 𝑸 B ↔ A ~ 𝑸 B
17 15 16 anbi12d ⊢ x = A → x ∈ 𝑸 ∧ x ~ 𝑸 B ↔ A ∈ 𝑸 ∧ A ~ 𝑸 B
18 eleq1 ⊢ x = B → x ∈ 𝑸 ↔ B ∈ 𝑸
19 breq1 ⊢ x = B → x ~ 𝑸 B ↔ B ~ 𝑸 B
20 18 19 anbi12d ⊢ x = B → x ∈ 𝑸 ∧ x ~ 𝑸 B ↔ B ∈ 𝑸 ∧ B ~ 𝑸 B
21 17 20 moi ⊢ A ∈ 𝑸 ∧ B ∈ 𝑸 ∧ ∃* x x ∈ 𝑸 ∧ x ~ 𝑸 B ∧ A ∈ 𝑸 ∧ A ~ 𝑸 B ∧ B ∈ 𝑸 ∧ B ~ 𝑸 B → A = B
22 1 8 9 14 21 syl112anc ⊢ A ∈ 𝑸 ∧ B ∈ 𝑸 ∧ A ~ 𝑸 B → A = B