Metamath Proof Explorer

Theorem 2pthon3v

Description: For a vertex adjacent to two other vertices there is a simple path of length 2 between these other vertices in a hypergraph. (Contributed by Alexander van der Vekens, 4-Dec-2017) (Revised by AV, 24-Jan-2021)

Ref Expression
Hypotheses 2pthon3v.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2pthon3v.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion 2pthon3v ( ( ( 𝐺 ∈ UHGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ) → ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐶 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 2 ) )

Proof

Step Hyp Ref Expression
1 2pthon3v.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 2pthon3v.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 edgval ⊢ ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 )
4 2 3 eqtri ⊢ 𝐸 = ran ( iEdg ‘ 𝐺 )
5 4 eleq2i ⊢ ( { 𝐴 , 𝐵 } ∈ 𝐸 ↔ { 𝐴 , 𝐵 } ∈ ran ( iEdg ‘ 𝐺 ) )
6 eqid ⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
7 1 6 uhgrf ⊢ ( 𝐺 ∈ UHGraph → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ ( 𝒫 𝑉 ∖ { ∅ } ) )
8 7 ffnd ⊢ ( 𝐺 ∈ UHGraph → ( iEdg ‘ 𝐺 ) Fn dom ( iEdg ‘ 𝐺 ) )
9 fvelrnb ⊢ ( ( iEdg ‘ 𝐺 ) Fn dom ( iEdg ‘ 𝐺 ) → ( { 𝐴 , 𝐵 } ∈ ran ( iEdg ‘ 𝐺 ) ↔ ∃ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) = { 𝐴 , 𝐵 } ) )
10 8 9 syl ⊢ ( 𝐺 ∈ UHGraph → ( { 𝐴 , 𝐵 } ∈ ran ( iEdg ‘ 𝐺 ) ↔ ∃ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) = { 𝐴 , 𝐵 } ) )
11 5 10 syl5bb ⊢ ( 𝐺 ∈ UHGraph → ( { 𝐴 , 𝐵 } ∈ 𝐸 ↔ ∃ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) = { 𝐴 , 𝐵 } ) )
12 4 eleq2i ⊢ ( { 𝐵 , 𝐶 } ∈ 𝐸 ↔ { 𝐵 , 𝐶 } ∈ ran ( iEdg ‘ 𝐺 ) )
13 fvelrnb ⊢ ( ( iEdg ‘ 𝐺 ) Fn dom ( iEdg ‘ 𝐺 ) → ( { 𝐵 , 𝐶 } ∈ ran ( iEdg ‘ 𝐺 ) ↔ ∃ 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) = { 𝐵 , 𝐶 } ) )
14 8 13 syl ⊢ ( 𝐺 ∈ UHGraph → ( { 𝐵 , 𝐶 } ∈ ran ( iEdg ‘ 𝐺 ) ↔ ∃ 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) = { 𝐵 , 𝐶 } ) )
15 12 14 syl5bb ⊢ ( 𝐺 ∈ UHGraph → ( { 𝐵 , 𝐶 } ∈ 𝐸 ↔ ∃ 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) = { 𝐵 , 𝐶 } ) )
16 11 15 anbi12d ⊢ ( 𝐺 ∈ UHGraph → ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ↔ ( ∃ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) = { 𝐴 , 𝐵 } ∧ ∃ 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) = { 𝐵 , 𝐶 } ) ) )
17 16 adantr ⊢ ( ( 𝐺 ∈ UHGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ↔ ( ∃ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) = { 𝐴 , 𝐵 } ∧ ∃ 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) = { 𝐵 , 𝐶 } ) ) )
18 17 adantr ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ↔ ( ∃ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) = { 𝐴 , 𝐵 } ∧ ∃ 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) = { 𝐵 , 𝐶 } ) ) )
19 reeanv ⊢ ( ∃ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∃ 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ( ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) = { 𝐴 , 𝐵 } ∧ ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) = { 𝐵 , 𝐶 } ) ↔ ( ∃ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) = { 𝐴 , 𝐵 } ∧ ∃ 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) = { 𝐵 , 𝐶 } ) )
20 18 19 bitr4di ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ↔ ∃ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∃ 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ( ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) = { 𝐴 , 𝐵 } ∧ ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) = { 𝐵 , 𝐶 } ) ) )
21 df-s2 ⊢ ⟨“ 𝑖 𝑗 ”⟩ = ( ⟨“ 𝑖 ”⟩ ++ ⟨“ 𝑗 ”⟩ )
22 21 ovexi ⊢ ⟨“ 𝑖 𝑗 ”⟩ ∈ V
23 df-s3 ⊢ ⟨“ 𝐴 𝐵 𝐶 ”⟩ = ( ⟨“ 𝐴 𝐵 ”⟩ ++ ⟨“ 𝐶 ”⟩ )
24 23 ovexi ⊢ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ V
25 22 24 pm3.2i ⊢ ( ⟨“ 𝑖 𝑗 ”⟩ ∈ V ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ V )
26 eqid ⊢ ⟨“ 𝐴 𝐵 𝐶 ”⟩ = ⟨“ 𝐴 𝐵 𝐶 ”⟩
27 eqid ⊢ ⟨“ 𝑖 𝑗 ”⟩ = ⟨“ 𝑖 𝑗 ”⟩
28 simp-4r ⊢ ( ( ( ( ( 𝐺 ∈ UHGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) ∧ ( 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∧ 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ) ) ∧ ( ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) = { 𝐴 , 𝐵 } ∧ ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) = { 𝐵 , 𝐶 } ) ) → ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) )
29 3simpb ⊢ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) → ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) )
30 29 ad3antlr ⊢ ( ( ( ( ( 𝐺 ∈ UHGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) ∧ ( 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∧ 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ) ) ∧ ( ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) = { 𝐴 , 𝐵 } ∧ ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) = { 𝐵 , 𝐶 } ) ) → ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) )
31 eqimss2 ⊢ ( ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) = { 𝐴 , 𝐵 } → { 𝐴 , 𝐵 } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) )
32 eqimss2 ⊢ ( ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) = { 𝐵 , 𝐶 } → { 𝐵 , 𝐶 } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) )
33 31 32 anim12i ⊢ ( ( ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) = { 𝐴 , 𝐵 } ∧ ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) = { 𝐵 , 𝐶 } ) → ( { 𝐴 , 𝐵 } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ∧ { 𝐵 , 𝐶 } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ) )
34 33 adantl ⊢ ( ( ( ( ( 𝐺 ∈ UHGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) ∧ ( 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∧ 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ) ) ∧ ( ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) = { 𝐴 , 𝐵 } ∧ ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) = { 𝐵 , 𝐶 } ) ) → ( { 𝐴 , 𝐵 } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ∧ { 𝐵 , 𝐶 } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ) )
35 fveqeq2 ⊢ ( 𝑖 = 𝑗 → ( ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) = { 𝐴 , 𝐵 } ↔ ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) = { 𝐴 , 𝐵 } ) )
36 35 anbi1d ⊢ ( 𝑖 = 𝑗 → ( ( ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) = { 𝐴 , 𝐵 } ∧ ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) = { 𝐵 , 𝐶 } ) ↔ ( ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) = { 𝐴 , 𝐵 } ∧ ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) = { 𝐵 , 𝐶 } ) ) )
37 eqtr2 ⊢ ( ( ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) = { 𝐴 , 𝐵 } ∧ ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) = { 𝐵 , 𝐶 } ) → { 𝐴 , 𝐵 } = { 𝐵 , 𝐶 } )
38 3simpa ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) )
39 3simpc ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) )
40 preq12bg ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( { 𝐴 , 𝐵 } = { 𝐵 , 𝐶 } ↔ ( ( 𝐴 = 𝐵 ∧ 𝐵 = 𝐶 ) ∨ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐵 ) ) ) )
41 38 39 40 syl2anc ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( { 𝐴 , 𝐵 } = { 𝐵 , 𝐶 } ↔ ( ( 𝐴 = 𝐵 ∧ 𝐵 = 𝐶 ) ∨ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐵 ) ) ) )
42 eqneqall ⊢ ( 𝐴 = 𝐵 → ( 𝐴 ≠ 𝐵 → 𝑖 ≠ 𝑗 ) )
43 42 com12 ⊢ ( 𝐴 ≠ 𝐵 → ( 𝐴 = 𝐵 → 𝑖 ≠ 𝑗 ) )
44 43 3ad2ant1 ⊢ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) → ( 𝐴 = 𝐵 → 𝑖 ≠ 𝑗 ) )
45 44 com12 ⊢ ( 𝐴 = 𝐵 → ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) → 𝑖 ≠ 𝑗 ) )
46 45 adantr ⊢ ( ( 𝐴 = 𝐵 ∧ 𝐵 = 𝐶 ) → ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) → 𝑖 ≠ 𝑗 ) )
47 eqneqall ⊢ ( 𝐴 = 𝐶 → ( 𝐴 ≠ 𝐶 → 𝑖 ≠ 𝑗 ) )
48 47 com12 ⊢ ( 𝐴 ≠ 𝐶 → ( 𝐴 = 𝐶 → 𝑖 ≠ 𝑗 ) )
49 48 3ad2ant2 ⊢ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) → ( 𝐴 = 𝐶 → 𝑖 ≠ 𝑗 ) )
50 49 com12 ⊢ ( 𝐴 = 𝐶 → ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) → 𝑖 ≠ 𝑗 ) )
51 50 adantr ⊢ ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐵 ) → ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) → 𝑖 ≠ 𝑗 ) )
52 46 51 jaoi ⊢ ( ( ( 𝐴 = 𝐵 ∧ 𝐵 = 𝐶 ) ∨ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐵 ) ) → ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) → 𝑖 ≠ 𝑗 ) )
53 41 52 syl6bi ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( { 𝐴 , 𝐵 } = { 𝐵 , 𝐶 } → ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) → 𝑖 ≠ 𝑗 ) ) )
54 53 com23 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) → ( { 𝐴 , 𝐵 } = { 𝐵 , 𝐶 } → 𝑖 ≠ 𝑗 ) ) )
55 54 adantl ⊢ ( ( 𝐺 ∈ UHGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) → ( { 𝐴 , 𝐵 } = { 𝐵 , 𝐶 } → 𝑖 ≠ 𝑗 ) ) )
56 55 imp ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → ( { 𝐴 , 𝐵 } = { 𝐵 , 𝐶 } → 𝑖 ≠ 𝑗 ) )
57 56 com12 ⊢ ( { 𝐴 , 𝐵 } = { 𝐵 , 𝐶 } → ( ( ( 𝐺 ∈ UHGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → 𝑖 ≠ 𝑗 ) )
58 37 57 syl ⊢ ( ( ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) = { 𝐴 , 𝐵 } ∧ ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) = { 𝐵 , 𝐶 } ) → ( ( ( 𝐺 ∈ UHGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → 𝑖 ≠ 𝑗 ) )
59 36 58 syl6bi ⊢ ( 𝑖 = 𝑗 → ( ( ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) = { 𝐴 , 𝐵 } ∧ ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) = { 𝐵 , 𝐶 } ) → ( ( ( 𝐺 ∈ UHGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → 𝑖 ≠ 𝑗 ) ) )
60 59 com23 ⊢ ( 𝑖 = 𝑗 → ( ( ( 𝐺 ∈ UHGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → ( ( ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) = { 𝐴 , 𝐵 } ∧ ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) = { 𝐵 , 𝐶 } ) → 𝑖 ≠ 𝑗 ) ) )
61 2a1 ⊢ ( 𝑖 ≠ 𝑗 → ( ( ( 𝐺 ∈ UHGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → ( ( ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) = { 𝐴 , 𝐵 } ∧ ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) = { 𝐵 , 𝐶 } ) → 𝑖 ≠ 𝑗 ) ) )
62 60 61 pm2.61ine ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → ( ( ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) = { 𝐴 , 𝐵 } ∧ ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) = { 𝐵 , 𝐶 } ) → 𝑖 ≠ 𝑗 ) )
63 62 adantr ⊢ ( ( ( ( 𝐺 ∈ UHGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) ∧ ( 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∧ 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ) ) → ( ( ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) = { 𝐴 , 𝐵 } ∧ ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) = { 𝐵 , 𝐶 } ) → 𝑖 ≠ 𝑗 ) )
64 63 imp ⊢ ( ( ( ( ( 𝐺 ∈ UHGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) ∧ ( 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∧ 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ) ) ∧ ( ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) = { 𝐴 , 𝐵 } ∧ ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) = { 𝐵 , 𝐶 } ) ) → 𝑖 ≠ 𝑗 )
65 simplr2 ⊢ ( ( ( ( 𝐺 ∈ UHGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) ∧ ( 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∧ 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ) ) → 𝐴 ≠ 𝐶 )
66 65 adantr ⊢ ( ( ( ( ( 𝐺 ∈ UHGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) ∧ ( 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∧ 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ) ) ∧ ( ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) = { 𝐴 , 𝐵 } ∧ ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) = { 𝐵 , 𝐶 } ) ) → 𝐴 ≠ 𝐶 )
67 26 27 28 30 34 1 6 64 66 2pthond ⊢ ( ( ( ( ( 𝐺 ∈ UHGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) ∧ ( 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∧ 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ) ) ∧ ( ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) = { 𝐴 , 𝐵 } ∧ ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) = { 𝐵 , 𝐶 } ) ) → ⟨“ 𝑖 𝑗 ”⟩ ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐶 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ )
68 s2len ⊢ ( ♯ ‘ ⟨“ 𝑖 𝑗 ”⟩ ) = 2
69 67 68 jctir ⊢ ( ( ( ( ( 𝐺 ∈ UHGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) ∧ ( 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∧ 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ) ) ∧ ( ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) = { 𝐴 , 𝐵 } ∧ ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) = { 𝐵 , 𝐶 } ) ) → ( ⟨“ 𝑖 𝑗 ”⟩ ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐶 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∧ ( ♯ ‘ ⟨“ 𝑖 𝑗 ”⟩ ) = 2 ) )
70 breq12 ⊢ ( ( 𝑓 = ⟨“ 𝑖 𝑗 ”⟩ ∧ 𝑝 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) → ( 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐶 ) 𝑝 ↔ ⟨“ 𝑖 𝑗 ”⟩ ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐶 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) )
71 fveqeq2 ⊢ ( 𝑓 = ⟨“ 𝑖 𝑗 ”⟩ → ( ( ♯ ‘ 𝑓 ) = 2 ↔ ( ♯ ‘ ⟨“ 𝑖 𝑗 ”⟩ ) = 2 ) )
72 71 adantr ⊢ ( ( 𝑓 = ⟨“ 𝑖 𝑗 ”⟩ ∧ 𝑝 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) → ( ( ♯ ‘ 𝑓 ) = 2 ↔ ( ♯ ‘ ⟨“ 𝑖 𝑗 ”⟩ ) = 2 ) )
73 70 72 anbi12d ⊢ ( ( 𝑓 = ⟨“ 𝑖 𝑗 ”⟩ ∧ 𝑝 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) → ( ( 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐶 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ↔ ( ⟨“ 𝑖 𝑗 ”⟩ ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐶 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∧ ( ♯ ‘ ⟨“ 𝑖 𝑗 ”⟩ ) = 2 ) ) )
74 73 spc2egv ⊢ ( ( ⟨“ 𝑖 𝑗 ”⟩ ∈ V ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ V ) → ( ( ⟨“ 𝑖 𝑗 ”⟩ ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐶 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∧ ( ♯ ‘ ⟨“ 𝑖 𝑗 ”⟩ ) = 2 ) → ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐶 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) )
75 25 69 74 mpsyl ⊢ ( ( ( ( ( 𝐺 ∈ UHGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) ∧ ( 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∧ 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ) ) ∧ ( ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) = { 𝐴 , 𝐵 } ∧ ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) = { 𝐵 , 𝐶 } ) ) → ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐶 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 2 ) )
76 75 ex ⊢ ( ( ( ( 𝐺 ∈ UHGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) ∧ ( 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∧ 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ) ) → ( ( ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) = { 𝐴 , 𝐵 } ∧ ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) = { 𝐵 , 𝐶 } ) → ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐶 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) )
77 76 rexlimdvva ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → ( ∃ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∃ 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ( ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) = { 𝐴 , 𝐵 } ∧ ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) = { 𝐵 , 𝐶 } ) → ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐶 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) )
78 20 77 sylbid ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) → ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐶 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) )
79 78 3impia ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ) → ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐶 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 2 ) )