Metamath Proof Explorer

Theorem snstriedgval

Description: The set of indexed edges of a graph without edges represented as an extensible structure with vertices as base set and no indexed edges. See iedgvalsnop for the (degenerate) case where V = ( Basendx ) . (Contributed by AV, 24-Sep-2020)

Ref Expression
Hypotheses snstrvtxval.v 
|- V e. _V
snstrvtxval.g 
|- G = { <. ( Base ` ndx ) , V >. }
Assertion snstriedgval 
|- ( V =/= ( Base ` ndx ) -> ( iEdg ` G ) = (/) )

Proof

Step Hyp Ref Expression
1 snstrvtxval.v 
 |-  V e. _V
2 snstrvtxval.g 
 |-  G = { <. ( Base ` ndx ) , V >. }
3 iedgval 
 |-  ( iEdg ` G ) = if ( G e. ( _V X. _V ) , ( 2nd ` G ) , ( .ef ` G ) )
4 3 a1i 
 |-  ( V =/= ( Base ` ndx ) -> ( iEdg ` G ) = if ( G e. ( _V X. _V ) , ( 2nd ` G ) , ( .ef ` G ) ) )
5 necom 
 |-  ( V =/= ( Base ` ndx ) <-> ( Base ` ndx ) =/= V )
6 fvex 
 |-  ( Base ` ndx ) e. _V
7 6 1 2 funsndifnop 
 |-  ( ( Base ` ndx ) =/= V -> -. G e. ( _V X. _V ) )
8 5 7 sylbi 
 |-  ( V =/= ( Base ` ndx ) -> -. G e. ( _V X. _V ) )
9 8 iffalsed 
 |-  ( V =/= ( Base ` ndx ) -> if ( G e. ( _V X. _V ) , ( 2nd ` G ) , ( .ef ` G ) ) = ( .ef ` G ) )
10 snex 
 |-  { <. ( Base ` ndx ) , V >. } e. _V
11 10 a1i 
 |-  ( G = { <. ( Base ` ndx ) , V >. } -> { <. ( Base ` ndx ) , V >. } e. _V )
12 2 11 eqeltrid 
 |-  ( G = { <. ( Base ` ndx ) , V >. } -> G e. _V )
13 edgfndxid 
 |-  ( G e. _V -> ( .ef ` G ) = ( G ` ( .ef ` ndx ) ) )
14 2 12 13 mp2b 
 |-  ( .ef ` G ) = ( G ` ( .ef ` ndx ) )
15 basendxnedgfndx 
 |-  ( Base ` ndx ) =/= ( .ef ` ndx )
16 15 nesymi 
 |-  -. ( .ef ` ndx ) = ( Base ` ndx )
17 16 a1i 
 |-  ( V =/= ( Base ` ndx ) -> -. ( .ef ` ndx ) = ( Base ` ndx ) )
18 fvex 
 |-  ( .ef ` ndx ) e. _V
19 18 elsn 
 |-  ( ( .ef ` ndx ) e. { ( Base ` ndx ) } <-> ( .ef ` ndx ) = ( Base ` ndx ) )
20 17 19 sylnibr 
 |-  ( V =/= ( Base ` ndx ) -> -. ( .ef ` ndx ) e. { ( Base ` ndx ) } )
21 2 dmeqi 
 |-  dom G = dom { <. ( Base ` ndx ) , V >. }
22 dmsnopg 
 |-  ( V e. _V -> dom { <. ( Base ` ndx ) , V >. } = { ( Base ` ndx ) } )
23 1 22 mp1i 
 |-  ( V =/= ( Base ` ndx ) -> dom { <. ( Base ` ndx ) , V >. } = { ( Base ` ndx ) } )
24 21 23 eqtrid 
 |-  ( V =/= ( Base ` ndx ) -> dom G = { ( Base ` ndx ) } )
25 20 24 neleqtrrd 
 |-  ( V =/= ( Base ` ndx ) -> -. ( .ef ` ndx ) e. dom G )
26 ndmfv 
 |-  ( -. ( .ef ` ndx ) e. dom G -> ( G ` ( .ef ` ndx ) ) = (/) )
27 25 26 syl 
 |-  ( V =/= ( Base ` ndx ) -> ( G ` ( .ef ` ndx ) ) = (/) )
28 14 27 eqtrid 
 |-  ( V =/= ( Base ` ndx ) -> ( .ef ` G ) = (/) )
29 4 9 28 3eqtrd 
 |-  ( V =/= ( Base ` ndx ) -> ( iEdg ` G ) = (/) )