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

Metamath Proof Explorer

Theorem structgrssvtxlem

Description: Lemma for structgrssvtx and structgrssiedg . (Contributed by AV, 14-Oct-2020) (Proof shortened by AV, 12-Nov-2021)

Ref Expression
Hypotheses structgrssvtx.g 
|- ( ph -> G Struct X )
structgrssvtx.v 
|- ( ph -> V e. Y )
structgrssvtx.e 
|- ( ph -> E e. Z )
structgrssvtx.s 
|- ( ph -> { <. ( Base ` ndx ) , V >. , <. ( .ef ` ndx ) , E >. } C_ G )
Assertion structgrssvtxlem 
|- ( ph -> 2 <_ ( # ` dom G ) )

Proof

Step Hyp Ref Expression
1 structgrssvtx.g 
 |-  ( ph -> G Struct X )
2 structgrssvtx.v 
 |-  ( ph -> V e. Y )
3 structgrssvtx.e 
 |-  ( ph -> E e. Z )
4 structgrssvtx.s 
 |-  ( ph -> { <. ( Base ` ndx ) , V >. , <. ( .ef ` ndx ) , E >. } C_ G )
5 fvexd 
 |-  ( ph -> ( Base ` ndx ) e. _V )
6 fvexd 
 |-  ( ph -> ( .ef ` ndx ) e. _V )
7 structex 
 |-  ( G Struct X -> G e. _V )
8 1 7 syl 
 |-  ( ph -> G e. _V )
9 basendxnedgfndx 
 |-  ( Base ` ndx ) =/= ( .ef ` ndx )
10 9 a1i 
 |-  ( ph -> ( Base ` ndx ) =/= ( .ef ` ndx ) )
11 5 6 2 3 8 10 4 hashdmpropge2 
 |-  ( ph -> 2 <_ ( # ` dom G ) )