Theorem fusgreg2wsplem

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

	Ref	Expression
Hypotheses	frgrhash2wsp.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	fusgreg2wsp.m	⊢ 𝑀 = ( 𝑎 ∈ 𝑉 ↦ { 𝑤 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑤 ‘ 1 ) = 𝑎 } )
Assertion	fusgreg2wsplem	⊢ ( 𝑁 ∈ 𝑉 → ( 𝑝 ∈ ( 𝑀 ‘ 𝑁 ) ↔ ( 𝑝 ∈ ( 2 WSPathsN 𝐺 ) ∧ ( 𝑝 ‘ 1 ) = 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		frgrhash2wsp.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		fusgreg2wsp.m	⊢ 𝑀 = ( 𝑎 ∈ 𝑉 ↦ { 𝑤 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑤 ‘ 1 ) = 𝑎 } )
3		eqeq2	⊢ ( 𝑎 = 𝑁 → ( ( 𝑤 ‘ 1 ) = 𝑎 ↔ ( 𝑤 ‘ 1 ) = 𝑁 ) )
4	3	rabbidv	⊢ ( 𝑎 = 𝑁 → { 𝑤 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑤 ‘ 1 ) = 𝑎 } = { 𝑤 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑤 ‘ 1 ) = 𝑁 } )
5		ovex	⊢ ( 2 WSPathsN 𝐺 ) ∈ V
6	5	rabex	⊢ { 𝑤 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑤 ‘ 1 ) = 𝑁 } ∈ V
7	4 2 6	fvmpt	⊢ ( 𝑁 ∈ 𝑉 → ( 𝑀 ‘ 𝑁 ) = { 𝑤 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑤 ‘ 1 ) = 𝑁 } )
8	7	eleq2d	⊢ ( 𝑁 ∈ 𝑉 → ( 𝑝 ∈ ( 𝑀 ‘ 𝑁 ) ↔ 𝑝 ∈ { 𝑤 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑤 ‘ 1 ) = 𝑁 } ) )
9		fveq1	⊢ ( 𝑤 = 𝑝 → ( 𝑤 ‘ 1 ) = ( 𝑝 ‘ 1 ) )
10	9	eqeq1d	⊢ ( 𝑤 = 𝑝 → ( ( 𝑤 ‘ 1 ) = 𝑁 ↔ ( 𝑝 ‘ 1 ) = 𝑁 ) )
11	10	elrab	⊢ ( 𝑝 ∈ { 𝑤 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑤 ‘ 1 ) = 𝑁 } ↔ ( 𝑝 ∈ ( 2 WSPathsN 𝐺 ) ∧ ( 𝑝 ‘ 1 ) = 𝑁 ) )
12	8 11	bitrdi	⊢ ( 𝑁 ∈ 𝑉 → ( 𝑝 ∈ ( 𝑀 ‘ 𝑁 ) ↔ ( 𝑝 ∈ ( 2 WSPathsN 𝐺 ) ∧ ( 𝑝 ‘ 1 ) = 𝑁 ) ) )