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 e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> ( A ~Q B <-> ( /Q ` A ) = ( /Q ` B ) ) )

Proof

Step Hyp Ref Expression
1 nqercl 
 |-  ( A e. ( N. X. N. ) -> ( /Q ` A ) e. Q. )
2 1 3ad2ant1 
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) /\ A ~Q B ) -> ( /Q ` A ) e. Q. )
3 nqercl 
 |-  ( B e. ( N. X. N. ) -> ( /Q ` B ) e. Q. )
4 3 3ad2ant2 
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) /\ A ~Q B ) -> ( /Q ` B ) e. Q. )
5 enqer 
 |-  ~Q Er ( N. X. N. )
6 5 a1i 
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) /\ A ~Q B ) -> ~Q Er ( N. X. N. ) )
7 nqerrel 
 |-  ( A e. ( N. X. N. ) -> A ~Q ( /Q ` A ) )
8 7 3ad2ant1 
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) /\ A ~Q B ) -> A ~Q ( /Q ` A ) )
9 simp3 
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) /\ A ~Q B ) -> A ~Q B )
10 6 8 9 ertr3d 
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) /\ A ~Q B ) -> ( /Q ` A ) ~Q B )
11 nqerrel 
 |-  ( B e. ( N. X. N. ) -> B ~Q ( /Q ` B ) )
12 11 3ad2ant2 
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) /\ A ~Q B ) -> B ~Q ( /Q ` B ) )
13 6 10 12 ertrd 
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) /\ A ~Q B ) -> ( /Q ` A ) ~Q ( /Q ` B ) )
14 enqeq 
 |-  ( ( ( /Q ` A ) e. Q. /\ ( /Q ` B ) e. Q. /\ ( /Q ` A ) ~Q ( /Q ` B ) ) -> ( /Q ` A ) = ( /Q ` B ) )
15 2 4 13 14 syl3anc 
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) /\ A ~Q B ) -> ( /Q ` A ) = ( /Q ` B ) )
16 15 3expia 
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> ( A ~Q B -> ( /Q ` A ) = ( /Q ` B ) ) )
17 5 a1i 
 |-  ( ( A e. ( N. X. N. ) /\ ( B e. ( N. X. N. ) /\ ( /Q ` A ) = ( /Q ` B ) ) ) -> ~Q Er ( N. X. N. ) )
18 7 adantr 
 |-  ( ( A e. ( N. X. N. ) /\ ( B e. ( N. X. N. ) /\ ( /Q ` A ) = ( /Q ` B ) ) ) -> A ~Q ( /Q ` A ) )
19 simprr 
 |-  ( ( A e. ( N. X. N. ) /\ ( B e. ( N. X. N. ) /\ ( /Q ` A ) = ( /Q ` B ) ) ) -> ( /Q ` A ) = ( /Q ` B ) )
20 18 19 breqtrd 
 |-  ( ( A e. ( N. X. N. ) /\ ( B e. ( N. X. N. ) /\ ( /Q ` A ) = ( /Q ` B ) ) ) -> A ~Q ( /Q ` B ) )
21 11 ad2antrl 
 |-  ( ( A e. ( N. X. N. ) /\ ( B e. ( N. X. N. ) /\ ( /Q ` A ) = ( /Q ` B ) ) ) -> B ~Q ( /Q ` B ) )
22 17 20 21 ertr4d 
 |-  ( ( A e. ( N. X. N. ) /\ ( B e. ( N. X. N. ) /\ ( /Q ` A ) = ( /Q ` B ) ) ) -> A ~Q B )
23 22 expr 
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> ( ( /Q ` A ) = ( /Q ` B ) -> A ~Q B ) )
24 16 23 impbid 
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> ( A ~Q B <-> ( /Q ` A ) = ( /Q ` B ) ) )