Metamath Proof Explorer

Theorem lgricngricex

Description: There are two different locally isomorphic graphs which are not isomorphic. (Contributed by AV, 23-Nov-2025)

Ref Expression
Assertion lgricngricex ∃ 𝑔 ∃ ℎ ( 𝑔 ≃𝑙𝑔𝑟 ℎ ∧ ¬ 𝑔 ≃𝑔𝑟 ℎ )

Proof

Step Hyp Ref Expression
1 gpg5grlic ⊢ ( 5 gPetersenGr 1 ) ≃𝑙𝑔𝑟 ( 5 gPetersenGr 2 )
2 gpg5ngric ⊢ ¬ ( 5 gPetersenGr 1 ) ≃𝑔𝑟 ( 5 gPetersenGr 2 )
3 ovex ⊢ ( 5 gPetersenGr 1 ) ∈ V
4 ovex ⊢ ( 5 gPetersenGr 2 ) ∈ V
5 breq12 ⊢ ( ( 𝑔 = ( 5 gPetersenGr 1 ) ∧ ℎ = ( 5 gPetersenGr 2 ) ) → ( 𝑔 ≃𝑙𝑔𝑟 ℎ ↔ ( 5 gPetersenGr 1 ) ≃𝑙𝑔𝑟 ( 5 gPetersenGr 2 ) ) )
6 breq12 ⊢ ( ( 𝑔 = ( 5 gPetersenGr 1 ) ∧ ℎ = ( 5 gPetersenGr 2 ) ) → ( 𝑔 ≃𝑔𝑟 ℎ ↔ ( 5 gPetersenGr 1 ) ≃𝑔𝑟 ( 5 gPetersenGr 2 ) ) )
7 6 notbid ⊢ ( ( 𝑔 = ( 5 gPetersenGr 1 ) ∧ ℎ = ( 5 gPetersenGr 2 ) ) → ( ¬ 𝑔 ≃𝑔𝑟 ℎ ↔ ¬ ( 5 gPetersenGr 1 ) ≃𝑔𝑟 ( 5 gPetersenGr 2 ) ) )
8 5 7 anbi12d ⊢ ( ( 𝑔 = ( 5 gPetersenGr 1 ) ∧ ℎ = ( 5 gPetersenGr 2 ) ) → ( ( 𝑔 ≃𝑙𝑔𝑟 ℎ ∧ ¬ 𝑔 ≃𝑔𝑟 ℎ ) ↔ ( ( 5 gPetersenGr 1 ) ≃𝑙𝑔𝑟 ( 5 gPetersenGr 2 ) ∧ ¬ ( 5 gPetersenGr 1 ) ≃𝑔𝑟 ( 5 gPetersenGr 2 ) ) ) )
9 3 4 8 spc2ev ⊢ ( ( ( 5 gPetersenGr 1 ) ≃𝑙𝑔𝑟 ( 5 gPetersenGr 2 ) ∧ ¬ ( 5 gPetersenGr 1 ) ≃𝑔𝑟 ( 5 gPetersenGr 2 ) ) → ∃ 𝑔 ∃ ℎ ( 𝑔 ≃𝑙𝑔𝑟 ℎ ∧ ¬ 𝑔 ≃𝑔𝑟 ℎ ) )
10 1 2 9 mp2an ⊢ ∃ 𝑔 ∃ ℎ ( 𝑔 ≃𝑙𝑔𝑟 ℎ ∧ ¬ 𝑔 ≃𝑔𝑟 ℎ )