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

Metamath Proof Explorer

Theorem usgredg2vlem2

Description: Lemma 2 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 usgredg2vlem2 ( ( 𝐺 ∈ 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 6 biimpi ⊢ ( 𝑌 ∈ 𝐴 → ( 𝑌 ∈ dom 𝐸 ∧ 𝑁 ∈ ( 𝐸 ‘ 𝑌 ) ) )
8 1 2 usgredgreu ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑌 ∈ dom 𝐸 ∧ 𝑁 ∈ ( 𝐸 ‘ 𝑌 ) ) → ∃! 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑌 ) = { 𝑁 , 𝑧 } )
9 8 3expb ⊢ ( ( 𝐺 ∈ USGraph ∧ ( 𝑌 ∈ dom 𝐸 ∧ 𝑁 ∈ ( 𝐸 ‘ 𝑌 ) ) ) → ∃! 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑌 ) = { 𝑁 , 𝑧 } )
10 1 2 3 usgredg2vlem1 ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑌 ∈ 𝐴 ) → ( ℩ 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑌 ) = { 𝑧 , 𝑁 } ) ∈ 𝑉 )
11 10 adantlr ⊢ ( ( ( 𝐺 ∈ USGraph ∧ ( 𝑌 ∈ dom 𝐸 ∧ 𝑁 ∈ ( 𝐸 ‘ 𝑌 ) ) ) ∧ 𝑌 ∈ 𝐴 ) → ( ℩ 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑌 ) = { 𝑧 , 𝑁 } ) ∈ 𝑉 )
12 11 ad4ant23 ⊢ ( ( ( ( ∃! 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑌 ) = { 𝑁 , 𝑧 } ∧ ( 𝐺 ∈ USGraph ∧ ( 𝑌 ∈ dom 𝐸 ∧ 𝑁 ∈ ( 𝐸 ‘ 𝑌 ) ) ) ) ∧ 𝑌 ∈ 𝐴 ) ∧ 𝐼 = ( ℩ 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑌 ) = { 𝑧 , 𝑁 } ) ) → ( ℩ 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑌 ) = { 𝑧 , 𝑁 } ) ∈ 𝑉 )
13 eleq1 ⊢ ( 𝐼 = ( ℩ 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑌 ) = { 𝑧 , 𝑁 } ) → ( 𝐼 ∈ 𝑉 ↔ ( ℩ 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑌 ) = { 𝑧 , 𝑁 } ) ∈ 𝑉 ) )
14 13 adantl ⊢ ( ( ( ( ∃! 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑌 ) = { 𝑁 , 𝑧 } ∧ ( 𝐺 ∈ USGraph ∧ ( 𝑌 ∈ dom 𝐸 ∧ 𝑁 ∈ ( 𝐸 ‘ 𝑌 ) ) ) ) ∧ 𝑌 ∈ 𝐴 ) ∧ 𝐼 = ( ℩ 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑌 ) = { 𝑧 , 𝑁 } ) ) → ( 𝐼 ∈ 𝑉 ↔ ( ℩ 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑌 ) = { 𝑧 , 𝑁 } ) ∈ 𝑉 ) )
15 12 14 mpbird ⊢ ( ( ( ( ∃! 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑌 ) = { 𝑁 , 𝑧 } ∧ ( 𝐺 ∈ USGraph ∧ ( 𝑌 ∈ dom 𝐸 ∧ 𝑁 ∈ ( 𝐸 ‘ 𝑌 ) ) ) ) ∧ 𝑌 ∈ 𝐴 ) ∧ 𝐼 = ( ℩ 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑌 ) = { 𝑧 , 𝑁 } ) ) → 𝐼 ∈ 𝑉 )
16 prcom ⊢ { 𝑁 , 𝑧 } = { 𝑧 , 𝑁 }
17 16 eqeq2i ⊢ ( ( 𝐸 ‘ 𝑌 ) = { 𝑁 , 𝑧 } ↔ ( 𝐸 ‘ 𝑌 ) = { 𝑧 , 𝑁 } )
18 17 reubii ⊢ ( ∃! 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑌 ) = { 𝑁 , 𝑧 } ↔ ∃! 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑌 ) = { 𝑧 , 𝑁 } )
19 18 biimpi ⊢ ( ∃! 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑌 ) = { 𝑁 , 𝑧 } → ∃! 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑌 ) = { 𝑧 , 𝑁 } )
20 19 ad3antrrr ⊢ ( ( ( ( ∃! 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑌 ) = { 𝑁 , 𝑧 } ∧ ( 𝐺 ∈ USGraph ∧ ( 𝑌 ∈ dom 𝐸 ∧ 𝑁 ∈ ( 𝐸 ‘ 𝑌 ) ) ) ) ∧ 𝑌 ∈ 𝐴 ) ∧ 𝐼 = ( ℩ 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑌 ) = { 𝑧 , 𝑁 } ) ) → ∃! 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑌 ) = { 𝑧 , 𝑁 } )
21 preq1 ⊢ ( 𝑧 = 𝐼 → { 𝑧 , 𝑁 } = { 𝐼 , 𝑁 } )
22 21 eqeq2d ⊢ ( 𝑧 = 𝐼 → ( ( 𝐸 ‘ 𝑌 ) = { 𝑧 , 𝑁 } ↔ ( 𝐸 ‘ 𝑌 ) = { 𝐼 , 𝑁 } ) )
23 22 riota2 ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ∃! 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑌 ) = { 𝑧 , 𝑁 } ) → ( ( 𝐸 ‘ 𝑌 ) = { 𝐼 , 𝑁 } ↔ ( ℩ 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑌 ) = { 𝑧 , 𝑁 } ) = 𝐼 ) )
24 15 20 23 syl2anc ⊢ ( ( ( ( ∃! 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑌 ) = { 𝑁 , 𝑧 } ∧ ( 𝐺 ∈ USGraph ∧ ( 𝑌 ∈ dom 𝐸 ∧ 𝑁 ∈ ( 𝐸 ‘ 𝑌 ) ) ) ) ∧ 𝑌 ∈ 𝐴 ) ∧ 𝐼 = ( ℩ 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑌 ) = { 𝑧 , 𝑁 } ) ) → ( ( 𝐸 ‘ 𝑌 ) = { 𝐼 , 𝑁 } ↔ ( ℩ 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑌 ) = { 𝑧 , 𝑁 } ) = 𝐼 ) )
25 24 exbiri ⊢ ( ( ( ∃! 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑌 ) = { 𝑁 , 𝑧 } ∧ ( 𝐺 ∈ USGraph ∧ ( 𝑌 ∈ dom 𝐸 ∧ 𝑁 ∈ ( 𝐸 ‘ 𝑌 ) ) ) ) ∧ 𝑌 ∈ 𝐴 ) → ( 𝐼 = ( ℩ 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑌 ) = { 𝑧 , 𝑁 } ) → ( ( ℩ 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑌 ) = { 𝑧 , 𝑁 } ) = 𝐼 → ( 𝐸 ‘ 𝑌 ) = { 𝐼 , 𝑁 } ) ) )
26 25 com13 ⊢ ( ( ℩ 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑌 ) = { 𝑧 , 𝑁 } ) = 𝐼 → ( 𝐼 = ( ℩ 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑌 ) = { 𝑧 , 𝑁 } ) → ( ( ( ∃! 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑌 ) = { 𝑁 , 𝑧 } ∧ ( 𝐺 ∈ USGraph ∧ ( 𝑌 ∈ dom 𝐸 ∧ 𝑁 ∈ ( 𝐸 ‘ 𝑌 ) ) ) ) ∧ 𝑌 ∈ 𝐴 ) → ( 𝐸 ‘ 𝑌 ) = { 𝐼 , 𝑁 } ) ) )
27 26 eqcoms ⊢ ( 𝐼 = ( ℩ 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑌 ) = { 𝑧 , 𝑁 } ) → ( 𝐼 = ( ℩ 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑌 ) = { 𝑧 , 𝑁 } ) → ( ( ( ∃! 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑌 ) = { 𝑁 , 𝑧 } ∧ ( 𝐺 ∈ USGraph ∧ ( 𝑌 ∈ dom 𝐸 ∧ 𝑁 ∈ ( 𝐸 ‘ 𝑌 ) ) ) ) ∧ 𝑌 ∈ 𝐴 ) → ( 𝐸 ‘ 𝑌 ) = { 𝐼 , 𝑁 } ) ) )
28 27 pm2.43i ⊢ ( 𝐼 = ( ℩ 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑌 ) = { 𝑧 , 𝑁 } ) → ( ( ( ∃! 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑌 ) = { 𝑁 , 𝑧 } ∧ ( 𝐺 ∈ USGraph ∧ ( 𝑌 ∈ dom 𝐸 ∧ 𝑁 ∈ ( 𝐸 ‘ 𝑌 ) ) ) ) ∧ 𝑌 ∈ 𝐴 ) → ( 𝐸 ‘ 𝑌 ) = { 𝐼 , 𝑁 } ) )
29 28 expdcom ⊢ ( ( ∃! 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑌 ) = { 𝑁 , 𝑧 } ∧ ( 𝐺 ∈ USGraph ∧ ( 𝑌 ∈ dom 𝐸 ∧ 𝑁 ∈ ( 𝐸 ‘ 𝑌 ) ) ) ) → ( 𝑌 ∈ 𝐴 → ( 𝐼 = ( ℩ 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑌 ) = { 𝑧 , 𝑁 } ) → ( 𝐸 ‘ 𝑌 ) = { 𝐼 , 𝑁 } ) ) )
30 9 29 mpancom ⊢ ( ( 𝐺 ∈ USGraph ∧ ( 𝑌 ∈ dom 𝐸 ∧ 𝑁 ∈ ( 𝐸 ‘ 𝑌 ) ) ) → ( 𝑌 ∈ 𝐴 → ( 𝐼 = ( ℩ 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑌 ) = { 𝑧 , 𝑁 } ) → ( 𝐸 ‘ 𝑌 ) = { 𝐼 , 𝑁 } ) ) )
31 30 expcom ⊢ ( ( 𝑌 ∈ dom 𝐸 ∧ 𝑁 ∈ ( 𝐸 ‘ 𝑌 ) ) → ( 𝐺 ∈ USGraph → ( 𝑌 ∈ 𝐴 → ( 𝐼 = ( ℩ 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑌 ) = { 𝑧 , 𝑁 } ) → ( 𝐸 ‘ 𝑌 ) = { 𝐼 , 𝑁 } ) ) ) )
32 31 com23 ⊢ ( ( 𝑌 ∈ dom 𝐸 ∧ 𝑁 ∈ ( 𝐸 ‘ 𝑌 ) ) → ( 𝑌 ∈ 𝐴 → ( 𝐺 ∈ USGraph → ( 𝐼 = ( ℩ 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑌 ) = { 𝑧 , 𝑁 } ) → ( 𝐸 ‘ 𝑌 ) = { 𝐼 , 𝑁 } ) ) ) )
33 7 32 mpcom ⊢ ( 𝑌 ∈ 𝐴 → ( 𝐺 ∈ USGraph → ( 𝐼 = ( ℩ 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑌 ) = { 𝑧 , 𝑁 } ) → ( 𝐸 ‘ 𝑌 ) = { 𝐼 , 𝑁 } ) ) )
34 33 impcom ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑌 ∈ 𝐴 ) → ( 𝐼 = ( ℩ 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑌 ) = { 𝑧 , 𝑁 } ) → ( 𝐸 ‘ 𝑌 ) = { 𝐼 , 𝑁 } ) )