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 ‘ 𝐺 ) ) ) )