Metamath Proof Explorer

Theorem nqereq

Description: The function /Q acts as a substitute for equivalence classes, and it satisfies the fundamental requirement for equivalence representatives: the representatives are equal iff the members are equivalent. (Contributed by Mario Carneiro, 6-May-2013) (Revised by Mario Carneiro, 12-Aug-2015) (New usage is discouraged.)

Ref Expression
Assertion nqereq ⊢ A ∈ 𝑵 × 𝑵 ∧ B ∈ 𝑵 × 𝑵 → A ~ 𝑸 B ↔ / 𝑸 ⁡ A = / 𝑸 ⁡ B

Proof

Step Hyp Ref Expression
1 nqercl ⊢ A ∈ 𝑵 × 𝑵 → / 𝑸 ⁡ A ∈ 𝑸
2 1 3ad2ant1 ⊢ A ∈ 𝑵 × 𝑵 ∧ B ∈ 𝑵 × 𝑵 ∧ A ~ 𝑸 B → / 𝑸 ⁡ A ∈ 𝑸
3 nqercl ⊢ B ∈ 𝑵 × 𝑵 → / 𝑸 ⁡ B ∈ 𝑸
4 3 3ad2ant2 ⊢ A ∈ 𝑵 × 𝑵 ∧ B ∈ 𝑵 × 𝑵 ∧ A ~ 𝑸 B → / 𝑸 ⁡ B ∈ 𝑸
5 enqer ⊢ ~ 𝑸 Er 𝑵 × 𝑵
6 5 a1i ⊢ A ∈ 𝑵 × 𝑵 ∧ B ∈ 𝑵 × 𝑵 ∧ A ~ 𝑸 B → ~ 𝑸 Er 𝑵 × 𝑵
7 nqerrel ⊢ A ∈ 𝑵 × 𝑵 → A ~ 𝑸 / 𝑸 ⁡ A
8 7 3ad2ant1 ⊢ A ∈ 𝑵 × 𝑵 ∧ B ∈ 𝑵 × 𝑵 ∧ A ~ 𝑸 B → A ~ 𝑸 / 𝑸 ⁡ A
9 simp3 ⊢ A ∈ 𝑵 × 𝑵 ∧ B ∈ 𝑵 × 𝑵 ∧ A ~ 𝑸 B → A ~ 𝑸 B
10 6 8 9 ertr3d ⊢ A ∈ 𝑵 × 𝑵 ∧ B ∈ 𝑵 × 𝑵 ∧ A ~ 𝑸 B → / 𝑸 ⁡ A ~ 𝑸 B
11 nqerrel ⊢ B ∈ 𝑵 × 𝑵 → B ~ 𝑸 / 𝑸 ⁡ B
12 11 3ad2ant2 ⊢ A ∈ 𝑵 × 𝑵 ∧ B ∈ 𝑵 × 𝑵 ∧ A ~ 𝑸 B → B ~ 𝑸 / 𝑸 ⁡ B
13 6 10 12 ertrd ⊢ A ∈ 𝑵 × 𝑵 ∧ B ∈ 𝑵 × 𝑵 ∧ A ~ 𝑸 B → / 𝑸 ⁡ A ~ 𝑸 / 𝑸 ⁡ B
14 enqeq ⊢ / 𝑸 ⁡ A ∈ 𝑸 ∧ / 𝑸 ⁡ B ∈ 𝑸 ∧ / 𝑸 ⁡ A ~ 𝑸 / 𝑸 ⁡ B → / 𝑸 ⁡ A = / 𝑸 ⁡ B
15 2 4 13 14 syl3anc ⊢ A ∈ 𝑵 × 𝑵 ∧ B ∈ 𝑵 × 𝑵 ∧ A ~ 𝑸 B → / 𝑸 ⁡ A = / 𝑸 ⁡ B
16 15 3expia ⊢ A ∈ 𝑵 × 𝑵 ∧ B ∈ 𝑵 × 𝑵 → A ~ 𝑸 B → / 𝑸 ⁡ A = / 𝑸 ⁡ B
17 5 a1i ⊢ A ∈ 𝑵 × 𝑵 ∧ B ∈ 𝑵 × 𝑵 ∧ / 𝑸 ⁡ A = / 𝑸 ⁡ B → ~ 𝑸 Er 𝑵 × 𝑵
18 7 adantr ⊢ A ∈ 𝑵 × 𝑵 ∧ B ∈ 𝑵 × 𝑵 ∧ / 𝑸 ⁡ A = / 𝑸 ⁡ B → A ~ 𝑸 / 𝑸 ⁡ A
19 simprr ⊢ A ∈ 𝑵 × 𝑵 ∧ B ∈ 𝑵 × 𝑵 ∧ / 𝑸 ⁡ A = / 𝑸 ⁡ B → / 𝑸 ⁡ A = / 𝑸 ⁡ B
20 18 19 breqtrd ⊢ A ∈ 𝑵 × 𝑵 ∧ B ∈ 𝑵 × 𝑵 ∧ / 𝑸 ⁡ A = / 𝑸 ⁡ B → A ~ 𝑸 / 𝑸 ⁡ B
21 11 ad2antrl ⊢ A ∈ 𝑵 × 𝑵 ∧ B ∈ 𝑵 × 𝑵 ∧ / 𝑸 ⁡ A = / 𝑸 ⁡ B → B ~ 𝑸 / 𝑸 ⁡ B
22 17 20 21 ertr4d ⊢ A ∈ 𝑵 × 𝑵 ∧ B ∈ 𝑵 × 𝑵 ∧ / 𝑸 ⁡ A = / 𝑸 ⁡ B → A ~ 𝑸 B
23 22 expr ⊢ A ∈ 𝑵 × 𝑵 ∧ B ∈ 𝑵 × 𝑵 → / 𝑸 ⁡ A = / 𝑸 ⁡ B → A ~ 𝑸 B
24 16 23 impbid ⊢ A ∈ 𝑵 × 𝑵 ∧ B ∈ 𝑵 × 𝑵 → A ~ 𝑸 B ↔ / 𝑸 ⁡ A = / 𝑸 ⁡ B