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 ⊢ E = Edg ⁡ G
Assertion umgr2adedgwlklem ⊢ G ∈ UMGraph ∧ A B ∈ E ∧ B C ∈ E → A ≠ B ∧ B ≠ C ∧ A ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G ∧ C ∈ Vtx ⁡ G

Proof

Step Hyp Ref Expression
1 umgr2adedgwlk.e ⊢ E = Edg ⁡ G
2 1 umgredgne ⊢ G ∈ UMGraph ∧ A B ∈ E → A ≠ B
3 2 ex ⊢ G ∈ UMGraph → A B ∈ E → A ≠ B
4 1 umgredgne ⊢ G ∈ UMGraph ∧ B C ∈ E → B ≠ C
5 4 ex ⊢ G ∈ UMGraph → B C ∈ E → B ≠ C
6 3 5 anim12d ⊢ G ∈ UMGraph → A B ∈ E ∧ B C ∈ E → A ≠ B ∧ B ≠ C
7 6 3impib ⊢ G ∈ UMGraph ∧ A B ∈ E ∧ B C ∈ E → A ≠ B ∧ B ≠ C
8 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
9 8 1 umgrpredgv ⊢ G ∈ UMGraph ∧ A B ∈ E → A ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G
10 9 simpld ⊢ G ∈ UMGraph ∧ A B ∈ E → A ∈ Vtx ⁡ G
11 10 3adant3 ⊢ G ∈ UMGraph ∧ A B ∈ E ∧ B C ∈ E → A ∈ Vtx ⁡ G
12 8 1 umgrpredgv ⊢ G ∈ UMGraph ∧ B C ∈ E → B ∈ Vtx ⁡ G ∧ C ∈ Vtx ⁡ G
13 12 simpld ⊢ G ∈ UMGraph ∧ B C ∈ E → B ∈ Vtx ⁡ G
14 13 3adant2 ⊢ G ∈ UMGraph ∧ A B ∈ E ∧ B C ∈ E → B ∈ Vtx ⁡ G
15 12 simprd ⊢ G ∈ UMGraph ∧ B C ∈ E → C ∈ Vtx ⁡ G
16 15 3adant2 ⊢ G ∈ UMGraph ∧ A B ∈ E ∧ B C ∈ E → C ∈ Vtx ⁡ G
17 11 14 16 3jca ⊢ G ∈ UMGraph ∧ A B ∈ E ∧ B C ∈ E → A ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G ∧ C ∈ Vtx ⁡ G
18 7 17 jca ⊢ G ∈ UMGraph ∧ A B ∈ E ∧ B C ∈ E → A ≠ B ∧ B ≠ C ∧ A ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G ∧ C ∈ Vtx ⁡ G