Step | Hyp | Ref
| Expression |
1 | | iscusgrvtx.v |
. . 3
⊢ 𝑉 = (Vtx‘𝐺) |
2 | | iscusgredg.v |
. . 3
⊢ 𝐸 = (Edg‘𝐺) |
3 | 1, 2 | iscusgredg 26720 |
. 2
⊢ (𝐺 ∈ ComplUSGraph ↔
(𝐺 ∈ USGraph ∧
∀𝑣 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑣}){𝑛, 𝑣} ∈ 𝐸)) |
4 | | usgredgss 26457 |
. . . . 5
⊢ (𝐺 ∈ USGraph →
(Edg‘𝐺) ⊆
{𝑥 ∈ 𝒫
(Vtx‘𝐺) ∣
(♯‘𝑥) =
2}) |
5 | 1 | pweqi 4381 |
. . . . . 6
⊢ 𝒫
𝑉 = 𝒫
(Vtx‘𝐺) |
6 | | rabeq 3404 |
. . . . . 6
⊢
(𝒫 𝑉 =
𝒫 (Vtx‘𝐺)
→ {𝑥 ∈ 𝒫
𝑉 ∣
(♯‘𝑥) = 2} =
{𝑥 ∈ 𝒫
(Vtx‘𝐺) ∣
(♯‘𝑥) =
2}) |
7 | 5, 6 | ax-mp 5 |
. . . . 5
⊢ {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2} = {𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ (♯‘𝑥) = 2} |
8 | 4, 2, 7 | 3sstr4g 3870 |
. . . 4
⊢ (𝐺 ∈ USGraph → 𝐸 ⊆ {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2}) |
9 | 8 | adantr 474 |
. . 3
⊢ ((𝐺 ∈ USGraph ∧
∀𝑣 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑣}){𝑛, 𝑣} ∈ 𝐸) → 𝐸 ⊆ {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2}) |
10 | | elss2prb 13557 |
. . . . 5
⊢ (𝑝 ∈ {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2} ↔ ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑦 ≠ 𝑧 ∧ 𝑝 = {𝑦, 𝑧})) |
11 | | sneq 4406 |
. . . . . . . . . . . . . . 15
⊢ (𝑣 = 𝑦 → {𝑣} = {𝑦}) |
12 | 11 | difeq2d 3954 |
. . . . . . . . . . . . . 14
⊢ (𝑣 = 𝑦 → (𝑉 ∖ {𝑣}) = (𝑉 ∖ {𝑦})) |
13 | | preq2 4486 |
. . . . . . . . . . . . . . 15
⊢ (𝑣 = 𝑦 → {𝑛, 𝑣} = {𝑛, 𝑦}) |
14 | 13 | eleq1d 2890 |
. . . . . . . . . . . . . 14
⊢ (𝑣 = 𝑦 → ({𝑛, 𝑣} ∈ 𝐸 ↔ {𝑛, 𝑦} ∈ 𝐸)) |
15 | 12, 14 | raleqbidv 3363 |
. . . . . . . . . . . . 13
⊢ (𝑣 = 𝑦 → (∀𝑛 ∈ (𝑉 ∖ {𝑣}){𝑛, 𝑣} ∈ 𝐸 ↔ ∀𝑛 ∈ (𝑉 ∖ {𝑦}){𝑛, 𝑦} ∈ 𝐸)) |
16 | 15 | rspcv 3521 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ 𝑉 → (∀𝑣 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑣}){𝑛, 𝑣} ∈ 𝐸 → ∀𝑛 ∈ (𝑉 ∖ {𝑦}){𝑛, 𝑦} ∈ 𝐸)) |
17 | 16 | adantr 474 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉) → (∀𝑣 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑣}){𝑛, 𝑣} ∈ 𝐸 → ∀𝑛 ∈ (𝑉 ∖ {𝑦}){𝑛, 𝑦} ∈ 𝐸)) |
18 | 17 | adantr 474 |
. . . . . . . . . 10
⊢ (((𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉) ∧ (𝑦 ≠ 𝑧 ∧ 𝑝 = {𝑦, 𝑧})) → (∀𝑣 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑣}){𝑛, 𝑣} ∈ 𝐸 → ∀𝑛 ∈ (𝑉 ∖ {𝑦}){𝑛, 𝑦} ∈ 𝐸)) |
19 | | simpr 479 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉) → 𝑧 ∈ 𝑉) |
20 | | necom 3051 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ≠ 𝑧 ↔ 𝑧 ≠ 𝑦) |
21 | 20 | biimpi 208 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ≠ 𝑧 → 𝑧 ≠ 𝑦) |
22 | 21 | adantr 474 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ≠ 𝑧 ∧ 𝑝 = {𝑦, 𝑧}) → 𝑧 ≠ 𝑦) |
23 | 19, 22 | anim12i 608 |
. . . . . . . . . . . 12
⊢ (((𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉) ∧ (𝑦 ≠ 𝑧 ∧ 𝑝 = {𝑦, 𝑧})) → (𝑧 ∈ 𝑉 ∧ 𝑧 ≠ 𝑦)) |
24 | | eldifsn 4535 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ (𝑉 ∖ {𝑦}) ↔ (𝑧 ∈ 𝑉 ∧ 𝑧 ≠ 𝑦)) |
25 | 23, 24 | sylibr 226 |
. . . . . . . . . . 11
⊢ (((𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉) ∧ (𝑦 ≠ 𝑧 ∧ 𝑝 = {𝑦, 𝑧})) → 𝑧 ∈ (𝑉 ∖ {𝑦})) |
26 | | preq1 4485 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑧 → {𝑛, 𝑦} = {𝑧, 𝑦}) |
27 | 26 | eleq1d 2890 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑧 → ({𝑛, 𝑦} ∈ 𝐸 ↔ {𝑧, 𝑦} ∈ 𝐸)) |
28 | 27 | rspcv 3521 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ (𝑉 ∖ {𝑦}) → (∀𝑛 ∈ (𝑉 ∖ {𝑦}){𝑛, 𝑦} ∈ 𝐸 → {𝑧, 𝑦} ∈ 𝐸)) |
29 | 25, 28 | syl 17 |
. . . . . . . . . 10
⊢ (((𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉) ∧ (𝑦 ≠ 𝑧 ∧ 𝑝 = {𝑦, 𝑧})) → (∀𝑛 ∈ (𝑉 ∖ {𝑦}){𝑛, 𝑦} ∈ 𝐸 → {𝑧, 𝑦} ∈ 𝐸)) |
30 | | id 22 |
. . . . . . . . . . . . . . . 16
⊢ (𝑝 = {𝑦, 𝑧} → 𝑝 = {𝑦, 𝑧}) |
31 | | prcom 4484 |
. . . . . . . . . . . . . . . 16
⊢ {𝑦, 𝑧} = {𝑧, 𝑦} |
32 | 30, 31 | syl6req 2877 |
. . . . . . . . . . . . . . 15
⊢ (𝑝 = {𝑦, 𝑧} → {𝑧, 𝑦} = 𝑝) |
33 | 32 | eleq1d 2890 |
. . . . . . . . . . . . . 14
⊢ (𝑝 = {𝑦, 𝑧} → ({𝑧, 𝑦} ∈ 𝐸 ↔ 𝑝 ∈ 𝐸)) |
34 | 33 | biimpd 221 |
. . . . . . . . . . . . 13
⊢ (𝑝 = {𝑦, 𝑧} → ({𝑧, 𝑦} ∈ 𝐸 → 𝑝 ∈ 𝐸)) |
35 | 34 | a1d 25 |
. . . . . . . . . . . 12
⊢ (𝑝 = {𝑦, 𝑧} → (𝐺 ∈ USGraph → ({𝑧, 𝑦} ∈ 𝐸 → 𝑝 ∈ 𝐸))) |
36 | 35 | ad2antll 722 |
. . . . . . . . . . 11
⊢ (((𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉) ∧ (𝑦 ≠ 𝑧 ∧ 𝑝 = {𝑦, 𝑧})) → (𝐺 ∈ USGraph → ({𝑧, 𝑦} ∈ 𝐸 → 𝑝 ∈ 𝐸))) |
37 | 36 | com23 86 |
. . . . . . . . . 10
⊢ (((𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉) ∧ (𝑦 ≠ 𝑧 ∧ 𝑝 = {𝑦, 𝑧})) → ({𝑧, 𝑦} ∈ 𝐸 → (𝐺 ∈ USGraph → 𝑝 ∈ 𝐸))) |
38 | 18, 29, 37 | 3syld 60 |
. . . . . . . . 9
⊢ (((𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉) ∧ (𝑦 ≠ 𝑧 ∧ 𝑝 = {𝑦, 𝑧})) → (∀𝑣 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑣}){𝑛, 𝑣} ∈ 𝐸 → (𝐺 ∈ USGraph → 𝑝 ∈ 𝐸))) |
39 | 38 | ex 403 |
. . . . . . . 8
⊢ ((𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉) → ((𝑦 ≠ 𝑧 ∧ 𝑝 = {𝑦, 𝑧}) → (∀𝑣 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑣}){𝑛, 𝑣} ∈ 𝐸 → (𝐺 ∈ USGraph → 𝑝 ∈ 𝐸)))) |
40 | 39 | rexlimivv 3245 |
. . . . . . 7
⊢
(∃𝑦 ∈
𝑉 ∃𝑧 ∈ 𝑉 (𝑦 ≠ 𝑧 ∧ 𝑝 = {𝑦, 𝑧}) → (∀𝑣 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑣}){𝑛, 𝑣} ∈ 𝐸 → (𝐺 ∈ USGraph → 𝑝 ∈ 𝐸))) |
41 | 40 | com13 88 |
. . . . . 6
⊢ (𝐺 ∈ USGraph →
(∀𝑣 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑣}){𝑛, 𝑣} ∈ 𝐸 → (∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑦 ≠ 𝑧 ∧ 𝑝 = {𝑦, 𝑧}) → 𝑝 ∈ 𝐸))) |
42 | 41 | imp 397 |
. . . . 5
⊢ ((𝐺 ∈ USGraph ∧
∀𝑣 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑣}){𝑛, 𝑣} ∈ 𝐸) → (∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑦 ≠ 𝑧 ∧ 𝑝 = {𝑦, 𝑧}) → 𝑝 ∈ 𝐸)) |
43 | 10, 42 | syl5bi 234 |
. . . 4
⊢ ((𝐺 ∈ USGraph ∧
∀𝑣 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑣}){𝑛, 𝑣} ∈ 𝐸) → (𝑝 ∈ {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2} → 𝑝 ∈ 𝐸)) |
44 | 43 | ssrdv 3832 |
. . 3
⊢ ((𝐺 ∈ USGraph ∧
∀𝑣 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑣}){𝑛, 𝑣} ∈ 𝐸) → {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2} ⊆ 𝐸) |
45 | 9, 44 | eqssd 3843 |
. 2
⊢ ((𝐺 ∈ USGraph ∧
∀𝑣 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑣}){𝑛, 𝑣} ∈ 𝐸) → 𝐸 = {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2}) |
46 | 3, 45 | sylbi 209 |
1
⊢ (𝐺 ∈ ComplUSGraph →
𝐸 = {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2}) |