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 ∈ ℕ
structvtxvallem.b ⊢ Base ndx < S
structvtxvallem.g ⊢ G = Base ndx V S E
Assertion structvtxvallem ⊢ V ∈ X ∧ E ∈ Y → 2 ≤ dom ⁡ G

Proof

Step Hyp Ref Expression
1 structvtxvallem.s ⊢ S ∈ ℕ
2 structvtxvallem.b ⊢ Base ndx < S
3 structvtxvallem.g ⊢ G = Base ndx V S E
4 fvexd ⊢ V ∈ X ∧ E ∈ Y → Base ndx ∈ V
5 1 a1i ⊢ V ∈ X ∧ E ∈ Y → S ∈ ℕ
6 simpl ⊢ V ∈ X ∧ E ∈ Y → V ∈ X
7 simpr ⊢ V ∈ X ∧ E ∈ Y → E ∈ Y
8 prex ⊢ Base ndx V S E ∈ V
9 3 8 eqeltri ⊢ G ∈ V
10 9 a1i ⊢ V ∈ X ∧ E ∈ Y → G ∈ V
11 basendxnn ⊢ Base ndx ∈ ℕ
12 11 nnrei ⊢ Base ndx ∈ ℝ
13 12 2 ltneii ⊢ Base ndx ≠ S
14 13 a1i ⊢ V ∈ X ∧ E ∈ Y → Base ndx ≠ S
15 3 eqimss2i ⊢ Base ndx V S E ⊆ G
16 15 a1i ⊢ V ∈ X ∧ E ∈ Y → Base ndx V S E ⊆ G
17 4 5 6 7 10 14 16 hashdmpropge2 ⊢ V ∈ X ∧ E ∈ Y → 2 ≤ dom ⁡ G