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 } )