Step | Hyp | Ref
| Expression |
1 | | iscusgrvtx.v |
. . 3
⊢ 𝑉 = (Vtx‘𝐺) |
2 | | iscusgredg.v |
. . 3
⊢ 𝐸 = (Edg‘𝐺) |
3 | 1, 2 | iscusgredg 40645 |
. 2
⊢ (𝐺 ∈ ComplUSGraph ↔
(𝐺 ∈ USGraph ∧
∀𝑣 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑣}){𝑛, 𝑣} ∈ 𝐸)) |
4 | | usgredgss 40390 |
. . . . 5
⊢ (𝐺 ∈ USGraph →
(Edg‘𝐺) ⊆
{𝑥 ∈ 𝒫
(Vtx‘𝐺) ∣
(#‘𝑥) =
2}) |
5 | 1 | pweqi 4112 |
. . . . . 6
⊢ 𝒫
𝑉 = 𝒫
(Vtx‘𝐺) |
6 | | rabeq 3166 |
. . . . . 6
⊢
(𝒫 𝑉 =
𝒫 (Vtx‘𝐺)
→ {𝑥 ∈ 𝒫
𝑉 ∣ (#‘𝑥) = 2} = {𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ (#‘𝑥) = 2}) |
7 | 5, 6 | ax-mp 5 |
. . . . 5
⊢ {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2} = {𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ (#‘𝑥) = 2} |
8 | 4, 2, 7 | 3sstr4g 3609 |
. . . 4
⊢ (𝐺 ∈ USGraph → 𝐸 ⊆ {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2}) |
9 | 8 | adantr 480 |
. . 3
⊢ ((𝐺 ∈ USGraph ∧
∀𝑣 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑣}){𝑛, 𝑣} ∈ 𝐸) → 𝐸 ⊆ {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2}) |
10 | | elss2prb 13123 |
. . . . 5
⊢ (𝑝 ∈ {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2} ↔ ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑦 ≠ 𝑧 ∧ 𝑝 = {𝑦, 𝑧})) |
11 | | sneq 4135 |
. . . . . . . . . . . . . . 15
⊢ (𝑣 = 𝑦 → {𝑣} = {𝑦}) |
12 | 11 | difeq2d 3690 |
. . . . . . . . . . . . . 14
⊢ (𝑣 = 𝑦 → (𝑉 ∖ {𝑣}) = (𝑉 ∖ {𝑦})) |
13 | | preq2 4213 |
. . . . . . . . . . . . . . 15
⊢ (𝑣 = 𝑦 → {𝑛, 𝑣} = {𝑛, 𝑦}) |
14 | 13 | eleq1d 2672 |
. . . . . . . . . . . . . 14
⊢ (𝑣 = 𝑦 → ({𝑛, 𝑣} ∈ 𝐸 ↔ {𝑛, 𝑦} ∈ 𝐸)) |
15 | 12, 14 | raleqbidv 3129 |
. . . . . . . . . . . . 13
⊢ (𝑣 = 𝑦 → (∀𝑛 ∈ (𝑉 ∖ {𝑣}){𝑛, 𝑣} ∈ 𝐸 ↔ ∀𝑛 ∈ (𝑉 ∖ {𝑦}){𝑛, 𝑦} ∈ 𝐸)) |
16 | 15 | rspcv 3278 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ 𝑉 → (∀𝑣 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑣}){𝑛, 𝑣} ∈ 𝐸 → ∀𝑛 ∈ (𝑉 ∖ {𝑦}){𝑛, 𝑦} ∈ 𝐸)) |
17 | 16 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉) → (∀𝑣 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑣}){𝑛, 𝑣} ∈ 𝐸 → ∀𝑛 ∈ (𝑉 ∖ {𝑦}){𝑛, 𝑦} ∈ 𝐸)) |
18 | 17 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉) ∧ (𝑦 ≠ 𝑧 ∧ 𝑝 = {𝑦, 𝑧})) → (∀𝑣 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑣}){𝑛, 𝑣} ∈ 𝐸 → ∀𝑛 ∈ (𝑉 ∖ {𝑦}){𝑛, 𝑦} ∈ 𝐸)) |
19 | | simpr 476 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉) → 𝑧 ∈ 𝑉) |
20 | | necom 2835 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ≠ 𝑧 ↔ 𝑧 ≠ 𝑦) |
21 | 20 | biimpi 205 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ≠ 𝑧 → 𝑧 ≠ 𝑦) |
22 | 21 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ≠ 𝑧 ∧ 𝑝 = {𝑦, 𝑧}) → 𝑧 ≠ 𝑦) |
23 | 19, 22 | anim12i 588 |
. . . . . . . . . . . 12
⊢ (((𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉) ∧ (𝑦 ≠ 𝑧 ∧ 𝑝 = {𝑦, 𝑧})) → (𝑧 ∈ 𝑉 ∧ 𝑧 ≠ 𝑦)) |
24 | | eldifsn 4260 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ (𝑉 ∖ {𝑦}) ↔ (𝑧 ∈ 𝑉 ∧ 𝑧 ≠ 𝑦)) |
25 | 23, 24 | sylibr 223 |
. . . . . . . . . . 11
⊢ (((𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉) ∧ (𝑦 ≠ 𝑧 ∧ 𝑝 = {𝑦, 𝑧})) → 𝑧 ∈ (𝑉 ∖ {𝑦})) |
26 | | preq1 4212 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑧 → {𝑛, 𝑦} = {𝑧, 𝑦}) |
27 | 26 | eleq1d 2672 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑧 → ({𝑛, 𝑦} ∈ 𝐸 ↔ {𝑧, 𝑦} ∈ 𝐸)) |
28 | 27 | rspcv 3278 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ (𝑉 ∖ {𝑦}) → (∀𝑛 ∈ (𝑉 ∖ {𝑦}){𝑛, 𝑦} ∈ 𝐸 → {𝑧, 𝑦} ∈ 𝐸)) |
29 | 25, 28 | syl 17 |
. . . . . . . . . 10
⊢ (((𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉) ∧ (𝑦 ≠ 𝑧 ∧ 𝑝 = {𝑦, 𝑧})) → (∀𝑛 ∈ (𝑉 ∖ {𝑦}){𝑛, 𝑦} ∈ 𝐸 → {𝑧, 𝑦} ∈ 𝐸)) |
30 | | id 22 |
. . . . . . . . . . . . . . . 16
⊢ (𝑝 = {𝑦, 𝑧} → 𝑝 = {𝑦, 𝑧}) |
31 | | prcom 4211 |
. . . . . . . . . . . . . . . 16
⊢ {𝑦, 𝑧} = {𝑧, 𝑦} |
32 | 30, 31 | syl6req 2661 |
. . . . . . . . . . . . . . 15
⊢ (𝑝 = {𝑦, 𝑧} → {𝑧, 𝑦} = 𝑝) |
33 | 32 | eleq1d 2672 |
. . . . . . . . . . . . . 14
⊢ (𝑝 = {𝑦, 𝑧} → ({𝑧, 𝑦} ∈ 𝐸 ↔ 𝑝 ∈ 𝐸)) |
34 | 33 | biimpd 218 |
. . . . . . . . . . . . 13
⊢ (𝑝 = {𝑦, 𝑧} → ({𝑧, 𝑦} ∈ 𝐸 → 𝑝 ∈ 𝐸)) |
35 | 34 | a1d 25 |
. . . . . . . . . . . 12
⊢ (𝑝 = {𝑦, 𝑧} → (𝐺 ∈ USGraph → ({𝑧, 𝑦} ∈ 𝐸 → 𝑝 ∈ 𝐸))) |
36 | 35 | ad2antll 761 |
. . . . . . . . . . 11
⊢ (((𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉) ∧ (𝑦 ≠ 𝑧 ∧ 𝑝 = {𝑦, 𝑧})) → (𝐺 ∈ USGraph → ({𝑧, 𝑦} ∈ 𝐸 → 𝑝 ∈ 𝐸))) |
37 | 36 | com23 84 |
. . . . . . . . . 10
⊢ (((𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉) ∧ (𝑦 ≠ 𝑧 ∧ 𝑝 = {𝑦, 𝑧})) → ({𝑧, 𝑦} ∈ 𝐸 → (𝐺 ∈ USGraph → 𝑝 ∈ 𝐸))) |
38 | 18, 29, 37 | 3syld 58 |
. . . . . . . . 9
⊢ (((𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉) ∧ (𝑦 ≠ 𝑧 ∧ 𝑝 = {𝑦, 𝑧})) → (∀𝑣 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑣}){𝑛, 𝑣} ∈ 𝐸 → (𝐺 ∈ USGraph → 𝑝 ∈ 𝐸))) |
39 | 38 | ex 449 |
. . . . . . . 8
⊢ ((𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉) → ((𝑦 ≠ 𝑧 ∧ 𝑝 = {𝑦, 𝑧}) → (∀𝑣 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑣}){𝑛, 𝑣} ∈ 𝐸 → (𝐺 ∈ USGraph → 𝑝 ∈ 𝐸)))) |
40 | 39 | rexlimivv 3018 |
. . . . . . 7
⊢
(∃𝑦 ∈
𝑉 ∃𝑧 ∈ 𝑉 (𝑦 ≠ 𝑧 ∧ 𝑝 = {𝑦, 𝑧}) → (∀𝑣 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑣}){𝑛, 𝑣} ∈ 𝐸 → (𝐺 ∈ USGraph → 𝑝 ∈ 𝐸))) |
41 | 40 | com13 86 |
. . . . . 6
⊢ (𝐺 ∈ USGraph →
(∀𝑣 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑣}){𝑛, 𝑣} ∈ 𝐸 → (∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑦 ≠ 𝑧 ∧ 𝑝 = {𝑦, 𝑧}) → 𝑝 ∈ 𝐸))) |
42 | 41 | imp 444 |
. . . . 5
⊢ ((𝐺 ∈ USGraph ∧
∀𝑣 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑣}){𝑛, 𝑣} ∈ 𝐸) → (∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑦 ≠ 𝑧 ∧ 𝑝 = {𝑦, 𝑧}) → 𝑝 ∈ 𝐸)) |
43 | 10, 42 | syl5bi 231 |
. . . 4
⊢ ((𝐺 ∈ USGraph ∧
∀𝑣 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑣}){𝑛, 𝑣} ∈ 𝐸) → (𝑝 ∈ {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2} → 𝑝 ∈ 𝐸)) |
44 | 43 | ssrdv 3574 |
. . 3
⊢ ((𝐺 ∈ USGraph ∧
∀𝑣 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑣}){𝑛, 𝑣} ∈ 𝐸) → {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2} ⊆ 𝐸) |
45 | 9, 44 | eqssd 3585 |
. 2
⊢ ((𝐺 ∈ USGraph ∧
∀𝑣 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑣}){𝑛, 𝑣} ∈ 𝐸) → 𝐸 = {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2}) |
46 | 3, 45 | sylbi 206 |
1
⊢ (𝐺 ∈ ComplUSGraph →
𝐸 = {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2}) |