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 \in V ⟼ \{w \in (2 WSPathsN G) \| w (1) = a\})$
Assertion	fusgreg2wsplem	$⊢ N \in V \to (p \in M (N) \leftrightarrow (p \in (2 WSPathsN G) \land p (1) = N))$

Step	Hyp	Ref	Expression
1		frgrhash2wsp.v	$⊢ V = Vtx (G)$
2		fusgreg2wsp.m	$⊢ M = (a \in V ⟼ \{w \in (2 WSPathsN G) \| w (1) = a\})$
3		eqeq2	$⊢ a = N \to (w (1) = a \leftrightarrow w (1) = N)$
4	3	rabbidv	$⊢ a = N \to \{w \in (2 WSPathsN G) \| w (1) = a\} = \{w \in (2 WSPathsN G) \| w (1) = N\}$
5		ovex	$⊢ 2 WSPathsN G \in V$
6	5	rabex	$⊢ \{w \in (2 WSPathsN G) \| w (1) = N\} \in V$
7	4 2 6	fvmpt	$⊢ N \in V \to M (N) = \{w \in (2 WSPathsN G) \| w (1) = N\}$
8	7	eleq2d	$⊢ N \in V \to (p \in M (N) \leftrightarrow p \in \{w \in (2 WSPathsN G) \| w (1) = N\})$
9		fveq1	$⊢ w = p \to w (1) = p (1)$
10	9	eqeq1d	$⊢ w = p \to (w (1) = N \leftrightarrow p (1) = N)$
11	10	elrab	$⊢ p \in \{w \in (2 WSPathsN G) \| w (1) = N\} \leftrightarrow (p \in (2 WSPathsN G) \land p (1) = N)$
12	8 11	bitrdi	$⊢ N \in V \to (p \in M (N) \leftrightarrow (p \in (2 WSPathsN G) \land p (1) = N))$

Metamath Proof Explorer