Step |
Hyp |
Ref |
Expression |
1 |
|
usgruhgr |
⊢ ( 𝐺 ∈ USGraph → 𝐺 ∈ UHGraph ) |
2 |
|
eqid |
⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 ) |
3 |
2
|
uhgredgiedgb |
⊢ ( 𝐺 ∈ UHGraph → ( 𝐸 ∈ ( Edg ‘ 𝐺 ) ↔ ∃ 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) 𝐸 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ) ) |
4 |
1 3
|
syl |
⊢ ( 𝐺 ∈ USGraph → ( 𝐸 ∈ ( Edg ‘ 𝐺 ) ↔ ∃ 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) 𝐸 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ) ) |
5 |
|
eqid |
⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 ) |
6 |
5 2
|
usgredgreu |
⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∧ 𝑌 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ) → ∃! 𝑦 ∈ ( Vtx ‘ 𝐺 ) ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = { 𝑌 , 𝑦 } ) |
7 |
6
|
3expia |
⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ) → ( 𝑌 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) → ∃! 𝑦 ∈ ( Vtx ‘ 𝐺 ) ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = { 𝑌 , 𝑦 } ) ) |
8 |
7
|
3adant3 |
⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∧ 𝐸 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ) → ( 𝑌 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) → ∃! 𝑦 ∈ ( Vtx ‘ 𝐺 ) ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = { 𝑌 , 𝑦 } ) ) |
9 |
|
eleq2 |
⊢ ( 𝐸 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) → ( 𝑌 ∈ 𝐸 ↔ 𝑌 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ) ) |
10 |
|
eqeq1 |
⊢ ( 𝐸 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) → ( 𝐸 = { 𝑌 , 𝑦 } ↔ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = { 𝑌 , 𝑦 } ) ) |
11 |
10
|
reubidv |
⊢ ( 𝐸 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) → ( ∃! 𝑦 ∈ ( Vtx ‘ 𝐺 ) 𝐸 = { 𝑌 , 𝑦 } ↔ ∃! 𝑦 ∈ ( Vtx ‘ 𝐺 ) ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = { 𝑌 , 𝑦 } ) ) |
12 |
9 11
|
imbi12d |
⊢ ( 𝐸 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) → ( ( 𝑌 ∈ 𝐸 → ∃! 𝑦 ∈ ( Vtx ‘ 𝐺 ) 𝐸 = { 𝑌 , 𝑦 } ) ↔ ( 𝑌 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) → ∃! 𝑦 ∈ ( Vtx ‘ 𝐺 ) ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = { 𝑌 , 𝑦 } ) ) ) |
13 |
12
|
3ad2ant3 |
⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∧ 𝐸 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ) → ( ( 𝑌 ∈ 𝐸 → ∃! 𝑦 ∈ ( Vtx ‘ 𝐺 ) 𝐸 = { 𝑌 , 𝑦 } ) ↔ ( 𝑌 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) → ∃! 𝑦 ∈ ( Vtx ‘ 𝐺 ) ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = { 𝑌 , 𝑦 } ) ) ) |
14 |
8 13
|
mpbird |
⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∧ 𝐸 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ) → ( 𝑌 ∈ 𝐸 → ∃! 𝑦 ∈ ( Vtx ‘ 𝐺 ) 𝐸 = { 𝑌 , 𝑦 } ) ) |
15 |
14
|
3exp |
⊢ ( 𝐺 ∈ USGraph → ( 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) → ( 𝐸 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) → ( 𝑌 ∈ 𝐸 → ∃! 𝑦 ∈ ( Vtx ‘ 𝐺 ) 𝐸 = { 𝑌 , 𝑦 } ) ) ) ) |
16 |
15
|
rexlimdv |
⊢ ( 𝐺 ∈ USGraph → ( ∃ 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) 𝐸 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) → ( 𝑌 ∈ 𝐸 → ∃! 𝑦 ∈ ( Vtx ‘ 𝐺 ) 𝐸 = { 𝑌 , 𝑦 } ) ) ) |
17 |
4 16
|
sylbid |
⊢ ( 𝐺 ∈ USGraph → ( 𝐸 ∈ ( Edg ‘ 𝐺 ) → ( 𝑌 ∈ 𝐸 → ∃! 𝑦 ∈ ( Vtx ‘ 𝐺 ) 𝐸 = { 𝑌 , 𝑦 } ) ) ) |
18 |
17
|
3imp |
⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐸 ∈ ( Edg ‘ 𝐺 ) ∧ 𝑌 ∈ 𝐸 ) → ∃! 𝑦 ∈ ( Vtx ‘ 𝐺 ) 𝐸 = { 𝑌 , 𝑦 } ) |