Metamath Proof Explorer


Theorem isubgr3stgrlem4

Description: Lemma 4 for isubgr3stgr . (Contributed by AV, 24-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 ‘ 𝐺 )
Assertion isubgr3stgrlem4 ( ( 𝐴 = 𝑋 ∧ ( 𝐹 : 𝐶1-1-onto𝑊 ∧ ( 𝐹𝑋 ) = 0 ) ∧ ( 𝐴𝐵𝐴𝐶𝐵𝐶 ) ) → ∃ 𝑧 ∈ ( 1 ... 𝑁 ) ( 𝐹 “ { 𝐴 , 𝐵 } ) = { 0 , 𝑧 } )

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 preq2 ( 𝑧 = ( 𝐹𝐵 ) → { 0 , 𝑧 } = { 0 , ( 𝐹𝐵 ) } )
9 8 eqeq2d ( 𝑧 = ( 𝐹𝐵 ) → ( ( 𝐹 “ { 𝑋 , 𝐵 } ) = { 0 , 𝑧 } ↔ ( 𝐹 “ { 𝑋 , 𝐵 } ) = { 0 , ( 𝐹𝐵 ) } ) )
10 f1of ( 𝐹 : 𝐶1-1-onto𝑊𝐹 : 𝐶𝑊 )
11 10 adantr ( ( 𝐹 : 𝐶1-1-onto𝑊 ∧ ( 𝐹𝑋 ) = 0 ) → 𝐹 : 𝐶𝑊 )
12 11 adantr ( ( ( 𝐹 : 𝐶1-1-onto𝑊 ∧ ( 𝐹𝑋 ) = 0 ) ∧ ( 𝑋𝐵𝑋𝐶𝐵𝐶 ) ) → 𝐹 : 𝐶𝑊 )
13 simpr3 ( ( ( 𝐹 : 𝐶1-1-onto𝑊 ∧ ( 𝐹𝑋 ) = 0 ) ∧ ( 𝑋𝐵𝑋𝐶𝐵𝐶 ) ) → 𝐵𝐶 )
14 12 13 ffvelcdmd ( ( ( 𝐹 : 𝐶1-1-onto𝑊 ∧ ( 𝐹𝑋 ) = 0 ) ∧ ( 𝑋𝐵𝑋𝐶𝐵𝐶 ) ) → ( 𝐹𝐵 ) ∈ 𝑊 )
15 5 fveq2i ( Vtx ‘ 𝑆 ) = ( Vtx ‘ ( StarGr ‘ 𝑁 ) )
16 stgrvtx ( 𝑁 ∈ ℕ0 → ( Vtx ‘ ( StarGr ‘ 𝑁 ) ) = ( 0 ... 𝑁 ) )
17 4 16 ax-mp ( Vtx ‘ ( StarGr ‘ 𝑁 ) ) = ( 0 ... 𝑁 )
18 6 15 17 3eqtri 𝑊 = ( 0 ... 𝑁 )
19 18 eleq2i ( ( 𝐹𝐵 ) ∈ 𝑊 ↔ ( 𝐹𝐵 ) ∈ ( 0 ... 𝑁 ) )
20 fz0sn0fz1 ( 𝑁 ∈ ℕ0 → ( 0 ... 𝑁 ) = ( { 0 } ∪ ( 1 ... 𝑁 ) ) )
21 4 20 ax-mp ( 0 ... 𝑁 ) = ( { 0 } ∪ ( 1 ... 𝑁 ) )
22 21 eleq2i ( ( 𝐹𝐵 ) ∈ ( 0 ... 𝑁 ) ↔ ( 𝐹𝐵 ) ∈ ( { 0 } ∪ ( 1 ... 𝑁 ) ) )
23 elun ( ( 𝐹𝐵 ) ∈ ( { 0 } ∪ ( 1 ... 𝑁 ) ) ↔ ( ( 𝐹𝐵 ) ∈ { 0 } ∨ ( 𝐹𝐵 ) ∈ ( 1 ... 𝑁 ) ) )
24 fvex ( 𝐹𝐵 ) ∈ V
25 24 elsn ( ( 𝐹𝐵 ) ∈ { 0 } ↔ ( 𝐹𝐵 ) = 0 )
26 25 orbi1i ( ( ( 𝐹𝐵 ) ∈ { 0 } ∨ ( 𝐹𝐵 ) ∈ ( 1 ... 𝑁 ) ) ↔ ( ( 𝐹𝐵 ) = 0 ∨ ( 𝐹𝐵 ) ∈ ( 1 ... 𝑁 ) ) )
27 23 26 bitri ( ( 𝐹𝐵 ) ∈ ( { 0 } ∪ ( 1 ... 𝑁 ) ) ↔ ( ( 𝐹𝐵 ) = 0 ∨ ( 𝐹𝐵 ) ∈ ( 1 ... 𝑁 ) ) )
28 19 22 27 3bitri ( ( 𝐹𝐵 ) ∈ 𝑊 ↔ ( ( 𝐹𝐵 ) = 0 ∨ ( 𝐹𝐵 ) ∈ ( 1 ... 𝑁 ) ) )
29 eqeq2 ( ( 𝐹𝑋 ) = 0 → ( ( 𝐹𝐵 ) = ( 𝐹𝑋 ) ↔ ( 𝐹𝐵 ) = 0 ) )
30 29 adantl ( ( 𝐹 : 𝐶1-1-onto𝑊 ∧ ( 𝐹𝑋 ) = 0 ) → ( ( 𝐹𝐵 ) = ( 𝐹𝑋 ) ↔ ( 𝐹𝐵 ) = 0 ) )
31 30 adantr ( ( ( 𝐹 : 𝐶1-1-onto𝑊 ∧ ( 𝐹𝑋 ) = 0 ) ∧ ( 𝑋𝐵𝑋𝐶𝐵𝐶 ) ) → ( ( 𝐹𝐵 ) = ( 𝐹𝑋 ) ↔ ( 𝐹𝐵 ) = 0 ) )
32 f1of1 ( 𝐹 : 𝐶1-1-onto𝑊𝐹 : 𝐶1-1𝑊 )
33 dff14a ( 𝐹 : 𝐶1-1𝑊 ↔ ( 𝐹 : 𝐶𝑊 ∧ ∀ 𝑎𝐶𝑏𝐶 ( 𝑎𝑏 → ( 𝐹𝑎 ) ≠ ( 𝐹𝑏 ) ) ) )
34 simpl ( ( 𝑎 = 𝑋𝑏 = 𝐵 ) → 𝑎 = 𝑋 )
35 simpr ( ( 𝑎 = 𝑋𝑏 = 𝐵 ) → 𝑏 = 𝐵 )
36 34 35 neeq12d ( ( 𝑎 = 𝑋𝑏 = 𝐵 ) → ( 𝑎𝑏𝑋𝐵 ) )
37 fveq2 ( 𝑎 = 𝑋 → ( 𝐹𝑎 ) = ( 𝐹𝑋 ) )
38 37 adantr ( ( 𝑎 = 𝑋𝑏 = 𝐵 ) → ( 𝐹𝑎 ) = ( 𝐹𝑋 ) )
39 fveq2 ( 𝑏 = 𝐵 → ( 𝐹𝑏 ) = ( 𝐹𝐵 ) )
40 39 adantl ( ( 𝑎 = 𝑋𝑏 = 𝐵 ) → ( 𝐹𝑏 ) = ( 𝐹𝐵 ) )
41 38 40 neeq12d ( ( 𝑎 = 𝑋𝑏 = 𝐵 ) → ( ( 𝐹𝑎 ) ≠ ( 𝐹𝑏 ) ↔ ( 𝐹𝑋 ) ≠ ( 𝐹𝐵 ) ) )
42 36 41 imbi12d ( ( 𝑎 = 𝑋𝑏 = 𝐵 ) → ( ( 𝑎𝑏 → ( 𝐹𝑎 ) ≠ ( 𝐹𝑏 ) ) ↔ ( 𝑋𝐵 → ( 𝐹𝑋 ) ≠ ( 𝐹𝐵 ) ) ) )
43 42 rspc2gv ( ( 𝑋𝐶𝐵𝐶 ) → ( ∀ 𝑎𝐶𝑏𝐶 ( 𝑎𝑏 → ( 𝐹𝑎 ) ≠ ( 𝐹𝑏 ) ) → ( 𝑋𝐵 → ( 𝐹𝑋 ) ≠ ( 𝐹𝐵 ) ) ) )
44 43 3adant1 ( ( 𝑋𝐵𝑋𝐶𝐵𝐶 ) → ( ∀ 𝑎𝐶𝑏𝐶 ( 𝑎𝑏 → ( 𝐹𝑎 ) ≠ ( 𝐹𝑏 ) ) → ( 𝑋𝐵 → ( 𝐹𝑋 ) ≠ ( 𝐹𝐵 ) ) ) )
45 id ( ( 𝑋𝐵 → ( 𝐹𝑋 ) ≠ ( 𝐹𝐵 ) ) → ( 𝑋𝐵 → ( 𝐹𝑋 ) ≠ ( 𝐹𝐵 ) ) )
46 eqneqall ( ( 𝐹𝑋 ) = ( 𝐹𝐵 ) → ( ( 𝐹𝑋 ) ≠ ( 𝐹𝐵 ) → ( 𝐹𝐵 ) ∈ ( 1 ... 𝑁 ) ) )
47 46 eqcoms ( ( 𝐹𝐵 ) = ( 𝐹𝑋 ) → ( ( 𝐹𝑋 ) ≠ ( 𝐹𝐵 ) → ( 𝐹𝐵 ) ∈ ( 1 ... 𝑁 ) ) )
48 47 com12 ( ( 𝐹𝑋 ) ≠ ( 𝐹𝐵 ) → ( ( 𝐹𝐵 ) = ( 𝐹𝑋 ) → ( 𝐹𝐵 ) ∈ ( 1 ... 𝑁 ) ) )
49 45 48 syl6com ( 𝑋𝐵 → ( ( 𝑋𝐵 → ( 𝐹𝑋 ) ≠ ( 𝐹𝐵 ) ) → ( ( 𝐹𝐵 ) = ( 𝐹𝑋 ) → ( 𝐹𝐵 ) ∈ ( 1 ... 𝑁 ) ) ) )
50 49 3ad2ant1 ( ( 𝑋𝐵𝑋𝐶𝐵𝐶 ) → ( ( 𝑋𝐵 → ( 𝐹𝑋 ) ≠ ( 𝐹𝐵 ) ) → ( ( 𝐹𝐵 ) = ( 𝐹𝑋 ) → ( 𝐹𝐵 ) ∈ ( 1 ... 𝑁 ) ) ) )
51 44 50 syld ( ( 𝑋𝐵𝑋𝐶𝐵𝐶 ) → ( ∀ 𝑎𝐶𝑏𝐶 ( 𝑎𝑏 → ( 𝐹𝑎 ) ≠ ( 𝐹𝑏 ) ) → ( ( 𝐹𝐵 ) = ( 𝐹𝑋 ) → ( 𝐹𝐵 ) ∈ ( 1 ... 𝑁 ) ) ) )
52 51 adantld ( ( 𝑋𝐵𝑋𝐶𝐵𝐶 ) → ( ( 𝐹 : 𝐶𝑊 ∧ ∀ 𝑎𝐶𝑏𝐶 ( 𝑎𝑏 → ( 𝐹𝑎 ) ≠ ( 𝐹𝑏 ) ) ) → ( ( 𝐹𝐵 ) = ( 𝐹𝑋 ) → ( 𝐹𝐵 ) ∈ ( 1 ... 𝑁 ) ) ) )
53 33 52 biimtrid ( ( 𝑋𝐵𝑋𝐶𝐵𝐶 ) → ( 𝐹 : 𝐶1-1𝑊 → ( ( 𝐹𝐵 ) = ( 𝐹𝑋 ) → ( 𝐹𝐵 ) ∈ ( 1 ... 𝑁 ) ) ) )
54 32 53 syl5com ( 𝐹 : 𝐶1-1-onto𝑊 → ( ( 𝑋𝐵𝑋𝐶𝐵𝐶 ) → ( ( 𝐹𝐵 ) = ( 𝐹𝑋 ) → ( 𝐹𝐵 ) ∈ ( 1 ... 𝑁 ) ) ) )
55 54 adantr ( ( 𝐹 : 𝐶1-1-onto𝑊 ∧ ( 𝐹𝑋 ) = 0 ) → ( ( 𝑋𝐵𝑋𝐶𝐵𝐶 ) → ( ( 𝐹𝐵 ) = ( 𝐹𝑋 ) → ( 𝐹𝐵 ) ∈ ( 1 ... 𝑁 ) ) ) )
56 55 imp ( ( ( 𝐹 : 𝐶1-1-onto𝑊 ∧ ( 𝐹𝑋 ) = 0 ) ∧ ( 𝑋𝐵𝑋𝐶𝐵𝐶 ) ) → ( ( 𝐹𝐵 ) = ( 𝐹𝑋 ) → ( 𝐹𝐵 ) ∈ ( 1 ... 𝑁 ) ) )
57 31 56 sylbird ( ( ( 𝐹 : 𝐶1-1-onto𝑊 ∧ ( 𝐹𝑋 ) = 0 ) ∧ ( 𝑋𝐵𝑋𝐶𝐵𝐶 ) ) → ( ( 𝐹𝐵 ) = 0 → ( 𝐹𝐵 ) ∈ ( 1 ... 𝑁 ) ) )
58 idd ( ( ( 𝐹 : 𝐶1-1-onto𝑊 ∧ ( 𝐹𝑋 ) = 0 ) ∧ ( 𝑋𝐵𝑋𝐶𝐵𝐶 ) ) → ( ( 𝐹𝐵 ) ∈ ( 1 ... 𝑁 ) → ( 𝐹𝐵 ) ∈ ( 1 ... 𝑁 ) ) )
59 57 58 jaod ( ( ( 𝐹 : 𝐶1-1-onto𝑊 ∧ ( 𝐹𝑋 ) = 0 ) ∧ ( 𝑋𝐵𝑋𝐶𝐵𝐶 ) ) → ( ( ( 𝐹𝐵 ) = 0 ∨ ( 𝐹𝐵 ) ∈ ( 1 ... 𝑁 ) ) → ( 𝐹𝐵 ) ∈ ( 1 ... 𝑁 ) ) )
60 28 59 biimtrid ( ( ( 𝐹 : 𝐶1-1-onto𝑊 ∧ ( 𝐹𝑋 ) = 0 ) ∧ ( 𝑋𝐵𝑋𝐶𝐵𝐶 ) ) → ( ( 𝐹𝐵 ) ∈ 𝑊 → ( 𝐹𝐵 ) ∈ ( 1 ... 𝑁 ) ) )
61 14 60 mpd ( ( ( 𝐹 : 𝐶1-1-onto𝑊 ∧ ( 𝐹𝑋 ) = 0 ) ∧ ( 𝑋𝐵𝑋𝐶𝐵𝐶 ) ) → ( 𝐹𝐵 ) ∈ ( 1 ... 𝑁 ) )
62 f1ofn ( 𝐹 : 𝐶1-1-onto𝑊𝐹 Fn 𝐶 )
63 62 adantr ( ( 𝐹 : 𝐶1-1-onto𝑊 ∧ ( 𝐹𝑋 ) = 0 ) → 𝐹 Fn 𝐶 )
64 3simpc ( ( 𝑋𝐵𝑋𝐶𝐵𝐶 ) → ( 𝑋𝐶𝐵𝐶 ) )
65 63 64 anim12i ( ( ( 𝐹 : 𝐶1-1-onto𝑊 ∧ ( 𝐹𝑋 ) = 0 ) ∧ ( 𝑋𝐵𝑋𝐶𝐵𝐶 ) ) → ( 𝐹 Fn 𝐶 ∧ ( 𝑋𝐶𝐵𝐶 ) ) )
66 3anass ( ( 𝐹 Fn 𝐶𝑋𝐶𝐵𝐶 ) ↔ ( 𝐹 Fn 𝐶 ∧ ( 𝑋𝐶𝐵𝐶 ) ) )
67 65 66 sylibr ( ( ( 𝐹 : 𝐶1-1-onto𝑊 ∧ ( 𝐹𝑋 ) = 0 ) ∧ ( 𝑋𝐵𝑋𝐶𝐵𝐶 ) ) → ( 𝐹 Fn 𝐶𝑋𝐶𝐵𝐶 ) )
68 fnimapr ( ( 𝐹 Fn 𝐶𝑋𝐶𝐵𝐶 ) → ( 𝐹 “ { 𝑋 , 𝐵 } ) = { ( 𝐹𝑋 ) , ( 𝐹𝐵 ) } )
69 67 68 syl ( ( ( 𝐹 : 𝐶1-1-onto𝑊 ∧ ( 𝐹𝑋 ) = 0 ) ∧ ( 𝑋𝐵𝑋𝐶𝐵𝐶 ) ) → ( 𝐹 “ { 𝑋 , 𝐵 } ) = { ( 𝐹𝑋 ) , ( 𝐹𝐵 ) } )
70 simpr ( ( 𝐹 : 𝐶1-1-onto𝑊 ∧ ( 𝐹𝑋 ) = 0 ) → ( 𝐹𝑋 ) = 0 )
71 70 adantr ( ( ( 𝐹 : 𝐶1-1-onto𝑊 ∧ ( 𝐹𝑋 ) = 0 ) ∧ ( 𝑋𝐵𝑋𝐶𝐵𝐶 ) ) → ( 𝐹𝑋 ) = 0 )
72 71 preq1d ( ( ( 𝐹 : 𝐶1-1-onto𝑊 ∧ ( 𝐹𝑋 ) = 0 ) ∧ ( 𝑋𝐵𝑋𝐶𝐵𝐶 ) ) → { ( 𝐹𝑋 ) , ( 𝐹𝐵 ) } = { 0 , ( 𝐹𝐵 ) } )
73 69 72 eqtrd ( ( ( 𝐹 : 𝐶1-1-onto𝑊 ∧ ( 𝐹𝑋 ) = 0 ) ∧ ( 𝑋𝐵𝑋𝐶𝐵𝐶 ) ) → ( 𝐹 “ { 𝑋 , 𝐵 } ) = { 0 , ( 𝐹𝐵 ) } )
74 9 61 73 rspcedvdw ( ( ( 𝐹 : 𝐶1-1-onto𝑊 ∧ ( 𝐹𝑋 ) = 0 ) ∧ ( 𝑋𝐵𝑋𝐶𝐵𝐶 ) ) → ∃ 𝑧 ∈ ( 1 ... 𝑁 ) ( 𝐹 “ { 𝑋 , 𝐵 } ) = { 0 , 𝑧 } )
75 74 ex ( ( 𝐹 : 𝐶1-1-onto𝑊 ∧ ( 𝐹𝑋 ) = 0 ) → ( ( 𝑋𝐵𝑋𝐶𝐵𝐶 ) → ∃ 𝑧 ∈ ( 1 ... 𝑁 ) ( 𝐹 “ { 𝑋 , 𝐵 } ) = { 0 , 𝑧 } ) )
76 neeq1 ( 𝐴 = 𝑋 → ( 𝐴𝐵𝑋𝐵 ) )
77 eleq1 ( 𝐴 = 𝑋 → ( 𝐴𝐶𝑋𝐶 ) )
78 76 77 3anbi12d ( 𝐴 = 𝑋 → ( ( 𝐴𝐵𝐴𝐶𝐵𝐶 ) ↔ ( 𝑋𝐵𝑋𝐶𝐵𝐶 ) ) )
79 preq1 ( 𝐴 = 𝑋 → { 𝐴 , 𝐵 } = { 𝑋 , 𝐵 } )
80 79 imaeq2d ( 𝐴 = 𝑋 → ( 𝐹 “ { 𝐴 , 𝐵 } ) = ( 𝐹 “ { 𝑋 , 𝐵 } ) )
81 80 eqeq1d ( 𝐴 = 𝑋 → ( ( 𝐹 “ { 𝐴 , 𝐵 } ) = { 0 , 𝑧 } ↔ ( 𝐹 “ { 𝑋 , 𝐵 } ) = { 0 , 𝑧 } ) )
82 81 rexbidv ( 𝐴 = 𝑋 → ( ∃ 𝑧 ∈ ( 1 ... 𝑁 ) ( 𝐹 “ { 𝐴 , 𝐵 } ) = { 0 , 𝑧 } ↔ ∃ 𝑧 ∈ ( 1 ... 𝑁 ) ( 𝐹 “ { 𝑋 , 𝐵 } ) = { 0 , 𝑧 } ) )
83 78 82 imbi12d ( 𝐴 = 𝑋 → ( ( ( 𝐴𝐵𝐴𝐶𝐵𝐶 ) → ∃ 𝑧 ∈ ( 1 ... 𝑁 ) ( 𝐹 “ { 𝐴 , 𝐵 } ) = { 0 , 𝑧 } ) ↔ ( ( 𝑋𝐵𝑋𝐶𝐵𝐶 ) → ∃ 𝑧 ∈ ( 1 ... 𝑁 ) ( 𝐹 “ { 𝑋 , 𝐵 } ) = { 0 , 𝑧 } ) ) )
84 75 83 imbitrrid ( 𝐴 = 𝑋 → ( ( 𝐹 : 𝐶1-1-onto𝑊 ∧ ( 𝐹𝑋 ) = 0 ) → ( ( 𝐴𝐵𝐴𝐶𝐵𝐶 ) → ∃ 𝑧 ∈ ( 1 ... 𝑁 ) ( 𝐹 “ { 𝐴 , 𝐵 } ) = { 0 , 𝑧 } ) ) )
85 84 3imp ( ( 𝐴 = 𝑋 ∧ ( 𝐹 : 𝐶1-1-onto𝑊 ∧ ( 𝐹𝑋 ) = 0 ) ∧ ( 𝐴𝐵𝐴𝐶𝐵𝐶 ) ) → ∃ 𝑧 ∈ ( 1 ... 𝑁 ) ( 𝐹 “ { 𝐴 , 𝐵 } ) = { 0 , 𝑧 } )