Step |
Hyp |
Ref |
Expression |
1 |
|
nbusgrf1o1.v |
⊢ 𝑉 = ( Vtx ‘ 𝐺 ) |
2 |
|
nbusgrf1o1.e |
⊢ 𝐸 = ( Edg ‘ 𝐺 ) |
3 |
|
nbusgrf1o1.n |
⊢ 𝑁 = ( 𝐺 NeighbVtx 𝑈 ) |
4 |
|
nbusgrf1o1.i |
⊢ 𝐼 = { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } |
5 |
|
nbusgrf1o.f |
⊢ 𝐹 = ( 𝑛 ∈ 𝑁 ↦ { 𝑈 , 𝑛 } ) |
6 |
3
|
eleq2i |
⊢ ( 𝑛 ∈ 𝑁 ↔ 𝑛 ∈ ( 𝐺 NeighbVtx 𝑈 ) ) |
7 |
2
|
nbusgreledg |
⊢ ( 𝐺 ∈ USGraph → ( 𝑛 ∈ ( 𝐺 NeighbVtx 𝑈 ) ↔ { 𝑛 , 𝑈 } ∈ 𝐸 ) ) |
8 |
7
|
adantr |
⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) → ( 𝑛 ∈ ( 𝐺 NeighbVtx 𝑈 ) ↔ { 𝑛 , 𝑈 } ∈ 𝐸 ) ) |
9 |
|
prcom |
⊢ { 𝑛 , 𝑈 } = { 𝑈 , 𝑛 } |
10 |
9
|
eleq1i |
⊢ ( { 𝑛 , 𝑈 } ∈ 𝐸 ↔ { 𝑈 , 𝑛 } ∈ 𝐸 ) |
11 |
10
|
biimpi |
⊢ ( { 𝑛 , 𝑈 } ∈ 𝐸 → { 𝑈 , 𝑛 } ∈ 𝐸 ) |
12 |
11
|
adantl |
⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) ∧ { 𝑛 , 𝑈 } ∈ 𝐸 ) → { 𝑈 , 𝑛 } ∈ 𝐸 ) |
13 |
|
prid1g |
⊢ ( 𝑈 ∈ 𝑉 → 𝑈 ∈ { 𝑈 , 𝑛 } ) |
14 |
13
|
adantl |
⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) → 𝑈 ∈ { 𝑈 , 𝑛 } ) |
15 |
14
|
adantr |
⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) ∧ { 𝑛 , 𝑈 } ∈ 𝐸 ) → 𝑈 ∈ { 𝑈 , 𝑛 } ) |
16 |
|
eleq2 |
⊢ ( 𝑒 = { 𝑈 , 𝑛 } → ( 𝑈 ∈ 𝑒 ↔ 𝑈 ∈ { 𝑈 , 𝑛 } ) ) |
17 |
16 4
|
elrab2 |
⊢ ( { 𝑈 , 𝑛 } ∈ 𝐼 ↔ ( { 𝑈 , 𝑛 } ∈ 𝐸 ∧ 𝑈 ∈ { 𝑈 , 𝑛 } ) ) |
18 |
12 15 17
|
sylanbrc |
⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) ∧ { 𝑛 , 𝑈 } ∈ 𝐸 ) → { 𝑈 , 𝑛 } ∈ 𝐼 ) |
19 |
18
|
ex |
⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) → ( { 𝑛 , 𝑈 } ∈ 𝐸 → { 𝑈 , 𝑛 } ∈ 𝐼 ) ) |
20 |
8 19
|
sylbid |
⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) → ( 𝑛 ∈ ( 𝐺 NeighbVtx 𝑈 ) → { 𝑈 , 𝑛 } ∈ 𝐼 ) ) |
21 |
6 20
|
syl5bi |
⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) → ( 𝑛 ∈ 𝑁 → { 𝑈 , 𝑛 } ∈ 𝐼 ) ) |
22 |
21
|
ralrimiv |
⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) → ∀ 𝑛 ∈ 𝑁 { 𝑈 , 𝑛 } ∈ 𝐼 ) |
23 |
4
|
rabeq2i |
⊢ ( 𝑒 ∈ 𝐼 ↔ ( 𝑒 ∈ 𝐸 ∧ 𝑈 ∈ 𝑒 ) ) |
24 |
2 3
|
edgnbusgreu |
⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) ∧ ( 𝑒 ∈ 𝐸 ∧ 𝑈 ∈ 𝑒 ) ) → ∃! 𝑛 ∈ 𝑁 𝑒 = { 𝑈 , 𝑛 } ) |
25 |
23 24
|
sylan2b |
⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) ∧ 𝑒 ∈ 𝐼 ) → ∃! 𝑛 ∈ 𝑁 𝑒 = { 𝑈 , 𝑛 } ) |
26 |
25
|
ralrimiva |
⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) → ∀ 𝑒 ∈ 𝐼 ∃! 𝑛 ∈ 𝑁 𝑒 = { 𝑈 , 𝑛 } ) |
27 |
5
|
f1ompt |
⊢ ( 𝐹 : 𝑁 –1-1-onto→ 𝐼 ↔ ( ∀ 𝑛 ∈ 𝑁 { 𝑈 , 𝑛 } ∈ 𝐼 ∧ ∀ 𝑒 ∈ 𝐼 ∃! 𝑛 ∈ 𝑁 𝑒 = { 𝑈 , 𝑛 } ) ) |
28 |
22 26 27
|
sylanbrc |
⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) → 𝐹 : 𝑁 –1-1-onto→ 𝐼 ) |