Metamath Proof Explorer

Theorem fusgreg2wsplem

Description: Lemma for fusgreg2wsp and related theorems. (Contributed by AV, 8-Jan-2022)

Ref Expression
Hypotheses frgrhash2wsp.v ⊢ V = Vtx ⁡ G
fusgreg2wsp.m ⊢ M = a ∈ V ⟼ w ∈ 2 WSPathsN G | w ⁡ 1 = a
Assertion fusgreg2wsplem ⊢ N ∈ V → p ∈ M ⁡ N ↔ p ∈ 2 WSPathsN G ∧ p ⁡ 1 = N

Proof

Step Hyp Ref Expression
1 frgrhash2wsp.v ⊢ V = Vtx ⁡ G
2 fusgreg2wsp.m ⊢ M = a ∈ V ⟼ w ∈ 2 WSPathsN G | w ⁡ 1 = a
3 eqeq2 ⊢ a = N → w ⁡ 1 = a ↔ w ⁡ 1 = N
4 3 rabbidv ⊢ a = N → w ∈ 2 WSPathsN G | w ⁡ 1 = a = w ∈ 2 WSPathsN G | w ⁡ 1 = N
5 ovex ⊢ 2 WSPathsN G ∈ V
6 5 rabex ⊢ w ∈ 2 WSPathsN G | w ⁡ 1 = N ∈ V
7 4 2 6 fvmpt ⊢ N ∈ V → M ⁡ N = w ∈ 2 WSPathsN G | w ⁡ 1 = N
8 7 eleq2d ⊢ N ∈ V → p ∈ M ⁡ N ↔ p ∈ w ∈ 2 WSPathsN G | w ⁡ 1 = N
9 fveq1 ⊢ w = p → w ⁡ 1 = p ⁡ 1
10 9 eqeq1d ⊢ w = p → w ⁡ 1 = N ↔ p ⁡ 1 = N
11 10 elrab ⊢ p ∈ w ∈ 2 WSPathsN G | w ⁡ 1 = N ↔ p ∈ 2 WSPathsN G ∧ p ⁡ 1 = N
12 8 11 bitrdi ⊢ N ∈ V → p ∈ M ⁡ N ↔ p ∈ 2 WSPathsN G ∧ p ⁡ 1 = N