Theorem usgredg2vlem1

Description: Lemma 1 for usgredg2v . (Contributed by Alexander van der Vekens, 4-Jan-2018) (Revised by AV, 18-Oct-2020)

	Ref	Expression
Hypotheses	usgredg2v.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	usgredg2v.e	⊢ 𝐸 = ( iEdg ‘ 𝐺 )
	usgredg2v.a	⊢ 𝐴 = { 𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ ( 𝐸 ‘ 𝑥 ) }
Assertion	usgredg2vlem1	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑌 ∈ 𝐴 ) → ( ℩ 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑌 ) = { 𝑧 , 𝑁 } ) ∈ 𝑉 )

Proof

Step	Hyp	Ref	Expression
1		usgredg2v.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		usgredg2v.e	⊢ 𝐸 = ( iEdg ‘ 𝐺 )
3		usgredg2v.a	⊢ 𝐴 = { 𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ ( 𝐸 ‘ 𝑥 ) }
4		fveq2	⊢ ( 𝑥 = 𝑌 → ( 𝐸 ‘ 𝑥 ) = ( 𝐸 ‘ 𝑌 ) )
5	4	eleq2d	⊢ ( 𝑥 = 𝑌 → ( 𝑁 ∈ ( 𝐸 ‘ 𝑥 ) ↔ 𝑁 ∈ ( 𝐸 ‘ 𝑌 ) ) )
6	5 3	elrab2	⊢ ( 𝑌 ∈ 𝐴 ↔ ( 𝑌 ∈ dom 𝐸 ∧ 𝑁 ∈ ( 𝐸 ‘ 𝑌 ) ) )
7	1 2	usgredgreu	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑌 ∈ dom 𝐸 ∧ 𝑁 ∈ ( 𝐸 ‘ 𝑌 ) ) → ∃! 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑌 ) = { 𝑁 , 𝑧 } )
8		prcom	⊢ { 𝑁 , 𝑧 } = { 𝑧 , 𝑁 }
9	8	eqeq2i	⊢ ( ( 𝐸 ‘ 𝑌 ) = { 𝑁 , 𝑧 } ↔ ( 𝐸 ‘ 𝑌 ) = { 𝑧 , 𝑁 } )
10	9	reubii	⊢ ( ∃! 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑌 ) = { 𝑁 , 𝑧 } ↔ ∃! 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑌 ) = { 𝑧 , 𝑁 } )
11	7 10	sylib	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑌 ∈ dom 𝐸 ∧ 𝑁 ∈ ( 𝐸 ‘ 𝑌 ) ) → ∃! 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑌 ) = { 𝑧 , 𝑁 } )
12	11	3expb	⊢ ( ( 𝐺 ∈ USGraph ∧ ( 𝑌 ∈ dom 𝐸 ∧ 𝑁 ∈ ( 𝐸 ‘ 𝑌 ) ) ) → ∃! 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑌 ) = { 𝑧 , 𝑁 } )
13		riotacl	⊢ ( ∃! 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑌 ) = { 𝑧 , 𝑁 } → ( ℩ 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑌 ) = { 𝑧 , 𝑁 } ) ∈ 𝑉 )
14	12 13	syl	⊢ ( ( 𝐺 ∈ USGraph ∧ ( 𝑌 ∈ dom 𝐸 ∧ 𝑁 ∈ ( 𝐸 ‘ 𝑌 ) ) ) → ( ℩ 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑌 ) = { 𝑧 , 𝑁 } ) ∈ 𝑉 )
15	6 14	sylan2b	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑌 ∈ 𝐴 ) → ( ℩ 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑌 ) = { 𝑧 , 𝑁 } ) ∈ 𝑉 )