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

Metamath Proof Explorer

Theorem umgr2adedgwlklem

Description: Lemma for umgr2adedgwlk , umgr2adedgspth , etc. (Contributed by Alexander van der Vekens, 1-Feb-2018) (Revised by AV, 29-Jan-2021)

Ref Expression
Hypothesis umgr2adedgwlk.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion umgr2adedgwlklem ( ( 𝐺 ∈ UMGraph ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) → ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐶 ∈ ( Vtx ‘ 𝐺 ) ) ) )

Proof

Step Hyp Ref Expression
1 umgr2adedgwlk.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
2 1 umgredgne ⊢ ( ( 𝐺 ∈ UMGraph ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) → 𝐴 ≠ 𝐵 )
3 2 ex ⊢ ( 𝐺 ∈ UMGraph → ( { 𝐴 , 𝐵 } ∈ 𝐸 → 𝐴 ≠ 𝐵 ) )
4 1 umgredgne ⊢ ( ( 𝐺 ∈ UMGraph ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) → 𝐵 ≠ 𝐶 )
5 4 ex ⊢ ( 𝐺 ∈ UMGraph → ( { 𝐵 , 𝐶 } ∈ 𝐸 → 𝐵 ≠ 𝐶 ) )
6 3 5 anim12d ⊢ ( 𝐺 ∈ UMGraph → ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) → ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ) )
7 6 3impib ⊢ ( ( 𝐺 ∈ UMGraph ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) → ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) )
8 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
9 8 1 umgrpredgv ⊢ ( ( 𝐺 ∈ UMGraph ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) → ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) )
10 9 simpld ⊢ ( ( 𝐺 ∈ UMGraph ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) → 𝐴 ∈ ( Vtx ‘ 𝐺 ) )
11 10 3adant3 ⊢ ( ( 𝐺 ∈ UMGraph ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) → 𝐴 ∈ ( Vtx ‘ 𝐺 ) )
12 8 1 umgrpredgv ⊢ ( ( 𝐺 ∈ UMGraph ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) → ( 𝐵 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐶 ∈ ( Vtx ‘ 𝐺 ) ) )
13 12 simpld ⊢ ( ( 𝐺 ∈ UMGraph ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) → 𝐵 ∈ ( Vtx ‘ 𝐺 ) )
14 13 3adant2 ⊢ ( ( 𝐺 ∈ UMGraph ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) → 𝐵 ∈ ( Vtx ‘ 𝐺 ) )
15 12 simprd ⊢ ( ( 𝐺 ∈ UMGraph ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) → 𝐶 ∈ ( Vtx ‘ 𝐺 ) )
16 15 3adant2 ⊢ ( ( 𝐺 ∈ UMGraph ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) → 𝐶 ∈ ( Vtx ‘ 𝐺 ) )
17 11 14 16 3jca ⊢ ( ( 𝐺 ∈ UMGraph ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) → ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐶 ∈ ( Vtx ‘ 𝐺 ) ) )
18 7 17 jca ⊢ ( ( 𝐺 ∈ UMGraph ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) → ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐶 ∈ ( Vtx ‘ 𝐺 ) ) ) )