Metamath Proof Explorer

Theorem isubgr3stgrlem4

Description: Lemma 4 for isubgr3stgr . (Contributed by AV, 24-Sep-2025)

Ref Expression
Hypotheses isubgr3stgr.v 
|- V = ( Vtx ` G )
isubgr3stgr.u 
|- U = ( G NeighbVtx X )
isubgr3stgr.c 
|- C = ( G ClNeighbVtx X )
isubgr3stgr.n 
|- N e. NN0
isubgr3stgr.s 
|- S = ( StarGr ` N )
isubgr3stgr.w 
|- W = ( Vtx ` S )
isubgr3stgr.e 
|- E = ( Edg ` G )
Assertion isubgr3stgrlem4 
|- ( ( A = X /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) /\ ( A =/= B /\ A e. C /\ B e. C ) ) -> E. z e. ( 1 ... N ) ( F " { A , B } ) = { 0 , z } )

Proof

Step Hyp Ref Expression
1 isubgr3stgr.v 
 |-  V = ( Vtx ` G )
2 isubgr3stgr.u 
 |-  U = ( G NeighbVtx X )
3 isubgr3stgr.c 
 |-  C = ( G ClNeighbVtx X )
4 isubgr3stgr.n 
 |-  N e. NN0
5 isubgr3stgr.s 
 |-  S = ( StarGr ` N )
6 isubgr3stgr.w 
 |-  W = ( Vtx ` S )
7 isubgr3stgr.e 
 |-  E = ( Edg ` G )
8 preq2 
 |-  ( z = ( F ` B ) -> { 0 , z } = { 0 , ( F ` B ) } )
9 8 eqeq2d 
 |-  ( z = ( F ` B ) -> ( ( F " { X , B } ) = { 0 , z } <-> ( F " { X , B } ) = { 0 , ( F ` B ) } ) )
10 f1of 
 |-  ( F : C -1-1-onto-> W -> F : C --> W )
11 10 adantr 
 |-  ( ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) -> F : C --> W )
12 11 adantr 
 |-  ( ( ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) /\ ( X =/= B /\ X e. C /\ B e. C ) ) -> F : C --> W )
13 simpr3 
 |-  ( ( ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) /\ ( X =/= B /\ X e. C /\ B e. C ) ) -> B e. C )
14 12 13 ffvelcdmd 
 |-  ( ( ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) /\ ( X =/= B /\ X e. C /\ B e. C ) ) -> ( F ` B ) e. W )
15 5 fveq2i 
 |-  ( Vtx ` S ) = ( Vtx ` ( StarGr ` N ) )
16 stgrvtx 
 |-  ( N e. NN0 -> ( Vtx ` ( StarGr ` N ) ) = ( 0 ... N ) )
17 4 16 ax-mp 
 |-  ( Vtx ` ( StarGr ` N ) ) = ( 0 ... N )
18 6 15 17 3eqtri 
 |-  W = ( 0 ... N )
19 18 eleq2i 
 |-  ( ( F ` B ) e. W <-> ( F ` B ) e. ( 0 ... N ) )
20 fz0sn0fz1 
 |-  ( N e. NN0 -> ( 0 ... N ) = ( { 0 } u. ( 1 ... N ) ) )
21 4 20 ax-mp 
 |-  ( 0 ... N ) = ( { 0 } u. ( 1 ... N ) )
22 21 eleq2i 
 |-  ( ( F ` B ) e. ( 0 ... N ) <-> ( F ` B ) e. ( { 0 } u. ( 1 ... N ) ) )
23 elun 
 |-  ( ( F ` B ) e. ( { 0 } u. ( 1 ... N ) ) <-> ( ( F ` B ) e. { 0 } \/ ( F ` B ) e. ( 1 ... N ) ) )
24 fvex 
 |-  ( F ` B ) e. _V
25 24 elsn 
 |-  ( ( F ` B ) e. { 0 } <-> ( F ` B ) = 0 )
26 25 orbi1i 
 |-  ( ( ( F ` B ) e. { 0 } \/ ( F ` B ) e. ( 1 ... N ) ) <-> ( ( F ` B ) = 0 \/ ( F ` B ) e. ( 1 ... N ) ) )
27 23 26 bitri 
 |-  ( ( F ` B ) e. ( { 0 } u. ( 1 ... N ) ) <-> ( ( F ` B ) = 0 \/ ( F ` B ) e. ( 1 ... N ) ) )
28 19 22 27 3bitri 
 |-  ( ( F ` B ) e. W <-> ( ( F ` B ) = 0 \/ ( F ` B ) e. ( 1 ... N ) ) )
29 eqeq2 
 |-  ( ( F ` X ) = 0 -> ( ( F ` B ) = ( F ` X ) <-> ( F ` B ) = 0 ) )
30 29 adantl 
 |-  ( ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) -> ( ( F ` B ) = ( F ` X ) <-> ( F ` B ) = 0 ) )
31 30 adantr 
 |-  ( ( ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) /\ ( X =/= B /\ X e. C /\ B e. C ) ) -> ( ( F ` B ) = ( F ` X ) <-> ( F ` B ) = 0 ) )
32 f1of1 
 |-  ( F : C -1-1-onto-> W -> F : C -1-1-> W )
33 dff14a 
 |-  ( F : C -1-1-> W <-> ( F : C --> W /\ A. a e. C A. b e. C ( a =/= b -> ( F ` a ) =/= ( F ` b ) ) ) )
34 simpl 
 |-  ( ( a = X /\ b = B ) -> a = X )
35 simpr 
 |-  ( ( a = X /\ b = B ) -> b = B )
36 34 35 neeq12d 
 |-  ( ( a = X /\ b = B ) -> ( a =/= b <-> X =/= B ) )
37 fveq2 
 |-  ( a = X -> ( F ` a ) = ( F ` X ) )
38 37 adantr 
 |-  ( ( a = X /\ b = B ) -> ( F ` a ) = ( F ` X ) )
39 fveq2 
 |-  ( b = B -> ( F ` b ) = ( F ` B ) )
40 39 adantl 
 |-  ( ( a = X /\ b = B ) -> ( F ` b ) = ( F ` B ) )
41 38 40 neeq12d 
 |-  ( ( a = X /\ b = B ) -> ( ( F ` a ) =/= ( F ` b ) <-> ( F ` X ) =/= ( F ` B ) ) )
42 36 41 imbi12d 
 |-  ( ( a = X /\ b = B ) -> ( ( a =/= b -> ( F ` a ) =/= ( F ` b ) ) <-> ( X =/= B -> ( F ` X ) =/= ( F ` B ) ) ) )
43 42 rspc2gv 
 |-  ( ( X e. C /\ B e. C ) -> ( A. a e. C A. b e. C ( a =/= b -> ( F ` a ) =/= ( F ` b ) ) -> ( X =/= B -> ( F ` X ) =/= ( F ` B ) ) ) )
44 43 3adant1 
 |-  ( ( X =/= B /\ X e. C /\ B e. C ) -> ( A. a e. C A. b e. C ( a =/= b -> ( F ` a ) =/= ( F ` b ) ) -> ( X =/= B -> ( F ` X ) =/= ( F ` B ) ) ) )
45 id 
 |-  ( ( X =/= B -> ( F ` X ) =/= ( F ` B ) ) -> ( X =/= B -> ( F ` X ) =/= ( F ` B ) ) )
46 eqneqall 
 |-  ( ( F ` X ) = ( F ` B ) -> ( ( F ` X ) =/= ( F ` B ) -> ( F ` B ) e. ( 1 ... N ) ) )
47 46 eqcoms 
 |-  ( ( F ` B ) = ( F ` X ) -> ( ( F ` X ) =/= ( F ` B ) -> ( F ` B ) e. ( 1 ... N ) ) )
48 47 com12 
 |-  ( ( F ` X ) =/= ( F ` B ) -> ( ( F ` B ) = ( F ` X ) -> ( F ` B ) e. ( 1 ... N ) ) )
49 45 48 syl6com 
 |-  ( X =/= B -> ( ( X =/= B -> ( F ` X ) =/= ( F ` B ) ) -> ( ( F ` B ) = ( F ` X ) -> ( F ` B ) e. ( 1 ... N ) ) ) )
50 49 3ad2ant1 
 |-  ( ( X =/= B /\ X e. C /\ B e. C ) -> ( ( X =/= B -> ( F ` X ) =/= ( F ` B ) ) -> ( ( F ` B ) = ( F ` X ) -> ( F ` B ) e. ( 1 ... N ) ) ) )
51 44 50 syld 
 |-  ( ( X =/= B /\ X e. C /\ B e. C ) -> ( A. a e. C A. b e. C ( a =/= b -> ( F ` a ) =/= ( F ` b ) ) -> ( ( F ` B ) = ( F ` X ) -> ( F ` B ) e. ( 1 ... N ) ) ) )
52 51 adantld 
 |-  ( ( X =/= B /\ X e. C /\ B e. C ) -> ( ( F : C --> W /\ A. a e. C A. b e. C ( a =/= b -> ( F ` a ) =/= ( F ` b ) ) ) -> ( ( F ` B ) = ( F ` X ) -> ( F ` B ) e. ( 1 ... N ) ) ) )
53 33 52 biimtrid 
 |-  ( ( X =/= B /\ X e. C /\ B e. C ) -> ( F : C -1-1-> W -> ( ( F ` B ) = ( F ` X ) -> ( F ` B ) e. ( 1 ... N ) ) ) )
54 32 53 syl5com 
 |-  ( F : C -1-1-onto-> W -> ( ( X =/= B /\ X e. C /\ B e. C ) -> ( ( F ` B ) = ( F ` X ) -> ( F ` B ) e. ( 1 ... N ) ) ) )
55 54 adantr 
 |-  ( ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) -> ( ( X =/= B /\ X e. C /\ B e. C ) -> ( ( F ` B ) = ( F ` X ) -> ( F ` B ) e. ( 1 ... N ) ) ) )
56 55 imp 
 |-  ( ( ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) /\ ( X =/= B /\ X e. C /\ B e. C ) ) -> ( ( F ` B ) = ( F ` X ) -> ( F ` B ) e. ( 1 ... N ) ) )
57 31 56 sylbird 
 |-  ( ( ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) /\ ( X =/= B /\ X e. C /\ B e. C ) ) -> ( ( F ` B ) = 0 -> ( F ` B ) e. ( 1 ... N ) ) )
58 idd 
 |-  ( ( ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) /\ ( X =/= B /\ X e. C /\ B e. C ) ) -> ( ( F ` B ) e. ( 1 ... N ) -> ( F ` B ) e. ( 1 ... N ) ) )
59 57 58 jaod 
 |-  ( ( ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) /\ ( X =/= B /\ X e. C /\ B e. C ) ) -> ( ( ( F ` B ) = 0 \/ ( F ` B ) e. ( 1 ... N ) ) -> ( F ` B ) e. ( 1 ... N ) ) )
60 28 59 biimtrid 
 |-  ( ( ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) /\ ( X =/= B /\ X e. C /\ B e. C ) ) -> ( ( F ` B ) e. W -> ( F ` B ) e. ( 1 ... N ) ) )
61 14 60 mpd 
 |-  ( ( ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) /\ ( X =/= B /\ X e. C /\ B e. C ) ) -> ( F ` B ) e. ( 1 ... N ) )
62 f1ofn 
 |-  ( F : C -1-1-onto-> W -> F Fn C )
63 62 adantr 
 |-  ( ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) -> F Fn C )
64 3simpc 
 |-  ( ( X =/= B /\ X e. C /\ B e. C ) -> ( X e. C /\ B e. C ) )
65 63 64 anim12i 
 |-  ( ( ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) /\ ( X =/= B /\ X e. C /\ B e. C ) ) -> ( F Fn C /\ ( X e. C /\ B e. C ) ) )
66 3anass 
 |-  ( ( F Fn C /\ X e. C /\ B e. C ) <-> ( F Fn C /\ ( X e. C /\ B e. C ) ) )
67 65 66 sylibr 
 |-  ( ( ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) /\ ( X =/= B /\ X e. C /\ B e. C ) ) -> ( F Fn C /\ X e. C /\ B e. C ) )
68 fnimapr 
 |-  ( ( F Fn C /\ X e. C /\ B e. C ) -> ( F " { X , B } ) = { ( F ` X ) , ( F ` B ) } )
69 67 68 syl 
 |-  ( ( ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) /\ ( X =/= B /\ X e. C /\ B e. C ) ) -> ( F " { X , B } ) = { ( F ` X ) , ( F ` B ) } )
70 simpr 
 |-  ( ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) -> ( F ` X ) = 0 )
71 70 adantr 
 |-  ( ( ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) /\ ( X =/= B /\ X e. C /\ B e. C ) ) -> ( F ` X ) = 0 )
72 71 preq1d 
 |-  ( ( ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) /\ ( X =/= B /\ X e. C /\ B e. C ) ) -> { ( F ` X ) , ( F ` B ) } = { 0 , ( F ` B ) } )
73 69 72 eqtrd 
 |-  ( ( ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) /\ ( X =/= B /\ X e. C /\ B e. C ) ) -> ( F " { X , B } ) = { 0 , ( F ` B ) } )
74 9 61 73 rspcedvdw 
 |-  ( ( ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) /\ ( X =/= B /\ X e. C /\ B e. C ) ) -> E. z e. ( 1 ... N ) ( F " { X , B } ) = { 0 , z } )
75 74 ex 
 |-  ( ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) -> ( ( X =/= B /\ X e. C /\ B e. C ) -> E. z e. ( 1 ... N ) ( F " { X , B } ) = { 0 , z } ) )
76 neeq1 
 |-  ( A = X -> ( A =/= B <-> X =/= B ) )
77 eleq1 
 |-  ( A = X -> ( A e. C <-> X e. C ) )
78 76 77 3anbi12d 
 |-  ( A = X -> ( ( A =/= B /\ A e. C /\ B e. C ) <-> ( X =/= B /\ X e. C /\ B e. C ) ) )
79 preq1 
 |-  ( A = X -> { A , B } = { X , B } )
80 79 imaeq2d 
 |-  ( A = X -> ( F " { A , B } ) = ( F " { X , B } ) )
81 80 eqeq1d 
 |-  ( A = X -> ( ( F " { A , B } ) = { 0 , z } <-> ( F " { X , B } ) = { 0 , z } ) )
82 81 rexbidv 
 |-  ( A = X -> ( E. z e. ( 1 ... N ) ( F " { A , B } ) = { 0 , z } <-> E. z e. ( 1 ... N ) ( F " { X , B } ) = { 0 , z } ) )
83 78 82 imbi12d 
 |-  ( A = X -> ( ( ( A =/= B /\ A e. C /\ B e. C ) -> E. z e. ( 1 ... N ) ( F " { A , B } ) = { 0 , z } ) <-> ( ( X =/= B /\ X e. C /\ B e. C ) -> E. z e. ( 1 ... N ) ( F " { X , B } ) = { 0 , z } ) ) )
84 75 83 imbitrrid 
 |-  ( A = X -> ( ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) -> ( ( A =/= B /\ A e. C /\ B e. C ) -> E. z e. ( 1 ... N ) ( F " { A , B } ) = { 0 , z } ) ) )
85 84 3imp 
 |-  ( ( A = X /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) /\ ( A =/= B /\ A e. C /\ B e. C ) ) -> E. z e. ( 1 ... N ) ( F " { A , B } ) = { 0 , z } )