Metamath Proof Explorer

Theorem usgr2pth0

Description: In a simply graph, there is a path of length 2 iff there are three distinct vertices so that one of them is connected to each of the two others by an edge. (Contributed by Alexander van der Vekens, 27-Jan-2018) (Revised by AV, 5-Jun-2021)

Ref Expression
Hypotheses usgr2pthlem.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
usgr2pthlem.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
Assertion usgr2pth0 ( 𝐺 ∈ USGraph → ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( ♯ ‘ 𝐹 ) = 2 ) ↔ ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ 𝑃 : ( 0 ... 2 ) –1-1→ 𝑉 ∧ ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑧 ∧ ( 𝑃 ‘ 2 ) = 𝑦 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑧 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑧 , 𝑦 } ) ) ) ) )

Proof

Step Hyp Ref Expression
1 usgr2pthlem.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 usgr2pthlem.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
3 1 2 usgr2pth ⊢ ( 𝐺 ∈ USGraph → ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( ♯ ‘ 𝐹 ) = 2 ) ↔ ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ 𝑃 : ( 0 ... 2 ) –1-1→ 𝑉 ∧ ∃ 𝑥 ∈ 𝑉 ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 } ) ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 , 𝑧 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑧 ∧ ( 𝑃 ‘ 2 ) = 𝑦 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑧 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑧 , 𝑦 } ) ) ) ) )
4 r19.42v ⊢ ( ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 , 𝑧 } ) ( 𝑧 ≠ 𝑥 ∧ ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑧 ∧ ( 𝑃 ‘ 2 ) = 𝑦 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑧 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑧 , 𝑦 } ) ) ) ↔ ( 𝑧 ≠ 𝑥 ∧ ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 , 𝑧 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑧 ∧ ( 𝑃 ‘ 2 ) = 𝑦 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑧 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑧 , 𝑦 } ) ) ) )
5 rexdifpr ⊢ ( ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 , 𝑧 } ) ( 𝑧 ≠ 𝑥 ∧ ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑧 ∧ ( 𝑃 ‘ 2 ) = 𝑦 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑧 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑧 , 𝑦 } ) ) ) ↔ ∃ 𝑦 ∈ 𝑉 ( 𝑦 ≠ 𝑥 ∧ 𝑦 ≠ 𝑧 ∧ ( 𝑧 ≠ 𝑥 ∧ ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑧 ∧ ( 𝑃 ‘ 2 ) = 𝑦 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑧 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑧 , 𝑦 } ) ) ) ) )
6 4 5 bitr3i ⊢ ( ( 𝑧 ≠ 𝑥 ∧ ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 , 𝑧 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑧 ∧ ( 𝑃 ‘ 2 ) = 𝑦 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑧 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑧 , 𝑦 } ) ) ) ↔ ∃ 𝑦 ∈ 𝑉 ( 𝑦 ≠ 𝑥 ∧ 𝑦 ≠ 𝑧 ∧ ( 𝑧 ≠ 𝑥 ∧ ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑧 ∧ ( 𝑃 ‘ 2 ) = 𝑦 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑧 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑧 , 𝑦 } ) ) ) ) )
7 6 rexbii ⊢ ( ∃ 𝑧 ∈ 𝑉 ( 𝑧 ≠ 𝑥 ∧ ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 , 𝑧 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑧 ∧ ( 𝑃 ‘ 2 ) = 𝑦 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑧 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑧 , 𝑦 } ) ) ) ↔ ∃ 𝑧 ∈ 𝑉 ∃ 𝑦 ∈ 𝑉 ( 𝑦 ≠ 𝑥 ∧ 𝑦 ≠ 𝑧 ∧ ( 𝑧 ≠ 𝑥 ∧ ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑧 ∧ ( 𝑃 ‘ 2 ) = 𝑦 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑧 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑧 , 𝑦 } ) ) ) ) )
8 rexcom ⊢ ( ∃ 𝑧 ∈ 𝑉 ∃ 𝑦 ∈ 𝑉 ( 𝑦 ≠ 𝑥 ∧ 𝑦 ≠ 𝑧 ∧ ( 𝑧 ≠ 𝑥 ∧ ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑧 ∧ ( 𝑃 ‘ 2 ) = 𝑦 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑧 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑧 , 𝑦 } ) ) ) ) ↔ ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ 𝑉 ( 𝑦 ≠ 𝑥 ∧ 𝑦 ≠ 𝑧 ∧ ( 𝑧 ≠ 𝑥 ∧ ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑧 ∧ ( 𝑃 ‘ 2 ) = 𝑦 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑧 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑧 , 𝑦 } ) ) ) ) )
9 df-3an ⊢ ( ( 𝑦 ≠ 𝑥 ∧ 𝑦 ≠ 𝑧 ∧ ( 𝑧 ≠ 𝑥 ∧ ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑧 ∧ ( 𝑃 ‘ 2 ) = 𝑦 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑧 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑧 , 𝑦 } ) ) ) ) ↔ ( ( 𝑦 ≠ 𝑥 ∧ 𝑦 ≠ 𝑧 ) ∧ ( 𝑧 ≠ 𝑥 ∧ ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑧 ∧ ( 𝑃 ‘ 2 ) = 𝑦 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑧 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑧 , 𝑦 } ) ) ) ) )
10 anass ⊢ ( ( ( ( 𝑦 ≠ 𝑥 ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑧 ≠ 𝑥 ) ∧ ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑧 ∧ ( 𝑃 ‘ 2 ) = 𝑦 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑧 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑧 , 𝑦 } ) ) ) ↔ ( ( 𝑦 ≠ 𝑥 ∧ 𝑦 ≠ 𝑧 ) ∧ ( 𝑧 ≠ 𝑥 ∧ ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑧 ∧ ( 𝑃 ‘ 2 ) = 𝑦 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑧 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑧 , 𝑦 } ) ) ) ) )
11 anass ⊢ ( ( ( ( 𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑥 ) ∧ ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑧 ∧ ( 𝑃 ‘ 2 ) = 𝑦 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑧 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑧 , 𝑦 } ) ) ) ↔ ( ( 𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ) ∧ ( 𝑦 ≠ 𝑥 ∧ ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑧 ∧ ( 𝑃 ‘ 2 ) = 𝑦 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑧 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑧 , 𝑦 } ) ) ) ) )
12 anass ⊢ ( ( ( 𝑦 ≠ 𝑥 ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑧 ≠ 𝑥 ) ↔ ( 𝑦 ≠ 𝑥 ∧ ( 𝑦 ≠ 𝑧 ∧ 𝑧 ≠ 𝑥 ) ) )
13 ancom ⊢ ( ( 𝑦 ≠ 𝑥 ∧ ( 𝑦 ≠ 𝑧 ∧ 𝑧 ≠ 𝑥 ) ) ↔ ( ( 𝑦 ≠ 𝑧 ∧ 𝑧 ≠ 𝑥 ) ∧ 𝑦 ≠ 𝑥 ) )
14 necom ⊢ ( 𝑦 ≠ 𝑧 ↔ 𝑧 ≠ 𝑦 )
15 14 anbi2ci ⊢ ( ( 𝑦 ≠ 𝑧 ∧ 𝑧 ≠ 𝑥 ) ↔ ( 𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ) )
16 15 anbi1i ⊢ ( ( ( 𝑦 ≠ 𝑧 ∧ 𝑧 ≠ 𝑥 ) ∧ 𝑦 ≠ 𝑥 ) ↔ ( ( 𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑥 ) )
17 12 13 16 3bitri ⊢ ( ( ( 𝑦 ≠ 𝑥 ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑧 ≠ 𝑥 ) ↔ ( ( 𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑥 ) )
18 17 anbi1i ⊢ ( ( ( ( 𝑦 ≠ 𝑥 ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑧 ≠ 𝑥 ) ∧ ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑧 ∧ ( 𝑃 ‘ 2 ) = 𝑦 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑧 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑧 , 𝑦 } ) ) ) ↔ ( ( ( 𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑥 ) ∧ ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑧 ∧ ( 𝑃 ‘ 2 ) = 𝑦 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑧 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑧 , 𝑦 } ) ) ) )
19 df-3an ⊢ ( ( 𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ ( 𝑦 ≠ 𝑥 ∧ ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑧 ∧ ( 𝑃 ‘ 2 ) = 𝑦 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑧 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑧 , 𝑦 } ) ) ) ) ↔ ( ( 𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ) ∧ ( 𝑦 ≠ 𝑥 ∧ ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑧 ∧ ( 𝑃 ‘ 2 ) = 𝑦 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑧 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑧 , 𝑦 } ) ) ) ) )
20 11 18 19 3bitr4i ⊢ ( ( ( ( 𝑦 ≠ 𝑥 ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑧 ≠ 𝑥 ) ∧ ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑧 ∧ ( 𝑃 ‘ 2 ) = 𝑦 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑧 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑧 , 𝑦 } ) ) ) ↔ ( 𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ ( 𝑦 ≠ 𝑥 ∧ ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑧 ∧ ( 𝑃 ‘ 2 ) = 𝑦 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑧 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑧 , 𝑦 } ) ) ) ) )
21 9 10 20 3bitr2i ⊢ ( ( 𝑦 ≠ 𝑥 ∧ 𝑦 ≠ 𝑧 ∧ ( 𝑧 ≠ 𝑥 ∧ ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑧 ∧ ( 𝑃 ‘ 2 ) = 𝑦 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑧 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑧 , 𝑦 } ) ) ) ) ↔ ( 𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ ( 𝑦 ≠ 𝑥 ∧ ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑧 ∧ ( 𝑃 ‘ 2 ) = 𝑦 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑧 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑧 , 𝑦 } ) ) ) ) )
22 21 rexbii ⊢ ( ∃ 𝑧 ∈ 𝑉 ( 𝑦 ≠ 𝑥 ∧ 𝑦 ≠ 𝑧 ∧ ( 𝑧 ≠ 𝑥 ∧ ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑧 ∧ ( 𝑃 ‘ 2 ) = 𝑦 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑧 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑧 , 𝑦 } ) ) ) ) ↔ ∃ 𝑧 ∈ 𝑉 ( 𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ ( 𝑦 ≠ 𝑥 ∧ ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑧 ∧ ( 𝑃 ‘ 2 ) = 𝑦 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑧 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑧 , 𝑦 } ) ) ) ) )
23 rexdifpr ⊢ ( ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( 𝑦 ≠ 𝑥 ∧ ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑧 ∧ ( 𝑃 ‘ 2 ) = 𝑦 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑧 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑧 , 𝑦 } ) ) ) ↔ ∃ 𝑧 ∈ 𝑉 ( 𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ ( 𝑦 ≠ 𝑥 ∧ ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑧 ∧ ( 𝑃 ‘ 2 ) = 𝑦 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑧 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑧 , 𝑦 } ) ) ) ) )
24 r19.42v ⊢ ( ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( 𝑦 ≠ 𝑥 ∧ ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑧 ∧ ( 𝑃 ‘ 2 ) = 𝑦 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑧 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑧 , 𝑦 } ) ) ) ↔ ( 𝑦 ≠ 𝑥 ∧ ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑧 ∧ ( 𝑃 ‘ 2 ) = 𝑦 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑧 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑧 , 𝑦 } ) ) ) )
25 22 23 24 3bitr2i ⊢ ( ∃ 𝑧 ∈ 𝑉 ( 𝑦 ≠ 𝑥 ∧ 𝑦 ≠ 𝑧 ∧ ( 𝑧 ≠ 𝑥 ∧ ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑧 ∧ ( 𝑃 ‘ 2 ) = 𝑦 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑧 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑧 , 𝑦 } ) ) ) ) ↔ ( 𝑦 ≠ 𝑥 ∧ ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑧 ∧ ( 𝑃 ‘ 2 ) = 𝑦 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑧 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑧 , 𝑦 } ) ) ) )
26 25 rexbii ⊢ ( ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ 𝑉 ( 𝑦 ≠ 𝑥 ∧ 𝑦 ≠ 𝑧 ∧ ( 𝑧 ≠ 𝑥 ∧ ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑧 ∧ ( 𝑃 ‘ 2 ) = 𝑦 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑧 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑧 , 𝑦 } ) ) ) ) ↔ ∃ 𝑦 ∈ 𝑉 ( 𝑦 ≠ 𝑥 ∧ ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑧 ∧ ( 𝑃 ‘ 2 ) = 𝑦 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑧 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑧 , 𝑦 } ) ) ) )
27 7 8 26 3bitri ⊢ ( ∃ 𝑧 ∈ 𝑉 ( 𝑧 ≠ 𝑥 ∧ ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 , 𝑧 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑧 ∧ ( 𝑃 ‘ 2 ) = 𝑦 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑧 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑧 , 𝑦 } ) ) ) ↔ ∃ 𝑦 ∈ 𝑉 ( 𝑦 ≠ 𝑥 ∧ ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑧 ∧ ( 𝑃 ‘ 2 ) = 𝑦 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑧 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑧 , 𝑦 } ) ) ) )
28 rexdifsn ⊢ ( ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 } ) ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 , 𝑧 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑧 ∧ ( 𝑃 ‘ 2 ) = 𝑦 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑧 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑧 , 𝑦 } ) ) ↔ ∃ 𝑧 ∈ 𝑉 ( 𝑧 ≠ 𝑥 ∧ ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 , 𝑧 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑧 ∧ ( 𝑃 ‘ 2 ) = 𝑦 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑧 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑧 , 𝑦 } ) ) ) )
29 rexdifsn ⊢ ( ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑧 ∧ ( 𝑃 ‘ 2 ) = 𝑦 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑧 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑧 , 𝑦 } ) ) ↔ ∃ 𝑦 ∈ 𝑉 ( 𝑦 ≠ 𝑥 ∧ ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑧 ∧ ( 𝑃 ‘ 2 ) = 𝑦 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑧 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑧 , 𝑦 } ) ) ) )
30 27 28 29 3bitr4i ⊢ ( ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 } ) ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 , 𝑧 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑧 ∧ ( 𝑃 ‘ 2 ) = 𝑦 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑧 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑧 , 𝑦 } ) ) ↔ ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑧 ∧ ( 𝑃 ‘ 2 ) = 𝑦 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑧 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑧 , 𝑦 } ) ) )
31 30 a1i ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑥 ∈ 𝑉 ) → ( ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 } ) ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 , 𝑧 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑧 ∧ ( 𝑃 ‘ 2 ) = 𝑦 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑧 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑧 , 𝑦 } ) ) ↔ ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑧 ∧ ( 𝑃 ‘ 2 ) = 𝑦 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑧 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑧 , 𝑦 } ) ) ) )
32 31 rexbidva ⊢ ( 𝐺 ∈ USGraph → ( ∃ 𝑥 ∈ 𝑉 ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 } ) ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 , 𝑧 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑧 ∧ ( 𝑃 ‘ 2 ) = 𝑦 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑧 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑧 , 𝑦 } ) ) ↔ ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑧 ∧ ( 𝑃 ‘ 2 ) = 𝑦 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑧 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑧 , 𝑦 } ) ) ) )
33 32 3anbi3d ⊢ ( 𝐺 ∈ USGraph → ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ 𝑃 : ( 0 ... 2 ) –1-1→ 𝑉 ∧ ∃ 𝑥 ∈ 𝑉 ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 } ) ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 , 𝑧 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑧 ∧ ( 𝑃 ‘ 2 ) = 𝑦 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑧 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑧 , 𝑦 } ) ) ) ↔ ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ 𝑃 : ( 0 ... 2 ) –1-1→ 𝑉 ∧ ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑧 ∧ ( 𝑃 ‘ 2 ) = 𝑦 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑧 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑧 , 𝑦 } ) ) ) ) )
34 3 33 bitrd ⊢ ( 𝐺 ∈ USGraph → ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( ♯ ‘ 𝐹 ) = 2 ) ↔ ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ 𝑃 : ( 0 ... 2 ) –1-1→ 𝑉 ∧ ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑧 ∧ ( 𝑃 ‘ 2 ) = 𝑦 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑧 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑧 , 𝑦 } ) ) ) ) )