Step |
Hyp |
Ref |
Expression |
1 |
|
opeq1 |
⊢ ( 𝐴 = 𝐵 → 〈 𝐴 , 𝐵 〉 = 〈 𝐵 , 𝐵 〉 ) |
2 |
1
|
breq1d |
⊢ ( 𝐴 = 𝐵 → ( 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐶 , 𝐷 〉 ↔ 〈 𝐵 , 𝐵 〉 Cgr 〈 𝐶 , 𝐷 〉 ) ) |
3 |
2
|
biimpac |
⊢ ( ( 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐶 , 𝐷 〉 ∧ 𝐴 = 𝐵 ) → 〈 𝐵 , 𝐵 〉 Cgr 〈 𝐶 , 𝐷 〉 ) |
4 |
|
simp1 |
⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑁 ∈ ℕ ) |
5 |
|
simp2r |
⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) |
6 |
|
simp3l |
⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) |
7 |
|
simp3r |
⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) |
8 |
|
cgrid2 |
⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 〈 𝐵 , 𝐵 〉 Cgr 〈 𝐶 , 𝐷 〉 → 𝐶 = 𝐷 ) ) |
9 |
4 5 6 7 8
|
syl13anc |
⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 〈 𝐵 , 𝐵 〉 Cgr 〈 𝐶 , 𝐷 〉 → 𝐶 = 𝐷 ) ) |
10 |
3 9
|
syl5 |
⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐶 , 𝐷 〉 ∧ 𝐴 = 𝐵 ) → 𝐶 = 𝐷 ) ) |
11 |
10
|
expdimp |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐶 , 𝐷 〉 ) → ( 𝐴 = 𝐵 → 𝐶 = 𝐷 ) ) |
12 |
|
opeq1 |
⊢ ( 𝐶 = 𝐷 → 〈 𝐶 , 𝐷 〉 = 〈 𝐷 , 𝐷 〉 ) |
13 |
12
|
breq2d |
⊢ ( 𝐶 = 𝐷 → ( 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐶 , 𝐷 〉 ↔ 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐷 , 𝐷 〉 ) ) |
14 |
13
|
biimpac |
⊢ ( ( 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐶 , 𝐷 〉 ∧ 𝐶 = 𝐷 ) → 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐷 , 𝐷 〉 ) |
15 |
|
simp2l |
⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) |
16 |
|
axcgrid |
⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐷 , 𝐷 〉 → 𝐴 = 𝐵 ) ) |
17 |
4 15 5 7 16
|
syl13anc |
⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐷 , 𝐷 〉 → 𝐴 = 𝐵 ) ) |
18 |
14 17
|
syl5 |
⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐶 , 𝐷 〉 ∧ 𝐶 = 𝐷 ) → 𝐴 = 𝐵 ) ) |
19 |
18
|
expdimp |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐶 , 𝐷 〉 ) → ( 𝐶 = 𝐷 → 𝐴 = 𝐵 ) ) |
20 |
11 19
|
impbid |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐶 , 𝐷 〉 ) → ( 𝐴 = 𝐵 ↔ 𝐶 = 𝐷 ) ) |
21 |
20
|
ex |
⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐶 , 𝐷 〉 → ( 𝐴 = 𝐵 ↔ 𝐶 = 𝐷 ) ) ) |