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