Step | Hyp | Ref
| Expression |
1 | | uvtxnbgra 26021 |
. . . 4
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ (𝑉 UnivVertex 𝐸)) → (〈𝑉, 𝐸〉 Neighbors 𝑁) = (𝑉 ∖ {𝑁})) |
2 | 1 | ex 449 |
. . 3
⊢ (𝑉 USGrph 𝐸 → (𝑁 ∈ (𝑉 UnivVertex 𝐸) → (〈𝑉, 𝐸〉 Neighbors 𝑁) = (𝑉 ∖ {𝑁}))) |
3 | 2 | adantr 480 |
. 2
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉) → (𝑁 ∈ (𝑉 UnivVertex 𝐸) → (〈𝑉, 𝐸〉 Neighbors 𝑁) = (𝑉 ∖ {𝑁}))) |
4 | | nbusgra 25957 |
. . . . 5
⊢ (𝑉 USGrph 𝐸 → (〈𝑉, 𝐸〉 Neighbors 𝑁) = {𝑣 ∈ 𝑉 ∣ {𝑁, 𝑣} ∈ ran 𝐸}) |
5 | 4 | eqeq1d 2612 |
. . . 4
⊢ (𝑉 USGrph 𝐸 → ((〈𝑉, 𝐸〉 Neighbors 𝑁) = (𝑉 ∖ {𝑁}) ↔ {𝑣 ∈ 𝑉 ∣ {𝑁, 𝑣} ∈ ran 𝐸} = (𝑉 ∖ {𝑁}))) |
6 | 5 | adantr 480 |
. . 3
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉) → ((〈𝑉, 𝐸〉 Neighbors 𝑁) = (𝑉 ∖ {𝑁}) ↔ {𝑣 ∈ 𝑉 ∣ {𝑁, 𝑣} ∈ ran 𝐸} = (𝑉 ∖ {𝑁}))) |
7 | | simplr 788 |
. . . . 5
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉) ∧ {𝑣 ∈ 𝑉 ∣ {𝑁, 𝑣} ∈ ran 𝐸} = (𝑉 ∖ {𝑁})) → 𝑁 ∈ 𝑉) |
8 | | prcom 4211 |
. . . . . . . . . . . 12
⊢ {𝑁, 𝑛} = {𝑛, 𝑁} |
9 | 8 | eleq1i 2679 |
. . . . . . . . . . 11
⊢ ({𝑁, 𝑛} ∈ ran 𝐸 ↔ {𝑛, 𝑁} ∈ ran 𝐸) |
10 | 9 | biimpi 205 |
. . . . . . . . . 10
⊢ ({𝑁, 𝑛} ∈ ran 𝐸 → {𝑛, 𝑁} ∈ ran 𝐸) |
11 | 10 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉) → ({𝑁, 𝑛} ∈ ran 𝐸 → {𝑛, 𝑁} ∈ ran 𝐸)) |
12 | 11 | ralrimivw 2950 |
. . . . . . . 8
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉) → ∀𝑛 ∈ 𝑉 ({𝑁, 𝑛} ∈ ran 𝐸 → {𝑛, 𝑁} ∈ ran 𝐸)) |
13 | | preq2 4213 |
. . . . . . . . . 10
⊢ (𝑣 = 𝑛 → {𝑁, 𝑣} = {𝑁, 𝑛}) |
14 | 13 | eleq1d 2672 |
. . . . . . . . 9
⊢ (𝑣 = 𝑛 → ({𝑁, 𝑣} ∈ ran 𝐸 ↔ {𝑁, 𝑛} ∈ ran 𝐸)) |
15 | 14 | ralrab 3335 |
. . . . . . . 8
⊢
(∀𝑛 ∈
{𝑣 ∈ 𝑉 ∣ {𝑁, 𝑣} ∈ ran 𝐸} {𝑛, 𝑁} ∈ ran 𝐸 ↔ ∀𝑛 ∈ 𝑉 ({𝑁, 𝑛} ∈ ran 𝐸 → {𝑛, 𝑁} ∈ ran 𝐸)) |
16 | 12, 15 | sylibr 223 |
. . . . . . 7
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉) → ∀𝑛 ∈ {𝑣 ∈ 𝑉 ∣ {𝑁, 𝑣} ∈ ran 𝐸} {𝑛, 𝑁} ∈ ran 𝐸) |
17 | 16 | adantr 480 |
. . . . . 6
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉) ∧ {𝑣 ∈ 𝑉 ∣ {𝑁, 𝑣} ∈ ran 𝐸} = (𝑉 ∖ {𝑁})) → ∀𝑛 ∈ {𝑣 ∈ 𝑉 ∣ {𝑁, 𝑣} ∈ ran 𝐸} {𝑛, 𝑁} ∈ ran 𝐸) |
18 | | eqcom 2617 |
. . . . . . . . 9
⊢ ({𝑣 ∈ 𝑉 ∣ {𝑁, 𝑣} ∈ ran 𝐸} = (𝑉 ∖ {𝑁}) ↔ (𝑉 ∖ {𝑁}) = {𝑣 ∈ 𝑉 ∣ {𝑁, 𝑣} ∈ ran 𝐸}) |
19 | 18 | biimpi 205 |
. . . . . . . 8
⊢ ({𝑣 ∈ 𝑉 ∣ {𝑁, 𝑣} ∈ ran 𝐸} = (𝑉 ∖ {𝑁}) → (𝑉 ∖ {𝑁}) = {𝑣 ∈ 𝑉 ∣ {𝑁, 𝑣} ∈ ran 𝐸}) |
20 | 19 | adantl 481 |
. . . . . . 7
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉) ∧ {𝑣 ∈ 𝑉 ∣ {𝑁, 𝑣} ∈ ran 𝐸} = (𝑉 ∖ {𝑁})) → (𝑉 ∖ {𝑁}) = {𝑣 ∈ 𝑉 ∣ {𝑁, 𝑣} ∈ ran 𝐸}) |
21 | 20 | raleqdv 3121 |
. . . . . 6
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉) ∧ {𝑣 ∈ 𝑉 ∣ {𝑁, 𝑣} ∈ ran 𝐸} = (𝑉 ∖ {𝑁})) → (∀𝑛 ∈ (𝑉 ∖ {𝑁}){𝑛, 𝑁} ∈ ran 𝐸 ↔ ∀𝑛 ∈ {𝑣 ∈ 𝑉 ∣ {𝑁, 𝑣} ∈ ran 𝐸} {𝑛, 𝑁} ∈ ran 𝐸)) |
22 | 17, 21 | mpbird 246 |
. . . . 5
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉) ∧ {𝑣 ∈ 𝑉 ∣ {𝑁, 𝑣} ∈ ran 𝐸} = (𝑉 ∖ {𝑁})) → ∀𝑛 ∈ (𝑉 ∖ {𝑁}){𝑛, 𝑁} ∈ ran 𝐸) |
23 | | usgrav 25867 |
. . . . . . . 8
⊢ (𝑉 USGrph 𝐸 → (𝑉 ∈ V ∧ 𝐸 ∈ V)) |
24 | | uvtxel 26017 |
. . . . . . . 8
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑁 ∈ (𝑉 UnivVertex 𝐸) ↔ (𝑁 ∈ 𝑉 ∧ ∀𝑛 ∈ (𝑉 ∖ {𝑁}){𝑛, 𝑁} ∈ ran 𝐸))) |
25 | 23, 24 | syl 17 |
. . . . . . 7
⊢ (𝑉 USGrph 𝐸 → (𝑁 ∈ (𝑉 UnivVertex 𝐸) ↔ (𝑁 ∈ 𝑉 ∧ ∀𝑛 ∈ (𝑉 ∖ {𝑁}){𝑛, 𝑁} ∈ ran 𝐸))) |
26 | 25 | adantr 480 |
. . . . . 6
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉) → (𝑁 ∈ (𝑉 UnivVertex 𝐸) ↔ (𝑁 ∈ 𝑉 ∧ ∀𝑛 ∈ (𝑉 ∖ {𝑁}){𝑛, 𝑁} ∈ ran 𝐸))) |
27 | 26 | adantr 480 |
. . . . 5
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉) ∧ {𝑣 ∈ 𝑉 ∣ {𝑁, 𝑣} ∈ ran 𝐸} = (𝑉 ∖ {𝑁})) → (𝑁 ∈ (𝑉 UnivVertex 𝐸) ↔ (𝑁 ∈ 𝑉 ∧ ∀𝑛 ∈ (𝑉 ∖ {𝑁}){𝑛, 𝑁} ∈ ran 𝐸))) |
28 | 7, 22, 27 | mpbir2and 959 |
. . . 4
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉) ∧ {𝑣 ∈ 𝑉 ∣ {𝑁, 𝑣} ∈ ran 𝐸} = (𝑉 ∖ {𝑁})) → 𝑁 ∈ (𝑉 UnivVertex 𝐸)) |
29 | 28 | ex 449 |
. . 3
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉) → ({𝑣 ∈ 𝑉 ∣ {𝑁, 𝑣} ∈ ran 𝐸} = (𝑉 ∖ {𝑁}) → 𝑁 ∈ (𝑉 UnivVertex 𝐸))) |
30 | 6, 29 | sylbid 229 |
. 2
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉) → ((〈𝑉, 𝐸〉 Neighbors 𝑁) = (𝑉 ∖ {𝑁}) → 𝑁 ∈ (𝑉 UnivVertex 𝐸))) |
31 | 3, 30 | impbid 201 |
1
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉) → (𝑁 ∈ (𝑉 UnivVertex 𝐸) ↔ (〈𝑉, 𝐸〉 Neighbors 𝑁) = (𝑉 ∖ {𝑁}))) |