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