Metamath Proof Explorer

Theorem structiedg0val

Description: The set of indexed edges of an extensible structure with a base set and another slot not being the slot for edge functions is empty. (Contributed by AV, 23-Sep-2020) (Proof shortened by AV, 12-Nov-2021)

Ref Expression
Hypotheses structvtxvallem.s 
|- S e. NN
structvtxvallem.b 
|- ( Base ` ndx ) < S
structvtxvallem.g 
|- G = { <. ( Base ` ndx ) , V >. , <. S , E >. }
Assertion structiedg0val 
|- ( ( V e. X /\ E e. Y /\ S =/= ( .ef ` ndx ) ) -> ( iEdg ` G ) = (/) )

Proof

Step Hyp Ref Expression
1 structvtxvallem.s 
 |-  S e. NN
2 structvtxvallem.b 
 |-  ( Base ` ndx ) < S
3 structvtxvallem.g 
 |-  G = { <. ( Base ` ndx ) , V >. , <. S , E >. }
4 3 2 1 2strstr1 
 |-  G Struct <. ( Base ` ndx ) , S >.
5 structn0fun 
 |-  ( G Struct <. ( Base ` ndx ) , S >. -> Fun ( G \ { (/) } ) )
6 1 2 3 structvtxvallem 
 |-  ( ( V e. X /\ E e. Y ) -> 2 <_ ( # ` dom G ) )
7 funiedgdmge2val 
 |-  ( ( Fun ( G \ { (/) } ) /\ 2 <_ ( # ` dom G ) ) -> ( iEdg ` G ) = ( .ef ` G ) )
8 5 6 7 syl2an 
 |-  ( ( G Struct <. ( Base ` ndx ) , S >. /\ ( V e. X /\ E e. Y ) ) -> ( iEdg ` G ) = ( .ef ` G ) )
9 4 8 mpan 
 |-  ( ( V e. X /\ E e. Y ) -> ( iEdg ` G ) = ( .ef ` G ) )
10 9 3adant3 
 |-  ( ( V e. X /\ E e. Y /\ S =/= ( .ef ` ndx ) ) -> ( iEdg ` G ) = ( .ef ` G ) )
11 prex 
 |-  { <. ( Base ` ndx ) , V >. , <. S , E >. } e. _V
12 11 a1i 
 |-  ( G = { <. ( Base ` ndx ) , V >. , <. S , E >. } -> { <. ( Base ` ndx ) , V >. , <. S , E >. } e. _V )
13 3 12 eqeltrid 
 |-  ( G = { <. ( Base ` ndx ) , V >. , <. S , E >. } -> G e. _V )
14 edgfndxid 
 |-  ( G e. _V -> ( .ef ` G ) = ( G ` ( .ef ` ndx ) ) )
15 3 13 14 mp2b 
 |-  ( .ef ` G ) = ( G ` ( .ef ` ndx ) )
16 slotsbaseefdif 
 |-  ( Base ` ndx ) =/= ( .ef ` ndx )
17 16 nesymi 
 |-  -. ( .ef ` ndx ) = ( Base ` ndx )
18 17 a1i 
 |-  ( ( V e. X /\ E e. Y /\ S =/= ( .ef ` ndx ) ) -> -. ( .ef ` ndx ) = ( Base ` ndx ) )
19 neneq 
 |-  ( S =/= ( .ef ` ndx ) -> -. S = ( .ef ` ndx ) )
20 eqcom 
 |-  ( ( .ef ` ndx ) = S <-> S = ( .ef ` ndx ) )
21 19 20 sylnibr 
 |-  ( S =/= ( .ef ` ndx ) -> -. ( .ef ` ndx ) = S )
22 21 3ad2ant3 
 |-  ( ( V e. X /\ E e. Y /\ S =/= ( .ef ` ndx ) ) -> -. ( .ef ` ndx ) = S )
23 ioran 
 |-  ( -. ( ( .ef ` ndx ) = ( Base ` ndx ) \/ ( .ef ` ndx ) = S ) <-> ( -. ( .ef ` ndx ) = ( Base ` ndx ) /\ -. ( .ef ` ndx ) = S ) )
24 18 22 23 sylanbrc 
 |-  ( ( V e. X /\ E e. Y /\ S =/= ( .ef ` ndx ) ) -> -. ( ( .ef ` ndx ) = ( Base ` ndx ) \/ ( .ef ` ndx ) = S ) )
25 fvex 
 |-  ( .ef ` ndx ) e. _V
26 25 elpr 
 |-  ( ( .ef ` ndx ) e. { ( Base ` ndx ) , S } <-> ( ( .ef ` ndx ) = ( Base ` ndx ) \/ ( .ef ` ndx ) = S ) )
27 24 26 sylnibr 
 |-  ( ( V e. X /\ E e. Y /\ S =/= ( .ef ` ndx ) ) -> -. ( .ef ` ndx ) e. { ( Base ` ndx ) , S } )
28 3 dmeqi 
 |-  dom G = dom { <. ( Base ` ndx ) , V >. , <. S , E >. }
29 dmpropg 
 |-  ( ( V e. X /\ E e. Y ) -> dom { <. ( Base ` ndx ) , V >. , <. S , E >. } = { ( Base ` ndx ) , S } )
30 29 3adant3 
 |-  ( ( V e. X /\ E e. Y /\ S =/= ( .ef ` ndx ) ) -> dom { <. ( Base ` ndx ) , V >. , <. S , E >. } = { ( Base ` ndx ) , S } )
31 28 30 syl5eq 
 |-  ( ( V e. X /\ E e. Y /\ S =/= ( .ef ` ndx ) ) -> dom G = { ( Base ` ndx ) , S } )
32 27 31 neleqtrrd 
 |-  ( ( V e. X /\ E e. Y /\ S =/= ( .ef ` ndx ) ) -> -. ( .ef ` ndx ) e. dom G )
33 ndmfv 
 |-  ( -. ( .ef ` ndx ) e. dom G -> ( G ` ( .ef ` ndx ) ) = (/) )
34 32 33 syl 
 |-  ( ( V e. X /\ E e. Y /\ S =/= ( .ef ` ndx ) ) -> ( G ` ( .ef ` ndx ) ) = (/) )
35 15 34 syl5eq 
 |-  ( ( V e. X /\ E e. Y /\ S =/= ( .ef ` ndx ) ) -> ( .ef ` G ) = (/) )
36 10 35 eqtrd 
 |-  ( ( V e. X /\ E e. Y /\ S =/= ( .ef ` ndx ) ) -> ( iEdg ` G ) = (/) )