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 ‘ 𝑁 ) ) ) → ( 𝐹𝐽 ) ∈ 𝐼 )