Step | Hyp | Ref
| Expression |
1 | | upgredg.e |
. . . . . . 7
⊢ 𝐸 = (Edg‘𝐺) |
2 | | edgaval 25794 |
. . . . . . 7
⊢ (𝐺 ∈ UPGraph →
(Edg‘𝐺) = ran
(iEdg‘𝐺)) |
3 | 1, 2 | syl5eq 2656 |
. . . . . 6
⊢ (𝐺 ∈ UPGraph → 𝐸 = ran (iEdg‘𝐺)) |
4 | 3 | eleq2d 2673 |
. . . . 5
⊢ (𝐺 ∈ UPGraph → (𝐶 ∈ 𝐸 ↔ 𝐶 ∈ ran (iEdg‘𝐺))) |
5 | | upgredg.v |
. . . . . . . 8
⊢ 𝑉 = (Vtx‘𝐺) |
6 | | eqid 2610 |
. . . . . . . 8
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) |
7 | 5, 6 | upgrf 25753 |
. . . . . . 7
⊢ (𝐺 ∈ UPGraph →
(iEdg‘𝐺):dom
(iEdg‘𝐺)⟶{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) ≤ 2}) |
8 | | frn 5966 |
. . . . . . 7
⊢
((iEdg‘𝐺):dom
(iEdg‘𝐺)⟶{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) ≤ 2} → ran
(iEdg‘𝐺) ⊆
{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣
(#‘𝑥) ≤
2}) |
9 | 7, 8 | syl 17 |
. . . . . 6
⊢ (𝐺 ∈ UPGraph → ran
(iEdg‘𝐺) ⊆
{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣
(#‘𝑥) ≤
2}) |
10 | 9 | sseld 3567 |
. . . . 5
⊢ (𝐺 ∈ UPGraph → (𝐶 ∈ ran (iEdg‘𝐺) → 𝐶 ∈ {𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) ≤ 2})) |
11 | 4, 10 | sylbid 229 |
. . . 4
⊢ (𝐺 ∈ UPGraph → (𝐶 ∈ 𝐸 → 𝐶 ∈ {𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) ≤ 2})) |
12 | 11 | imp 444 |
. . 3
⊢ ((𝐺 ∈ UPGraph ∧ 𝐶 ∈ 𝐸) → 𝐶 ∈ {𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) ≤ 2}) |
13 | | fveq2 6103 |
. . . . . 6
⊢ (𝑥 = 𝐶 → (#‘𝑥) = (#‘𝐶)) |
14 | 13 | breq1d 4593 |
. . . . 5
⊢ (𝑥 = 𝐶 → ((#‘𝑥) ≤ 2 ↔ (#‘𝐶) ≤ 2)) |
15 | 14 | elrab 3331 |
. . . 4
⊢ (𝐶 ∈ {𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) ≤ 2} ↔ (𝐶 ∈ (𝒫 𝑉 ∖ {∅}) ∧
(#‘𝐶) ≤
2)) |
16 | | 2nn0 11186 |
. . . . . . 7
⊢ 2 ∈
ℕ0 |
17 | | hashbnd 12985 |
. . . . . . 7
⊢ ((𝐶 ∈ (𝒫 𝑉 ∖ {∅}) ∧ 2
∈ ℕ0 ∧ (#‘𝐶) ≤ 2) → 𝐶 ∈ Fin) |
18 | 16, 17 | mp3an2 1404 |
. . . . . 6
⊢ ((𝐶 ∈ (𝒫 𝑉 ∖ {∅}) ∧
(#‘𝐶) ≤ 2) →
𝐶 ∈
Fin) |
19 | | hashcl 13009 |
. . . . . 6
⊢ (𝐶 ∈ Fin →
(#‘𝐶) ∈
ℕ0) |
20 | 18, 19 | syl 17 |
. . . . 5
⊢ ((𝐶 ∈ (𝒫 𝑉 ∖ {∅}) ∧
(#‘𝐶) ≤ 2) →
(#‘𝐶) ∈
ℕ0) |
21 | | nn0re 11178 |
. . . . . . . . 9
⊢
((#‘𝐶) ∈
ℕ0 → (#‘𝐶) ∈ ℝ) |
22 | | 2re 10967 |
. . . . . . . . . 10
⊢ 2 ∈
ℝ |
23 | 22 | a1i 11 |
. . . . . . . . 9
⊢
((#‘𝐶) ∈
ℕ0 → 2 ∈ ℝ) |
24 | 21, 23 | leloed 10059 |
. . . . . . . 8
⊢
((#‘𝐶) ∈
ℕ0 → ((#‘𝐶) ≤ 2 ↔ ((#‘𝐶) < 2 ∨ (#‘𝐶) = 2))) |
25 | 24 | adantl 481 |
. . . . . . 7
⊢ ((𝐶 ∈ (𝒫 𝑉 ∖ {∅}) ∧
(#‘𝐶) ∈
ℕ0) → ((#‘𝐶) ≤ 2 ↔ ((#‘𝐶) < 2 ∨ (#‘𝐶) = 2))) |
26 | | nn0lt2 11317 |
. . . . . . . . . . 11
⊢
(((#‘𝐶) ∈
ℕ0 ∧ (#‘𝐶) < 2) → ((#‘𝐶) = 0 ∨ (#‘𝐶) = 1)) |
27 | 26 | ex 449 |
. . . . . . . . . 10
⊢
((#‘𝐶) ∈
ℕ0 → ((#‘𝐶) < 2 → ((#‘𝐶) = 0 ∨ (#‘𝐶) = 1))) |
28 | 27 | adantl 481 |
. . . . . . . . 9
⊢ ((𝐶 ∈ (𝒫 𝑉 ∖ {∅}) ∧
(#‘𝐶) ∈
ℕ0) → ((#‘𝐶) < 2 → ((#‘𝐶) = 0 ∨ (#‘𝐶) = 1))) |
29 | | eldifsn 4260 |
. . . . . . . . . . . 12
⊢ (𝐶 ∈ (𝒫 𝑉 ∖ {∅}) ↔
(𝐶 ∈ 𝒫 𝑉 ∧ 𝐶 ≠ ∅)) |
30 | | hasheq0 13015 |
. . . . . . . . . . . . . 14
⊢ (𝐶 ∈ 𝒫 𝑉 → ((#‘𝐶) = 0 ↔ 𝐶 = ∅)) |
31 | 30 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝐶 ∈ 𝒫 𝑉 ∧ 𝐶 ≠ ∅) → ((#‘𝐶) = 0 ↔ 𝐶 = ∅)) |
32 | | eqneqall 2793 |
. . . . . . . . . . . . . . 15
⊢ (𝐶 = ∅ → (𝐶 ≠ ∅ →
∃𝑎∃𝑏((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝐶 = {𝑎, 𝑏}))) |
33 | 32 | com12 32 |
. . . . . . . . . . . . . 14
⊢ (𝐶 ≠ ∅ → (𝐶 = ∅ → ∃𝑎∃𝑏((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝐶 = {𝑎, 𝑏}))) |
34 | 33 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝐶 ∈ 𝒫 𝑉 ∧ 𝐶 ≠ ∅) → (𝐶 = ∅ → ∃𝑎∃𝑏((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝐶 = {𝑎, 𝑏}))) |
35 | 31, 34 | sylbid 229 |
. . . . . . . . . . . 12
⊢ ((𝐶 ∈ 𝒫 𝑉 ∧ 𝐶 ≠ ∅) → ((#‘𝐶) = 0 → ∃𝑎∃𝑏((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝐶 = {𝑎, 𝑏}))) |
36 | 29, 35 | sylbi 206 |
. . . . . . . . . . 11
⊢ (𝐶 ∈ (𝒫 𝑉 ∖ {∅}) →
((#‘𝐶) = 0 →
∃𝑎∃𝑏((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝐶 = {𝑎, 𝑏}))) |
37 | 36 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ (𝒫 𝑉 ∖ {∅}) ∧
(#‘𝐶) ∈
ℕ0) → ((#‘𝐶) = 0 → ∃𝑎∃𝑏((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝐶 = {𝑎, 𝑏}))) |
38 | | hash1snb 13068 |
. . . . . . . . . . . 12
⊢ (𝐶 ∈ (𝒫 𝑉 ∖ {∅}) →
((#‘𝐶) = 1 ↔
∃𝑐 𝐶 = {𝑐})) |
39 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐶 = {𝑐} → (𝐶 ∈ 𝒫 𝑉 ↔ {𝑐} ∈ 𝒫 𝑉)) |
40 | | vex 3176 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 𝑐 ∈ V |
41 | 40 | snelpw 4840 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑐 ∈ 𝑉 ↔ {𝑐} ∈ 𝒫 𝑉) |
42 | 41 | biimpri 217 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ({𝑐} ∈ 𝒫 𝑉 → 𝑐 ∈ 𝑉) |
43 | 42 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐶 = {𝑐} → ({𝑐} ∈ 𝒫 𝑉 → 𝑐 ∈ 𝑉)) |
44 | 39, 43 | sylbid 229 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐶 = {𝑐} → (𝐶 ∈ 𝒫 𝑉 → 𝑐 ∈ 𝑉)) |
45 | 44 | com12 32 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐶 ∈ 𝒫 𝑉 → (𝐶 = {𝑐} → 𝑐 ∈ 𝑉)) |
46 | 45 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐶 ∈ 𝒫 𝑉 ∧ 𝐶 ≠ ∅) → (𝐶 = {𝑐} → 𝑐 ∈ 𝑉)) |
47 | 29, 46 | sylbi 206 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐶 ∈ (𝒫 𝑉 ∖ {∅}) →
(𝐶 = {𝑐} → 𝑐 ∈ 𝑉)) |
48 | 47 | imp 444 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐶 ∈ (𝒫 𝑉 ∖ {∅}) ∧ 𝐶 = {𝑐}) → 𝑐 ∈ 𝑉) |
49 | | id 22 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐶 = {𝑐} → 𝐶 = {𝑐}) |
50 | | dfsn2 4138 |
. . . . . . . . . . . . . . . . . 18
⊢ {𝑐} = {𝑐, 𝑐} |
51 | 49, 50 | syl6eq 2660 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐶 = {𝑐} → 𝐶 = {𝑐, 𝑐}) |
52 | 51 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐶 ∈ (𝒫 𝑉 ∖ {∅}) ∧ 𝐶 = {𝑐}) → 𝐶 = {𝑐, 𝑐}) |
53 | | preq1 4212 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 = 𝑐 → {𝑎, 𝑏} = {𝑐, 𝑏}) |
54 | 53 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = 𝑐 → (𝐶 = {𝑎, 𝑏} ↔ 𝐶 = {𝑐, 𝑏})) |
55 | | preq2 4213 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑏 = 𝑐 → {𝑐, 𝑏} = {𝑐, 𝑐}) |
56 | 55 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 = 𝑐 → (𝐶 = {𝑐, 𝑏} ↔ 𝐶 = {𝑐, 𝑐})) |
57 | 54, 56 | rspc2ev 3295 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑐 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ∧ 𝐶 = {𝑐, 𝑐}) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝐶 = {𝑎, 𝑏}) |
58 | 48, 48, 52, 57 | syl3anc 1318 |
. . . . . . . . . . . . . . 15
⊢ ((𝐶 ∈ (𝒫 𝑉 ∖ {∅}) ∧ 𝐶 = {𝑐}) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝐶 = {𝑎, 𝑏}) |
59 | | r2ex 3043 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑎 ∈
𝑉 ∃𝑏 ∈ 𝑉 𝐶 = {𝑎, 𝑏} ↔ ∃𝑎∃𝑏((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝐶 = {𝑎, 𝑏})) |
60 | 58, 59 | sylib 207 |
. . . . . . . . . . . . . 14
⊢ ((𝐶 ∈ (𝒫 𝑉 ∖ {∅}) ∧ 𝐶 = {𝑐}) → ∃𝑎∃𝑏((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝐶 = {𝑎, 𝑏})) |
61 | 60 | ex 449 |
. . . . . . . . . . . . 13
⊢ (𝐶 ∈ (𝒫 𝑉 ∖ {∅}) →
(𝐶 = {𝑐} → ∃𝑎∃𝑏((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝐶 = {𝑎, 𝑏}))) |
62 | 61 | exlimdv 1848 |
. . . . . . . . . . . 12
⊢ (𝐶 ∈ (𝒫 𝑉 ∖ {∅}) →
(∃𝑐 𝐶 = {𝑐} → ∃𝑎∃𝑏((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝐶 = {𝑎, 𝑏}))) |
63 | 38, 62 | sylbid 229 |
. . . . . . . . . . 11
⊢ (𝐶 ∈ (𝒫 𝑉 ∖ {∅}) →
((#‘𝐶) = 1 →
∃𝑎∃𝑏((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝐶 = {𝑎, 𝑏}))) |
64 | 63 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ (𝒫 𝑉 ∖ {∅}) ∧
(#‘𝐶) ∈
ℕ0) → ((#‘𝐶) = 1 → ∃𝑎∃𝑏((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝐶 = {𝑎, 𝑏}))) |
65 | 37, 64 | jaod 394 |
. . . . . . . . 9
⊢ ((𝐶 ∈ (𝒫 𝑉 ∖ {∅}) ∧
(#‘𝐶) ∈
ℕ0) → (((#‘𝐶) = 0 ∨ (#‘𝐶) = 1) → ∃𝑎∃𝑏((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝐶 = {𝑎, 𝑏}))) |
66 | 28, 65 | syld 46 |
. . . . . . . 8
⊢ ((𝐶 ∈ (𝒫 𝑉 ∖ {∅}) ∧
(#‘𝐶) ∈
ℕ0) → ((#‘𝐶) < 2 → ∃𝑎∃𝑏((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝐶 = {𝑎, 𝑏}))) |
67 | | hash2sspr 13124 |
. . . . . . . . . . . . 13
⊢ ((𝐶 ∈ 𝒫 𝑉 ∧ (#‘𝐶) = 2) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝐶 = {𝑎, 𝑏}) |
68 | 67 | ex 449 |
. . . . . . . . . . . 12
⊢ (𝐶 ∈ 𝒫 𝑉 → ((#‘𝐶) = 2 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝐶 = {𝑎, 𝑏})) |
69 | 68 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝐶 ∈ 𝒫 𝑉 ∧ 𝐶 ≠ ∅) → ((#‘𝐶) = 2 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝐶 = {𝑎, 𝑏})) |
70 | 29, 69 | sylbi 206 |
. . . . . . . . . 10
⊢ (𝐶 ∈ (𝒫 𝑉 ∖ {∅}) →
((#‘𝐶) = 2 →
∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝐶 = {𝑎, 𝑏})) |
71 | 70, 59 | syl6ib 240 |
. . . . . . . . 9
⊢ (𝐶 ∈ (𝒫 𝑉 ∖ {∅}) →
((#‘𝐶) = 2 →
∃𝑎∃𝑏((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝐶 = {𝑎, 𝑏}))) |
72 | 71 | adantr 480 |
. . . . . . . 8
⊢ ((𝐶 ∈ (𝒫 𝑉 ∖ {∅}) ∧
(#‘𝐶) ∈
ℕ0) → ((#‘𝐶) = 2 → ∃𝑎∃𝑏((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝐶 = {𝑎, 𝑏}))) |
73 | 66, 72 | jaod 394 |
. . . . . . 7
⊢ ((𝐶 ∈ (𝒫 𝑉 ∖ {∅}) ∧
(#‘𝐶) ∈
ℕ0) → (((#‘𝐶) < 2 ∨ (#‘𝐶) = 2) → ∃𝑎∃𝑏((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝐶 = {𝑎, 𝑏}))) |
74 | 25, 73 | sylbid 229 |
. . . . . 6
⊢ ((𝐶 ∈ (𝒫 𝑉 ∖ {∅}) ∧
(#‘𝐶) ∈
ℕ0) → ((#‘𝐶) ≤ 2 → ∃𝑎∃𝑏((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝐶 = {𝑎, 𝑏}))) |
75 | 74 | impancom 455 |
. . . . 5
⊢ ((𝐶 ∈ (𝒫 𝑉 ∖ {∅}) ∧
(#‘𝐶) ≤ 2) →
((#‘𝐶) ∈
ℕ0 → ∃𝑎∃𝑏((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝐶 = {𝑎, 𝑏}))) |
76 | 20, 75 | mpd 15 |
. . . 4
⊢ ((𝐶 ∈ (𝒫 𝑉 ∖ {∅}) ∧
(#‘𝐶) ≤ 2) →
∃𝑎∃𝑏((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝐶 = {𝑎, 𝑏})) |
77 | 15, 76 | sylbi 206 |
. . 3
⊢ (𝐶 ∈ {𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) ≤ 2} → ∃𝑎∃𝑏((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝐶 = {𝑎, 𝑏})) |
78 | 12, 77 | syl 17 |
. 2
⊢ ((𝐺 ∈ UPGraph ∧ 𝐶 ∈ 𝐸) → ∃𝑎∃𝑏((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝐶 = {𝑎, 𝑏})) |
79 | 78, 59 | sylibr 223 |
1
⊢ ((𝐺 ∈ UPGraph ∧ 𝐶 ∈ 𝐸) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝐶 = {𝑎, 𝑏}) |