| Step | Hyp | Ref
| Expression |
| 1 | | nbuhgr.v |
. . . 4
⊢ 𝑉 = (Vtx‘𝐺) |
| 2 | | nbuhgr.e |
. . . 4
⊢ 𝐸 = (Edg‘𝐺) |
| 3 | 1, 2 | nbgrval 29353 |
. . 3
⊢ (𝑁 ∈ 𝑉 → (𝐺 NeighbVtx 𝑁) = {𝑣 ∈ (𝑉 ∖ {𝑁}) ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑣} ⊆ 𝑒}) |
| 4 | 3 | adantl 481 |
. 2
⊢ ((𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉) → (𝐺 NeighbVtx 𝑁) = {𝑣 ∈ (𝑉 ∖ {𝑁}) ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑣} ⊆ 𝑒}) |
| 5 | | eldifi 4131 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (𝑉 ∖ {𝑁}) → 𝑥 ∈ 𝑉) |
| 6 | 5 | adantl 481 |
. . . . . . . . 9
⊢ (((𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝑥 ∈ (𝑉 ∖ {𝑁})) → 𝑥 ∈ 𝑉) |
| 7 | 6 | adantr 480 |
. . . . . . . 8
⊢ ((((𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝑥 ∈ (𝑉 ∖ {𝑁})) ∧ (𝑒 ∈ 𝐸 ∧ {𝑁, 𝑥} ⊆ 𝑒)) → 𝑥 ∈ 𝑉) |
| 8 | | umgrupgr 29120 |
. . . . . . . . . . . . 13
⊢ (𝐺 ∈ UMGraph → 𝐺 ∈
UPGraph) |
| 9 | 8 | ad4antr 732 |
. . . . . . . . . . . 12
⊢
(((((𝐺 ∈
UMGraph ∧ 𝑁 ∈
𝑉) ∧ 𝑥 ∈ (𝑉 ∖ {𝑁})) ∧ 𝑒 ∈ 𝐸) ∧ {𝑁, 𝑥} ⊆ 𝑒) → 𝐺 ∈ UPGraph) |
| 10 | | simpr 484 |
. . . . . . . . . . . . 13
⊢ ((((𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝑥 ∈ (𝑉 ∖ {𝑁})) ∧ 𝑒 ∈ 𝐸) → 𝑒 ∈ 𝐸) |
| 11 | 10 | adantr 480 |
. . . . . . . . . . . 12
⊢
(((((𝐺 ∈
UMGraph ∧ 𝑁 ∈
𝑉) ∧ 𝑥 ∈ (𝑉 ∖ {𝑁})) ∧ 𝑒 ∈ 𝐸) ∧ {𝑁, 𝑥} ⊆ 𝑒) → 𝑒 ∈ 𝐸) |
| 12 | | simpr 484 |
. . . . . . . . . . . 12
⊢
(((((𝐺 ∈
UMGraph ∧ 𝑁 ∈
𝑉) ∧ 𝑥 ∈ (𝑉 ∖ {𝑁})) ∧ 𝑒 ∈ 𝐸) ∧ {𝑁, 𝑥} ⊆ 𝑒) → {𝑁, 𝑥} ⊆ 𝑒) |
| 13 | | simpr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉) → 𝑁 ∈ 𝑉) |
| 14 | 13 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝑥 ∈ (𝑉 ∖ {𝑁})) → 𝑁 ∈ 𝑉) |
| 15 | | vex 3484 |
. . . . . . . . . . . . . . . 16
⊢ 𝑥 ∈ V |
| 16 | 15 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (((𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝑥 ∈ (𝑉 ∖ {𝑁})) → 𝑥 ∈ V) |
| 17 | | eldifsn 4786 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (𝑉 ∖ {𝑁}) ↔ (𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 𝑁)) |
| 18 | | simpr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 𝑁) → 𝑥 ≠ 𝑁) |
| 19 | 18 | necomd 2996 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 𝑁) → 𝑁 ≠ 𝑥) |
| 20 | 17, 19 | sylbi 217 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (𝑉 ∖ {𝑁}) → 𝑁 ≠ 𝑥) |
| 21 | 20 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝑥 ∈ (𝑉 ∖ {𝑁})) → 𝑁 ≠ 𝑥) |
| 22 | 14, 16, 21 | 3jca 1129 |
. . . . . . . . . . . . . 14
⊢ (((𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝑥 ∈ (𝑉 ∖ {𝑁})) → (𝑁 ∈ 𝑉 ∧ 𝑥 ∈ V ∧ 𝑁 ≠ 𝑥)) |
| 23 | 22 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((((𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝑥 ∈ (𝑉 ∖ {𝑁})) ∧ 𝑒 ∈ 𝐸) → (𝑁 ∈ 𝑉 ∧ 𝑥 ∈ V ∧ 𝑁 ≠ 𝑥)) |
| 24 | 23 | adantr 480 |
. . . . . . . . . . . 12
⊢
(((((𝐺 ∈
UMGraph ∧ 𝑁 ∈
𝑉) ∧ 𝑥 ∈ (𝑉 ∖ {𝑁})) ∧ 𝑒 ∈ 𝐸) ∧ {𝑁, 𝑥} ⊆ 𝑒) → (𝑁 ∈ 𝑉 ∧ 𝑥 ∈ V ∧ 𝑁 ≠ 𝑥)) |
| 25 | 1, 2 | upgredgpr 29159 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ UPGraph ∧ 𝑒 ∈ 𝐸 ∧ {𝑁, 𝑥} ⊆ 𝑒) ∧ (𝑁 ∈ 𝑉 ∧ 𝑥 ∈ V ∧ 𝑁 ≠ 𝑥)) → {𝑁, 𝑥} = 𝑒) |
| 26 | 9, 11, 12, 24, 25 | syl31anc 1375 |
. . . . . . . . . . 11
⊢
(((((𝐺 ∈
UMGraph ∧ 𝑁 ∈
𝑉) ∧ 𝑥 ∈ (𝑉 ∖ {𝑁})) ∧ 𝑒 ∈ 𝐸) ∧ {𝑁, 𝑥} ⊆ 𝑒) → {𝑁, 𝑥} = 𝑒) |
| 27 | 26 | ex 412 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝑥 ∈ (𝑉 ∖ {𝑁})) ∧ 𝑒 ∈ 𝐸) → ({𝑁, 𝑥} ⊆ 𝑒 → {𝑁, 𝑥} = 𝑒)) |
| 28 | | eleq1 2829 |
. . . . . . . . . . 11
⊢ ({𝑁, 𝑥} = 𝑒 → ({𝑁, 𝑥} ∈ 𝐸 ↔ 𝑒 ∈ 𝐸)) |
| 29 | 28 | biimprd 248 |
. . . . . . . . . 10
⊢ ({𝑁, 𝑥} = 𝑒 → (𝑒 ∈ 𝐸 → {𝑁, 𝑥} ∈ 𝐸)) |
| 30 | 27, 10, 29 | syl6ci 71 |
. . . . . . . . 9
⊢ ((((𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝑥 ∈ (𝑉 ∖ {𝑁})) ∧ 𝑒 ∈ 𝐸) → ({𝑁, 𝑥} ⊆ 𝑒 → {𝑁, 𝑥} ∈ 𝐸)) |
| 31 | 30 | impr 454 |
. . . . . . . 8
⊢ ((((𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝑥 ∈ (𝑉 ∖ {𝑁})) ∧ (𝑒 ∈ 𝐸 ∧ {𝑁, 𝑥} ⊆ 𝑒)) → {𝑁, 𝑥} ∈ 𝐸) |
| 32 | 7, 31 | jca 511 |
. . . . . . 7
⊢ ((((𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝑥 ∈ (𝑉 ∖ {𝑁})) ∧ (𝑒 ∈ 𝐸 ∧ {𝑁, 𝑥} ⊆ 𝑒)) → (𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ 𝐸)) |
| 33 | 32 | rexlimdvaa 3156 |
. . . . . 6
⊢ (((𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝑥 ∈ (𝑉 ∖ {𝑁})) → (∃𝑒 ∈ 𝐸 {𝑁, 𝑥} ⊆ 𝑒 → (𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ 𝐸))) |
| 34 | 33 | expimpd 453 |
. . . . 5
⊢ ((𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉) → ((𝑥 ∈ (𝑉 ∖ {𝑁}) ∧ ∃𝑒 ∈ 𝐸 {𝑁, 𝑥} ⊆ 𝑒) → (𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ 𝐸))) |
| 35 | | simprl 771 |
. . . . . . . 8
⊢ (((𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉) ∧ (𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ 𝐸)) → 𝑥 ∈ 𝑉) |
| 36 | 2 | umgredgne 29162 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ UMGraph ∧ {𝑁, 𝑥} ∈ 𝐸) → 𝑁 ≠ 𝑥) |
| 37 | 36 | ad2ant2rl 749 |
. . . . . . . . 9
⊢ (((𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉) ∧ (𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ 𝐸)) → 𝑁 ≠ 𝑥) |
| 38 | 37 | necomd 2996 |
. . . . . . . 8
⊢ (((𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉) ∧ (𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ 𝐸)) → 𝑥 ≠ 𝑁) |
| 39 | 35, 38, 17 | sylanbrc 583 |
. . . . . . 7
⊢ (((𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉) ∧ (𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ 𝐸)) → 𝑥 ∈ (𝑉 ∖ {𝑁})) |
| 40 | | simpr 484 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ 𝐸) → {𝑁, 𝑥} ∈ 𝐸) |
| 41 | 40 | adantl 481 |
. . . . . . . 8
⊢ (((𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉) ∧ (𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ 𝐸)) → {𝑁, 𝑥} ∈ 𝐸) |
| 42 | | sseq2 4010 |
. . . . . . . . 9
⊢ (𝑒 = {𝑁, 𝑥} → ({𝑁, 𝑥} ⊆ 𝑒 ↔ {𝑁, 𝑥} ⊆ {𝑁, 𝑥})) |
| 43 | 42 | adantl 481 |
. . . . . . . 8
⊢ ((((𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉) ∧ (𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ 𝐸)) ∧ 𝑒 = {𝑁, 𝑥}) → ({𝑁, 𝑥} ⊆ 𝑒 ↔ {𝑁, 𝑥} ⊆ {𝑁, 𝑥})) |
| 44 | | ssidd 4007 |
. . . . . . . 8
⊢ (((𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉) ∧ (𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ 𝐸)) → {𝑁, 𝑥} ⊆ {𝑁, 𝑥}) |
| 45 | 41, 43, 44 | rspcedvd 3624 |
. . . . . . 7
⊢ (((𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉) ∧ (𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ 𝐸)) → ∃𝑒 ∈ 𝐸 {𝑁, 𝑥} ⊆ 𝑒) |
| 46 | 39, 45 | jca 511 |
. . . . . 6
⊢ (((𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉) ∧ (𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ 𝐸)) → (𝑥 ∈ (𝑉 ∖ {𝑁}) ∧ ∃𝑒 ∈ 𝐸 {𝑁, 𝑥} ⊆ 𝑒)) |
| 47 | 46 | ex 412 |
. . . . 5
⊢ ((𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉) → ((𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ 𝐸) → (𝑥 ∈ (𝑉 ∖ {𝑁}) ∧ ∃𝑒 ∈ 𝐸 {𝑁, 𝑥} ⊆ 𝑒))) |
| 48 | 34, 47 | impbid 212 |
. . . 4
⊢ ((𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉) → ((𝑥 ∈ (𝑉 ∖ {𝑁}) ∧ ∃𝑒 ∈ 𝐸 {𝑁, 𝑥} ⊆ 𝑒) ↔ (𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ 𝐸))) |
| 49 | | preq2 4734 |
. . . . . . 7
⊢ (𝑣 = 𝑥 → {𝑁, 𝑣} = {𝑁, 𝑥}) |
| 50 | 49 | sseq1d 4015 |
. . . . . 6
⊢ (𝑣 = 𝑥 → ({𝑁, 𝑣} ⊆ 𝑒 ↔ {𝑁, 𝑥} ⊆ 𝑒)) |
| 51 | 50 | rexbidv 3179 |
. . . . 5
⊢ (𝑣 = 𝑥 → (∃𝑒 ∈ 𝐸 {𝑁, 𝑣} ⊆ 𝑒 ↔ ∃𝑒 ∈ 𝐸 {𝑁, 𝑥} ⊆ 𝑒)) |
| 52 | 51 | elrab 3692 |
. . . 4
⊢ (𝑥 ∈ {𝑣 ∈ (𝑉 ∖ {𝑁}) ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑣} ⊆ 𝑒} ↔ (𝑥 ∈ (𝑉 ∖ {𝑁}) ∧ ∃𝑒 ∈ 𝐸 {𝑁, 𝑥} ⊆ 𝑒)) |
| 53 | | preq2 4734 |
. . . . . 6
⊢ (𝑛 = 𝑥 → {𝑁, 𝑛} = {𝑁, 𝑥}) |
| 54 | 53 | eleq1d 2826 |
. . . . 5
⊢ (𝑛 = 𝑥 → ({𝑁, 𝑛} ∈ 𝐸 ↔ {𝑁, 𝑥} ∈ 𝐸)) |
| 55 | 54 | elrab 3692 |
. . . 4
⊢ (𝑥 ∈ {𝑛 ∈ 𝑉 ∣ {𝑁, 𝑛} ∈ 𝐸} ↔ (𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ 𝐸)) |
| 56 | 48, 52, 55 | 3bitr4g 314 |
. . 3
⊢ ((𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉) → (𝑥 ∈ {𝑣 ∈ (𝑉 ∖ {𝑁}) ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑣} ⊆ 𝑒} ↔ 𝑥 ∈ {𝑛 ∈ 𝑉 ∣ {𝑁, 𝑛} ∈ 𝐸})) |
| 57 | 56 | eqrdv 2735 |
. 2
⊢ ((𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉) → {𝑣 ∈ (𝑉 ∖ {𝑁}) ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑣} ⊆ 𝑒} = {𝑛 ∈ 𝑉 ∣ {𝑁, 𝑛} ∈ 𝐸}) |
| 58 | 4, 57 | eqtrd 2777 |
1
⊢ ((𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉) → (𝐺 NeighbVtx 𝑁) = {𝑛 ∈ 𝑉 ∣ {𝑁, 𝑛} ∈ 𝐸}) |