| Step | Hyp | Ref
| Expression |
| 1 | | usgrexi.p |
. . 3
⊢ 𝑃 = {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2} |
| 2 | 1 | usgrexi 29458 |
. 2
⊢ (𝑉 ∈ 𝑊 → 〈𝑉, ( I ↾ 𝑃)〉 ∈ USGraph) |
| 3 | 1 | cusgrexilem1 29456 |
. . . . . . . . 9
⊢ (𝑉 ∈ 𝑊 → ( I ↾ 𝑃) ∈ V) |
| 4 | | opvtxfv 29021 |
. . . . . . . . . 10
⊢ ((𝑉 ∈ 𝑊 ∧ ( I ↾ 𝑃) ∈ V) → (Vtx‘〈𝑉, ( I ↾ 𝑃)〉) = 𝑉) |
| 5 | 4 | eqcomd 2743 |
. . . . . . . . 9
⊢ ((𝑉 ∈ 𝑊 ∧ ( I ↾ 𝑃) ∈ V) → 𝑉 = (Vtx‘〈𝑉, ( I ↾ 𝑃)〉)) |
| 6 | 3, 5 | mpdan 687 |
. . . . . . . 8
⊢ (𝑉 ∈ 𝑊 → 𝑉 = (Vtx‘〈𝑉, ( I ↾ 𝑃)〉)) |
| 7 | 6 | eleq2d 2827 |
. . . . . . 7
⊢ (𝑉 ∈ 𝑊 → (𝑣 ∈ 𝑉 ↔ 𝑣 ∈ (Vtx‘〈𝑉, ( I ↾ 𝑃)〉))) |
| 8 | 7 | biimpa 476 |
. . . . . 6
⊢ ((𝑉 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉) → 𝑣 ∈ (Vtx‘〈𝑉, ( I ↾ 𝑃)〉)) |
| 9 | | eldifi 4131 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ (𝑉 ∖ {𝑣}) → 𝑛 ∈ 𝑉) |
| 10 | 9 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝑉 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉) ∧ 𝑛 ∈ (𝑉 ∖ {𝑣})) → 𝑛 ∈ 𝑉) |
| 11 | 3, 4 | mpdan 687 |
. . . . . . . . . . . . 13
⊢ (𝑉 ∈ 𝑊 → (Vtx‘〈𝑉, ( I ↾ 𝑃)〉) = 𝑉) |
| 12 | 11 | eleq2d 2827 |
. . . . . . . . . . . 12
⊢ (𝑉 ∈ 𝑊 → (𝑛 ∈ (Vtx‘〈𝑉, ( I ↾ 𝑃)〉) ↔ 𝑛 ∈ 𝑉)) |
| 13 | 12 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝑉 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉) ∧ 𝑛 ∈ (𝑉 ∖ {𝑣})) → (𝑛 ∈ (Vtx‘〈𝑉, ( I ↾ 𝑃)〉) ↔ 𝑛 ∈ 𝑉)) |
| 14 | 10, 13 | mpbird 257 |
. . . . . . . . . 10
⊢ (((𝑉 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉) ∧ 𝑛 ∈ (𝑉 ∖ {𝑣})) → 𝑛 ∈ (Vtx‘〈𝑉, ( I ↾ 𝑃)〉)) |
| 15 | | simplr 769 |
. . . . . . . . . . 11
⊢ (((𝑉 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉) ∧ 𝑛 ∈ (𝑉 ∖ {𝑣})) → 𝑣 ∈ 𝑉) |
| 16 | 11 | eleq2d 2827 |
. . . . . . . . . . . 12
⊢ (𝑉 ∈ 𝑊 → (𝑣 ∈ (Vtx‘〈𝑉, ( I ↾ 𝑃)〉) ↔ 𝑣 ∈ 𝑉)) |
| 17 | 16 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝑉 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉) ∧ 𝑛 ∈ (𝑉 ∖ {𝑣})) → (𝑣 ∈ (Vtx‘〈𝑉, ( I ↾ 𝑃)〉) ↔ 𝑣 ∈ 𝑉)) |
| 18 | 15, 17 | mpbird 257 |
. . . . . . . . . 10
⊢ (((𝑉 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉) ∧ 𝑛 ∈ (𝑉 ∖ {𝑣})) → 𝑣 ∈ (Vtx‘〈𝑉, ( I ↾ 𝑃)〉)) |
| 19 | 14, 18 | jca 511 |
. . . . . . . . 9
⊢ (((𝑉 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉) ∧ 𝑛 ∈ (𝑉 ∖ {𝑣})) → (𝑛 ∈ (Vtx‘〈𝑉, ( I ↾ 𝑃)〉) ∧ 𝑣 ∈ (Vtx‘〈𝑉, ( I ↾ 𝑃)〉))) |
| 20 | | eldifsni 4790 |
. . . . . . . . . 10
⊢ (𝑛 ∈ (𝑉 ∖ {𝑣}) → 𝑛 ≠ 𝑣) |
| 21 | 20 | adantl 481 |
. . . . . . . . 9
⊢ (((𝑉 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉) ∧ 𝑛 ∈ (𝑉 ∖ {𝑣})) → 𝑛 ≠ 𝑣) |
| 22 | 1 | cusgrexilem2 29459 |
. . . . . . . . . 10
⊢ (((𝑉 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉) ∧ 𝑛 ∈ (𝑉 ∖ {𝑣})) → ∃𝑒 ∈ ran ( I ↾ 𝑃){𝑣, 𝑛} ⊆ 𝑒) |
| 23 | | edgval 29066 |
. . . . . . . . . . . . 13
⊢
(Edg‘〈𝑉,
( I ↾ 𝑃)〉) = ran
(iEdg‘〈𝑉, ( I
↾ 𝑃)〉) |
| 24 | | opiedgfv 29024 |
. . . . . . . . . . . . . . 15
⊢ ((𝑉 ∈ 𝑊 ∧ ( I ↾ 𝑃) ∈ V) → (iEdg‘〈𝑉, ( I ↾ 𝑃)〉) = ( I ↾ 𝑃)) |
| 25 | 3, 24 | mpdan 687 |
. . . . . . . . . . . . . 14
⊢ (𝑉 ∈ 𝑊 → (iEdg‘〈𝑉, ( I ↾ 𝑃)〉) = ( I ↾ 𝑃)) |
| 26 | 25 | rneqd 5949 |
. . . . . . . . . . . . 13
⊢ (𝑉 ∈ 𝑊 → ran (iEdg‘〈𝑉, ( I ↾ 𝑃)〉) = ran ( I ↾ 𝑃)) |
| 27 | 23, 26 | eqtrid 2789 |
. . . . . . . . . . . 12
⊢ (𝑉 ∈ 𝑊 → (Edg‘〈𝑉, ( I ↾ 𝑃)〉) = ran ( I ↾ 𝑃)) |
| 28 | 27 | rexeqdv 3327 |
. . . . . . . . . . 11
⊢ (𝑉 ∈ 𝑊 → (∃𝑒 ∈ (Edg‘〈𝑉, ( I ↾ 𝑃)〉){𝑣, 𝑛} ⊆ 𝑒 ↔ ∃𝑒 ∈ ran ( I ↾ 𝑃){𝑣, 𝑛} ⊆ 𝑒)) |
| 29 | 28 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝑉 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉) ∧ 𝑛 ∈ (𝑉 ∖ {𝑣})) → (∃𝑒 ∈ (Edg‘〈𝑉, ( I ↾ 𝑃)〉){𝑣, 𝑛} ⊆ 𝑒 ↔ ∃𝑒 ∈ ran ( I ↾ 𝑃){𝑣, 𝑛} ⊆ 𝑒)) |
| 30 | 22, 29 | mpbird 257 |
. . . . . . . . 9
⊢ (((𝑉 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉) ∧ 𝑛 ∈ (𝑉 ∖ {𝑣})) → ∃𝑒 ∈ (Edg‘〈𝑉, ( I ↾ 𝑃)〉){𝑣, 𝑛} ⊆ 𝑒) |
| 31 | | eqid 2737 |
. . . . . . . . . 10
⊢
(Vtx‘〈𝑉,
( I ↾ 𝑃)〉) =
(Vtx‘〈𝑉, ( I
↾ 𝑃)〉) |
| 32 | | eqid 2737 |
. . . . . . . . . 10
⊢
(Edg‘〈𝑉,
( I ↾ 𝑃)〉) =
(Edg‘〈𝑉, ( I
↾ 𝑃)〉) |
| 33 | 31, 32 | nbgrel 29357 |
. . . . . . . . 9
⊢ (𝑛 ∈ (〈𝑉, ( I ↾ 𝑃)〉 NeighbVtx 𝑣) ↔ ((𝑛 ∈ (Vtx‘〈𝑉, ( I ↾ 𝑃)〉) ∧ 𝑣 ∈ (Vtx‘〈𝑉, ( I ↾ 𝑃)〉)) ∧ 𝑛 ≠ 𝑣 ∧ ∃𝑒 ∈ (Edg‘〈𝑉, ( I ↾ 𝑃)〉){𝑣, 𝑛} ⊆ 𝑒)) |
| 34 | 19, 21, 30, 33 | syl3anbrc 1344 |
. . . . . . . 8
⊢ (((𝑉 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉) ∧ 𝑛 ∈ (𝑉 ∖ {𝑣})) → 𝑛 ∈ (〈𝑉, ( I ↾ 𝑃)〉 NeighbVtx 𝑣)) |
| 35 | 34 | ralrimiva 3146 |
. . . . . . 7
⊢ ((𝑉 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉) → ∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ (〈𝑉, ( I ↾ 𝑃)〉 NeighbVtx 𝑣)) |
| 36 | 11 | adantr 480 |
. . . . . . . 8
⊢ ((𝑉 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉) → (Vtx‘〈𝑉, ( I ↾ 𝑃)〉) = 𝑉) |
| 37 | 36 | difeq1d 4125 |
. . . . . . 7
⊢ ((𝑉 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉) → ((Vtx‘〈𝑉, ( I ↾ 𝑃)〉) ∖ {𝑣}) = (𝑉 ∖ {𝑣})) |
| 38 | 35, 37 | raleqtrrdv 3330 |
. . . . . 6
⊢ ((𝑉 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉) → ∀𝑛 ∈ ((Vtx‘〈𝑉, ( I ↾ 𝑃)〉) ∖ {𝑣})𝑛 ∈ (〈𝑉, ( I ↾ 𝑃)〉 NeighbVtx 𝑣)) |
| 39 | 31 | uvtxel 29405 |
. . . . . 6
⊢ (𝑣 ∈
(UnivVtx‘〈𝑉, ( I
↾ 𝑃)〉) ↔
(𝑣 ∈
(Vtx‘〈𝑉, ( I
↾ 𝑃)〉) ∧
∀𝑛 ∈
((Vtx‘〈𝑉, ( I
↾ 𝑃)〉) ∖
{𝑣})𝑛 ∈ (〈𝑉, ( I ↾ 𝑃)〉 NeighbVtx 𝑣))) |
| 40 | 8, 38, 39 | sylanbrc 583 |
. . . . 5
⊢ ((𝑉 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉) → 𝑣 ∈ (UnivVtx‘〈𝑉, ( I ↾ 𝑃)〉)) |
| 41 | 40 | ralrimiva 3146 |
. . . 4
⊢ (𝑉 ∈ 𝑊 → ∀𝑣 ∈ 𝑉 𝑣 ∈ (UnivVtx‘〈𝑉, ( I ↾ 𝑃)〉)) |
| 42 | 41, 11 | raleqtrrdv 3330 |
. . 3
⊢ (𝑉 ∈ 𝑊 → ∀𝑣 ∈ (Vtx‘〈𝑉, ( I ↾ 𝑃)〉)𝑣 ∈ (UnivVtx‘〈𝑉, ( I ↾ 𝑃)〉)) |
| 43 | | opex 5469 |
. . . 4
⊢
〈𝑉, ( I ↾
𝑃)〉 ∈
V |
| 44 | 31 | iscplgr 29432 |
. . . 4
⊢
(〈𝑉, ( I
↾ 𝑃)〉 ∈ V
→ (〈𝑉, ( I
↾ 𝑃)〉 ∈
ComplGraph ↔ ∀𝑣
∈ (Vtx‘〈𝑉,
( I ↾ 𝑃)〉)𝑣 ∈
(UnivVtx‘〈𝑉, ( I
↾ 𝑃)〉))) |
| 45 | 43, 44 | mp1i 13 |
. . 3
⊢ (𝑉 ∈ 𝑊 → (〈𝑉, ( I ↾ 𝑃)〉 ∈ ComplGraph ↔
∀𝑣 ∈
(Vtx‘〈𝑉, ( I
↾ 𝑃)〉)𝑣 ∈
(UnivVtx‘〈𝑉, ( I
↾ 𝑃)〉))) |
| 46 | 42, 45 | mpbird 257 |
. 2
⊢ (𝑉 ∈ 𝑊 → 〈𝑉, ( I ↾ 𝑃)〉 ∈ ComplGraph) |
| 47 | | iscusgr 29435 |
. 2
⊢
(〈𝑉, ( I
↾ 𝑃)〉 ∈
ComplUSGraph ↔ (〈𝑉, ( I ↾ 𝑃)〉 ∈ USGraph ∧ 〈𝑉, ( I ↾ 𝑃)〉 ∈ ComplGraph)) |
| 48 | 2, 46, 47 | sylanbrc 583 |
1
⊢ (𝑉 ∈ 𝑊 → 〈𝑉, ( I ↾ 𝑃)〉 ∈
ComplUSGraph) |