Metamath Proof Explorer

Theorem usgr2pth

Description: In a simple 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) (Proof shortened by AV, 31-Oct-2021)

Ref Expression
Hypotheses usgr2pthlem.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
usgr2pthlem.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
Assertion usgr2pth ( 𝐺 ∈ 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 usgr2pthspth ⊢ ( ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ) → ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ↔ 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ) )
4 usgrupgr ⊢ ( 𝐺 ∈ USGraph → 𝐺 ∈ UPGraph )
5 4 adantr ⊢ ( ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ) → 𝐺 ∈ UPGraph )
6 isspth ⊢ ( 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ↔ ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ∧ Fun ◡ 𝑃 ) )
7 6 a1i ⊢ ( 𝐺 ∈ UPGraph → ( 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ↔ ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ∧ Fun ◡ 𝑃 ) ) )
8 1 2 upgrf1istrl ⊢ ( 𝐺 ∈ UPGraph → ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ↔ ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐼 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ) )
9 8 anbi1d ⊢ ( 𝐺 ∈ UPGraph → ( ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ∧ Fun ◡ 𝑃 ) ↔ ( ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐼 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ∧ Fun ◡ 𝑃 ) ) )
10 oveq2 ⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = ( 0 ..^ 2 ) )
11 f1eq2 ⊢ ( ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = ( 0 ..^ 2 ) → ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐼 ↔ 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ) )
12 10 11 syl ⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐼 ↔ 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ) )
13 12 biimpd ⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐼 → 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ) )
14 13 adantl ⊢ ( ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ) → ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐼 → 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ) )
15 14 com12 ⊢ ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐼 → ( ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ) → 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ) )
16 15 3ad2ant1 ⊢ ( ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐼 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) → ( ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ) → 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ) )
17 16 ad2antrl ⊢ ( ( 𝐺 ∈ UPGraph ∧ ( ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐼 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ∧ Fun ◡ 𝑃 ) ) → ( ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ) → 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ) )
18 oveq2 ⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( 0 ... ( ♯ ‘ 𝐹 ) ) = ( 0 ... 2 ) )
19 18 feq2d ⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ↔ 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ) )
20 df-f1 ⊢ ( 𝑃 : ( 0 ... 2 ) –1-1→ 𝑉 ↔ ( 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ∧ Fun ◡ 𝑃 ) )
21 20 simplbi2 ⊢ ( 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 → ( Fun ◡ 𝑃 → 𝑃 : ( 0 ... 2 ) –1-1→ 𝑉 ) )
22 21 a1i ⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 → ( Fun ◡ 𝑃 → 𝑃 : ( 0 ... 2 ) –1-1→ 𝑉 ) ) )
23 19 22 sylbid ⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 → ( Fun ◡ 𝑃 → 𝑃 : ( 0 ... 2 ) –1-1→ 𝑉 ) ) )
24 23 adantl ⊢ ( ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ) → ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 → ( Fun ◡ 𝑃 → 𝑃 : ( 0 ... 2 ) –1-1→ 𝑉 ) ) )
25 24 com3l ⊢ ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 → ( Fun ◡ 𝑃 → ( ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ) → 𝑃 : ( 0 ... 2 ) –1-1→ 𝑉 ) ) )
26 25 3ad2ant2 ⊢ ( ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐼 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) → ( Fun ◡ 𝑃 → ( ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ) → 𝑃 : ( 0 ... 2 ) –1-1→ 𝑉 ) ) )
27 26 imp ⊢ ( ( ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐼 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ∧ Fun ◡ 𝑃 ) → ( ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ) → 𝑃 : ( 0 ... 2 ) –1-1→ 𝑉 ) )
28 27 adantl ⊢ ( ( 𝐺 ∈ UPGraph ∧ ( ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐼 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ∧ Fun ◡ 𝑃 ) ) → ( ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ) → 𝑃 : ( 0 ... 2 ) –1-1→ 𝑉 ) )
29 1 2 usgr2pthlem ⊢ ( ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐼 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) → ( ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ) → ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) ) )
30 29 ad2antrl ⊢ ( ( 𝐺 ∈ UPGraph ∧ ( ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐼 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ∧ Fun ◡ 𝑃 ) ) → ( ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ) → ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) ) )
31 17 28 30 3jcad ⊢ ( ( 𝐺 ∈ UPGraph ∧ ( ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐼 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ∧ Fun ◡ 𝑃 ) ) → ( ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ) → ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ 𝑃 : ( 0 ... 2 ) –1-1→ 𝑉 ∧ ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) ) ) )
32 31 ex ⊢ ( 𝐺 ∈ UPGraph → ( ( ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐼 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ∧ Fun ◡ 𝑃 ) → ( ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ) → ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ 𝑃 : ( 0 ... 2 ) –1-1→ 𝑉 ∧ ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) ) ) ) )
33 9 32 sylbid ⊢ ( 𝐺 ∈ UPGraph → ( ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ∧ Fun ◡ 𝑃 ) → ( ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ) → ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ 𝑃 : ( 0 ... 2 ) –1-1→ 𝑉 ∧ ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) ) ) ) )
34 7 33 sylbid ⊢ ( 𝐺 ∈ UPGraph → ( 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 → ( ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ) → ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ 𝑃 : ( 0 ... 2 ) –1-1→ 𝑉 ∧ ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) ) ) ) )
35 34 com23 ⊢ ( 𝐺 ∈ UPGraph → ( ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ) → ( 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 → ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ 𝑃 : ( 0 ... 2 ) –1-1→ 𝑉 ∧ ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) ) ) ) )
36 5 35 mpcom ⊢ ( ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ) → ( 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 → ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ 𝑃 : ( 0 ... 2 ) –1-1→ 𝑉 ∧ ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) ) ) )
37 3 36 sylbid ⊢ ( ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ) → ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 → ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ 𝑃 : ( 0 ... 2 ) –1-1→ 𝑉 ∧ ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) ) ) )
38 37 ex ⊢ ( 𝐺 ∈ USGraph → ( ( ♯ ‘ 𝐹 ) = 2 → ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 → ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ 𝑃 : ( 0 ... 2 ) –1-1→ 𝑉 ∧ ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) ) ) ) )
39 38 impcomd ⊢ ( 𝐺 ∈ USGraph → ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( ♯ ‘ 𝐹 ) = 2 ) → ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ 𝑃 : ( 0 ... 2 ) –1-1→ 𝑉 ∧ ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) ) ) )
40 2nn0 ⊢ 2 ∈ ℕ0
41 f1f ⊢ ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 → 𝐹 : ( 0 ..^ 2 ) ⟶ dom 𝐼 )
42 fnfzo0hash ⊢ ( ( 2 ∈ ℕ0 ∧ 𝐹 : ( 0 ..^ 2 ) ⟶ dom 𝐼 ) → ( ♯ ‘ 𝐹 ) = 2 )
43 40 41 42 sylancr ⊢ ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 → ( ♯ ‘ 𝐹 ) = 2 )
44 oveq2 ⊢ ( 2 = ( ♯ ‘ 𝐹 ) → ( 0 ..^ 2 ) = ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
45 44 eqcoms ⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( 0 ..^ 2 ) = ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
46 f1eq2 ⊢ ( ( 0 ..^ 2 ) = ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ↔ 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐼 ) )
47 45 46 syl ⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ↔ 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐼 ) )
48 47 biimpd ⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 → 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐼 ) )
49 48 imp ⊢ ( ( ( ♯ ‘ 𝐹 ) = 2 ∧ 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ) → 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐼 )
50 49 adantr ⊢ ( ( ( ( ♯ ‘ 𝐹 ) = 2 ∧ 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ) ∧ 𝑃 : ( 0 ... 2 ) –1-1→ 𝑉 ) → 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐼 )
51 50 ad2antrr ⊢ ( ( ( ( ( ( ♯ ‘ 𝐹 ) = 2 ∧ 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ) ∧ 𝑃 : ( 0 ... 2 ) –1-1→ 𝑉 ) ∧ ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) ) ∧ 𝐺 ∈ USGraph ) → 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐼 )
52 f1f ⊢ ( 𝑃 : ( 0 ... 2 ) –1-1→ 𝑉 → 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 )
53 oveq2 ⊢ ( 2 = ( ♯ ‘ 𝐹 ) → ( 0 ... 2 ) = ( 0 ... ( ♯ ‘ 𝐹 ) ) )
54 53 eqcoms ⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( 0 ... 2 ) = ( 0 ... ( ♯ ‘ 𝐹 ) ) )
55 54 adantr ⊢ ( ( ( ♯ ‘ 𝐹 ) = 2 ∧ 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ) → ( 0 ... 2 ) = ( 0 ... ( ♯ ‘ 𝐹 ) ) )
56 55 feq2d ⊢ ( ( ( ♯ ‘ 𝐹 ) = 2 ∧ 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ) → ( 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ↔ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ) )
57 52 56 syl5ib ⊢ ( ( ( ♯ ‘ 𝐹 ) = 2 ∧ 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ) → ( 𝑃 : ( 0 ... 2 ) –1-1→ 𝑉 → 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ) )
58 57 imp ⊢ ( ( ( ( ♯ ‘ 𝐹 ) = 2 ∧ 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ) ∧ 𝑃 : ( 0 ... 2 ) –1-1→ 𝑉 ) → 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 )
59 58 ad2antrr ⊢ ( ( ( ( ( ( ♯ ‘ 𝐹 ) = 2 ∧ 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ) ∧ 𝑃 : ( 0 ... 2 ) –1-1→ 𝑉 ) ∧ ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) ) ∧ 𝐺 ∈ USGraph ) → 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 )
60 eqcom ⊢ ( ( 𝑃 ‘ 0 ) = 𝑥 ↔ 𝑥 = ( 𝑃 ‘ 0 ) )
61 60 biimpi ⊢ ( ( 𝑃 ‘ 0 ) = 𝑥 → 𝑥 = ( 𝑃 ‘ 0 ) )
62 61 3ad2ant1 ⊢ ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) → 𝑥 = ( 𝑃 ‘ 0 ) )
63 eqcom ⊢ ( ( 𝑃 ‘ 1 ) = 𝑦 ↔ 𝑦 = ( 𝑃 ‘ 1 ) )
64 63 biimpi ⊢ ( ( 𝑃 ‘ 1 ) = 𝑦 → 𝑦 = ( 𝑃 ‘ 1 ) )
65 64 3ad2ant2 ⊢ ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) → 𝑦 = ( 𝑃 ‘ 1 ) )
66 62 65 preq12d ⊢ ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) → { 𝑥 , 𝑦 } = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } )
67 66 eqeq2d ⊢ ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) → ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ↔ ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ) )
68 67 biimpcd ⊢ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } → ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) → ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ) )
69 68 adantr ⊢ ( ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) → ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) → ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ) )
70 69 impcom ⊢ ( ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) → ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } )
71 eqcom ⊢ ( ( 𝑃 ‘ 2 ) = 𝑧 ↔ 𝑧 = ( 𝑃 ‘ 2 ) )
72 71 biimpi ⊢ ( ( 𝑃 ‘ 2 ) = 𝑧 → 𝑧 = ( 𝑃 ‘ 2 ) )
73 72 3ad2ant3 ⊢ ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) → 𝑧 = ( 𝑃 ‘ 2 ) )
74 65 73 preq12d ⊢ ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) → { 𝑦 , 𝑧 } = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } )
75 74 eqeq2d ⊢ ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) → ( ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ↔ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) )
76 75 biimpcd ⊢ ( ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } → ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) → ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) )
77 76 adantl ⊢ ( ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) → ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) → ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) )
78 77 impcom ⊢ ( ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) → ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } )
79 70 78 jca ⊢ ( ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) → ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) )
80 79 rexlimivw ⊢ ( ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) → ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) )
81 80 rexlimivw ⊢ ( ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) → ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) )
82 81 rexlimivw ⊢ ( ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) → ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) )
83 82 a1i13 ⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) → ( 𝐺 ∈ USGraph → ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ) )
84 fzo0to2pr ⊢ ( 0 ..^ 2 ) = { 0 , 1 }
85 10 84 eqtrdi ⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = { 0 , 1 } )
86 85 raleqdv ⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ↔ ∀ 𝑖 ∈ { 0 , 1 } ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) )
87 2wlklem ⊢ ( ∀ 𝑖 ∈ { 0 , 1 } ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ↔ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) )
88 86 87 bitrdi ⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ↔ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) )
89 88 imbi2d ⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( ( 𝐺 ∈ USGraph → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ↔ ( 𝐺 ∈ USGraph → ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ) )
90 83 89 sylibrd ⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) → ( 𝐺 ∈ USGraph → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ) )
91 90 ad2antrr ⊢ ( ( ( ( ♯ ‘ 𝐹 ) = 2 ∧ 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ) ∧ 𝑃 : ( 0 ... 2 ) –1-1→ 𝑉 ) → ( ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) → ( 𝐺 ∈ USGraph → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ) )
92 91 imp ⊢ ( ( ( ( ( ♯ ‘ 𝐹 ) = 2 ∧ 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ) ∧ 𝑃 : ( 0 ... 2 ) –1-1→ 𝑉 ) ∧ ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) ) → ( 𝐺 ∈ USGraph → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) )
93 92 imp ⊢ ( ( ( ( ( ( ♯ ‘ 𝐹 ) = 2 ∧ 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ) ∧ 𝑃 : ( 0 ... 2 ) –1-1→ 𝑉 ) ∧ ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) ) ∧ 𝐺 ∈ USGraph ) → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } )
94 51 59 93 3jca ⊢ ( ( ( ( ( ( ♯ ‘ 𝐹 ) = 2 ∧ 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ) ∧ 𝑃 : ( 0 ... 2 ) –1-1→ 𝑉 ) ∧ ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) ) ∧ 𝐺 ∈ USGraph ) → ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐼 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) )
95 20 simprbi ⊢ ( 𝑃 : ( 0 ... 2 ) –1-1→ 𝑉 → Fun ◡ 𝑃 )
96 95 adantl ⊢ ( ( ( ( ♯ ‘ 𝐹 ) = 2 ∧ 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ) ∧ 𝑃 : ( 0 ... 2 ) –1-1→ 𝑉 ) → Fun ◡ 𝑃 )
97 96 ad2antrr ⊢ ( ( ( ( ( ( ♯ ‘ 𝐹 ) = 2 ∧ 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ) ∧ 𝑃 : ( 0 ... 2 ) –1-1→ 𝑉 ) ∧ ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) ) ∧ 𝐺 ∈ USGraph ) → Fun ◡ 𝑃 )
98 94 97 jca ⊢ ( ( ( ( ( ( ♯ ‘ 𝐹 ) = 2 ∧ 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ) ∧ 𝑃 : ( 0 ... 2 ) –1-1→ 𝑉 ) ∧ ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) ) ∧ 𝐺 ∈ USGraph ) → ( ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐼 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ∧ Fun ◡ 𝑃 ) )
99 7 9 bitrd ⊢ ( 𝐺 ∈ UPGraph → ( 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ↔ ( ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐼 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ∧ Fun ◡ 𝑃 ) ) )
100 4 99 syl ⊢ ( 𝐺 ∈ USGraph → ( 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ↔ ( ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐼 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ∧ Fun ◡ 𝑃 ) ) )
101 100 adantl ⊢ ( ( ( ( ( ( ♯ ‘ 𝐹 ) = 2 ∧ 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ) ∧ 𝑃 : ( 0 ... 2 ) –1-1→ 𝑉 ) ∧ ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) ) ∧ 𝐺 ∈ USGraph ) → ( 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ↔ ( ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐼 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ∧ Fun ◡ 𝑃 ) ) )
102 98 101 mpbird ⊢ ( ( ( ( ( ( ♯ ‘ 𝐹 ) = 2 ∧ 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ) ∧ 𝑃 : ( 0 ... 2 ) –1-1→ 𝑉 ) ∧ ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) ) ∧ 𝐺 ∈ USGraph ) → 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 )
103 simpr ⊢ ( ( ( ( ( ( ♯ ‘ 𝐹 ) = 2 ∧ 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ) ∧ 𝑃 : ( 0 ... 2 ) –1-1→ 𝑉 ) ∧ ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) ) ∧ 𝐺 ∈ USGraph ) → 𝐺 ∈ USGraph )
104 simp-4l ⊢ ( ( ( ( ( ( ♯ ‘ 𝐹 ) = 2 ∧ 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ) ∧ 𝑃 : ( 0 ... 2 ) –1-1→ 𝑉 ) ∧ ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) ) ∧ 𝐺 ∈ USGraph ) → ( ♯ ‘ 𝐹 ) = 2 )
105 103 104 3 syl2anc ⊢ ( ( ( ( ( ( ♯ ‘ 𝐹 ) = 2 ∧ 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ) ∧ 𝑃 : ( 0 ... 2 ) –1-1→ 𝑉 ) ∧ ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) ) ∧ 𝐺 ∈ USGraph ) → ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ↔ 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ) )
106 102 105 mpbird ⊢ ( ( ( ( ( ( ♯ ‘ 𝐹 ) = 2 ∧ 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ) ∧ 𝑃 : ( 0 ... 2 ) –1-1→ 𝑉 ) ∧ ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) ) ∧ 𝐺 ∈ USGraph ) → 𝐹 ( Paths ‘ 𝐺 ) 𝑃 )
107 106 104 jca ⊢ ( ( ( ( ( ( ♯ ‘ 𝐹 ) = 2 ∧ 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ) ∧ 𝑃 : ( 0 ... 2 ) –1-1→ 𝑉 ) ∧ ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) ) ∧ 𝐺 ∈ USGraph ) → ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( ♯ ‘ 𝐹 ) = 2 ) )
108 107 ex ⊢ ( ( ( ( ( ♯ ‘ 𝐹 ) = 2 ∧ 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ) ∧ 𝑃 : ( 0 ... 2 ) –1-1→ 𝑉 ) ∧ ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) ) → ( 𝐺 ∈ USGraph → ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( ♯ ‘ 𝐹 ) = 2 ) ) )
109 108 exp41 ⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 → ( 𝑃 : ( 0 ... 2 ) –1-1→ 𝑉 → ( ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) → ( 𝐺 ∈ USGraph → ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( ♯ ‘ 𝐹 ) = 2 ) ) ) ) ) )
110 43 109 mpcom ⊢ ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 → ( 𝑃 : ( 0 ... 2 ) –1-1→ 𝑉 → ( ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) → ( 𝐺 ∈ USGraph → ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( ♯ ‘ 𝐹 ) = 2 ) ) ) ) )
111 110 3imp ⊢ ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ 𝑃 : ( 0 ... 2 ) –1-1→ 𝑉 ∧ ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) ) → ( 𝐺 ∈ USGraph → ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( ♯ ‘ 𝐹 ) = 2 ) ) )
112 111 com12 ⊢ ( 𝐺 ∈ USGraph → ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ 𝑃 : ( 0 ... 2 ) –1-1→ 𝑉 ∧ ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) ) → ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( ♯ ‘ 𝐹 ) = 2 ) ) )
113 39 112 impbid ⊢ ( 𝐺 ∈ USGraph → ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( ♯ ‘ 𝐹 ) = 2 ) ↔ ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ 𝑃 : ( 0 ... 2 ) –1-1→ 𝑉 ∧ ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) ) ) )