This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem umgr2edg1

Description: If a vertex is adjacent to two different vertices in a multigraph, there is not only one edge starting at this vertex. (Contributed by Alexander van der Vekens, 10-Dec-2017) (Revised by AV, 8-Jun-2021)

Ref Expression
Hypotheses usgrf1oedg.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
usgrf1oedg.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion umgr2edg1 ( ( ( 𝐺 ∈ UMGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( { 𝑁 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ) ) → ¬ ∃! 𝑥 ∈ dom 𝐼 𝑁 ∈ ( 𝐼 ‘ 𝑥 ) )

Proof

Step Hyp Ref Expression
1 usgrf1oedg.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
2 usgrf1oedg.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 1 2 umgr2edg ⊢ ( ( ( 𝐺 ∈ UMGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( { 𝑁 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ) ) → ∃ 𝑥 ∈ dom 𝐼 ∃ 𝑦 ∈ dom 𝐼 ( 𝑥 ≠ 𝑦 ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑥 ) ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑦 ) ) )
4 3anrot ⊢ ( ( 𝑥 ≠ 𝑦 ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑥 ) ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑦 ) ) ↔ ( 𝑁 ∈ ( 𝐼 ‘ 𝑥 ) ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) )
5 df-ne ⊢ ( 𝑥 ≠ 𝑦 ↔ ¬ 𝑥 = 𝑦 )
6 5 3anbi3i ⊢ ( ( 𝑁 ∈ ( 𝐼 ‘ 𝑥 ) ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ↔ ( 𝑁 ∈ ( 𝐼 ‘ 𝑥 ) ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑦 ) ∧ ¬ 𝑥 = 𝑦 ) )
7 4 6 bitri ⊢ ( ( 𝑥 ≠ 𝑦 ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑥 ) ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑦 ) ) ↔ ( 𝑁 ∈ ( 𝐼 ‘ 𝑥 ) ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑦 ) ∧ ¬ 𝑥 = 𝑦 ) )
8 df-3an ⊢ ( ( 𝑁 ∈ ( 𝐼 ‘ 𝑥 ) ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑦 ) ∧ ¬ 𝑥 = 𝑦 ) ↔ ( ( 𝑁 ∈ ( 𝐼 ‘ 𝑥 ) ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑦 ) ) ∧ ¬ 𝑥 = 𝑦 ) )
9 7 8 bitri ⊢ ( ( 𝑥 ≠ 𝑦 ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑥 ) ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑦 ) ) ↔ ( ( 𝑁 ∈ ( 𝐼 ‘ 𝑥 ) ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑦 ) ) ∧ ¬ 𝑥 = 𝑦 ) )
10 9 2rexbii ⊢ ( ∃ 𝑥 ∈ dom 𝐼 ∃ 𝑦 ∈ dom 𝐼 ( 𝑥 ≠ 𝑦 ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑥 ) ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑦 ) ) ↔ ∃ 𝑥 ∈ dom 𝐼 ∃ 𝑦 ∈ dom 𝐼 ( ( 𝑁 ∈ ( 𝐼 ‘ 𝑥 ) ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑦 ) ) ∧ ¬ 𝑥 = 𝑦 ) )
11 3 10 sylib ⊢ ( ( ( 𝐺 ∈ UMGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( { 𝑁 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ) ) → ∃ 𝑥 ∈ dom 𝐼 ∃ 𝑦 ∈ dom 𝐼 ( ( 𝑁 ∈ ( 𝐼 ‘ 𝑥 ) ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑦 ) ) ∧ ¬ 𝑥 = 𝑦 ) )
12 rexanali ⊢ ( ∃ 𝑦 ∈ dom 𝐼 ( ( 𝑁 ∈ ( 𝐼 ‘ 𝑥 ) ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑦 ) ) ∧ ¬ 𝑥 = 𝑦 ) ↔ ¬ ∀ 𝑦 ∈ dom 𝐼 ( ( 𝑁 ∈ ( 𝐼 ‘ 𝑥 ) ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑦 ) ) → 𝑥 = 𝑦 ) )
13 12 rexbii ⊢ ( ∃ 𝑥 ∈ dom 𝐼 ∃ 𝑦 ∈ dom 𝐼 ( ( 𝑁 ∈ ( 𝐼 ‘ 𝑥 ) ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑦 ) ) ∧ ¬ 𝑥 = 𝑦 ) ↔ ∃ 𝑥 ∈ dom 𝐼 ¬ ∀ 𝑦 ∈ dom 𝐼 ( ( 𝑁 ∈ ( 𝐼 ‘ 𝑥 ) ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑦 ) ) → 𝑥 = 𝑦 ) )
14 rexnal ⊢ ( ∃ 𝑥 ∈ dom 𝐼 ¬ ∀ 𝑦 ∈ dom 𝐼 ( ( 𝑁 ∈ ( 𝐼 ‘ 𝑥 ) ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑦 ) ) → 𝑥 = 𝑦 ) ↔ ¬ ∀ 𝑥 ∈ dom 𝐼 ∀ 𝑦 ∈ dom 𝐼 ( ( 𝑁 ∈ ( 𝐼 ‘ 𝑥 ) ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑦 ) ) → 𝑥 = 𝑦 ) )
15 13 14 bitri ⊢ ( ∃ 𝑥 ∈ dom 𝐼 ∃ 𝑦 ∈ dom 𝐼 ( ( 𝑁 ∈ ( 𝐼 ‘ 𝑥 ) ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑦 ) ) ∧ ¬ 𝑥 = 𝑦 ) ↔ ¬ ∀ 𝑥 ∈ dom 𝐼 ∀ 𝑦 ∈ dom 𝐼 ( ( 𝑁 ∈ ( 𝐼 ‘ 𝑥 ) ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑦 ) ) → 𝑥 = 𝑦 ) )
16 11 15 sylib ⊢ ( ( ( 𝐺 ∈ UMGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( { 𝑁 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ) ) → ¬ ∀ 𝑥 ∈ dom 𝐼 ∀ 𝑦 ∈ dom 𝐼 ( ( 𝑁 ∈ ( 𝐼 ‘ 𝑥 ) ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑦 ) ) → 𝑥 = 𝑦 ) )
17 16 intnand ⊢ ( ( ( 𝐺 ∈ UMGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( { 𝑁 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ) ) → ¬ ( ∃ 𝑥 ∈ dom 𝐼 𝑁 ∈ ( 𝐼 ‘ 𝑥 ) ∧ ∀ 𝑥 ∈ dom 𝐼 ∀ 𝑦 ∈ dom 𝐼 ( ( 𝑁 ∈ ( 𝐼 ‘ 𝑥 ) ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑦 ) ) → 𝑥 = 𝑦 ) ) )
18 fveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐼 ‘ 𝑥 ) = ( 𝐼 ‘ 𝑦 ) )
19 18 eleq2d ⊢ ( 𝑥 = 𝑦 → ( 𝑁 ∈ ( 𝐼 ‘ 𝑥 ) ↔ 𝑁 ∈ ( 𝐼 ‘ 𝑦 ) ) )
20 19 reu4 ⊢ ( ∃! 𝑥 ∈ dom 𝐼 𝑁 ∈ ( 𝐼 ‘ 𝑥 ) ↔ ( ∃ 𝑥 ∈ dom 𝐼 𝑁 ∈ ( 𝐼 ‘ 𝑥 ) ∧ ∀ 𝑥 ∈ dom 𝐼 ∀ 𝑦 ∈ dom 𝐼 ( ( 𝑁 ∈ ( 𝐼 ‘ 𝑥 ) ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑦 ) ) → 𝑥 = 𝑦 ) ) )
21 17 20 sylnibr ⊢ ( ( ( 𝐺 ∈ UMGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( { 𝑁 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ) ) → ¬ ∃! 𝑥 ∈ dom 𝐼 𝑁 ∈ ( 𝐼 ‘ 𝑥 ) )