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

Metamath Proof Explorer

Theorem cplgr1vlem

Description: Lemma for cplgr1v and cusgr1v . (Contributed by AV, 23-Mar-2021)

Ref Expression
Hypothesis cplgr0v.v ⊢ V = Vtx ⁡ G
Assertion cplgr1vlem ⊢ V = 1 → G ∈ V

Proof

Step Hyp Ref Expression
1 cplgr0v.v ⊢ V = Vtx ⁡ G
2 1 fvexi ⊢ V ∈ V
3 hash1snb ⊢ V ∈ V → V = 1 ↔ ∃ n V = n
4 2 3 ax-mp ⊢ V = 1 ↔ ∃ n V = n
5 vsnid ⊢ n ∈ n
6 eleq2 ⊢ V = n → n ∈ V ↔ n ∈ n
7 5 6 mpbiri ⊢ V = n → n ∈ V
8 1 1vgrex ⊢ n ∈ V → G ∈ V
9 7 8 syl ⊢ V = n → G ∈ V
10 9 exlimiv ⊢ ∃ n V = n → G ∈ V
11 4 10 sylbi ⊢ V = 1 → G ∈ V