Metamath Proof Explorer

Theorem isubgr3stgrlem7

Description: Lemma 7 for isubgr3stgr . (Contributed by AV, 29-Sep-2025)

Ref Expression
Hypotheses isubgr3stgr.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
isubgr3stgr.u ⊢ 𝑈 = ( 𝐺 NeighbVtx 𝑋 )
isubgr3stgr.c ⊢ 𝐶 = ( 𝐺 ClNeighbVtx 𝑋 )
isubgr3stgr.n ⊢ 𝑁 ∈ ℕ0
isubgr3stgr.s ⊢ 𝑆 = ( StarGr ‘ 𝑁 )
isubgr3stgr.w ⊢ 𝑊 = ( Vtx ‘ 𝑆 )
isubgr3stgr.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
isubgr3stgr.i ⊢ 𝐼 = ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) )
isubgr3stgr.h ⊢ 𝐻 = ( 𝑖 ∈ 𝐼 ↦ ( 𝐹 “ 𝑖 ) )
Assertion isubgr3stgrlem7 ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ∧ 𝐽 ∈ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) ) → ( ◡ 𝐹 “ 𝐽 ) ∈ 𝐼 )

Proof

Step Hyp Ref Expression
1 isubgr3stgr.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 isubgr3stgr.u ⊢ 𝑈 = ( 𝐺 NeighbVtx 𝑋 )
3 isubgr3stgr.c ⊢ 𝐶 = ( 𝐺 ClNeighbVtx 𝑋 )
4 isubgr3stgr.n ⊢ 𝑁 ∈ ℕ0
5 isubgr3stgr.s ⊢ 𝑆 = ( StarGr ‘ 𝑁 )
6 isubgr3stgr.w ⊢ 𝑊 = ( Vtx ‘ 𝑆 )
7 isubgr3stgr.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
8 isubgr3stgr.i ⊢ 𝐼 = ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) )
9 isubgr3stgr.h ⊢ 𝐻 = ( 𝑖 ∈ 𝐼 ↦ ( 𝐹 “ 𝑖 ) )
10 stgredgel ⊢ ( 𝑁 ∈ ℕ0 → ( 𝐽 ∈ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) ↔ ( 𝐽 ⊆ ( 0 ... 𝑁 ) ∧ ∃ 𝑦 ∈ ( 1 ... 𝑁 ) 𝐽 = { 0 , 𝑦 } ) ) )
11 4 10 mp1i ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) → ( 𝐽 ∈ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) ↔ ( 𝐽 ⊆ ( 0 ... 𝑁 ) ∧ ∃ 𝑦 ∈ ( 1 ... 𝑁 ) 𝐽 = { 0 , 𝑦 } ) ) )
12 c0ex ⊢ 0 ∈ V
13 12 a1i ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) → 0 ∈ V )
14 prssg ⊢ ( ( 0 ∈ V ∧ 𝑦 ∈ ( 1 ... 𝑁 ) ) → ( ( 0 ∈ ( 0 ... 𝑁 ) ∧ 𝑦 ∈ ( 0 ... 𝑁 ) ) ↔ { 0 , 𝑦 } ⊆ ( 0 ... 𝑁 ) ) )
15 13 14 sylan ⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) ∧ 𝑦 ∈ ( 1 ... 𝑁 ) ) → ( ( 0 ∈ ( 0 ... 𝑁 ) ∧ 𝑦 ∈ ( 0 ... 𝑁 ) ) ↔ { 0 , 𝑦 } ⊆ ( 0 ... 𝑁 ) ) )
16 f1ocnv ⊢ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 → ◡ 𝐹 : 𝑊 –1-1-onto→ 𝐶 )
17 f1ofn ⊢ ( ◡ 𝐹 : 𝑊 –1-1-onto→ 𝐶 → ◡ 𝐹 Fn 𝑊 )
18 5 fveq2i ⊢ ( Vtx ‘ 𝑆 ) = ( Vtx ‘ ( StarGr ‘ 𝑁 ) )
19 stgrvtx ⊢ ( 𝑁 ∈ ℕ0 → ( Vtx ‘ ( StarGr ‘ 𝑁 ) ) = ( 0 ... 𝑁 ) )
20 4 19 ax-mp ⊢ ( Vtx ‘ ( StarGr ‘ 𝑁 ) ) = ( 0 ... 𝑁 )
21 6 18 20 3eqtri ⊢ 𝑊 = ( 0 ... 𝑁 )
22 21 fneq2i ⊢ ( ◡ 𝐹 Fn 𝑊 ↔ ◡ 𝐹 Fn ( 0 ... 𝑁 ) )
23 17 22 sylib ⊢ ( ◡ 𝐹 : 𝑊 –1-1-onto→ 𝐶 → ◡ 𝐹 Fn ( 0 ... 𝑁 ) )
24 16 23 syl ⊢ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 → ◡ 𝐹 Fn ( 0 ... 𝑁 ) )
25 24 ad2antrl ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) → ◡ 𝐹 Fn ( 0 ... 𝑁 ) )
26 25 adantr ⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) ∧ 𝑦 ∈ ( 1 ... 𝑁 ) ) → ◡ 𝐹 Fn ( 0 ... 𝑁 ) )
27 26 anim1i ⊢ ( ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) ∧ 𝑦 ∈ ( 1 ... 𝑁 ) ) ∧ ( 0 ∈ ( 0 ... 𝑁 ) ∧ 𝑦 ∈ ( 0 ... 𝑁 ) ) ) → ( ◡ 𝐹 Fn ( 0 ... 𝑁 ) ∧ ( 0 ∈ ( 0 ... 𝑁 ) ∧ 𝑦 ∈ ( 0 ... 𝑁 ) ) ) )
28 3anass ⊢ ( ( ◡ 𝐹 Fn ( 0 ... 𝑁 ) ∧ 0 ∈ ( 0 ... 𝑁 ) ∧ 𝑦 ∈ ( 0 ... 𝑁 ) ) ↔ ( ◡ 𝐹 Fn ( 0 ... 𝑁 ) ∧ ( 0 ∈ ( 0 ... 𝑁 ) ∧ 𝑦 ∈ ( 0 ... 𝑁 ) ) ) )
29 27 28 sylibr ⊢ ( ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) ∧ 𝑦 ∈ ( 1 ... 𝑁 ) ) ∧ ( 0 ∈ ( 0 ... 𝑁 ) ∧ 𝑦 ∈ ( 0 ... 𝑁 ) ) ) → ( ◡ 𝐹 Fn ( 0 ... 𝑁 ) ∧ 0 ∈ ( 0 ... 𝑁 ) ∧ 𝑦 ∈ ( 0 ... 𝑁 ) ) )
30 29 ex ⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) ∧ 𝑦 ∈ ( 1 ... 𝑁 ) ) → ( ( 0 ∈ ( 0 ... 𝑁 ) ∧ 𝑦 ∈ ( 0 ... 𝑁 ) ) → ( ◡ 𝐹 Fn ( 0 ... 𝑁 ) ∧ 0 ∈ ( 0 ... 𝑁 ) ∧ 𝑦 ∈ ( 0 ... 𝑁 ) ) ) )
31 15 30 sylbird ⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) ∧ 𝑦 ∈ ( 1 ... 𝑁 ) ) → ( { 0 , 𝑦 } ⊆ ( 0 ... 𝑁 ) → ( ◡ 𝐹 Fn ( 0 ... 𝑁 ) ∧ 0 ∈ ( 0 ... 𝑁 ) ∧ 𝑦 ∈ ( 0 ... 𝑁 ) ) ) )
32 31 imp ⊢ ( ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) ∧ 𝑦 ∈ ( 1 ... 𝑁 ) ) ∧ { 0 , 𝑦 } ⊆ ( 0 ... 𝑁 ) ) → ( ◡ 𝐹 Fn ( 0 ... 𝑁 ) ∧ 0 ∈ ( 0 ... 𝑁 ) ∧ 𝑦 ∈ ( 0 ... 𝑁 ) ) )
33 fnimapr ⊢ ( ( ◡ 𝐹 Fn ( 0 ... 𝑁 ) ∧ 0 ∈ ( 0 ... 𝑁 ) ∧ 𝑦 ∈ ( 0 ... 𝑁 ) ) → ( ◡ 𝐹 “ { 0 , 𝑦 } ) = { ( ◡ 𝐹 ‘ 0 ) , ( ◡ 𝐹 ‘ 𝑦 ) } )
34 32 33 syl ⊢ ( ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) ∧ 𝑦 ∈ ( 1 ... 𝑁 ) ) ∧ { 0 , 𝑦 } ⊆ ( 0 ... 𝑁 ) ) → ( ◡ 𝐹 “ { 0 , 𝑦 } ) = { ( ◡ 𝐹 ‘ 0 ) , ( ◡ 𝐹 ‘ 𝑦 ) } )
35 1 clnbgrvtxel ⊢ ( 𝑋 ∈ 𝑉 → 𝑋 ∈ ( 𝐺 ClNeighbVtx 𝑋 ) )
36 35 adantl ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) → 𝑋 ∈ ( 𝐺 ClNeighbVtx 𝑋 ) )
37 36 3 eleqtrrdi ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) → 𝑋 ∈ 𝐶 )
38 simpl ⊢ ( ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) → 𝐹 : 𝐶 –1-1-onto→ 𝑊 )
39 37 38 anim12ci ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) → ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ 𝑋 ∈ 𝐶 ) )
40 simprr ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) → ( 𝐹 ‘ 𝑋 ) = 0 )
41 39 40 jca ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) → ( ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ 𝑋 ∈ 𝐶 ) ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) )
42 41 adantr ⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) ∧ 𝑦 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ 𝑋 ∈ 𝐶 ) ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) )
43 f1ocnvfv ⊢ ( ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ 𝑋 ∈ 𝐶 ) → ( ( 𝐹 ‘ 𝑋 ) = 0 → ( ◡ 𝐹 ‘ 0 ) = 𝑋 ) )
44 43 imp ⊢ ( ( ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ 𝑋 ∈ 𝐶 ) ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) → ( ◡ 𝐹 ‘ 0 ) = 𝑋 )
45 42 44 syl ⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) ∧ 𝑦 ∈ ( 1 ... 𝑁 ) ) → ( ◡ 𝐹 ‘ 0 ) = 𝑋 )
46 35 3 eleqtrrdi ⊢ ( 𝑋 ∈ 𝑉 → 𝑋 ∈ 𝐶 )
47 46 ad3antlr ⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) ∧ 𝑦 ∈ ( 1 ... 𝑁 ) ) → 𝑋 ∈ 𝐶 )
48 f1of ⊢ ( ◡ 𝐹 : 𝑊 –1-1-onto→ 𝐶 → ◡ 𝐹 : 𝑊 ⟶ 𝐶 )
49 16 48 syl ⊢ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 → ◡ 𝐹 : 𝑊 ⟶ 𝐶 )
50 49 ad2antrl ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) → ◡ 𝐹 : 𝑊 ⟶ 𝐶 )
51 50 adantr ⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) ∧ 𝑦 ∈ ( 1 ... 𝑁 ) ) → ◡ 𝐹 : 𝑊 ⟶ 𝐶 )
52 fz1ssfz0 ⊢ ( 1 ... 𝑁 ) ⊆ ( 0 ... 𝑁 )
53 52 sseli ⊢ ( 𝑦 ∈ ( 1 ... 𝑁 ) → 𝑦 ∈ ( 0 ... 𝑁 ) )
54 53 21 eleqtrrdi ⊢ ( 𝑦 ∈ ( 1 ... 𝑁 ) → 𝑦 ∈ 𝑊 )
55 54 adantl ⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) ∧ 𝑦 ∈ ( 1 ... 𝑁 ) ) → 𝑦 ∈ 𝑊 )
56 51 55 ffvelcdmd ⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) ∧ 𝑦 ∈ ( 1 ... 𝑁 ) ) → ( ◡ 𝐹 ‘ 𝑦 ) ∈ 𝐶 )
57 47 56 jca ⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) ∧ 𝑦 ∈ ( 1 ... 𝑁 ) ) → ( 𝑋 ∈ 𝐶 ∧ ( ◡ 𝐹 ‘ 𝑦 ) ∈ 𝐶 ) )
58 3 eleq2i ⊢ ( ( ◡ 𝐹 ‘ 𝑦 ) ∈ 𝐶 ↔ ( ◡ 𝐹 ‘ 𝑦 ) ∈ ( 𝐺 ClNeighbVtx 𝑋 ) )
59 usgrupgr ⊢ ( 𝐺 ∈ USGraph → 𝐺 ∈ UPGraph )
60 59 anim1i ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) → ( 𝐺 ∈ UPGraph ∧ 𝑋 ∈ 𝑉 ) )
61 60 ad2antrr ⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) ∧ 𝑦 ∈ ( 1 ... 𝑁 ) ) → ( 𝐺 ∈ UPGraph ∧ 𝑋 ∈ 𝑉 ) )
62 1 clnbgrssvtx ⊢ ( 𝐺 ClNeighbVtx 𝑋 ) ⊆ 𝑉
63 3 62 eqsstri ⊢ 𝐶 ⊆ 𝑉
64 63 56 sselid ⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) ∧ 𝑦 ∈ ( 1 ... 𝑁 ) ) → ( ◡ 𝐹 ‘ 𝑦 ) ∈ 𝑉 )
65 df-3an ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑋 ∈ 𝑉 ∧ ( ◡ 𝐹 ‘ 𝑦 ) ∈ 𝑉 ) ↔ ( ( 𝐺 ∈ UPGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( ◡ 𝐹 ‘ 𝑦 ) ∈ 𝑉 ) )
66 61 64 65 sylanbrc ⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) ∧ 𝑦 ∈ ( 1 ... 𝑁 ) ) → ( 𝐺 ∈ UPGraph ∧ 𝑋 ∈ 𝑉 ∧ ( ◡ 𝐹 ‘ 𝑦 ) ∈ 𝑉 ) )
67 66 ad2antrr ⊢ ( ( ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) ∧ 𝑦 ∈ ( 1 ... 𝑁 ) ) ∧ ( ◡ 𝐹 ‘ 0 ) = 𝑋 ) ∧ 𝑋 ∈ 𝐶 ) → ( 𝐺 ∈ UPGraph ∧ 𝑋 ∈ 𝑉 ∧ ( ◡ 𝐹 ‘ 𝑦 ) ∈ 𝑉 ) )
68 1 7 clnbupgrel ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑋 ∈ 𝑉 ∧ ( ◡ 𝐹 ‘ 𝑦 ) ∈ 𝑉 ) → ( ( ◡ 𝐹 ‘ 𝑦 ) ∈ ( 𝐺 ClNeighbVtx 𝑋 ) ↔ ( ( ◡ 𝐹 ‘ 𝑦 ) = 𝑋 ∨ { ( ◡ 𝐹 ‘ 𝑦 ) , 𝑋 } ∈ 𝐸 ) ) )
69 67 68 syl ⊢ ( ( ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) ∧ 𝑦 ∈ ( 1 ... 𝑁 ) ) ∧ ( ◡ 𝐹 ‘ 0 ) = 𝑋 ) ∧ 𝑋 ∈ 𝐶 ) → ( ( ◡ 𝐹 ‘ 𝑦 ) ∈ ( 𝐺 ClNeighbVtx 𝑋 ) ↔ ( ( ◡ 𝐹 ‘ 𝑦 ) = 𝑋 ∨ { ( ◡ 𝐹 ‘ 𝑦 ) , 𝑋 } ∈ 𝐸 ) ) )
70 58 69 bitrid ⊢ ( ( ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) ∧ 𝑦 ∈ ( 1 ... 𝑁 ) ) ∧ ( ◡ 𝐹 ‘ 0 ) = 𝑋 ) ∧ 𝑋 ∈ 𝐶 ) → ( ( ◡ 𝐹 ‘ 𝑦 ) ∈ 𝐶 ↔ ( ( ◡ 𝐹 ‘ 𝑦 ) = 𝑋 ∨ { ( ◡ 𝐹 ‘ 𝑦 ) , 𝑋 } ∈ 𝐸 ) ) )
71 eqeq2 ⊢ ( ( ◡ 𝐹 ‘ 0 ) = 𝑋 → ( ( ◡ 𝐹 ‘ 𝑦 ) = ( ◡ 𝐹 ‘ 0 ) ↔ ( ◡ 𝐹 ‘ 𝑦 ) = 𝑋 ) )
72 71 adantl ⊢ ( ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) ∧ 𝑦 ∈ ( 1 ... 𝑁 ) ) ∧ ( ◡ 𝐹 ‘ 0 ) = 𝑋 ) → ( ( ◡ 𝐹 ‘ 𝑦 ) = ( ◡ 𝐹 ‘ 0 ) ↔ ( ◡ 𝐹 ‘ 𝑦 ) = 𝑋 ) )
73 f1of1 ⊢ ( ◡ 𝐹 : 𝑊 –1-1-onto→ 𝐶 → ◡ 𝐹 : 𝑊 –1-1→ 𝐶 )
74 16 73 syl ⊢ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 → ◡ 𝐹 : 𝑊 –1-1→ 𝐶 )
75 74 ad2antrl ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) → ◡ 𝐹 : 𝑊 –1-1→ 𝐶 )
76 0elfz ⊢ ( 𝑁 ∈ ℕ0 → 0 ∈ ( 0 ... 𝑁 ) )
77 4 76 ax-mp ⊢ 0 ∈ ( 0 ... 𝑁 )
78 77 21 eleqtrri ⊢ 0 ∈ 𝑊
79 54 78 jctir ⊢ ( 𝑦 ∈ ( 1 ... 𝑁 ) → ( 𝑦 ∈ 𝑊 ∧ 0 ∈ 𝑊 ) )
80 f1veqaeq ⊢ ( ( ◡ 𝐹 : 𝑊 –1-1→ 𝐶 ∧ ( 𝑦 ∈ 𝑊 ∧ 0 ∈ 𝑊 ) ) → ( ( ◡ 𝐹 ‘ 𝑦 ) = ( ◡ 𝐹 ‘ 0 ) → 𝑦 = 0 ) )
81 75 79 80 syl2an ⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) ∧ 𝑦 ∈ ( 1 ... 𝑁 ) ) → ( ( ◡ 𝐹 ‘ 𝑦 ) = ( ◡ 𝐹 ‘ 0 ) → 𝑦 = 0 ) )
82 elfznn ⊢ ( 𝑦 ∈ ( 1 ... 𝑁 ) → 𝑦 ∈ ℕ )
83 nnne0 ⊢ ( 𝑦 ∈ ℕ → 𝑦 ≠ 0 )
84 eqneqall ⊢ ( 𝑦 = 0 → ( 𝑦 ≠ 0 → { 𝑋 , ( ◡ 𝐹 ‘ 𝑦 ) } ∈ 𝐸 ) )
85 83 84 syl5com ⊢ ( 𝑦 ∈ ℕ → ( 𝑦 = 0 → { 𝑋 , ( ◡ 𝐹 ‘ 𝑦 ) } ∈ 𝐸 ) )
86 82 85 syl ⊢ ( 𝑦 ∈ ( 1 ... 𝑁 ) → ( 𝑦 = 0 → { 𝑋 , ( ◡ 𝐹 ‘ 𝑦 ) } ∈ 𝐸 ) )
87 86 adantl ⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) ∧ 𝑦 ∈ ( 1 ... 𝑁 ) ) → ( 𝑦 = 0 → { 𝑋 , ( ◡ 𝐹 ‘ 𝑦 ) } ∈ 𝐸 ) )
88 81 87 syld ⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) ∧ 𝑦 ∈ ( 1 ... 𝑁 ) ) → ( ( ◡ 𝐹 ‘ 𝑦 ) = ( ◡ 𝐹 ‘ 0 ) → { 𝑋 , ( ◡ 𝐹 ‘ 𝑦 ) } ∈ 𝐸 ) )
89 88 adantr ⊢ ( ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) ∧ 𝑦 ∈ ( 1 ... 𝑁 ) ) ∧ ( ◡ 𝐹 ‘ 0 ) = 𝑋 ) → ( ( ◡ 𝐹 ‘ 𝑦 ) = ( ◡ 𝐹 ‘ 0 ) → { 𝑋 , ( ◡ 𝐹 ‘ 𝑦 ) } ∈ 𝐸 ) )
90 72 89 sylbird ⊢ ( ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) ∧ 𝑦 ∈ ( 1 ... 𝑁 ) ) ∧ ( ◡ 𝐹 ‘ 0 ) = 𝑋 ) → ( ( ◡ 𝐹 ‘ 𝑦 ) = 𝑋 → { 𝑋 , ( ◡ 𝐹 ‘ 𝑦 ) } ∈ 𝐸 ) )
91 90 adantr ⊢ ( ( ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) ∧ 𝑦 ∈ ( 1 ... 𝑁 ) ) ∧ ( ◡ 𝐹 ‘ 0 ) = 𝑋 ) ∧ 𝑋 ∈ 𝐶 ) → ( ( ◡ 𝐹 ‘ 𝑦 ) = 𝑋 → { 𝑋 , ( ◡ 𝐹 ‘ 𝑦 ) } ∈ 𝐸 ) )
92 prcom ⊢ { ( ◡ 𝐹 ‘ 𝑦 ) , 𝑋 } = { 𝑋 , ( ◡ 𝐹 ‘ 𝑦 ) }
93 92 eleq1i ⊢ ( { ( ◡ 𝐹 ‘ 𝑦 ) , 𝑋 } ∈ 𝐸 ↔ { 𝑋 , ( ◡ 𝐹 ‘ 𝑦 ) } ∈ 𝐸 )
94 93 biimpi ⊢ ( { ( ◡ 𝐹 ‘ 𝑦 ) , 𝑋 } ∈ 𝐸 → { 𝑋 , ( ◡ 𝐹 ‘ 𝑦 ) } ∈ 𝐸 )
95 94 a1i ⊢ ( ( ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) ∧ 𝑦 ∈ ( 1 ... 𝑁 ) ) ∧ ( ◡ 𝐹 ‘ 0 ) = 𝑋 ) ∧ 𝑋 ∈ 𝐶 ) → ( { ( ◡ 𝐹 ‘ 𝑦 ) , 𝑋 } ∈ 𝐸 → { 𝑋 , ( ◡ 𝐹 ‘ 𝑦 ) } ∈ 𝐸 ) )
96 91 95 jaod ⊢ ( ( ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) ∧ 𝑦 ∈ ( 1 ... 𝑁 ) ) ∧ ( ◡ 𝐹 ‘ 0 ) = 𝑋 ) ∧ 𝑋 ∈ 𝐶 ) → ( ( ( ◡ 𝐹 ‘ 𝑦 ) = 𝑋 ∨ { ( ◡ 𝐹 ‘ 𝑦 ) , 𝑋 } ∈ 𝐸 ) → { 𝑋 , ( ◡ 𝐹 ‘ 𝑦 ) } ∈ 𝐸 ) )
97 70 96 sylbid ⊢ ( ( ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) ∧ 𝑦 ∈ ( 1 ... 𝑁 ) ) ∧ ( ◡ 𝐹 ‘ 0 ) = 𝑋 ) ∧ 𝑋 ∈ 𝐶 ) → ( ( ◡ 𝐹 ‘ 𝑦 ) ∈ 𝐶 → { 𝑋 , ( ◡ 𝐹 ‘ 𝑦 ) } ∈ 𝐸 ) )
98 97 impr ⊢ ( ( ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) ∧ 𝑦 ∈ ( 1 ... 𝑁 ) ) ∧ ( ◡ 𝐹 ‘ 0 ) = 𝑋 ) ∧ ( 𝑋 ∈ 𝐶 ∧ ( ◡ 𝐹 ‘ 𝑦 ) ∈ 𝐶 ) ) → { 𝑋 , ( ◡ 𝐹 ‘ 𝑦 ) } ∈ 𝐸 )
99 prssi ⊢ ( ( 𝑋 ∈ 𝐶 ∧ ( ◡ 𝐹 ‘ 𝑦 ) ∈ 𝐶 ) → { 𝑋 , ( ◡ 𝐹 ‘ 𝑦 ) } ⊆ 𝐶 )
100 99 adantl ⊢ ( ( ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) ∧ 𝑦 ∈ ( 1 ... 𝑁 ) ) ∧ ( ◡ 𝐹 ‘ 0 ) = 𝑋 ) ∧ ( 𝑋 ∈ 𝐶 ∧ ( ◡ 𝐹 ‘ 𝑦 ) ∈ 𝐶 ) ) → { 𝑋 , ( ◡ 𝐹 ‘ 𝑦 ) } ⊆ 𝐶 )
101 98 100 jca ⊢ ( ( ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) ∧ 𝑦 ∈ ( 1 ... 𝑁 ) ) ∧ ( ◡ 𝐹 ‘ 0 ) = 𝑋 ) ∧ ( 𝑋 ∈ 𝐶 ∧ ( ◡ 𝐹 ‘ 𝑦 ) ∈ 𝐶 ) ) → ( { 𝑋 , ( ◡ 𝐹 ‘ 𝑦 ) } ∈ 𝐸 ∧ { 𝑋 , ( ◡ 𝐹 ‘ 𝑦 ) } ⊆ 𝐶 ) )
102 57 101 mpidan ⊢ ( ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) ∧ 𝑦 ∈ ( 1 ... 𝑁 ) ) ∧ ( ◡ 𝐹 ‘ 0 ) = 𝑋 ) → ( { 𝑋 , ( ◡ 𝐹 ‘ 𝑦 ) } ∈ 𝐸 ∧ { 𝑋 , ( ◡ 𝐹 ‘ 𝑦 ) } ⊆ 𝐶 ) )
103 preq1 ⊢ ( ( ◡ 𝐹 ‘ 0 ) = 𝑋 → { ( ◡ 𝐹 ‘ 0 ) , ( ◡ 𝐹 ‘ 𝑦 ) } = { 𝑋 , ( ◡ 𝐹 ‘ 𝑦 ) } )
104 103 eleq1d ⊢ ( ( ◡ 𝐹 ‘ 0 ) = 𝑋 → ( { ( ◡ 𝐹 ‘ 0 ) , ( ◡ 𝐹 ‘ 𝑦 ) } ∈ 𝐸 ↔ { 𝑋 , ( ◡ 𝐹 ‘ 𝑦 ) } ∈ 𝐸 ) )
105 103 sseq1d ⊢ ( ( ◡ 𝐹 ‘ 0 ) = 𝑋 → ( { ( ◡ 𝐹 ‘ 0 ) , ( ◡ 𝐹 ‘ 𝑦 ) } ⊆ 𝐶 ↔ { 𝑋 , ( ◡ 𝐹 ‘ 𝑦 ) } ⊆ 𝐶 ) )
106 104 105 anbi12d ⊢ ( ( ◡ 𝐹 ‘ 0 ) = 𝑋 → ( ( { ( ◡ 𝐹 ‘ 0 ) , ( ◡ 𝐹 ‘ 𝑦 ) } ∈ 𝐸 ∧ { ( ◡ 𝐹 ‘ 0 ) , ( ◡ 𝐹 ‘ 𝑦 ) } ⊆ 𝐶 ) ↔ ( { 𝑋 , ( ◡ 𝐹 ‘ 𝑦 ) } ∈ 𝐸 ∧ { 𝑋 , ( ◡ 𝐹 ‘ 𝑦 ) } ⊆ 𝐶 ) ) )
107 106 adantl ⊢ ( ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) ∧ 𝑦 ∈ ( 1 ... 𝑁 ) ) ∧ ( ◡ 𝐹 ‘ 0 ) = 𝑋 ) → ( ( { ( ◡ 𝐹 ‘ 0 ) , ( ◡ 𝐹 ‘ 𝑦 ) } ∈ 𝐸 ∧ { ( ◡ 𝐹 ‘ 0 ) , ( ◡ 𝐹 ‘ 𝑦 ) } ⊆ 𝐶 ) ↔ ( { 𝑋 , ( ◡ 𝐹 ‘ 𝑦 ) } ∈ 𝐸 ∧ { 𝑋 , ( ◡ 𝐹 ‘ 𝑦 ) } ⊆ 𝐶 ) ) )
108 102 107 mpbird ⊢ ( ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) ∧ 𝑦 ∈ ( 1 ... 𝑁 ) ) ∧ ( ◡ 𝐹 ‘ 0 ) = 𝑋 ) → ( { ( ◡ 𝐹 ‘ 0 ) , ( ◡ 𝐹 ‘ 𝑦 ) } ∈ 𝐸 ∧ { ( ◡ 𝐹 ‘ 0 ) , ( ◡ 𝐹 ‘ 𝑦 ) } ⊆ 𝐶 ) )
109 45 108 mpdan ⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) ∧ 𝑦 ∈ ( 1 ... 𝑁 ) ) → ( { ( ◡ 𝐹 ‘ 0 ) , ( ◡ 𝐹 ‘ 𝑦 ) } ∈ 𝐸 ∧ { ( ◡ 𝐹 ‘ 0 ) , ( ◡ 𝐹 ‘ 𝑦 ) } ⊆ 𝐶 ) )
110 109 adantr ⊢ ( ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) ∧ 𝑦 ∈ ( 1 ... 𝑁 ) ) ∧ { 0 , 𝑦 } ⊆ ( 0 ... 𝑁 ) ) → ( { ( ◡ 𝐹 ‘ 0 ) , ( ◡ 𝐹 ‘ 𝑦 ) } ∈ 𝐸 ∧ { ( ◡ 𝐹 ‘ 0 ) , ( ◡ 𝐹 ‘ 𝑦 ) } ⊆ 𝐶 ) )
111 usgruhgr ⊢ ( 𝐺 ∈ USGraph → 𝐺 ∈ UHGraph )
112 111 ad3antrrr ⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) ∧ 𝑦 ∈ ( 1 ... 𝑁 ) ) → 𝐺 ∈ UHGraph )
113 63 a1i ⊢ ( { 0 , 𝑦 } ⊆ ( 0 ... 𝑁 ) → 𝐶 ⊆ 𝑉 )
114 eqid ⊢ ( 𝐺 ISubGr 𝐶 ) = ( 𝐺 ISubGr 𝐶 )
115 1 7 114 8 isubgredg ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐶 ⊆ 𝑉 ) → ( { ( ◡ 𝐹 ‘ 0 ) , ( ◡ 𝐹 ‘ 𝑦 ) } ∈ 𝐼 ↔ ( { ( ◡ 𝐹 ‘ 0 ) , ( ◡ 𝐹 ‘ 𝑦 ) } ∈ 𝐸 ∧ { ( ◡ 𝐹 ‘ 0 ) , ( ◡ 𝐹 ‘ 𝑦 ) } ⊆ 𝐶 ) ) )
116 112 113 115 syl2an ⊢ ( ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) ∧ 𝑦 ∈ ( 1 ... 𝑁 ) ) ∧ { 0 , 𝑦 } ⊆ ( 0 ... 𝑁 ) ) → ( { ( ◡ 𝐹 ‘ 0 ) , ( ◡ 𝐹 ‘ 𝑦 ) } ∈ 𝐼 ↔ ( { ( ◡ 𝐹 ‘ 0 ) , ( ◡ 𝐹 ‘ 𝑦 ) } ∈ 𝐸 ∧ { ( ◡ 𝐹 ‘ 0 ) , ( ◡ 𝐹 ‘ 𝑦 ) } ⊆ 𝐶 ) ) )
117 110 116 mpbird ⊢ ( ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) ∧ 𝑦 ∈ ( 1 ... 𝑁 ) ) ∧ { 0 , 𝑦 } ⊆ ( 0 ... 𝑁 ) ) → { ( ◡ 𝐹 ‘ 0 ) , ( ◡ 𝐹 ‘ 𝑦 ) } ∈ 𝐼 )
118 34 117 eqeltrd ⊢ ( ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) ∧ 𝑦 ∈ ( 1 ... 𝑁 ) ) ∧ { 0 , 𝑦 } ⊆ ( 0 ... 𝑁 ) ) → ( ◡ 𝐹 “ { 0 , 𝑦 } ) ∈ 𝐼 )
119 118 ex ⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) ∧ 𝑦 ∈ ( 1 ... 𝑁 ) ) → ( { 0 , 𝑦 } ⊆ ( 0 ... 𝑁 ) → ( ◡ 𝐹 “ { 0 , 𝑦 } ) ∈ 𝐼 ) )
120 sseq1 ⊢ ( 𝐽 = { 0 , 𝑦 } → ( 𝐽 ⊆ ( 0 ... 𝑁 ) ↔ { 0 , 𝑦 } ⊆ ( 0 ... 𝑁 ) ) )
121 imaeq2 ⊢ ( 𝐽 = { 0 , 𝑦 } → ( ◡ 𝐹 “ 𝐽 ) = ( ◡ 𝐹 “ { 0 , 𝑦 } ) )
122 121 eleq1d ⊢ ( 𝐽 = { 0 , 𝑦 } → ( ( ◡ 𝐹 “ 𝐽 ) ∈ 𝐼 ↔ ( ◡ 𝐹 “ { 0 , 𝑦 } ) ∈ 𝐼 ) )
123 120 122 imbi12d ⊢ ( 𝐽 = { 0 , 𝑦 } → ( ( 𝐽 ⊆ ( 0 ... 𝑁 ) → ( ◡ 𝐹 “ 𝐽 ) ∈ 𝐼 ) ↔ ( { 0 , 𝑦 } ⊆ ( 0 ... 𝑁 ) → ( ◡ 𝐹 “ { 0 , 𝑦 } ) ∈ 𝐼 ) ) )
124 119 123 syl5ibrcom ⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) ∧ 𝑦 ∈ ( 1 ... 𝑁 ) ) → ( 𝐽 = { 0 , 𝑦 } → ( 𝐽 ⊆ ( 0 ... 𝑁 ) → ( ◡ 𝐹 “ 𝐽 ) ∈ 𝐼 ) ) )
125 124 rexlimdva ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) → ( ∃ 𝑦 ∈ ( 1 ... 𝑁 ) 𝐽 = { 0 , 𝑦 } → ( 𝐽 ⊆ ( 0 ... 𝑁 ) → ( ◡ 𝐹 “ 𝐽 ) ∈ 𝐼 ) ) )
126 125 impcomd ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) → ( ( 𝐽 ⊆ ( 0 ... 𝑁 ) ∧ ∃ 𝑦 ∈ ( 1 ... 𝑁 ) 𝐽 = { 0 , 𝑦 } ) → ( ◡ 𝐹 “ 𝐽 ) ∈ 𝐼 ) )
127 11 126 sylbid ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) → ( 𝐽 ∈ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) → ( ◡ 𝐹 “ 𝐽 ) ∈ 𝐼 ) )
128 127 3impia ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ∧ 𝐽 ∈ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) ) → ( ◡ 𝐹 “ 𝐽 ) ∈ 𝐼 )