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 ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) → ( 𝐴 ~Q 𝐵 ↔ ( [Q] ‘ 𝐴 ) = ( [Q] ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 nqercl ( 𝐴 ∈ ( N × N ) → ( [Q] ‘ 𝐴 ) ∈ Q )
2 1 3ad2ant1 ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ∧ 𝐴 ~Q 𝐵 ) → ( [Q] ‘ 𝐴 ) ∈ Q )
3 nqercl ( 𝐵 ∈ ( N × N ) → ( [Q] ‘ 𝐵 ) ∈ Q )
4 3 3ad2ant2 ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ∧ 𝐴 ~Q 𝐵 ) → ( [Q] ‘ 𝐵 ) ∈ Q )
5 enqer ~Q Er ( N × N )
6 5 a1i ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ∧ 𝐴 ~Q 𝐵 ) → ~Q Er ( N × N ) )
7 nqerrel ( 𝐴 ∈ ( N × N ) → 𝐴 ~Q ( [Q] ‘ 𝐴 ) )
8 7 3ad2ant1 ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ∧ 𝐴 ~Q 𝐵 ) → 𝐴 ~Q ( [Q] ‘ 𝐴 ) )
9 simp3 ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ∧ 𝐴 ~Q 𝐵 ) → 𝐴 ~Q 𝐵 )
10 6 8 9 ertr3d ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ∧ 𝐴 ~Q 𝐵 ) → ( [Q] ‘ 𝐴 ) ~Q 𝐵 )
11 nqerrel ( 𝐵 ∈ ( N × N ) → 𝐵 ~Q ( [Q] ‘ 𝐵 ) )
12 11 3ad2ant2 ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ∧ 𝐴 ~Q 𝐵 ) → 𝐵 ~Q ( [Q] ‘ 𝐵 ) )
13 6 10 12 ertrd ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ∧ 𝐴 ~Q 𝐵 ) → ( [Q] ‘ 𝐴 ) ~Q ( [Q] ‘ 𝐵 ) )
14 enqeq ( ( ( [Q] ‘ 𝐴 ) ∈ Q ∧ ( [Q] ‘ 𝐵 ) ∈ Q ∧ ( [Q] ‘ 𝐴 ) ~Q ( [Q] ‘ 𝐵 ) ) → ( [Q] ‘ 𝐴 ) = ( [Q] ‘ 𝐵 ) )
15 2 4 13 14 syl3anc ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ∧ 𝐴 ~Q 𝐵 ) → ( [Q] ‘ 𝐴 ) = ( [Q] ‘ 𝐵 ) )
16 15 3expia ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) → ( 𝐴 ~Q 𝐵 → ( [Q] ‘ 𝐴 ) = ( [Q] ‘ 𝐵 ) ) )
17 5 a1i ( ( 𝐴 ∈ ( N × N ) ∧ ( 𝐵 ∈ ( N × N ) ∧ ( [Q] ‘ 𝐴 ) = ( [Q] ‘ 𝐵 ) ) ) → ~Q Er ( N × N ) )
18 7 adantr ( ( 𝐴 ∈ ( N × N ) ∧ ( 𝐵 ∈ ( N × N ) ∧ ( [Q] ‘ 𝐴 ) = ( [Q] ‘ 𝐵 ) ) ) → 𝐴 ~Q ( [Q] ‘ 𝐴 ) )
19 simprr ( ( 𝐴 ∈ ( N × N ) ∧ ( 𝐵 ∈ ( N × N ) ∧ ( [Q] ‘ 𝐴 ) = ( [Q] ‘ 𝐵 ) ) ) → ( [Q] ‘ 𝐴 ) = ( [Q] ‘ 𝐵 ) )
20 18 19 breqtrd ( ( 𝐴 ∈ ( N × N ) ∧ ( 𝐵 ∈ ( N × N ) ∧ ( [Q] ‘ 𝐴 ) = ( [Q] ‘ 𝐵 ) ) ) → 𝐴 ~Q ( [Q] ‘ 𝐵 ) )
21 11 ad2antrl ( ( 𝐴 ∈ ( N × N ) ∧ ( 𝐵 ∈ ( N × N ) ∧ ( [Q] ‘ 𝐴 ) = ( [Q] ‘ 𝐵 ) ) ) → 𝐵 ~Q ( [Q] ‘ 𝐵 ) )
22 17 20 21 ertr4d ( ( 𝐴 ∈ ( N × N ) ∧ ( 𝐵 ∈ ( N × N ) ∧ ( [Q] ‘ 𝐴 ) = ( [Q] ‘ 𝐵 ) ) ) → 𝐴 ~Q 𝐵 )
23 22 expr ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) → ( ( [Q] ‘ 𝐴 ) = ( [Q] ‘ 𝐵 ) → 𝐴 ~Q 𝐵 ) )
24 16 23 impbid ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) → ( 𝐴 ~Q 𝐵 ↔ ( [Q] ‘ 𝐴 ) = ( [Q] ‘ 𝐵 ) ) )