Metamath Proof Explorer

Theorem cgrid2

Description: Identity law for congruence. (Contributed by Scott Fenton, 12-Jun-2013)

Ref Expression
Assertion cgrid2 ${⊢}\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\right)\to \left(⟨{A},{A}⟩\mathrm{Cgr}⟨{B},{C}⟩\to {B}={C}\right)$

Proof

Step Hyp Ref Expression
1 simpl ${⊢}\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\right)\to {N}\in ℕ$
2 simpr1 ${⊢}\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\right)\to {A}\in 𝔼\left({N}\right)$
3 simpr2 ${⊢}\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\right)\to {B}\in 𝔼\left({N}\right)$
4 simpr3 ${⊢}\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\right)\to {C}\in 𝔼\left({N}\right)$
5 cgrcom ${⊢}\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {A}\in 𝔼\left({N}\right)\right)\wedge \left({B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\right)\to \left(⟨{A},{A}⟩\mathrm{Cgr}⟨{B},{C}⟩↔⟨{B},{C}⟩\mathrm{Cgr}⟨{A},{A}⟩\right)$
6 1 2 2 3 4 5 syl122anc ${⊢}\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\right)\to \left(⟨{A},{A}⟩\mathrm{Cgr}⟨{B},{C}⟩↔⟨{B},{C}⟩\mathrm{Cgr}⟨{A},{A}⟩\right)$
7 3anrot ${⊢}\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)↔\left({B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\wedge {A}\in 𝔼\left({N}\right)\right)$
8 axcgrid ${⊢}\left({N}\in ℕ\wedge \left({B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\wedge {A}\in 𝔼\left({N}\right)\right)\right)\to \left(⟨{B},{C}⟩\mathrm{Cgr}⟨{A},{A}⟩\to {B}={C}\right)$
9 7 8 sylan2b ${⊢}\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\right)\to \left(⟨{B},{C}⟩\mathrm{Cgr}⟨{A},{A}⟩\to {B}={C}\right)$
10 6 9 sylbid ${⊢}\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\right)\to \left(⟨{A},{A}⟩\mathrm{Cgr}⟨{B},{C}⟩\to {B}={C}\right)$