Metamath Proof Explorer

Theorem isubgr3stgrlem1

Description: Lemma 1 for isubgr3stgr . (Contributed by AV, 16-Sep-2025)

Ref Expression
Hypotheses isubgr3stgr.v 
|- V = ( Vtx ` G )
isubgr3stgr.u 
|- U = ( G NeighbVtx X )
isubgr3stgr.c 
|- C = ( G ClNeighbVtx X )
isubgr3stgr.f 
|- F = ( H u. { <. X , Y >. } )
Assertion isubgr3stgrlem1 
|- ( ( H : U -1-1-onto-> R /\ X e. V /\ ( Y e. W /\ Y e/ R ) ) -> F : C -1-1-onto-> ( R u. { Y } ) )

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.f 
 |-  F = ( H u. { <. X , Y >. } )
5 f1oeq2 
 |-  ( U = ( G NeighbVtx X ) -> ( H : U -1-1-onto-> R <-> H : ( G NeighbVtx X ) -1-1-onto-> R ) )
6 2 5 ax-mp 
 |-  ( H : U -1-1-onto-> R <-> H : ( G NeighbVtx X ) -1-1-onto-> R )
7 6 biimpi 
 |-  ( H : U -1-1-onto-> R -> H : ( G NeighbVtx X ) -1-1-onto-> R )
8 7 3ad2ant1 
 |-  ( ( H : U -1-1-onto-> R /\ X e. V /\ ( Y e. W /\ Y e/ R ) ) -> H : ( G NeighbVtx X ) -1-1-onto-> R )
9 simpl 
 |-  ( ( Y e. W /\ Y e/ R ) -> Y e. W )
10 9 anim2i 
 |-  ( ( X e. V /\ ( Y e. W /\ Y e/ R ) ) -> ( X e. V /\ Y e. W ) )
11 10 3adant1 
 |-  ( ( H : U -1-1-onto-> R /\ X e. V /\ ( Y e. W /\ Y e/ R ) ) -> ( X e. V /\ Y e. W ) )
12 nbgrnself2 
 |-  X e/ ( G NeighbVtx X )
13 12 a1i 
 |-  ( ( H : U -1-1-onto-> R /\ X e. V /\ ( Y e. W /\ Y e/ R ) ) -> X e/ ( G NeighbVtx X ) )
14 simp3r 
 |-  ( ( H : U -1-1-onto-> R /\ X e. V /\ ( Y e. W /\ Y e/ R ) ) -> Y e/ R )
15 4 f1ounsn 
 |-  ( ( H : ( G NeighbVtx X ) -1-1-onto-> R /\ ( X e. V /\ Y e. W ) /\ ( X e/ ( G NeighbVtx X ) /\ Y e/ R ) ) -> F : ( ( G NeighbVtx X ) u. { X } ) -1-1-onto-> ( R u. { Y } ) )
16 8 11 13 14 15 syl112anc 
 |-  ( ( H : U -1-1-onto-> R /\ X e. V /\ ( Y e. W /\ Y e/ R ) ) -> F : ( ( G NeighbVtx X ) u. { X } ) -1-1-onto-> ( R u. { Y } ) )
17 1 dfclnbgr4 
 |-  ( X e. V -> ( G ClNeighbVtx X ) = ( { X } u. ( G NeighbVtx X ) ) )
18 17 3ad2ant2 
 |-  ( ( H : U -1-1-onto-> R /\ X e. V /\ ( Y e. W /\ Y e/ R ) ) -> ( G ClNeighbVtx X ) = ( { X } u. ( G NeighbVtx X ) ) )
19 uncom 
 |-  ( { X } u. ( G NeighbVtx X ) ) = ( ( G NeighbVtx X ) u. { X } )
20 18 19 eqtrdi 
 |-  ( ( H : U -1-1-onto-> R /\ X e. V /\ ( Y e. W /\ Y e/ R ) ) -> ( G ClNeighbVtx X ) = ( ( G NeighbVtx X ) u. { X } ) )
21 3 20 eqtrid 
 |-  ( ( H : U -1-1-onto-> R /\ X e. V /\ ( Y e. W /\ Y e/ R ) ) -> C = ( ( G NeighbVtx X ) u. { X } ) )
22 21 f1oeq2d 
 |-  ( ( H : U -1-1-onto-> R /\ X e. V /\ ( Y e. W /\ Y e/ R ) ) -> ( F : C -1-1-onto-> ( R u. { Y } ) <-> F : ( ( G NeighbVtx X ) u. { X } ) -1-1-onto-> ( R u. { Y } ) ) )
23 16 22 mpbird 
 |-  ( ( H : U -1-1-onto-> R /\ X e. V /\ ( Y e. W /\ Y e/ R ) ) -> F : C -1-1-onto-> ( R u. { Y } ) )