This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem structvtxvallem

Description: Lemma for structvtxval and structiedg0val . (Contributed by AV, 23-Sep-2020) (Revised 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 structvtxvallem 
|- ( ( V e. X /\ E e. Y ) -> 2 <_ ( # ` dom 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 fvexd 
 |-  ( ( V e. X /\ E e. Y ) -> ( Base ` ndx ) e. _V )
5 1 a1i 
 |-  ( ( V e. X /\ E e. Y ) -> S e. NN )
6 simpl 
 |-  ( ( V e. X /\ E e. Y ) -> V e. X )
7 simpr 
 |-  ( ( V e. X /\ E e. Y ) -> E e. Y )
8 prex 
 |-  { <. ( Base ` ndx ) , V >. , <. S , E >. } e. _V
9 3 8 eqeltri 
 |-  G e. _V
10 9 a1i 
 |-  ( ( V e. X /\ E e. Y ) -> G e. _V )
11 basendxnn 
 |-  ( Base ` ndx ) e. NN
12 11 nnrei 
 |-  ( Base ` ndx ) e. RR
13 12 2 ltneii 
 |-  ( Base ` ndx ) =/= S
14 13 a1i 
 |-  ( ( V e. X /\ E e. Y ) -> ( Base ` ndx ) =/= S )
15 3 eqimss2i 
 |-  { <. ( Base ` ndx ) , V >. , <. S , E >. } C_ G
16 15 a1i 
 |-  ( ( V e. X /\ E e. Y ) -> { <. ( Base ` ndx ) , V >. , <. S , E >. } C_ G )
17 4 5 6 7 10 14 16 hashdmpropge2 
 |-  ( ( V e. X /\ E e. Y ) -> 2 <_ ( # ` dom G ) )