Step |
Hyp |
Ref |
Expression |
1 |
|
simp1 |
⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑁 ∈ ℕ ) |
2 |
|
simp3 |
⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) |
3 |
|
simp2 |
⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) |
4 |
|
axcgrrflx |
⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) → 〈 𝐵 , 𝐴 〉 Cgr 〈 𝐴 , 𝐵 〉 ) |
5 |
4
|
3com23 |
⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → 〈 𝐵 , 𝐴 〉 Cgr 〈 𝐴 , 𝐵 〉 ) |
6 |
1 2 3 3 2 3 2 5 5
|
cgrtr4d |
⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐴 , 𝐵 〉 ) |