Step | Hyp | Ref
| Expression |
1 | | usgrexi.p |
. . 3
⊢ 𝑃 = {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2} |
2 | 1 | usgrexi 28965 |
. 2
⊢ (𝑉 ∈ 𝑊 → ⟨𝑉, ( I ↾ 𝑃)⟩ ∈ USGraph) |
3 | 1 | cusgrexilem1 28963 |
. . . . . . . . 9
⊢ (𝑉 ∈ 𝑊 → ( I ↾ 𝑃) ∈ V) |
4 | | opvtxfv 28531 |
. . . . . . . . . 10
⊢ ((𝑉 ∈ 𝑊 ∧ ( I ↾ 𝑃) ∈ V) → (Vtx‘⟨𝑉, ( I ↾ 𝑃)⟩) = 𝑉) |
5 | 4 | eqcomd 2736 |
. . . . . . . . 9
⊢ ((𝑉 ∈ 𝑊 ∧ ( I ↾ 𝑃) ∈ V) → 𝑉 = (Vtx‘⟨𝑉, ( I ↾ 𝑃)⟩)) |
6 | 3, 5 | mpdan 683 |
. . . . . . . 8
⊢ (𝑉 ∈ 𝑊 → 𝑉 = (Vtx‘⟨𝑉, ( I ↾ 𝑃)⟩)) |
7 | 6 | eleq2d 2817 |
. . . . . . 7
⊢ (𝑉 ∈ 𝑊 → (𝑣 ∈ 𝑉 ↔ 𝑣 ∈ (Vtx‘⟨𝑉, ( I ↾ 𝑃)⟩))) |
8 | 7 | biimpa 475 |
. . . . . 6
⊢ ((𝑉 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉) → 𝑣 ∈ (Vtx‘⟨𝑉, ( I ↾ 𝑃)⟩)) |
9 | | eldifi 4125 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ (𝑉 ∖ {𝑣}) → 𝑛 ∈ 𝑉) |
10 | 9 | adantl 480 |
. . . . . . . . . . 11
⊢ (((𝑉 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉) ∧ 𝑛 ∈ (𝑉 ∖ {𝑣})) → 𝑛 ∈ 𝑉) |
11 | 3, 4 | mpdan 683 |
. . . . . . . . . . . . 13
⊢ (𝑉 ∈ 𝑊 → (Vtx‘⟨𝑉, ( I ↾ 𝑃)⟩) = 𝑉) |
12 | 11 | eleq2d 2817 |
. . . . . . . . . . . 12
⊢ (𝑉 ∈ 𝑊 → (𝑛 ∈ (Vtx‘⟨𝑉, ( I ↾ 𝑃)⟩) ↔ 𝑛 ∈ 𝑉)) |
13 | 12 | ad2antrr 722 |
. . . . . . . . . . 11
⊢ (((𝑉 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉) ∧ 𝑛 ∈ (𝑉 ∖ {𝑣})) → (𝑛 ∈ (Vtx‘⟨𝑉, ( I ↾ 𝑃)⟩) ↔ 𝑛 ∈ 𝑉)) |
14 | 10, 13 | mpbird 256 |
. . . . . . . . . 10
⊢ (((𝑉 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉) ∧ 𝑛 ∈ (𝑉 ∖ {𝑣})) → 𝑛 ∈ (Vtx‘⟨𝑉, ( I ↾ 𝑃)⟩)) |
15 | | simplr 765 |
. . . . . . . . . . 11
⊢ (((𝑉 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉) ∧ 𝑛 ∈ (𝑉 ∖ {𝑣})) → 𝑣 ∈ 𝑉) |
16 | 11 | eleq2d 2817 |
. . . . . . . . . . . 12
⊢ (𝑉 ∈ 𝑊 → (𝑣 ∈ (Vtx‘⟨𝑉, ( I ↾ 𝑃)⟩) ↔ 𝑣 ∈ 𝑉)) |
17 | 16 | ad2antrr 722 |
. . . . . . . . . . 11
⊢ (((𝑉 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉) ∧ 𝑛 ∈ (𝑉 ∖ {𝑣})) → (𝑣 ∈ (Vtx‘⟨𝑉, ( I ↾ 𝑃)⟩) ↔ 𝑣 ∈ 𝑉)) |
18 | 15, 17 | mpbird 256 |
. . . . . . . . . 10
⊢ (((𝑉 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉) ∧ 𝑛 ∈ (𝑉 ∖ {𝑣})) → 𝑣 ∈ (Vtx‘⟨𝑉, ( I ↾ 𝑃)⟩)) |
19 | 14, 18 | jca 510 |
. . . . . . . . 9
⊢ (((𝑉 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉) ∧ 𝑛 ∈ (𝑉 ∖ {𝑣})) → (𝑛 ∈ (Vtx‘⟨𝑉, ( I ↾ 𝑃)⟩) ∧ 𝑣 ∈ (Vtx‘⟨𝑉, ( I ↾ 𝑃)⟩))) |
20 | | eldifsni 4792 |
. . . . . . . . . 10
⊢ (𝑛 ∈ (𝑉 ∖ {𝑣}) → 𝑛 ≠ 𝑣) |
21 | 20 | adantl 480 |
. . . . . . . . 9
⊢ (((𝑉 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉) ∧ 𝑛 ∈ (𝑉 ∖ {𝑣})) → 𝑛 ≠ 𝑣) |
22 | 1 | cusgrexilem2 28966 |
. . . . . . . . . 10
⊢ (((𝑉 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉) ∧ 𝑛 ∈ (𝑉 ∖ {𝑣})) → ∃𝑒 ∈ ran ( I ↾ 𝑃){𝑣, 𝑛} ⊆ 𝑒) |
23 | | edgval 28576 |
. . . . . . . . . . . . 13
⊢
(Edg‘⟨𝑉,
( I ↾ 𝑃)⟩) = ran
(iEdg‘⟨𝑉, ( I
↾ 𝑃)⟩) |
24 | | opiedgfv 28534 |
. . . . . . . . . . . . . . 15
⊢ ((𝑉 ∈ 𝑊 ∧ ( I ↾ 𝑃) ∈ V) → (iEdg‘⟨𝑉, ( I ↾ 𝑃)⟩) = ( I ↾ 𝑃)) |
25 | 3, 24 | mpdan 683 |
. . . . . . . . . . . . . 14
⊢ (𝑉 ∈ 𝑊 → (iEdg‘⟨𝑉, ( I ↾ 𝑃)⟩) = ( I ↾ 𝑃)) |
26 | 25 | rneqd 5936 |
. . . . . . . . . . . . 13
⊢ (𝑉 ∈ 𝑊 → ran (iEdg‘⟨𝑉, ( I ↾ 𝑃)⟩) = ran ( I ↾ 𝑃)) |
27 | 23, 26 | eqtrid 2782 |
. . . . . . . . . . . 12
⊢ (𝑉 ∈ 𝑊 → (Edg‘⟨𝑉, ( I ↾ 𝑃)⟩) = ran ( I ↾ 𝑃)) |
28 | 27 | rexeqdv 3324 |
. . . . . . . . . . 11
⊢ (𝑉 ∈ 𝑊 → (∃𝑒 ∈ (Edg‘⟨𝑉, ( I ↾ 𝑃)⟩){𝑣, 𝑛} ⊆ 𝑒 ↔ ∃𝑒 ∈ ran ( I ↾ 𝑃){𝑣, 𝑛} ⊆ 𝑒)) |
29 | 28 | ad2antrr 722 |
. . . . . . . . . 10
⊢ (((𝑉 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉) ∧ 𝑛 ∈ (𝑉 ∖ {𝑣})) → (∃𝑒 ∈ (Edg‘⟨𝑉, ( I ↾ 𝑃)⟩){𝑣, 𝑛} ⊆ 𝑒 ↔ ∃𝑒 ∈ ran ( I ↾ 𝑃){𝑣, 𝑛} ⊆ 𝑒)) |
30 | 22, 29 | mpbird 256 |
. . . . . . . . 9
⊢ (((𝑉 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉) ∧ 𝑛 ∈ (𝑉 ∖ {𝑣})) → ∃𝑒 ∈ (Edg‘⟨𝑉, ( I ↾ 𝑃)⟩){𝑣, 𝑛} ⊆ 𝑒) |
31 | | eqid 2730 |
. . . . . . . . . 10
⊢
(Vtx‘⟨𝑉,
( I ↾ 𝑃)⟩) =
(Vtx‘⟨𝑉, ( I
↾ 𝑃)⟩) |
32 | | eqid 2730 |
. . . . . . . . . 10
⊢
(Edg‘⟨𝑉,
( I ↾ 𝑃)⟩) =
(Edg‘⟨𝑉, ( I
↾ 𝑃)⟩) |
33 | 31, 32 | nbgrel 28864 |
. . . . . . . . 9
⊢ (𝑛 ∈ (⟨𝑉, ( I ↾ 𝑃)⟩ NeighbVtx 𝑣) ↔ ((𝑛 ∈ (Vtx‘⟨𝑉, ( I ↾ 𝑃)⟩) ∧ 𝑣 ∈ (Vtx‘⟨𝑉, ( I ↾ 𝑃)⟩)) ∧ 𝑛 ≠ 𝑣 ∧ ∃𝑒 ∈ (Edg‘⟨𝑉, ( I ↾ 𝑃)⟩){𝑣, 𝑛} ⊆ 𝑒)) |
34 | 19, 21, 30, 33 | syl3anbrc 1341 |
. . . . . . . 8
⊢ (((𝑉 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉) ∧ 𝑛 ∈ (𝑉 ∖ {𝑣})) → 𝑛 ∈ (⟨𝑉, ( I ↾ 𝑃)⟩ NeighbVtx 𝑣)) |
35 | 34 | ralrimiva 3144 |
. . . . . . 7
⊢ ((𝑉 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉) → ∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ (⟨𝑉, ( I ↾ 𝑃)⟩ NeighbVtx 𝑣)) |
36 | 11 | adantr 479 |
. . . . . . . . 9
⊢ ((𝑉 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉) → (Vtx‘⟨𝑉, ( I ↾ 𝑃)⟩) = 𝑉) |
37 | 36 | difeq1d 4120 |
. . . . . . . 8
⊢ ((𝑉 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉) → ((Vtx‘⟨𝑉, ( I ↾ 𝑃)⟩) ∖ {𝑣}) = (𝑉 ∖ {𝑣})) |
38 | 37 | raleqdv 3323 |
. . . . . . 7
⊢ ((𝑉 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉) → (∀𝑛 ∈ ((Vtx‘⟨𝑉, ( I ↾ 𝑃)⟩) ∖ {𝑣})𝑛 ∈ (⟨𝑉, ( I ↾ 𝑃)⟩ NeighbVtx 𝑣) ↔ ∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ (⟨𝑉, ( I ↾ 𝑃)⟩ NeighbVtx 𝑣))) |
39 | 35, 38 | mpbird 256 |
. . . . . 6
⊢ ((𝑉 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉) → ∀𝑛 ∈ ((Vtx‘⟨𝑉, ( I ↾ 𝑃)⟩) ∖ {𝑣})𝑛 ∈ (⟨𝑉, ( I ↾ 𝑃)⟩ NeighbVtx 𝑣)) |
40 | 31 | uvtxel 28912 |
. . . . . 6
⊢ (𝑣 ∈
(UnivVtx‘⟨𝑉, ( I
↾ 𝑃)⟩) ↔
(𝑣 ∈
(Vtx‘⟨𝑉, ( I
↾ 𝑃)⟩) ∧
∀𝑛 ∈
((Vtx‘⟨𝑉, ( I
↾ 𝑃)⟩) ∖
{𝑣})𝑛 ∈ (⟨𝑉, ( I ↾ 𝑃)⟩ NeighbVtx 𝑣))) |
41 | 8, 39, 40 | sylanbrc 581 |
. . . . 5
⊢ ((𝑉 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉) → 𝑣 ∈ (UnivVtx‘⟨𝑉, ( I ↾ 𝑃)⟩)) |
42 | 41 | ralrimiva 3144 |
. . . 4
⊢ (𝑉 ∈ 𝑊 → ∀𝑣 ∈ 𝑉 𝑣 ∈ (UnivVtx‘⟨𝑉, ( I ↾ 𝑃)⟩)) |
43 | 11 | raleqdv 3323 |
. . . 4
⊢ (𝑉 ∈ 𝑊 → (∀𝑣 ∈ (Vtx‘⟨𝑉, ( I ↾ 𝑃)⟩)𝑣 ∈ (UnivVtx‘⟨𝑉, ( I ↾ 𝑃)⟩) ↔ ∀𝑣 ∈ 𝑉 𝑣 ∈ (UnivVtx‘⟨𝑉, ( I ↾ 𝑃)⟩))) |
44 | 42, 43 | mpbird 256 |
. . 3
⊢ (𝑉 ∈ 𝑊 → ∀𝑣 ∈ (Vtx‘⟨𝑉, ( I ↾ 𝑃)⟩)𝑣 ∈ (UnivVtx‘⟨𝑉, ( I ↾ 𝑃)⟩)) |
45 | | opex 5463 |
. . . 4
⊢
⟨𝑉, ( I ↾
𝑃)⟩ ∈
V |
46 | 31 | iscplgr 28939 |
. . . 4
⊢
(⟨𝑉, ( I
↾ 𝑃)⟩ ∈ V
→ (⟨𝑉, ( I
↾ 𝑃)⟩ ∈
ComplGraph ↔ ∀𝑣
∈ (Vtx‘⟨𝑉,
( I ↾ 𝑃)⟩)𝑣 ∈
(UnivVtx‘⟨𝑉, ( I
↾ 𝑃)⟩))) |
47 | 45, 46 | mp1i 13 |
. . 3
⊢ (𝑉 ∈ 𝑊 → (⟨𝑉, ( I ↾ 𝑃)⟩ ∈ ComplGraph ↔
∀𝑣 ∈
(Vtx‘⟨𝑉, ( I
↾ 𝑃)⟩)𝑣 ∈
(UnivVtx‘⟨𝑉, ( I
↾ 𝑃)⟩))) |
48 | 44, 47 | mpbird 256 |
. 2
⊢ (𝑉 ∈ 𝑊 → ⟨𝑉, ( I ↾ 𝑃)⟩ ∈ ComplGraph) |
49 | | iscusgr 28942 |
. 2
⊢
(⟨𝑉, ( I
↾ 𝑃)⟩ ∈
ComplUSGraph ↔ (⟨𝑉, ( I ↾ 𝑃)⟩ ∈ USGraph ∧ ⟨𝑉, ( I ↾ 𝑃)⟩ ∈ ComplGraph)) |
50 | 2, 48, 49 | sylanbrc 581 |
1
⊢ (𝑉 ∈ 𝑊 → ⟨𝑉, ( I ↾ 𝑃)⟩ ∈
ComplUSGraph) |