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] ‘ 𝐵 ) ) )