Metamath Proof Explorer

Theorem grlimgrtrilem2

Description: Lemma 3 for grlimgrtri . (Contributed by AV, 23-Aug-2025)

Ref Expression
Hypotheses grlimgrtrilem1.v 
|- V = ( Vtx ` G )
grlimgrtrilem1.n 
|- N = ( G ClNeighbVtx a )
grlimgrtrilem1.i 
|- I = ( Edg ` G )
grlimgrtrilem1.k 
|- K = { x e. I | x C_ N }
grlimgrtrilem2.m 
|- M = ( H ClNeighbVtx ( F ` a ) )
grlimgrtrilem2.j 
|- J = ( Edg ` H )
grlimgrtrilem2.l 
|- L = { x e. J | x C_ M }
Assertion grlimgrtrilem2 
|- ( ( ( f : N -1-1-onto-> M /\ g : K -1-1-onto-> L ) /\ A. i e. K ( f " i ) = ( g ` i ) /\ { b , c } e. K ) -> { ( f ` b ) , ( f ` c ) } e. J )

Proof

Step Hyp Ref Expression
1 grlimgrtrilem1.v 
 |-  V = ( Vtx ` G )
2 grlimgrtrilem1.n 
 |-  N = ( G ClNeighbVtx a )
3 grlimgrtrilem1.i 
 |-  I = ( Edg ` G )
4 grlimgrtrilem1.k 
 |-  K = { x e. I | x C_ N }
5 grlimgrtrilem2.m 
 |-  M = ( H ClNeighbVtx ( F ` a ) )
6 grlimgrtrilem2.j 
 |-  J = ( Edg ` H )
7 grlimgrtrilem2.l 
 |-  L = { x e. J | x C_ M }
8 imaeq2 
 |-  ( i = { b , c } -> ( f " i ) = ( f " { b , c } ) )
9 fveq2 
 |-  ( i = { b , c } -> ( g ` i ) = ( g ` { b , c } ) )
10 8 9 eqeq12d 
 |-  ( i = { b , c } -> ( ( f " i ) = ( g ` i ) <-> ( f " { b , c } ) = ( g ` { b , c } ) ) )
11 10 rspcv 
 |-  ( { b , c } e. K -> ( A. i e. K ( f " i ) = ( g ` i ) -> ( f " { b , c } ) = ( g ` { b , c } ) ) )
12 f1ofn 
 |-  ( f : N -1-1-onto-> M -> f Fn N )
13 12 adantr 
 |-  ( ( f : N -1-1-onto-> M /\ g : K -1-1-onto-> L ) -> f Fn N )
14 13 adantl 
 |-  ( ( { b , c } e. K /\ ( f : N -1-1-onto-> M /\ g : K -1-1-onto-> L ) ) -> f Fn N )
15 4 eleq2i 
 |-  ( { b , c } e. K <-> { b , c } e. { x e. I | x C_ N } )
16 sseq1 
 |-  ( x = { b , c } -> ( x C_ N <-> { b , c } C_ N ) )
17 16 elrab 
 |-  ( { b , c } e. { x e. I | x C_ N } <-> ( { b , c } e. I /\ { b , c } C_ N ) )
18 15 17 bitri 
 |-  ( { b , c } e. K <-> ( { b , c } e. I /\ { b , c } C_ N ) )
19 vex 
 |-  b e. _V
20 vex 
 |-  c e. _V
21 19 20 prss 
 |-  ( ( b e. N /\ c e. N ) <-> { b , c } C_ N )
22 simpl 
 |-  ( ( b e. N /\ c e. N ) -> b e. N )
23 21 22 sylbir 
 |-  ( { b , c } C_ N -> b e. N )
24 18 23 simplbiim 
 |-  ( { b , c } e. K -> b e. N )
25 24 adantr 
 |-  ( ( { b , c } e. K /\ ( f : N -1-1-onto-> M /\ g : K -1-1-onto-> L ) ) -> b e. N )
26 simpr 
 |-  ( ( b e. N /\ c e. N ) -> c e. N )
27 21 26 sylbir 
 |-  ( { b , c } C_ N -> c e. N )
28 18 27 simplbiim 
 |-  ( { b , c } e. K -> c e. N )
29 28 adantr 
 |-  ( ( { b , c } e. K /\ ( f : N -1-1-onto-> M /\ g : K -1-1-onto-> L ) ) -> c e. N )
30 fnimapr 
 |-  ( ( f Fn N /\ b e. N /\ c e. N ) -> ( f " { b , c } ) = { ( f ` b ) , ( f ` c ) } )
31 14 25 29 30 syl3anc 
 |-  ( ( { b , c } e. K /\ ( f : N -1-1-onto-> M /\ g : K -1-1-onto-> L ) ) -> ( f " { b , c } ) = { ( f ` b ) , ( f ` c ) } )
32 31 eqeq1d 
 |-  ( ( { b , c } e. K /\ ( f : N -1-1-onto-> M /\ g : K -1-1-onto-> L ) ) -> ( ( f " { b , c } ) = ( g ` { b , c } ) <-> { ( f ` b ) , ( f ` c ) } = ( g ` { b , c } ) ) )
33 ssrab2 
 |-  { x e. J | x C_ M } C_ J
34 7 33 eqsstri 
 |-  L C_ J
35 f1of 
 |-  ( g : K -1-1-onto-> L -> g : K --> L )
36 35 adantl 
 |-  ( ( f : N -1-1-onto-> M /\ g : K -1-1-onto-> L ) -> g : K --> L )
37 36 adantl 
 |-  ( ( { b , c } e. K /\ ( f : N -1-1-onto-> M /\ g : K -1-1-onto-> L ) ) -> g : K --> L )
38 simpl 
 |-  ( ( { b , c } e. K /\ ( f : N -1-1-onto-> M /\ g : K -1-1-onto-> L ) ) -> { b , c } e. K )
39 37 38 ffvelcdmd 
 |-  ( ( { b , c } e. K /\ ( f : N -1-1-onto-> M /\ g : K -1-1-onto-> L ) ) -> ( g ` { b , c } ) e. L )
40 34 39 sselid 
 |-  ( ( { b , c } e. K /\ ( f : N -1-1-onto-> M /\ g : K -1-1-onto-> L ) ) -> ( g ` { b , c } ) e. J )
41 eleq1 
 |-  ( { ( f ` b ) , ( f ` c ) } = ( g ` { b , c } ) -> ( { ( f ` b ) , ( f ` c ) } e. J <-> ( g ` { b , c } ) e. J ) )
42 40 41 syl5ibrcom 
 |-  ( ( { b , c } e. K /\ ( f : N -1-1-onto-> M /\ g : K -1-1-onto-> L ) ) -> ( { ( f ` b ) , ( f ` c ) } = ( g ` { b , c } ) -> { ( f ` b ) , ( f ` c ) } e. J ) )
43 32 42 sylbid 
 |-  ( ( { b , c } e. K /\ ( f : N -1-1-onto-> M /\ g : K -1-1-onto-> L ) ) -> ( ( f " { b , c } ) = ( g ` { b , c } ) -> { ( f ` b ) , ( f ` c ) } e. J ) )
44 43 ex 
 |-  ( { b , c } e. K -> ( ( f : N -1-1-onto-> M /\ g : K -1-1-onto-> L ) -> ( ( f " { b , c } ) = ( g ` { b , c } ) -> { ( f ` b ) , ( f ` c ) } e. J ) ) )
45 44 com23 
 |-  ( { b , c } e. K -> ( ( f " { b , c } ) = ( g ` { b , c } ) -> ( ( f : N -1-1-onto-> M /\ g : K -1-1-onto-> L ) -> { ( f ` b ) , ( f ` c ) } e. J ) ) )
46 11 45 syld 
 |-  ( { b , c } e. K -> ( A. i e. K ( f " i ) = ( g ` i ) -> ( ( f : N -1-1-onto-> M /\ g : K -1-1-onto-> L ) -> { ( f ` b ) , ( f ` c ) } e. J ) ) )
47 46 3imp31 
 |-  ( ( ( f : N -1-1-onto-> M /\ g : K -1-1-onto-> L ) /\ A. i e. K ( f " i ) = ( g ` i ) /\ { b , c } e. K ) -> { ( f ` b ) , ( f ` c ) } e. J )