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

Metamath Proof Explorer

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 ∧ 𝑌 ∈ 𝐴 ) → ( ℩ 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑌 ) = { 𝑧 , 𝑁 } ) ∈ 𝑉 )