Metamath Proof Explorer

Theorem usgr2pthlem

Description: Lemma for usgr2pth . (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 usgr2pthlem ( ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐼 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) → ( ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ) → ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) ) )

Proof

Step Hyp Ref Expression
1 usgr2pthlem.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 usgr2pthlem.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
3 0nn0 ⊢ 0 ∈ ℕ0
4 2nn0 ⊢ 2 ∈ ℕ0
5 0le2 ⊢ 0 ≤ 2
6 elfz2nn0 ⊢ ( 0 ∈ ( 0 ... 2 ) ↔ ( 0 ∈ ℕ0 ∧ 2 ∈ ℕ0 ∧ 0 ≤ 2 ) )
7 3 4 5 6 mpbir3an ⊢ 0 ∈ ( 0 ... 2 )
8 ffvelrn ⊢ ( ( 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ∧ 0 ∈ ( 0 ... 2 ) ) → ( 𝑃 ‘ 0 ) ∈ 𝑉 )
9 7 8 mpan2 ⊢ ( 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 → ( 𝑃 ‘ 0 ) ∈ 𝑉 )
10 9 adantl ⊢ ( ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) ∧ 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ) → ( 𝑃 ‘ 0 ) ∈ 𝑉 )
11 1nn0 ⊢ 1 ∈ ℕ0
12 1le2 ⊢ 1 ≤ 2
13 elfz2nn0 ⊢ ( 1 ∈ ( 0 ... 2 ) ↔ ( 1 ∈ ℕ0 ∧ 2 ∈ ℕ0 ∧ 1 ≤ 2 ) )
14 11 4 12 13 mpbir3an ⊢ 1 ∈ ( 0 ... 2 )
15 ffvelrn ⊢ ( ( 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ∧ 1 ∈ ( 0 ... 2 ) ) → ( 𝑃 ‘ 1 ) ∈ 𝑉 )
16 14 15 mpan2 ⊢ ( 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 → ( 𝑃 ‘ 1 ) ∈ 𝑉 )
17 16 adantl ⊢ ( ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) ∧ 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ) → ( 𝑃 ‘ 1 ) ∈ 𝑉 )
18 simpr ⊢ ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) → 𝐺 ∈ USGraph )
19 fvex ⊢ ( 𝑃 ‘ 1 ) ∈ V
20 18 19 jctir ⊢ ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) → ( 𝐺 ∈ USGraph ∧ ( 𝑃 ‘ 1 ) ∈ V ) )
21 prcom ⊢ { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 0 ) }
22 21 eqeq2i ⊢ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ↔ ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 0 ) } )
23 22 biimpi ⊢ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } → ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 0 ) } )
24 23 adantr ⊢ ( ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) → ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 0 ) } )
25 24 ad2antlr ⊢ ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) → ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 0 ) } )
26 2 usgrnloopv ⊢ ( ( 𝐺 ∈ USGraph ∧ ( 𝑃 ‘ 1 ) ∈ V ) → ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 0 ) } → ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ 0 ) ) )
27 20 25 26 sylc ⊢ ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) → ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ 0 ) )
28 27 adantr ⊢ ( ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) ∧ 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ) → ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ 0 ) )
29 19 elsn ⊢ ( ( 𝑃 ‘ 1 ) ∈ { ( 𝑃 ‘ 0 ) } ↔ ( 𝑃 ‘ 1 ) = ( 𝑃 ‘ 0 ) )
30 29 necon3bbii ⊢ ( ¬ ( 𝑃 ‘ 1 ) ∈ { ( 𝑃 ‘ 0 ) } ↔ ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ 0 ) )
31 28 30 sylibr ⊢ ( ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) ∧ 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ) → ¬ ( 𝑃 ‘ 1 ) ∈ { ( 𝑃 ‘ 0 ) } )
32 17 31 eldifd ⊢ ( ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) ∧ 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ) → ( 𝑃 ‘ 1 ) ∈ ( 𝑉 ∖ { ( 𝑃 ‘ 0 ) } ) )
33 32 adantr ⊢ ( ( ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) ∧ 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ) ∧ 𝑥 = ( 𝑃 ‘ 0 ) ) → ( 𝑃 ‘ 1 ) ∈ ( 𝑉 ∖ { ( 𝑃 ‘ 0 ) } ) )
34 sneq ⊢ ( 𝑥 = ( 𝑃 ‘ 0 ) → { 𝑥 } = { ( 𝑃 ‘ 0 ) } )
35 34 difeq2d ⊢ ( 𝑥 = ( 𝑃 ‘ 0 ) → ( 𝑉 ∖ { 𝑥 } ) = ( 𝑉 ∖ { ( 𝑃 ‘ 0 ) } ) )
36 35 eleq2d ⊢ ( 𝑥 = ( 𝑃 ‘ 0 ) → ( ( 𝑃 ‘ 1 ) ∈ ( 𝑉 ∖ { 𝑥 } ) ↔ ( 𝑃 ‘ 1 ) ∈ ( 𝑉 ∖ { ( 𝑃 ‘ 0 ) } ) ) )
37 36 adantl ⊢ ( ( ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) ∧ 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ) ∧ 𝑥 = ( 𝑃 ‘ 0 ) ) → ( ( 𝑃 ‘ 1 ) ∈ ( 𝑉 ∖ { 𝑥 } ) ↔ ( 𝑃 ‘ 1 ) ∈ ( 𝑉 ∖ { ( 𝑃 ‘ 0 ) } ) ) )
38 33 37 mpbird ⊢ ( ( ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) ∧ 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ) ∧ 𝑥 = ( 𝑃 ‘ 0 ) ) → ( 𝑃 ‘ 1 ) ∈ ( 𝑉 ∖ { 𝑥 } ) )
39 2re ⊢ 2 ∈ ℝ
40 39 leidi ⊢ 2 ≤ 2
41 elfz2nn0 ⊢ ( 2 ∈ ( 0 ... 2 ) ↔ ( 2 ∈ ℕ0 ∧ 2 ∈ ℕ0 ∧ 2 ≤ 2 ) )
42 4 4 40 41 mpbir3an ⊢ 2 ∈ ( 0 ... 2 )
43 ffvelrn ⊢ ( ( 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ∧ 2 ∈ ( 0 ... 2 ) ) → ( 𝑃 ‘ 2 ) ∈ 𝑉 )
44 42 43 mpan2 ⊢ ( 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 → ( 𝑃 ‘ 2 ) ∈ 𝑉 )
45 44 adantl ⊢ ( ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) ∧ 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ) → ( 𝑃 ‘ 2 ) ∈ 𝑉 )
46 2 usgrf1 ⊢ ( 𝐺 ∈ USGraph → 𝐼 : dom 𝐼 –1-1→ ran 𝐼 )
47 46 ad2antlr ⊢ ( ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) ∧ 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ) → 𝐼 : dom 𝐼 –1-1→ ran 𝐼 )
48 simpl ⊢ ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) → 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 )
49 48 ad2antrr ⊢ ( ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) ∧ 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ) → 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 )
50 47 49 jca ⊢ ( ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) ∧ 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ) → ( 𝐼 : dom 𝐼 –1-1→ ran 𝐼 ∧ 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ) )
51 2nn ⊢ 2 ∈ ℕ
52 lbfzo0 ⊢ ( 0 ∈ ( 0 ..^ 2 ) ↔ 2 ∈ ℕ )
53 51 52 mpbir ⊢ 0 ∈ ( 0 ..^ 2 )
54 1lt2 ⊢ 1 < 2
55 elfzo0 ⊢ ( 1 ∈ ( 0 ..^ 2 ) ↔ ( 1 ∈ ℕ0 ∧ 2 ∈ ℕ ∧ 1 < 2 ) )
56 11 51 54 55 mpbir3an ⊢ 1 ∈ ( 0 ..^ 2 )
57 53 56 pm3.2i ⊢ ( 0 ∈ ( 0 ..^ 2 ) ∧ 1 ∈ ( 0 ..^ 2 ) )
58 57 a1i ⊢ ( ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) ∧ 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ) → ( 0 ∈ ( 0 ..^ 2 ) ∧ 1 ∈ ( 0 ..^ 2 ) ) )
59 0ne1 ⊢ 0 ≠ 1
60 59 a1i ⊢ ( ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) ∧ 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ) → 0 ≠ 1 )
61 50 58 60 3jca ⊢ ( ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) ∧ 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ) → ( ( 𝐼 : dom 𝐼 –1-1→ ran 𝐼 ∧ 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ) ∧ ( 0 ∈ ( 0 ..^ 2 ) ∧ 1 ∈ ( 0 ..^ 2 ) ) ∧ 0 ≠ 1 ) )
62 simpr ⊢ ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) → ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) )
63 62 ad2antrr ⊢ ( ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) ∧ 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ) → ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) )
64 2f1fvneq ⊢ ( ( ( 𝐼 : dom 𝐼 –1-1→ ran 𝐼 ∧ 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ) ∧ ( 0 ∈ ( 0 ..^ 2 ) ∧ 1 ∈ ( 0 ..^ 2 ) ) ∧ 0 ≠ 1 ) → ( ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) → { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ≠ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) )
65 61 63 64 sylc ⊢ ( ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) ∧ 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ) → { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ≠ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } )
66 necom ⊢ ( ( 𝑃 ‘ 2 ) ≠ ( 𝑃 ‘ 0 ) ↔ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) )
67 fvex ⊢ ( 𝑃 ‘ 0 ) ∈ V
68 fvex ⊢ ( 𝑃 ‘ 2 ) ∈ V
69 67 19 68 3pm3.2i ⊢ ( ( 𝑃 ‘ 0 ) ∈ V ∧ ( 𝑃 ‘ 1 ) ∈ V ∧ ( 𝑃 ‘ 2 ) ∈ V )
70 fvexd ⊢ ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) → ( 𝑃 ‘ 0 ) ∈ V )
71 simpl ⊢ ( ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) → ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } )
72 71 ad2antlr ⊢ ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) → ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } )
73 18 70 72 jca31 ⊢ ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) → ( ( 𝐺 ∈ USGraph ∧ ( 𝑃 ‘ 0 ) ∈ V ) ∧ ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ) )
74 73 adantr ⊢ ( ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) ∧ 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ) → ( ( 𝐺 ∈ USGraph ∧ ( 𝑃 ‘ 0 ) ∈ V ) ∧ ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ) )
75 2 usgrnloopv ⊢ ( ( 𝐺 ∈ USGraph ∧ ( 𝑃 ‘ 0 ) ∈ V ) → ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ) )
76 75 imp ⊢ ( ( ( 𝐺 ∈ USGraph ∧ ( 𝑃 ‘ 0 ) ∈ V ) ∧ ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ) → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) )
77 74 76 syl ⊢ ( ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) ∧ 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ) → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) )
78 pr1nebg ⊢ ( ( ( ( 𝑃 ‘ 0 ) ∈ V ∧ ( 𝑃 ‘ 1 ) ∈ V ∧ ( 𝑃 ‘ 2 ) ∈ V ) ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ) → ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ↔ { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ≠ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) )
79 69 77 78 sylancr ⊢ ( ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) ∧ 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ) → ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ↔ { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ≠ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) )
80 66 79 syl5bb ⊢ ( ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) ∧ 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ) → ( ( 𝑃 ‘ 2 ) ≠ ( 𝑃 ‘ 0 ) ↔ { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ≠ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) )
81 65 80 mpbird ⊢ ( ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) ∧ 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ) → ( 𝑃 ‘ 2 ) ≠ ( 𝑃 ‘ 0 ) )
82 fvexd ⊢ ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) → ( 𝑃 ‘ 2 ) ∈ V )
83 prcom ⊢ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } = { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 1 ) }
84 83 eqeq2i ⊢ ( ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ↔ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 1 ) } )
85 84 biimpi ⊢ ( ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } → ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 1 ) } )
86 85 adantl ⊢ ( ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) → ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 1 ) } )
87 86 ad2antlr ⊢ ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) → ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 1 ) } )
88 18 82 87 jca31 ⊢ ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) → ( ( 𝐺 ∈ USGraph ∧ ( 𝑃 ‘ 2 ) ∈ V ) ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 1 ) } ) )
89 88 adantr ⊢ ( ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) ∧ 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ) → ( ( 𝐺 ∈ USGraph ∧ ( 𝑃 ‘ 2 ) ∈ V ) ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 1 ) } ) )
90 2 usgrnloopv ⊢ ( ( 𝐺 ∈ USGraph ∧ ( 𝑃 ‘ 2 ) ∈ V ) → ( ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 1 ) } → ( 𝑃 ‘ 2 ) ≠ ( 𝑃 ‘ 1 ) ) )
91 90 imp ⊢ ( ( ( 𝐺 ∈ USGraph ∧ ( 𝑃 ‘ 2 ) ∈ V ) ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 1 ) } ) → ( 𝑃 ‘ 2 ) ≠ ( 𝑃 ‘ 1 ) )
92 89 91 syl ⊢ ( ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) ∧ 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ) → ( 𝑃 ‘ 2 ) ≠ ( 𝑃 ‘ 1 ) )
93 81 92 nelprd ⊢ ( ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) ∧ 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ) → ¬ ( 𝑃 ‘ 2 ) ∈ { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } )
94 45 93 eldifd ⊢ ( ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) ∧ 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ) → ( 𝑃 ‘ 2 ) ∈ ( 𝑉 ∖ { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ) )
95 94 ad2antrr ⊢ ( ( ( ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) ∧ 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ) ∧ 𝑥 = ( 𝑃 ‘ 0 ) ) ∧ 𝑦 = ( 𝑃 ‘ 1 ) ) → ( 𝑃 ‘ 2 ) ∈ ( 𝑉 ∖ { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ) )
96 preq12 ⊢ ( ( 𝑥 = ( 𝑃 ‘ 0 ) ∧ 𝑦 = ( 𝑃 ‘ 1 ) ) → { 𝑥 , 𝑦 } = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } )
97 96 difeq2d ⊢ ( ( 𝑥 = ( 𝑃 ‘ 0 ) ∧ 𝑦 = ( 𝑃 ‘ 1 ) ) → ( 𝑉 ∖ { 𝑥 , 𝑦 } ) = ( 𝑉 ∖ { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ) )
98 97 eleq2d ⊢ ( ( 𝑥 = ( 𝑃 ‘ 0 ) ∧ 𝑦 = ( 𝑃 ‘ 1 ) ) → ( ( 𝑃 ‘ 2 ) ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ↔ ( 𝑃 ‘ 2 ) ∈ ( 𝑉 ∖ { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ) ) )
99 98 adantll ⊢ ( ( ( ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) ∧ 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ) ∧ 𝑥 = ( 𝑃 ‘ 0 ) ) ∧ 𝑦 = ( 𝑃 ‘ 1 ) ) → ( ( 𝑃 ‘ 2 ) ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ↔ ( 𝑃 ‘ 2 ) ∈ ( 𝑉 ∖ { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ) ) )
100 95 99 mpbird ⊢ ( ( ( ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) ∧ 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ) ∧ 𝑥 = ( 𝑃 ‘ 0 ) ) ∧ 𝑦 = ( 𝑃 ‘ 1 ) ) → ( 𝑃 ‘ 2 ) ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) )
101 eqcom ⊢ ( 𝑥 = ( 𝑃 ‘ 0 ) ↔ ( 𝑃 ‘ 0 ) = 𝑥 )
102 eqcom ⊢ ( 𝑦 = ( 𝑃 ‘ 1 ) ↔ ( 𝑃 ‘ 1 ) = 𝑦 )
103 eqcom ⊢ ( 𝑧 = ( 𝑃 ‘ 2 ) ↔ ( 𝑃 ‘ 2 ) = 𝑧 )
104 101 102 103 3anbi123i ⊢ ( ( 𝑥 = ( 𝑃 ‘ 0 ) ∧ 𝑦 = ( 𝑃 ‘ 1 ) ∧ 𝑧 = ( 𝑃 ‘ 2 ) ) ↔ ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) )
105 104 biimpi ⊢ ( ( 𝑥 = ( 𝑃 ‘ 0 ) ∧ 𝑦 = ( 𝑃 ‘ 1 ) ∧ 𝑧 = ( 𝑃 ‘ 2 ) ) → ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) )
106 105 ad4ant123 ⊢ ( ( ( ( 𝑥 = ( 𝑃 ‘ 0 ) ∧ 𝑦 = ( 𝑃 ‘ 1 ) ) ∧ 𝑧 = ( 𝑃 ‘ 2 ) ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) → ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) )
107 101 biimpi ⊢ ( 𝑥 = ( 𝑃 ‘ 0 ) → ( 𝑃 ‘ 0 ) = 𝑥 )
108 107 ad2antrr ⊢ ( ( ( 𝑥 = ( 𝑃 ‘ 0 ) ∧ 𝑦 = ( 𝑃 ‘ 1 ) ) ∧ 𝑧 = ( 𝑃 ‘ 2 ) ) → ( 𝑃 ‘ 0 ) = 𝑥 )
109 102 biimpi ⊢ ( 𝑦 = ( 𝑃 ‘ 1 ) → ( 𝑃 ‘ 1 ) = 𝑦 )
110 109 ad2antlr ⊢ ( ( ( 𝑥 = ( 𝑃 ‘ 0 ) ∧ 𝑦 = ( 𝑃 ‘ 1 ) ) ∧ 𝑧 = ( 𝑃 ‘ 2 ) ) → ( 𝑃 ‘ 1 ) = 𝑦 )
111 108 110 preq12d ⊢ ( ( ( 𝑥 = ( 𝑃 ‘ 0 ) ∧ 𝑦 = ( 𝑃 ‘ 1 ) ) ∧ 𝑧 = ( 𝑃 ‘ 2 ) ) → { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } = { 𝑥 , 𝑦 } )
112 111 eqeq2d ⊢ ( ( ( 𝑥 = ( 𝑃 ‘ 0 ) ∧ 𝑦 = ( 𝑃 ‘ 1 ) ) ∧ 𝑧 = ( 𝑃 ‘ 2 ) ) → ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ↔ ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ) )
113 103 biimpi ⊢ ( 𝑧 = ( 𝑃 ‘ 2 ) → ( 𝑃 ‘ 2 ) = 𝑧 )
114 113 adantl ⊢ ( ( ( 𝑥 = ( 𝑃 ‘ 0 ) ∧ 𝑦 = ( 𝑃 ‘ 1 ) ) ∧ 𝑧 = ( 𝑃 ‘ 2 ) ) → ( 𝑃 ‘ 2 ) = 𝑧 )
115 110 114 preq12d ⊢ ( ( ( 𝑥 = ( 𝑃 ‘ 0 ) ∧ 𝑦 = ( 𝑃 ‘ 1 ) ) ∧ 𝑧 = ( 𝑃 ‘ 2 ) ) → { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } = { 𝑦 , 𝑧 } )
116 115 eqeq2d ⊢ ( ( ( 𝑥 = ( 𝑃 ‘ 0 ) ∧ 𝑦 = ( 𝑃 ‘ 1 ) ) ∧ 𝑧 = ( 𝑃 ‘ 2 ) ) → ( ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ↔ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) )
117 112 116 anbi12d ⊢ ( ( ( 𝑥 = ( 𝑃 ‘ 0 ) ∧ 𝑦 = ( 𝑃 ‘ 1 ) ) ∧ 𝑧 = ( 𝑃 ‘ 2 ) ) → ( ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ↔ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) )
118 117 biimpa ⊢ ( ( ( ( 𝑥 = ( 𝑃 ‘ 0 ) ∧ 𝑦 = ( 𝑃 ‘ 1 ) ) ∧ 𝑧 = ( 𝑃 ‘ 2 ) ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) → ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) )
119 106 118 jca ⊢ ( ( ( ( 𝑥 = ( 𝑃 ‘ 0 ) ∧ 𝑦 = ( 𝑃 ‘ 1 ) ) ∧ 𝑧 = ( 𝑃 ‘ 2 ) ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) → ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) )
120 119 exp41 ⊢ ( 𝑥 = ( 𝑃 ‘ 0 ) → ( 𝑦 = ( 𝑃 ‘ 1 ) → ( 𝑧 = ( 𝑃 ‘ 2 ) → ( ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) → ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) ) ) ) )
121 120 adantl ⊢ ( ( ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) ∧ 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ) ∧ 𝑥 = ( 𝑃 ‘ 0 ) ) → ( 𝑦 = ( 𝑃 ‘ 1 ) → ( 𝑧 = ( 𝑃 ‘ 2 ) → ( ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) → ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) ) ) ) )
122 121 imp31 ⊢ ( ( ( ( ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) ∧ 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ) ∧ 𝑥 = ( 𝑃 ‘ 0 ) ) ∧ 𝑦 = ( 𝑃 ‘ 1 ) ) ∧ 𝑧 = ( 𝑃 ‘ 2 ) ) → ( ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) → ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) ) )
123 100 122 rspcimedv ⊢ ( ( ( ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) ∧ 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ) ∧ 𝑥 = ( 𝑃 ‘ 0 ) ) ∧ 𝑦 = ( 𝑃 ‘ 1 ) ) → ( ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) → ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) ) )
124 38 123 rspcimedv ⊢ ( ( ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) ∧ 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ) ∧ 𝑥 = ( 𝑃 ‘ 0 ) ) → ( ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) → ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) ) )
125 10 124 rspcimedv ⊢ ( ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) ∧ 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ) → ( ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) → ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) ) )
126 125 exp41 ⊢ ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 → ( ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) → ( 𝐺 ∈ USGraph → ( 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 → ( ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) → ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) ) ) ) ) )
127 126 com15 ⊢ ( ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) → ( ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) → ( 𝐺 ∈ USGraph → ( 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 → ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 → ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) ) ) ) ) )
128 127 pm2.43i ⊢ ( ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) → ( 𝐺 ∈ USGraph → ( 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 → ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 → ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) ) ) ) )
129 128 com12 ⊢ ( 𝐺 ∈ USGraph → ( ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) → ( 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 → ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 → ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) ) ) ) )
130 129 adantr ⊢ ( ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ) → ( ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) → ( 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 → ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 → ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) ) ) ) )
131 oveq2 ⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = ( 0 ..^ 2 ) )
132 131 raleqdv ⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ↔ ∀ 𝑖 ∈ ( 0 ..^ 2 ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) )
133 fzo0to2pr ⊢ ( 0 ..^ 2 ) = { 0 , 1 }
134 133 raleqi ⊢ ( ∀ 𝑖 ∈ ( 0 ..^ 2 ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ↔ ∀ 𝑖 ∈ { 0 , 1 } ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } )
135 2wlklem ⊢ ( ∀ 𝑖 ∈ { 0 , 1 } ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ↔ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) )
136 134 135 bitri ⊢ ( ∀ 𝑖 ∈ ( 0 ..^ 2 ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ↔ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) )
137 132 136 bitrdi ⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ↔ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) )
138 137 adantl ⊢ ( ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ↔ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) )
139 oveq2 ⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( 0 ... ( ♯ ‘ 𝐹 ) ) = ( 0 ... 2 ) )
140 139 feq2d ⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ↔ 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ) )
141 140 adantl ⊢ ( ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ) → ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ↔ 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ) )
142 f1eq2 ⊢ ( ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = ( 0 ..^ 2 ) → ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐼 ↔ 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ) )
143 131 142 syl ⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐼 ↔ 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ) )
144 143 imbi1d ⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐼 → ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) ) ↔ ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 → ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) ) ) )
145 144 adantl ⊢ ( ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ) → ( ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐼 → ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) ) ↔ ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 → ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) ) ) )
146 141 145 imbi12d ⊢ ( ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ) → ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 → ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐼 → ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) ) ) ↔ ( 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 → ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 → ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) ) ) ) )
147 130 138 146 3imtr4d ⊢ ( ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } → ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 → ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐼 → ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) ) ) ) )
148 147 com14 ⊢ ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐼 → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } → ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 → ( ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ) → ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) ) ) ) )
149 148 com23 ⊢ ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐼 → ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } → ( ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ) → ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) ) ) ) )
150 149 3imp ⊢ ( ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐼 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) → ( ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ) → ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) ) )