Metamath Proof Explorer


Theorem subumgredg2

Description: An edge of a subgraph of a multigraph connects exactly two different vertices. (Contributed by AV, 26-Nov-2020)

Ref Expression
Hypotheses subumgredg2.v
|- V = ( Vtx ` S )
subumgredg2.i
|- I = ( iEdg ` S )
Assertion subumgredg2
|- ( ( S SubGraph G /\ G e. UMGraph /\ X e. dom I ) -> ( I ` X ) e. { e e. ~P V | ( # ` e ) = 2 } )

Proof

Step Hyp Ref Expression
1 subumgredg2.v
 |-  V = ( Vtx ` S )
2 subumgredg2.i
 |-  I = ( iEdg ` S )
3 fveqeq2
 |-  ( e = ( I ` X ) -> ( ( # ` e ) = 2 <-> ( # ` ( I ` X ) ) = 2 ) )
4 umgruhgr
 |-  ( G e. UMGraph -> G e. UHGraph )
5 4 3ad2ant2
 |-  ( ( S SubGraph G /\ G e. UMGraph /\ X e. dom I ) -> G e. UHGraph )
6 simp1
 |-  ( ( S SubGraph G /\ G e. UMGraph /\ X e. dom I ) -> S SubGraph G )
7 simp3
 |-  ( ( S SubGraph G /\ G e. UMGraph /\ X e. dom I ) -> X e. dom I )
8 1 2 5 6 7 subgruhgredgd
 |-  ( ( S SubGraph G /\ G e. UMGraph /\ X e. dom I ) -> ( I ` X ) e. ( ~P V \ { (/) } ) )
9 eqid
 |-  ( iEdg ` G ) = ( iEdg ` G )
10 9 uhgrfun
 |-  ( G e. UHGraph -> Fun ( iEdg ` G ) )
11 4 10 syl
 |-  ( G e. UMGraph -> Fun ( iEdg ` G ) )
12 11 3ad2ant2
 |-  ( ( S SubGraph G /\ G e. UMGraph /\ X e. dom I ) -> Fun ( iEdg ` G ) )
13 eqid
 |-  ( Vtx ` S ) = ( Vtx ` S )
14 eqid
 |-  ( Vtx ` G ) = ( Vtx ` G )
15 eqid
 |-  ( Edg ` S ) = ( Edg ` S )
16 13 14 2 9 15 subgrprop2
 |-  ( S SubGraph G -> ( ( Vtx ` S ) C_ ( Vtx ` G ) /\ I C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P ( Vtx ` S ) ) )
17 16 simp2d
 |-  ( S SubGraph G -> I C_ ( iEdg ` G ) )
18 17 3ad2ant1
 |-  ( ( S SubGraph G /\ G e. UMGraph /\ X e. dom I ) -> I C_ ( iEdg ` G ) )
19 funssfv
 |-  ( ( Fun ( iEdg ` G ) /\ I C_ ( iEdg ` G ) /\ X e. dom I ) -> ( ( iEdg ` G ) ` X ) = ( I ` X ) )
20 19 eqcomd
 |-  ( ( Fun ( iEdg ` G ) /\ I C_ ( iEdg ` G ) /\ X e. dom I ) -> ( I ` X ) = ( ( iEdg ` G ) ` X ) )
21 12 18 7 20 syl3anc
 |-  ( ( S SubGraph G /\ G e. UMGraph /\ X e. dom I ) -> ( I ` X ) = ( ( iEdg ` G ) ` X ) )
22 21 fveq2d
 |-  ( ( S SubGraph G /\ G e. UMGraph /\ X e. dom I ) -> ( # ` ( I ` X ) ) = ( # ` ( ( iEdg ` G ) ` X ) ) )
23 simp2
 |-  ( ( S SubGraph G /\ G e. UMGraph /\ X e. dom I ) -> G e. UMGraph )
24 2 dmeqi
 |-  dom I = dom ( iEdg ` S )
25 24 eleq2i
 |-  ( X e. dom I <-> X e. dom ( iEdg ` S ) )
26 subgreldmiedg
 |-  ( ( S SubGraph G /\ X e. dom ( iEdg ` S ) ) -> X e. dom ( iEdg ` G ) )
27 26 ex
 |-  ( S SubGraph G -> ( X e. dom ( iEdg ` S ) -> X e. dom ( iEdg ` G ) ) )
28 25 27 syl5bi
 |-  ( S SubGraph G -> ( X e. dom I -> X e. dom ( iEdg ` G ) ) )
29 28 a1d
 |-  ( S SubGraph G -> ( G e. UMGraph -> ( X e. dom I -> X e. dom ( iEdg ` G ) ) ) )
30 29 3imp
 |-  ( ( S SubGraph G /\ G e. UMGraph /\ X e. dom I ) -> X e. dom ( iEdg ` G ) )
31 14 9 umgredg2
 |-  ( ( G e. UMGraph /\ X e. dom ( iEdg ` G ) ) -> ( # ` ( ( iEdg ` G ) ` X ) ) = 2 )
32 23 30 31 syl2anc
 |-  ( ( S SubGraph G /\ G e. UMGraph /\ X e. dom I ) -> ( # ` ( ( iEdg ` G ) ` X ) ) = 2 )
33 22 32 eqtrd
 |-  ( ( S SubGraph G /\ G e. UMGraph /\ X e. dom I ) -> ( # ` ( I ` X ) ) = 2 )
34 3 8 33 elrabd
 |-  ( ( S SubGraph G /\ G e. UMGraph /\ X e. dom I ) -> ( I ` X ) e. { e e. ( ~P V \ { (/) } ) | ( # ` e ) = 2 } )
35 prprrab
 |-  { e e. ( ~P V \ { (/) } ) | ( # ` e ) = 2 } = { e e. ~P V | ( # ` e ) = 2 }
36 34 35 eleqtrdi
 |-  ( ( S SubGraph G /\ G e. UMGraph /\ X e. dom I ) -> ( I ` X ) e. { e e. ~P V | ( # ` e ) = 2 } )