Step | Hyp | Ref
| Expression |
1 | | usgrexi.p |
. . 3
⊢ 𝑃 = {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2} |
2 | 1 | usgrexi 40661 |
. 2
⊢ (𝑉 ∈ 𝑊 → 〈𝑉, ( I ↾ 𝑃)〉 ∈ USGraph ) |
3 | 1 | cusgraexilem1 25995 |
. . . . . . . . . 10
⊢ (𝑉 ∈ 𝑊 → ( I ↾ 𝑃) ∈ V) |
4 | | opvtxfv 25681 |
. . . . . . . . . . 11
⊢ ((𝑉 ∈ 𝑊 ∧ ( I ↾ 𝑃) ∈ V) → (Vtx‘〈𝑉, ( I ↾ 𝑃)〉) = 𝑉) |
5 | 4 | eqcomd 2616 |
. . . . . . . . . 10
⊢ ((𝑉 ∈ 𝑊 ∧ ( I ↾ 𝑃) ∈ V) → 𝑉 = (Vtx‘〈𝑉, ( I ↾ 𝑃)〉)) |
6 | 3, 5 | mpdan 699 |
. . . . . . . . 9
⊢ (𝑉 ∈ 𝑊 → 𝑉 = (Vtx‘〈𝑉, ( I ↾ 𝑃)〉)) |
7 | 6 | eleq2d 2673 |
. . . . . . . 8
⊢ (𝑉 ∈ 𝑊 → (𝑣 ∈ 𝑉 ↔ 𝑣 ∈ (Vtx‘〈𝑉, ( I ↾ 𝑃)〉))) |
8 | 7 | biimpa 500 |
. . . . . . 7
⊢ ((𝑉 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉) → 𝑣 ∈ (Vtx‘〈𝑉, ( I ↾ 𝑃)〉)) |
9 | | eldifi 3694 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ (𝑉 ∖ {𝑣}) → 𝑛 ∈ 𝑉) |
10 | 9 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((𝑉 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉) ∧ 𝑛 ∈ (𝑉 ∖ {𝑣})) → 𝑛 ∈ 𝑉) |
11 | 3, 4 | mpdan 699 |
. . . . . . . . . . . . . 14
⊢ (𝑉 ∈ 𝑊 → (Vtx‘〈𝑉, ( I ↾ 𝑃)〉) = 𝑉) |
12 | 11 | eleq2d 2673 |
. . . . . . . . . . . . 13
⊢ (𝑉 ∈ 𝑊 → (𝑛 ∈ (Vtx‘〈𝑉, ( I ↾ 𝑃)〉) ↔ 𝑛 ∈ 𝑉)) |
13 | 12 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ (((𝑉 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉) ∧ 𝑛 ∈ (𝑉 ∖ {𝑣})) → (𝑛 ∈ (Vtx‘〈𝑉, ( I ↾ 𝑃)〉) ↔ 𝑛 ∈ 𝑉)) |
14 | 10, 13 | mpbird 246 |
. . . . . . . . . . 11
⊢ (((𝑉 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉) ∧ 𝑛 ∈ (𝑉 ∖ {𝑣})) → 𝑛 ∈ (Vtx‘〈𝑉, ( I ↾ 𝑃)〉)) |
15 | | simpr 476 |
. . . . . . . . . . . . 13
⊢ ((𝑉 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉) → 𝑣 ∈ 𝑉) |
16 | 15 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝑉 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉) ∧ 𝑛 ∈ (𝑉 ∖ {𝑣})) → 𝑣 ∈ 𝑉) |
17 | 11 | eleq2d 2673 |
. . . . . . . . . . . . 13
⊢ (𝑉 ∈ 𝑊 → (𝑣 ∈ (Vtx‘〈𝑉, ( I ↾ 𝑃)〉) ↔ 𝑣 ∈ 𝑉)) |
18 | 17 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ (((𝑉 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉) ∧ 𝑛 ∈ (𝑉 ∖ {𝑣})) → (𝑣 ∈ (Vtx‘〈𝑉, ( I ↾ 𝑃)〉) ↔ 𝑣 ∈ 𝑉)) |
19 | 16, 18 | mpbird 246 |
. . . . . . . . . . 11
⊢ (((𝑉 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉) ∧ 𝑛 ∈ (𝑉 ∖ {𝑣})) → 𝑣 ∈ (Vtx‘〈𝑉, ( I ↾ 𝑃)〉)) |
20 | 14, 19 | jca 553 |
. . . . . . . . . 10
⊢ (((𝑉 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉) ∧ 𝑛 ∈ (𝑉 ∖ {𝑣})) → (𝑛 ∈ (Vtx‘〈𝑉, ( I ↾ 𝑃)〉) ∧ 𝑣 ∈ (Vtx‘〈𝑉, ( I ↾ 𝑃)〉))) |
21 | | eldifsn 4260 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ (𝑉 ∖ {𝑣}) ↔ (𝑛 ∈ 𝑉 ∧ 𝑛 ≠ 𝑣)) |
22 | | simpr 476 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈ 𝑉 ∧ 𝑛 ≠ 𝑣) → 𝑛 ≠ 𝑣) |
23 | 21, 22 | sylbi 206 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ (𝑉 ∖ {𝑣}) → 𝑛 ≠ 𝑣) |
24 | 23 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝑉 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉) ∧ 𝑛 ∈ (𝑉 ∖ {𝑣})) → 𝑛 ≠ 𝑣) |
25 | | prelpwi 4842 |
. . . . . . . . . . . . . 14
⊢ ((𝑣 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉) → {𝑣, 𝑛} ∈ 𝒫 𝑉) |
26 | 15, 9, 25 | syl2an 493 |
. . . . . . . . . . . . 13
⊢ (((𝑉 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉) ∧ 𝑛 ∈ (𝑉 ∖ {𝑣})) → {𝑣, 𝑛} ∈ 𝒫 𝑉) |
27 | 22 | necomd 2837 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈ 𝑉 ∧ 𝑛 ≠ 𝑣) → 𝑣 ≠ 𝑛) |
28 | 21, 27 | sylbi 206 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ (𝑉 ∖ {𝑣}) → 𝑣 ≠ 𝑛) |
29 | 28 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ (((𝑉 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉) ∧ 𝑛 ∈ (𝑉 ∖ {𝑣})) → 𝑣 ≠ 𝑛) |
30 | | hashprg 13043 |
. . . . . . . . . . . . . . 15
⊢ ((𝑣 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉) → (𝑣 ≠ 𝑛 ↔ (#‘{𝑣, 𝑛}) = 2)) |
31 | 15, 9, 30 | syl2an 493 |
. . . . . . . . . . . . . 14
⊢ (((𝑉 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉) ∧ 𝑛 ∈ (𝑉 ∖ {𝑣})) → (𝑣 ≠ 𝑛 ↔ (#‘{𝑣, 𝑛}) = 2)) |
32 | 29, 31 | mpbid 221 |
. . . . . . . . . . . . 13
⊢ (((𝑉 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉) ∧ 𝑛 ∈ (𝑉 ∖ {𝑣})) → (#‘{𝑣, 𝑛}) = 2) |
33 | | fveq2 6103 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = {𝑣, 𝑛} → (#‘𝑥) = (#‘{𝑣, 𝑛})) |
34 | 33 | eqeq1d 2612 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = {𝑣, 𝑛} → ((#‘𝑥) = 2 ↔ (#‘{𝑣, 𝑛}) = 2)) |
35 | | rnresi 5398 |
. . . . . . . . . . . . . . 15
⊢ ran ( I
↾ 𝑃) = 𝑃 |
36 | 35, 1 | eqtri 2632 |
. . . . . . . . . . . . . 14
⊢ ran ( I
↾ 𝑃) = {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2} |
37 | 34, 36 | elrab2 3333 |
. . . . . . . . . . . . 13
⊢ ({𝑣, 𝑛} ∈ ran ( I ↾ 𝑃) ↔ ({𝑣, 𝑛} ∈ 𝒫 𝑉 ∧ (#‘{𝑣, 𝑛}) = 2)) |
38 | 26, 32, 37 | sylanbrc 695 |
. . . . . . . . . . . 12
⊢ (((𝑉 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉) ∧ 𝑛 ∈ (𝑉 ∖ {𝑣})) → {𝑣, 𝑛} ∈ ran ( I ↾ 𝑃)) |
39 | | sseq2 3590 |
. . . . . . . . . . . . 13
⊢ (𝑒 = {𝑣, 𝑛} → ({𝑣, 𝑛} ⊆ 𝑒 ↔ {𝑣, 𝑛} ⊆ {𝑣, 𝑛})) |
40 | 39 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((((𝑉 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉) ∧ 𝑛 ∈ (𝑉 ∖ {𝑣})) ∧ 𝑒 = {𝑣, 𝑛}) → ({𝑣, 𝑛} ⊆ 𝑒 ↔ {𝑣, 𝑛} ⊆ {𝑣, 𝑛})) |
41 | | ssid 3587 |
. . . . . . . . . . . . 13
⊢ {𝑣, 𝑛} ⊆ {𝑣, 𝑛} |
42 | 41 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝑉 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉) ∧ 𝑛 ∈ (𝑉 ∖ {𝑣})) → {𝑣, 𝑛} ⊆ {𝑣, 𝑛}) |
43 | 38, 40, 42 | rspcedvd 3289 |
. . . . . . . . . . 11
⊢ (((𝑉 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉) ∧ 𝑛 ∈ (𝑉 ∖ {𝑣})) → ∃𝑒 ∈ ran ( I ↾ 𝑃){𝑣, 𝑛} ⊆ 𝑒) |
44 | | opex 4859 |
. . . . . . . . . . . . . . 15
⊢
〈𝑉, ( I ↾
𝑃)〉 ∈
V |
45 | | edgaval 25794 |
. . . . . . . . . . . . . . 15
⊢
(〈𝑉, ( I
↾ 𝑃)〉 ∈ V
→ (Edg‘〈𝑉,
( I ↾ 𝑃)〉) = ran
(iEdg‘〈𝑉, ( I
↾ 𝑃)〉)) |
46 | 44, 45 | mp1i 13 |
. . . . . . . . . . . . . 14
⊢ (𝑉 ∈ 𝑊 → (Edg‘〈𝑉, ( I ↾ 𝑃)〉) = ran (iEdg‘〈𝑉, ( I ↾ 𝑃)〉)) |
47 | | opiedgfv 25684 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑉 ∈ 𝑊 ∧ ( I ↾ 𝑃) ∈ V) → (iEdg‘〈𝑉, ( I ↾ 𝑃)〉) = ( I ↾ 𝑃)) |
48 | 3, 47 | mpdan 699 |
. . . . . . . . . . . . . . 15
⊢ (𝑉 ∈ 𝑊 → (iEdg‘〈𝑉, ( I ↾ 𝑃)〉) = ( I ↾ 𝑃)) |
49 | 48 | rneqd 5274 |
. . . . . . . . . . . . . 14
⊢ (𝑉 ∈ 𝑊 → ran (iEdg‘〈𝑉, ( I ↾ 𝑃)〉) = ran ( I ↾ 𝑃)) |
50 | 46, 49 | eqtrd 2644 |
. . . . . . . . . . . . 13
⊢ (𝑉 ∈ 𝑊 → (Edg‘〈𝑉, ( I ↾ 𝑃)〉) = ran ( I ↾ 𝑃)) |
51 | 50 | rexeqdv 3122 |
. . . . . . . . . . . 12
⊢ (𝑉 ∈ 𝑊 → (∃𝑒 ∈ (Edg‘〈𝑉, ( I ↾ 𝑃)〉){𝑣, 𝑛} ⊆ 𝑒 ↔ ∃𝑒 ∈ ran ( I ↾ 𝑃){𝑣, 𝑛} ⊆ 𝑒)) |
52 | 51 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝑉 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉) ∧ 𝑛 ∈ (𝑉 ∖ {𝑣})) → (∃𝑒 ∈ (Edg‘〈𝑉, ( I ↾ 𝑃)〉){𝑣, 𝑛} ⊆ 𝑒 ↔ ∃𝑒 ∈ ran ( I ↾ 𝑃){𝑣, 𝑛} ⊆ 𝑒)) |
53 | 43, 52 | mpbird 246 |
. . . . . . . . . 10
⊢ (((𝑉 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉) ∧ 𝑛 ∈ (𝑉 ∖ {𝑣})) → ∃𝑒 ∈ (Edg‘〈𝑉, ( I ↾ 𝑃)〉){𝑣, 𝑛} ⊆ 𝑒) |
54 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(Vtx‘〈𝑉,
( I ↾ 𝑃)〉) =
(Vtx‘〈𝑉, ( I
↾ 𝑃)〉) |
55 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(Edg‘〈𝑉,
( I ↾ 𝑃)〉) =
(Edg‘〈𝑉, ( I
↾ 𝑃)〉) |
56 | 54, 55 | nbgrel 40564 |
. . . . . . . . . . 11
⊢
(〈𝑉, ( I
↾ 𝑃)〉 ∈ V
→ (𝑛 ∈
(〈𝑉, ( I ↾ 𝑃)〉 NeighbVtx 𝑣) ↔ ((𝑛 ∈ (Vtx‘〈𝑉, ( I ↾ 𝑃)〉) ∧ 𝑣 ∈ (Vtx‘〈𝑉, ( I ↾ 𝑃)〉)) ∧ 𝑛 ≠ 𝑣 ∧ ∃𝑒 ∈ (Edg‘〈𝑉, ( I ↾ 𝑃)〉){𝑣, 𝑛} ⊆ 𝑒))) |
57 | 44, 56 | mp1i 13 |
. . . . . . . . . 10
⊢ (((𝑉 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉) ∧ 𝑛 ∈ (𝑉 ∖ {𝑣})) → (𝑛 ∈ (〈𝑉, ( I ↾ 𝑃)〉 NeighbVtx 𝑣) ↔ ((𝑛 ∈ (Vtx‘〈𝑉, ( I ↾ 𝑃)〉) ∧ 𝑣 ∈ (Vtx‘〈𝑉, ( I ↾ 𝑃)〉)) ∧ 𝑛 ≠ 𝑣 ∧ ∃𝑒 ∈ (Edg‘〈𝑉, ( I ↾ 𝑃)〉){𝑣, 𝑛} ⊆ 𝑒))) |
58 | 20, 24, 53, 57 | mpbir3and 1238 |
. . . . . . . . 9
⊢ (((𝑉 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉) ∧ 𝑛 ∈ (𝑉 ∖ {𝑣})) → 𝑛 ∈ (〈𝑉, ( I ↾ 𝑃)〉 NeighbVtx 𝑣)) |
59 | 58 | ralrimiva 2949 |
. . . . . . . 8
⊢ ((𝑉 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉) → ∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ (〈𝑉, ( I ↾ 𝑃)〉 NeighbVtx 𝑣)) |
60 | 11 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑉 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉) → (Vtx‘〈𝑉, ( I ↾ 𝑃)〉) = 𝑉) |
61 | 60 | difeq1d 3689 |
. . . . . . . . 9
⊢ ((𝑉 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉) → ((Vtx‘〈𝑉, ( I ↾ 𝑃)〉) ∖ {𝑣}) = (𝑉 ∖ {𝑣})) |
62 | 61 | raleqdv 3121 |
. . . . . . . 8
⊢ ((𝑉 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉) → (∀𝑛 ∈ ((Vtx‘〈𝑉, ( I ↾ 𝑃)〉) ∖ {𝑣})𝑛 ∈ (〈𝑉, ( I ↾ 𝑃)〉 NeighbVtx 𝑣) ↔ ∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ (〈𝑉, ( I ↾ 𝑃)〉 NeighbVtx 𝑣))) |
63 | 59, 62 | mpbird 246 |
. . . . . . 7
⊢ ((𝑉 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉) → ∀𝑛 ∈ ((Vtx‘〈𝑉, ( I ↾ 𝑃)〉) ∖ {𝑣})𝑛 ∈ (〈𝑉, ( I ↾ 𝑃)〉 NeighbVtx 𝑣)) |
64 | 8, 63 | jca 553 |
. . . . . 6
⊢ ((𝑉 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉) → (𝑣 ∈ (Vtx‘〈𝑉, ( I ↾ 𝑃)〉) ∧ ∀𝑛 ∈ ((Vtx‘〈𝑉, ( I ↾ 𝑃)〉) ∖ {𝑣})𝑛 ∈ (〈𝑉, ( I ↾ 𝑃)〉 NeighbVtx 𝑣))) |
65 | 54 | uvtxael 40614 |
. . . . . . 7
⊢
(〈𝑉, ( I
↾ 𝑃)〉 ∈ V
→ (𝑣 ∈
(UnivVtx‘〈𝑉, ( I
↾ 𝑃)〉) ↔
(𝑣 ∈
(Vtx‘〈𝑉, ( I
↾ 𝑃)〉) ∧
∀𝑛 ∈
((Vtx‘〈𝑉, ( I
↾ 𝑃)〉) ∖
{𝑣})𝑛 ∈ (〈𝑉, ( I ↾ 𝑃)〉 NeighbVtx 𝑣)))) |
66 | 44, 65 | mp1i 13 |
. . . . . 6
⊢ ((𝑉 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉) → (𝑣 ∈ (UnivVtx‘〈𝑉, ( I ↾ 𝑃)〉) ↔ (𝑣 ∈ (Vtx‘〈𝑉, ( I ↾ 𝑃)〉) ∧ ∀𝑛 ∈ ((Vtx‘〈𝑉, ( I ↾ 𝑃)〉) ∖ {𝑣})𝑛 ∈ (〈𝑉, ( I ↾ 𝑃)〉 NeighbVtx 𝑣)))) |
67 | 64, 66 | mpbird 246 |
. . . . 5
⊢ ((𝑉 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉) → 𝑣 ∈ (UnivVtx‘〈𝑉, ( I ↾ 𝑃)〉)) |
68 | 67 | ralrimiva 2949 |
. . . 4
⊢ (𝑉 ∈ 𝑊 → ∀𝑣 ∈ 𝑉 𝑣 ∈ (UnivVtx‘〈𝑉, ( I ↾ 𝑃)〉)) |
69 | 11 | raleqdv 3121 |
. . . 4
⊢ (𝑉 ∈ 𝑊 → (∀𝑣 ∈ (Vtx‘〈𝑉, ( I ↾ 𝑃)〉)𝑣 ∈ (UnivVtx‘〈𝑉, ( I ↾ 𝑃)〉) ↔ ∀𝑣 ∈ 𝑉 𝑣 ∈ (UnivVtx‘〈𝑉, ( I ↾ 𝑃)〉))) |
70 | 68, 69 | mpbird 246 |
. . 3
⊢ (𝑉 ∈ 𝑊 → ∀𝑣 ∈ (Vtx‘〈𝑉, ( I ↾ 𝑃)〉)𝑣 ∈ (UnivVtx‘〈𝑉, ( I ↾ 𝑃)〉)) |
71 | 54 | iscplgr 40636 |
. . . 4
⊢
(〈𝑉, ( I
↾ 𝑃)〉 ∈ V
→ (〈𝑉, ( I
↾ 𝑃)〉 ∈
ComplGraph ↔ ∀𝑣
∈ (Vtx‘〈𝑉,
( I ↾ 𝑃)〉)𝑣 ∈
(UnivVtx‘〈𝑉, ( I
↾ 𝑃)〉))) |
72 | 44, 71 | mp1i 13 |
. . 3
⊢ (𝑉 ∈ 𝑊 → (〈𝑉, ( I ↾ 𝑃)〉 ∈ ComplGraph ↔
∀𝑣 ∈
(Vtx‘〈𝑉, ( I
↾ 𝑃)〉)𝑣 ∈
(UnivVtx‘〈𝑉, ( I
↾ 𝑃)〉))) |
73 | 70, 72 | mpbird 246 |
. 2
⊢ (𝑉 ∈ 𝑊 → 〈𝑉, ( I ↾ 𝑃)〉 ∈ ComplGraph) |
74 | | iscusgr 40640 |
. 2
⊢
(〈𝑉, ( I
↾ 𝑃)〉 ∈
ComplUSGraph ↔ (〈𝑉, ( I ↾ 𝑃)〉 ∈ USGraph ∧ 〈𝑉, ( I ↾ 𝑃)〉 ∈ ComplGraph)) |
75 | 2, 73, 74 | sylanbrc 695 |
1
⊢ (𝑉 ∈ 𝑊 → 〈𝑉, ( I ↾ 𝑃)〉 ∈
ComplUSGraph) |